ghc/compiler/typecheck/TcUnify.lhs

   1 %
   2 % (c) The GRASP/AQUA Project, Glasgow University, 1992-1998
   3 %
   4 \section{Type subsumption and unification}
   5
   6 \begin{code}
   7 module TcUnify (
   8         -- Full-blown subsumption
   9   tcSubOff, tcSubExp, tcGen, subFunTy, TcHoleType,
  10   checkSigTyVars, checkSigTyVarsWrt, sigCtxt,
  11
  12         -- Various unifications
  13   unifyTauTy, unifyTauTyList, unifyTauTyLists,
  14   unifyFunTy, unifyListTy, unifyPArrTy, unifyTupleTy,
  15   unifyKind, unifyKinds, unifyOpenTypeKind,
  16
  17         -- Coercions
  18   Coercion, ExprCoFn, PatCoFn,
  19   (<$>), (<.>), mkCoercion,
  20   idCoercion, isIdCoercion
  21
  22   ) where
  23
  24 #include "HsVersions.h"
  25
  26
  27 import HsSyn            ( HsExpr(..) )
  28 import TcHsSyn          ( TypecheckedHsExpr, TcPat, mkHsLet )
  29 import TypeRep          ( Type(..), SourceType(..), TyNote(..),
  30                           openKindCon, typeCon )
  31
  32 import TcMonad          -- TcType, amongst others
  33 import TcType           ( TcKind, TcType, TcSigmaType, TcRhoType, TcTyVar, TcTauType,
  34                           TcTyVarSet, TcThetaType, TyVarDetails(SigTv),
  35                           isTauTy, isSigmaTy,
  36                           tcSplitAppTy_maybe, tcSplitTyConApp_maybe,
  37                           tcGetTyVar_maybe, tcGetTyVar,
  38                           mkTyConApp, mkFunTy, tyVarsOfType, mkPhiTy,
  39                           typeKind, tcSplitFunTy_maybe, mkForAllTys,
  40                           isHoleTyVar, isSkolemTyVar, isUserTyVar,
  41                           tidyOpenType, tidyOpenTypes, tidyOpenTyVar, tidyOpenTyVars,
  42                           eqKind, openTypeKind, liftedTypeKind, isTypeKind,
  43                           hasMoreBoxityInfo, tyVarBindingInfo, allDistinctTyVars
  44                         )
  45 import qualified Type   ( getTyVar_maybe )
  46 import Inst             ( LIE, emptyLIE, plusLIE,
  47                           newDicts, instToId, tcInstCall
  48                         )
  49 import TcMType          ( getTcTyVar, putTcTyVar, tcInstType, readHoleResult,
  50                           newTyVarTy, newTyVarTys, newBoxityVar, newHoleTyVarTy,
  51                           zonkTcType, zonkTcTyVars, zonkTcTyVarsAndFV, zonkTcTyVar )
  52 import TcSimplify       ( tcSimplifyCheck )
  53 import TysWiredIn       ( listTyCon, parrTyCon, mkListTy, mkPArrTy, mkTupleTy )
  54 import TcEnv            ( TcTyThing(..), tcGetGlobalTyVars, tcLEnvElts )
  55 import TyCon            ( tyConArity, isTupleTyCon, tupleTyConBoxity )
  56 import PprType          ( pprType )
  57 import Id               ( Id, mkSysLocal, idType )
  58 import Var              ( Var, varName, tyVarKind )
  59 import VarSet           ( emptyVarSet, unionVarSet, elemVarSet, varSetElems )
  60 import VarEnv
  61 import Name             ( isSystemName, getSrcLoc )
  62 import ErrUtils         ( Message )
  63 import BasicTypes       ( Boxity, Arity, isBoxed )
  64 import Util             ( equalLength )
  65 import Maybe            ( isNothing )
  66 import Outputable
  67 \end{code}
  68
  69 Notes on holes
  70 ~~~~~~~~~~~~~~
  71 * A hole is always filled in with an ordinary type, not another hole.
  72
  73 %************************************************************************
  74 %*                                                                      *
  75 \subsection{Subsumption}
  76 %*                                                                      *
  77 %************************************************************************
  78
  79 All the tcSub calls have the form
  80
  81                 tcSub expected_ty offered_ty
  82 which checks
  83                 offered_ty <= expected_ty
  84
  85 That is, that a value of type offered_ty is acceptable in
  86 a place expecting a value of type expected_ty.
  87
  88 It returns a coercion function
  89         co_fn :: offered_ty -> expected_ty
  90 which takes an HsExpr of type offered_ty into one of type
  91 expected_ty.
  92
  93 \begin{code}
  94 type TcHoleType = TcSigmaType   -- Either a TcSigmaType,
  95                                 -- or else a hole
  96
  97 tcSubExp :: TcHoleType  -> TcSigmaType -> TcM (ExprCoFn, LIE)
  98 tcSubOff :: TcSigmaType -> TcHoleType  -> TcM (ExprCoFn, LIE)
  99 tcSub    :: TcSigmaType -> TcSigmaType -> TcM (ExprCoFn, LIE)
 100 \end{code}
 101
 102 These two check for holes
 103
 104 \begin{code}
 105 tcSubExp expected_ty offered_ty
 106   = checkHole expected_ty offered_ty tcSub
 107
 108 tcSubOff expected_ty offered_ty
 109   = checkHole offered_ty expected_ty (\ off exp -> tcSub exp off)
 110
 111 -- checkHole looks for a hole in its first arg;
 112 -- If so, and it is uninstantiated, it fills in the hole
 113 --        with its second arg
 114 -- Otherwise it calls thing_inside, passing the two args, looking
 115 -- through any instantiated hole
 116
 117 checkHole (TyVarTy tv) other_ty thing_inside
 118   | isHoleTyVar tv
 119   = getTcTyVar tv       `thenNF_Tc` \ maybe_ty ->
 120     case maybe_ty of
 121         Just ty -> thing_inside ty other_ty
 122         Nothing -> putTcTyVar tv other_ty       `thenNF_Tc_`
 123                    returnTc (idCoercion, emptyLIE)
 124
 125 checkHole ty other_ty thing_inside
 126   = thing_inside ty other_ty
 127 \end{code}
 128
 129 No holes expected now.  Add some error-check context info.
 130
 131 \begin{code}
 132 tcSub expected_ty actual_ty
 133   = traceTc (text "tcSub" <+> details)          `thenNF_Tc_`
 134     tcAddErrCtxtM (unifyCtxt "type" expected_ty actual_ty)
 135                   (tc_sub expected_ty expected_ty actual_ty actual_ty)
 136   where
 137     details = vcat [text "Expected:" <+> ppr expected_ty,
 138                     text "Actual:  " <+> ppr actual_ty]
 139 \end{code}
 140
 141 tc_sub carries the types before and after expanding type synonyms
 142
 143 \begin{code}
 144 tc_sub :: TcSigmaType           -- expected_ty, before expanding synonyms
 145        -> TcSigmaType           --              ..and after
 146        -> TcSigmaType           -- actual_ty, before
 147        -> TcSigmaType           --              ..and after
 148        -> TcM (ExprCoFn, LIE)
 149
 150 -----------------------------------
 151 -- Expand synonyms
 152 tc_sub exp_sty (NoteTy _ exp_ty) act_sty act_ty = tc_sub exp_sty exp_ty act_sty act_ty
 153 tc_sub exp_sty exp_ty act_sty (NoteTy _ act_ty) = tc_sub exp_sty exp_ty act_sty act_ty
 154
 155 -----------------------------------
 156 -- Generalisation case
 157 --      actual_ty:   d:Eq b => b->b
 158 --      expected_ty: forall a. Ord a => a->a
 159 --      co_fn e      /\a. \d2:Ord a. let d = eqFromOrd d2 in e
 160
 161 -- It is essential to do this *before* the specialisation case
 162 -- Example:  f :: (Eq a => a->a) -> ...
 163 --           g :: Ord b => b->b
 164 -- Consider  f g !
 165
 166 tc_sub exp_sty expected_ty act_sty actual_ty
 167   | isSigmaTy expected_ty
 168   = tcGen expected_ty (tyVarsOfType actual_ty) (
 169         -- It's really important to check for escape wrt the free vars of
 170         -- both expected_ty *and* actual_ty
 171         \ body_exp_ty -> tc_sub body_exp_ty body_exp_ty act_sty actual_ty
 172     )                           `thenTc` \ (gen_fn, co_fn, lie) ->
 173     returnTc (gen_fn <.> co_fn, lie)
 174
 175 -----------------------------------
 176 -- Specialisation case:
 177 --      actual_ty:   forall a. Ord a => a->a
 178 --      expected_ty: Int -> Int
 179 --      co_fn e =    e Int dOrdInt
 180
 181 tc_sub exp_sty expected_ty act_sty actual_ty
 182   | isSigmaTy actual_ty
 183   = tcInstCall Rank2Origin actual_ty            `thenNF_Tc` \ (inst_fn, lie1, body_ty) ->
 184     tc_sub exp_sty expected_ty body_ty body_ty  `thenTc` \ (co_fn, lie2) ->
 185     returnTc (co_fn <.> mkCoercion inst_fn, lie1 `plusLIE` lie2)
 186
 187 -----------------------------------
 188 -- Function case
 189
 190 tc_sub _ (FunTy exp_arg exp_res) _ (FunTy act_arg act_res)
 191   = tcSub_fun exp_arg exp_res act_arg act_res
 192
 193 -----------------------------------
 194 -- Type variable meets function: imitate
 195 --
 196 -- NB 1: we can't just unify the type variable with the type
 197 --       because the type might not be a tau-type, and we aren't
 198 --       allowed to instantiate an ordinary type variable with
 199 --       a sigma-type
 200 --
 201 -- NB 2: can we short-cut to an error case?
 202 --       when the arg/res is not a tau-type?
 203 -- NO!  e.g.   f :: ((forall a. a->a) -> Int) -> Int
 204 --      then   x = (f,f)
 205 --      is perfectly fine!
 206
 207 tc_sub exp_sty exp_ty@(FunTy exp_arg exp_res) _ (TyVarTy tv)
 208   = ASSERT( not (isHoleTyVar tv) )
 209     getTcTyVar tv       `thenNF_Tc` \ maybe_ty ->
 210     case maybe_ty of
 211         Just ty -> tc_sub exp_sty exp_ty ty ty
 212         Nothing -> imitateFun tv exp_sty        `thenNF_Tc` \ (act_arg, act_res) ->
 213                    tcSub_fun exp_arg exp_res act_arg act_res
 214
 215 tc_sub _ (TyVarTy tv) act_sty act_ty@(FunTy act_arg act_res)
 216   = ASSERT( not (isHoleTyVar tv) )
 217     getTcTyVar tv       `thenNF_Tc` \ maybe_ty ->
 218     case maybe_ty of
 219         Just ty -> tc_sub ty ty act_sty act_ty
 220         Nothing -> imitateFun tv act_sty        `thenNF_Tc` \ (exp_arg, exp_res) ->
 221                    tcSub_fun exp_arg exp_res act_arg act_res
 222
 223 -----------------------------------
 224 -- Unification case
 225 -- If none of the above match, we revert to the plain unifier
 226 tc_sub exp_sty expected_ty act_sty actual_ty
 227   = uTys exp_sty expected_ty act_sty actual_ty  `thenTc_`
 228     returnTc (idCoercion, emptyLIE)
 229 \end{code}
 230
 231 %************************************************************************
 232 %*                                                                      *
 233 \subsection{Functions}
 234 %*                                                                      *
 235 %************************************************************************
 236
 237 \begin{code}
 238 tcSub_fun exp_arg exp_res act_arg act_res
 239   = tc_sub act_arg act_arg exp_arg exp_arg      `thenTc` \ (co_fn_arg, lie1) ->
 240     tc_sub exp_res exp_res act_res act_res      `thenTc` \ (co_fn_res, lie2) ->
 241     tcGetUnique                                 `thenNF_Tc` \ uniq ->
 242     let
 243         -- co_fn_arg :: HsExpr exp_arg -> HsExpr act_arg
 244         -- co_fn_res :: HsExpr act_res -> HsExpr exp_res
 245         -- co_fn     :: HsExpr (act_arg -> act_res) -> HsExpr (exp_arg -> exp_res)
 246         arg_id = mkSysLocal FSLIT("sub") uniq exp_arg
 247         coercion | isIdCoercion co_fn_arg,
 248                    isIdCoercion co_fn_res = idCoercion
 249                  | otherwise              = mkCoercion co_fn
 250
 251         co_fn e = DictLam [arg_id]
 252                      (co_fn_res <$> (HsApp e (co_fn_arg <$> (HsVar arg_id))))
 253                 -- Slight hack; using a "DictLam" to get an ordinary simple lambda
 254                 --      HsVar arg_id :: HsExpr exp_arg
 255                 --      co_fn_arg $it :: HsExpr act_arg
 256                 --      HsApp e $it   :: HsExpr act_res
 257                 --      co_fn_res $it :: HsExpr exp_res
 258     in
 259     returnTc (coercion, lie1 `plusLIE` lie2)
 260
 261 imitateFun :: TcTyVar -> TcType -> NF_TcM (TcType, TcType)
 262 imitateFun tv ty
 263   = ASSERT( not (isHoleTyVar tv) )
 264         -- NB: tv is an *ordinary* tyvar and so are the new ones
 265
 266         -- Check that tv isn't a type-signature type variable
 267         -- (This would be found later in checkSigTyVars, but
 268         --  we get a better error message if we do it here.)
 269     checkTcM (not (isSkolemTyVar tv))
 270              (failWithTcM (unifyWithSigErr tv ty))      `thenTc_`
 271
 272     newTyVarTy openTypeKind             `thenNF_Tc` \ arg ->
 273     newTyVarTy openTypeKind             `thenNF_Tc` \ res ->
 274     putTcTyVar tv (mkFunTy arg res)     `thenNF_Tc_`
 275     returnNF_Tc (arg,res)
 276 \end{code}
 277
 278
 279 %************************************************************************
 280 %*                                                                      *
 281 \subsection{Generalisation}
 282 %*                                                                      *
 283 %************************************************************************
 284
 285 \begin{code}
 286 tcGen :: TcSigmaType                            -- expected_ty
 287       -> TcTyVarSet                             -- Extra tyvars that the universally
 288                                                 --      quantified tyvars of expected_ty
 289                                                 --      must not be unified
 290       -> (TcRhoType -> TcM (result, LIE))       -- spec_ty
 291       -> TcM (ExprCoFn, result, LIE)
 292         -- The expression has type: spec_ty -> expected_ty
 293
 294 tcGen expected_ty extra_tvs thing_inside        -- We expect expected_ty to be a forall-type
 295                                                 -- If not, the call is a no-op
 296   = tcInstType SigTv expected_ty        `thenNF_Tc` \ (forall_tvs, theta, phi_ty) ->
 297
 298         -- Type-check the arg and unify with poly type
 299     thing_inside phi_ty                 `thenTc` \ (result, lie) ->
 300
 301         -- Check that the "forall_tvs" havn't been constrained
 302         -- The interesting bit here is that we must include the free variables
 303         -- of the expected_ty.  Here's an example:
 304         --       runST (newVar True)
 305         -- Here, if we don't make a check, we'll get a type (ST s (MutVar s Bool))
 306         -- for (newVar True), with s fresh.  Then we unify with the runST's arg type
 307         -- forall s'. ST s' a. That unifies s' with s, and a with MutVar s Bool.
 308         -- So now s' isn't unconstrained because it's linked to a.
 309         -- Conclusion: include the free vars of the expected_ty in the
 310         -- list of "free vars" for the signature check.
 311
 312     newDicts SignatureOrigin theta                      `thenNF_Tc` \ dicts ->
 313     tcSimplifyCheck sig_msg forall_tvs dicts lie        `thenTc` \ (free_lie, inst_binds) ->
 314     checkSigTyVarsWrt free_tvs forall_tvs               `thenTc` \ zonked_tvs ->
 315
 316     let
 317             -- This HsLet binds any Insts which came out of the simplification.
 318             -- It's a bit out of place here, but using AbsBind involves inventing
 319             -- a couple of new names which seems worse.
 320         dict_ids = map instToId dicts
 321         co_fn e  = TyLam zonked_tvs (DictLam dict_ids (mkHsLet inst_binds e))
 322     in
 323     returnTc (mkCoercion co_fn, result, free_lie)
 324   where
 325     free_tvs = tyVarsOfType expected_ty `unionVarSet` extra_tvs
 326     sig_msg  = ptext SLIT("When generalising the type of an expression")
 327 \end{code}
 328
 329
 330
 331 %************************************************************************
 332 %*                                                                      *
 333 \subsection{Coercion functions}
 334 %*                                                                      *
 335 %************************************************************************
 336
 337 \begin{code}
 338 type Coercion a = Maybe (a -> a)
 339         -- Nothing => identity fn
 340
 341 type ExprCoFn = Coercion TypecheckedHsExpr
 342 type PatCoFn  = Coercion TcPat
 343
 344 (<.>) :: Coercion a -> Coercion a -> Coercion a -- Composition
 345 Nothing <.> Nothing = Nothing
 346 Nothing <.> Just f  = Just f
 347 Just f  <.> Nothing = Just f
 348 Just f1 <.> Just f2 = Just (f1 . f2)
 349
 350 (<$>) :: Coercion a -> a -> a
 351 Just f  <$> e = f e
 352 Nothing <$> e = e
 353
 354 mkCoercion :: (a -> a) -> Coercion a
 355 mkCoercion f = Just f
 356
 357 idCoercion :: Coercion a
 358 idCoercion = Nothing
 359
 360 isIdCoercion :: Coercion a -> Bool
 361 isIdCoercion = isNothing
 362 \end{code}
 363
 364 %************************************************************************
 365 %*                                                                      *
 366 \subsection[Unify-exported]{Exported unification functions}
 367 %*                                                                      *
 368 %************************************************************************
 369
 370 The exported functions are all defined as versions of some
 371 non-exported generic functions.
 372
 373 Unify two @TauType@s.  Dead straightforward.
 374
 375 \begin{code}
 376 unifyTauTy :: TcTauType -> TcTauType -> TcM ()
 377 unifyTauTy ty1 ty2      -- ty1 expected, ty2 inferred
 378   =     -- The unifier should only ever see tau-types
 379         -- (no quantification whatsoever)
 380     ASSERT2( isTauTy ty1, ppr ty1 )
 381     ASSERT2( isTauTy ty2, ppr ty2 )
 382     tcAddErrCtxtM (unifyCtxt "type" ty1 ty2) $
 383     uTys ty1 ty1 ty2 ty2
 384 \end{code}
 385
 386 @unifyTauTyList@ unifies corresponding elements of two lists of
 387 @TauType@s.  It uses @uTys@ to do the real work.  The lists should be
 388 of equal length.  We charge down the list explicitly so that we can
 389 complain if their lengths differ.
 390
 391 \begin{code}
 392 unifyTauTyLists :: [TcTauType] -> [TcTauType] ->  TcM ()
 393 unifyTauTyLists []           []         = returnTc ()
 394 unifyTauTyLists (ty1:tys1) (ty2:tys2) = uTys ty1 ty1 ty2 ty2   `thenTc_`
 395                                         unifyTauTyLists tys1 tys2
 396 unifyTauTyLists ty1s ty2s = panic "Unify.unifyTauTyLists: mismatched type lists!"
 397 \end{code}
 398
 399 @unifyTauTyList@ takes a single list of @TauType@s and unifies them
 400 all together.  It is used, for example, when typechecking explicit
 401 lists, when all the elts should be of the same type.
 402
 403 \begin{code}
 404 unifyTauTyList :: [TcTauType] -> TcM ()
 405 unifyTauTyList []                = returnTc ()
 406 unifyTauTyList [ty]              = returnTc ()
 407 unifyTauTyList (ty1:tys@(ty2:_)) = unifyTauTy ty1 ty2   `thenTc_`
 408                                    unifyTauTyList tys
 409 \end{code}
 410
 411 %************************************************************************
 412 %*                                                                      *
 413 \subsection[Unify-uTys]{@uTys@: getting down to business}
 414 %*                                                                      *
 415 %************************************************************************
 416
 417 @uTys@ is the heart of the unifier.  Each arg happens twice, because
 418 we want to report errors in terms of synomyms if poss.  The first of
 419 the pair is used in error messages only; it is always the same as the
 420 second, except that if the first is a synonym then the second may be a
 421 de-synonym'd version.  This way we get better error messages.
 422
 423 We call the first one \tr{ps_ty1}, \tr{ps_ty2} for ``possible synomym''.
 424
 425 \begin{code}
 426 uTys :: TcTauType -> TcTauType  -- Error reporting ty1 and real ty1
 427                                 -- ty1 is the *expected* type
 428
 429      -> TcTauType -> TcTauType  -- Error reporting ty2 and real ty2
 430                                 -- ty2 is the *actual* type
 431      -> TcM ()
 432
 433         -- Always expand synonyms (see notes at end)
 434         -- (this also throws away FTVs)
 435 uTys ps_ty1 (NoteTy n1 ty1) ps_ty2 ty2 = uTys ps_ty1 ty1 ps_ty2 ty2
 436 uTys ps_ty1 ty1 ps_ty2 (NoteTy n2 ty2) = uTys ps_ty1 ty1 ps_ty2 ty2
 437
 438         -- Variables; go for uVar
 439 uTys ps_ty1 (TyVarTy tyvar1) ps_ty2 ty2 = uVar False tyvar1 ps_ty2 ty2
 440 uTys ps_ty1 ty1 ps_ty2 (TyVarTy tyvar2) = uVar True  tyvar2 ps_ty1 ty1
 441                                         -- "True" means args swapped
 442
 443         -- Predicates
 444 uTys _ (SourceTy (IParam n1 t1)) _ (SourceTy (IParam n2 t2))
 445   | n1 == n2 = uTys t1 t1 t2 t2
 446 uTys _ (SourceTy (ClassP c1 tys1)) _ (SourceTy (ClassP c2 tys2))
 447   | c1 == c2 = unifyTauTyLists tys1 tys2
 448 uTys _ (SourceTy (NType tc1 tys1)) _ (SourceTy (NType tc2 tys2))
 449   | tc1 == tc2 = unifyTauTyLists tys1 tys2
 450
 451         -- Functions; just check the two parts
 452 uTys _ (FunTy fun1 arg1) _ (FunTy fun2 arg2)
 453   = uTys fun1 fun1 fun2 fun2    `thenTc_`    uTys arg1 arg1 arg2 arg2
 454
 455         -- Type constructors must match
 456 uTys ps_ty1 (TyConApp con1 tys1) ps_ty2 (TyConApp con2 tys2)
 457   | con1 == con2 && equalLength tys1 tys2
 458   = unifyTauTyLists tys1 tys2
 459
 460   | con1 == openKindCon
 461         -- When we are doing kind checking, we might match a kind '?'
 462         -- against a kind '*' or '#'.  Notably, CCallable :: ? -> *, and
 463         -- (CCallable Int) and (CCallable Int#) are both OK
 464   = unifyOpenTypeKind ps_ty2
 465
 466         -- Applications need a bit of care!
 467         -- They can match FunTy and TyConApp, so use splitAppTy_maybe
 468         -- NB: we've already dealt with type variables and Notes,
 469         -- so if one type is an App the other one jolly well better be too
 470 uTys ps_ty1 (AppTy s1 t1) ps_ty2 ty2
 471   = case tcSplitAppTy_maybe ty2 of
 472         Just (s2,t2) -> uTys s1 s1 s2 s2        `thenTc_`    uTys t1 t1 t2 t2
 473         Nothing      -> unifyMisMatch ps_ty1 ps_ty2
 474
 475         -- Now the same, but the other way round
 476         -- Don't swap the types, because the error messages get worse
 477 uTys ps_ty1 ty1 ps_ty2 (AppTy s2 t2)
 478   = case tcSplitAppTy_maybe ty1 of
 479         Just (s1,t1) -> uTys s1 s1 s2 s2        `thenTc_`    uTys t1 t1 t2 t2
 480         Nothing      -> unifyMisMatch ps_ty1 ps_ty2
 481
 482         -- Not expecting for-alls in unification
 483         -- ... but the error message from the unifyMisMatch more informative
 484         -- than a panic message!
 485
 486         -- Anything else fails
 487 uTys ps_ty1 ty1 ps_ty2 ty2  = unifyMisMatch ps_ty1 ps_ty2
 488 \end{code}
 489
 490
 491 Notes on synonyms
 492 ~~~~~~~~~~~~~~~~~
 493 If you are tempted to make a short cut on synonyms, as in this
 494 pseudocode...
 495
 496 \begin{verbatim}
 497 -- NO   uTys (SynTy con1 args1 ty1) (SynTy con2 args2 ty2)
 498 -- NO     = if (con1 == con2) then
 499 -- NO   -- Good news!  Same synonym constructors, so we can shortcut
 500 -- NO   -- by unifying their arguments and ignoring their expansions.
 501 -- NO   unifyTauTypeLists args1 args2
 502 -- NO    else
 503 -- NO   -- Never mind.  Just expand them and try again
 504 -- NO   uTys ty1 ty2
 505 \end{verbatim}
 506
 507 then THINK AGAIN.  Here is the whole story, as detected and reported
 508 by Chris Okasaki \tr{<Chris_Okasaki@loch.mess.cs.cmu.edu>}:
 509 \begin{quotation}
 510 Here's a test program that should detect the problem:
 511
 512 \begin{verbatim}
 513         type Bogus a = Int
 514         x = (1 :: Bogus Char) :: Bogus Bool
 515 \end{verbatim}
 516
 517 The problem with [the attempted shortcut code] is that
 518 \begin{verbatim}
 519         con1 == con2
 520 \end{verbatim}
 521 is not a sufficient condition to be able to use the shortcut!
 522 You also need to know that the type synonym actually USES all
 523 its arguments.  For example, consider the following type synonym
 524 which does not use all its arguments.
 525 \begin{verbatim}
 526         type Bogus a = Int
 527 \end{verbatim}
 528
 529 If you ever tried unifying, say, \tr{Bogus Char} with \tr{Bogus Bool},
 530 the unifier would blithely try to unify \tr{Char} with \tr{Bool} and
 531 would fail, even though the expanded forms (both \tr{Int}) should
 532 match.
 533
 534 Similarly, unifying \tr{Bogus Char} with \tr{Bogus t} would
 535 unnecessarily bind \tr{t} to \tr{Char}.
 536
 537 ... You could explicitly test for the problem synonyms and mark them
 538 somehow as needing expansion, perhaps also issuing a warning to the
 539 user.
 540 \end{quotation}
 541
 542
 543 %************************************************************************
 544 %*                                                                      *
 545 \subsection[Unify-uVar]{@uVar@: unifying with a type variable}
 546 %*                                                                      *
 547 %************************************************************************
 548
 549 @uVar@ is called when at least one of the types being unified is a
 550 variable.  It does {\em not} assume that the variable is a fixed point
 551 of the substitution; rather, notice that @uVar@ (defined below) nips
 552 back into @uTys@ if it turns out that the variable is already bound.
 553
 554 \begin{code}
 555 uVar :: Bool            -- False => tyvar is the "expected"
 556                         -- True  => ty    is the "expected" thing
 557      -> TcTyVar
 558      -> TcTauType -> TcTauType  -- printing and real versions
 559      -> TcM ()
 560
 561 uVar swapped tv1 ps_ty2 ty2
 562   = traceTc (text "uVar" <+> ppr swapped <+> ppr tv1 <+> (ppr ps_ty2 $$ ppr ty2))       `thenNF_Tc_`
 563     getTcTyVar tv1      `thenNF_Tc` \ maybe_ty1 ->
 564     case maybe_ty1 of
 565         Just ty1 | swapped   -> uTys ps_ty2 ty2 ty1 ty1 -- Swap back
 566                  | otherwise -> uTys ty1 ty1 ps_ty2 ty2 -- Same order
 567         other       -> uUnboundVar swapped tv1 maybe_ty1 ps_ty2 ty2
 568
 569         -- Expand synonyms; ignore FTVs
 570 uUnboundVar swapped tv1 maybe_ty1 ps_ty2 (NoteTy n2 ty2)
 571   = uUnboundVar swapped tv1 maybe_ty1 ps_ty2 ty2
 572
 573
 574         -- The both-type-variable case
 575 uUnboundVar swapped tv1 maybe_ty1 ps_ty2 ty2@(TyVarTy tv2)
 576
 577         -- Same type variable => no-op
 578   | tv1 == tv2
 579   = returnTc ()
 580
 581         -- Distinct type variables
 582         -- ASSERT maybe_ty1 /= Just
 583   | otherwise
 584   = getTcTyVar tv2      `thenNF_Tc` \ maybe_ty2 ->
 585     case maybe_ty2 of
 586         Just ty2' -> uUnboundVar swapped tv1 maybe_ty1 ty2' ty2'
 587
 588         Nothing | update_tv2
 589
 590                 -> WARN( not (k1 `hasMoreBoxityInfo` k2), (ppr tv1 <+> ppr k1) $$ (ppr tv2 <+> ppr k2) )
 591                    putTcTyVar tv2 (TyVarTy tv1)         `thenNF_Tc_`
 592                    returnTc ()
 593                 |  otherwise
 594
 595                 -> WARN( not (k2 `hasMoreBoxityInfo` k1), (ppr tv2 <+> ppr k2) $$ (ppr tv1 <+> ppr k1) )
 596                    putTcTyVar tv1 ps_ty2                `thenNF_Tc_`
 597                    returnTc ()
 598   where
 599     k1 = tyVarKind tv1
 600     k2 = tyVarKind tv2
 601     update_tv2 = (k2 `eqKind` openTypeKind) || (not (k1 `eqKind` openTypeKind) && nicer_to_update_tv2)
 602                         -- Try to get rid of open type variables as soon as poss
 603
 604     nicer_to_update_tv2 =  isUserTyVar tv1
 605                                 -- Don't unify a signature type variable if poss
 606                         || isSystemName (varName tv2)
 607                                 -- Try to update sys-y type variables in preference to sig-y ones
 608
 609         -- Second one isn't a type variable
 610 uUnboundVar swapped tv1 maybe_ty1 ps_ty2 non_var_ty2
 611   =     -- Check that tv1 isn't a type-signature type variable
 612     checkTcM (not (isSkolemTyVar tv1))
 613              (failWithTcM (unifyWithSigErr tv1 ps_ty2)) `thenTc_`
 614
 615         -- Do the occurs check, and check that we are not
 616         -- unifying a type variable with a polytype
 617         -- Returns a zonked type ready for the update
 618     checkValue tv1 ps_ty2 non_var_ty2   `thenTc` \ ty2 ->
 619
 620         -- Check that the kinds match
 621     checkKinds swapped tv1 ty2          `thenTc_`
 622
 623         -- Perform the update
 624     putTcTyVar tv1 ty2                  `thenNF_Tc_`
 625     returnTc ()
 626 \end{code}
 627
 628 \begin{code}
 629 checkKinds swapped tv1 ty2
 630 -- We're about to unify a type variable tv1 with a non-tyvar-type ty2.
 631 -- ty2 has been zonked at this stage, which ensures that
 632 -- its kind has as much boxity information visible as possible.
 633   | tk2 `hasMoreBoxityInfo` tk1 = returnTc ()
 634
 635   | otherwise
 636         -- Either the kinds aren't compatible
 637         --      (can happen if we unify (a b) with (c d))
 638         -- or we are unifying a lifted type variable with an
 639         --      unlifted type: e.g.  (id 3#) is illegal
 640   = tcAddErrCtxtM (unifyKindCtxt swapped tv1 ty2)       $
 641     unifyMisMatch k1 k2
 642
 643   where
 644     (k1,k2) | swapped   = (tk2,tk1)
 645             | otherwise = (tk1,tk2)
 646     tk1 = tyVarKind tv1
 647     tk2 = typeKind ty2
 648 \end{code}
 649
 650 \begin{code}
 651 checkValue tv1 ps_ty2 non_var_ty2
 652 -- Do the occurs check, and check that we are not
 653 -- unifying a type variable with a polytype
 654 -- Return the type to update the type variable with, or fail
 655
 656 -- Basically we want to update     tv1 := ps_ty2
 657 -- because ps_ty2 has type-synonym info, which improves later error messages
 658 --
 659 -- But consider
 660 --      type A a = ()
 661 --
 662 --      f :: (A a -> a -> ()) -> ()
 663 --      f = \ _ -> ()
 664 --
 665 --      x :: ()
 666 --      x = f (\ x p -> p x)
 667 --
 668 -- In the application (p x), we try to match "t" with "A t".  If we go
 669 -- ahead and bind t to A t (= ps_ty2), we'll lead the type checker into
 670 -- an infinite loop later.
 671 -- But we should not reject the program, because A t = ().
 672 -- Rather, we should bind t to () (= non_var_ty2).
 673 --
 674 -- That's why we have this two-state occurs-check
 675   = zonkTcType ps_ty2                   `thenNF_Tc` \ ps_ty2' ->
 676     case okToUnifyWith tv1 ps_ty2' of {
 677         Nothing -> returnTc ps_ty2' ;   -- Success
 678         other ->
 679
 680     zonkTcType non_var_ty2              `thenNF_Tc` \ non_var_ty2' ->
 681     case okToUnifyWith tv1 non_var_ty2' of
 682         Nothing ->      -- This branch rarely succeeds, except in strange cases
 683                         -- like that in the example above
 684                     returnTc non_var_ty2'
 685
 686         Just problem -> failWithTcM (unifyCheck problem tv1 ps_ty2')
 687     }
 688
 689 data Problem = OccurCheck | NotMonoType
 690
 691 okToUnifyWith :: TcTyVar -> TcType -> Maybe Problem
 692 -- (okToUnifyWith tv ty) checks whether it's ok to unify
 693 --      tv :=: ty
 694 -- Nothing => ok
 695 -- Just p  => not ok, problem p
 696
 697 okToUnifyWith tv ty
 698   = ok ty
 699   where
 700     ok (TyVarTy tv') | tv == tv' = Just OccurCheck
 701                      | otherwise = Nothing
 702     ok (AppTy t1 t2)            = ok t1 `and` ok t2
 703     ok (FunTy t1 t2)            = ok t1 `and` ok t2
 704     ok (TyConApp _ ts)          = oks ts
 705     ok (ForAllTy _ _)           = Just NotMonoType
 706     ok (SourceTy st)            = ok_st st
 707     ok (NoteTy (FTVNote _) t)   = ok t
 708     ok (NoteTy (SynNote t1) t2) = ok t1 `and` ok t2
 709                 -- Type variables may be free in t1 but not t2
 710                 -- A forall may be in t2 but not t1
 711
 712     oks ts = foldr (and . ok) Nothing ts
 713
 714     ok_st (ClassP _ ts) = oks ts
 715     ok_st (IParam _ t)  = ok t
 716     ok_st (NType _ ts)  = oks ts
 717
 718     Nothing `and` m = m
 719     Just p  `and` m = Just p
 720 \end{code}
 721
 722 %************************************************************************
 723 %*                                                                      *
 724 \subsection[Unify-fun]{@unifyFunTy@}
 725 %*                                                                      *
 726 %************************************************************************
 727
 728 @subFunTy@ and @unifyFunTy@ is used to avoid the fruitless
 729 creation of type variables.
 730
 731 * subFunTy is used when we might be faced with a "hole" type variable,
 732   in which case we should create two new holes.
 733
 734 * unifyFunTy is used when we expect to encounter only "ordinary"
 735   type variables, so we should create new ordinary type variables
 736
 737 \begin{code}
 738 subFunTy :: TcHoleType  -- Fail if ty isn't a function type
 739                         -- If it's a hole, make two holes, feed them to...
 740          -> (TcHoleType -> TcHoleType -> TcM a) -- the thing inside
 741          -> TcM a       -- and bind the function type to the hole
 742
 743 subFunTy ty@(TyVarTy tyvar) thing_inside
 744   | isHoleTyVar tyvar
 745   =     -- This is the interesting case
 746     getTcTyVar tyvar    `thenNF_Tc` \ maybe_ty ->
 747     case maybe_ty of {
 748         Just ty' -> subFunTy ty' thing_inside ;
 749         Nothing  ->
 750
 751     newHoleTyVarTy              `thenNF_Tc` \ arg_ty ->
 752     newHoleTyVarTy              `thenNF_Tc` \ res_ty ->
 753
 754         -- Do the business
 755     thing_inside arg_ty res_ty  `thenTc` \ answer ->
 756
 757         -- Extract the answers
 758     readHoleResult arg_ty       `thenNF_Tc` \ arg_ty' ->
 759     readHoleResult res_ty       `thenNF_Tc` \ res_ty' ->
 760
 761         -- Write the answer into the incoming hole
 762     putTcTyVar tyvar (mkFunTy arg_ty' res_ty')  `thenNF_Tc_`
 763
 764         -- And return the answer
 765     returnTc answer }
 766
 767 subFunTy ty thing_inside
 768   = unifyFunTy ty       `thenTc` \ (arg,res) ->
 769     thing_inside arg res
 770
 771
 772 unifyFunTy :: TcRhoType                 -- Fail if ty isn't a function type
 773            -> TcM (TcType, TcType)      -- otherwise return arg and result types
 774
 775 unifyFunTy ty@(TyVarTy tyvar)
 776   = ASSERT( not (isHoleTyVar tyvar) )
 777     getTcTyVar tyvar    `thenNF_Tc` \ maybe_ty ->
 778     case maybe_ty of
 779         Just ty' -> unifyFunTy ty'
 780         Nothing  -> unify_fun_ty_help ty
 781
 782 unifyFunTy ty
 783   = case tcSplitFunTy_maybe ty of
 784         Just arg_and_res -> returnTc arg_and_res
 785         Nothing          -> unify_fun_ty_help ty
 786
 787 unify_fun_ty_help ty    -- Special cases failed, so revert to ordinary unification
 788   = newTyVarTy openTypeKind     `thenNF_Tc` \ arg ->
 789     newTyVarTy openTypeKind     `thenNF_Tc` \ res ->
 790     unifyTauTy ty (mkFunTy arg res)     `thenTc_`
 791     returnTc (arg,res)
 792 \end{code}
 793
 794 \begin{code}
 795 unifyListTy :: TcType              -- expected list type
 796             -> TcM TcType      -- list element type
 797
 798 unifyListTy ty@(TyVarTy tyvar)
 799   = getTcTyVar tyvar    `thenNF_Tc` \ maybe_ty ->
 800     case maybe_ty of
 801         Just ty' -> unifyListTy ty'
 802         other    -> unify_list_ty_help ty
 803
 804 unifyListTy ty
 805   = case tcSplitTyConApp_maybe ty of
 806         Just (tycon, [arg_ty]) | tycon == listTyCon -> returnTc arg_ty
 807         other                                       -> unify_list_ty_help ty
 808
 809 unify_list_ty_help ty   -- Revert to ordinary unification
 810   = newTyVarTy liftedTypeKind           `thenNF_Tc` \ elt_ty ->
 811     unifyTauTy ty (mkListTy elt_ty)     `thenTc_`
 812     returnTc elt_ty
 813
 814 -- variant for parallel arrays
 815 --
 816 unifyPArrTy :: TcType              -- expected list type
 817             -> TcM TcType          -- list element type
 818
 819 unifyPArrTy ty@(TyVarTy tyvar)
 820   = getTcTyVar tyvar    `thenNF_Tc` \ maybe_ty ->
 821     case maybe_ty of
 822       Just ty' -> unifyPArrTy ty'
 823       _        -> unify_parr_ty_help ty
 824 unifyPArrTy ty
 825   = case tcSplitTyConApp_maybe ty of
 826       Just (tycon, [arg_ty]) | tycon == parrTyCon -> returnTc arg_ty
 827       _                                           -> unify_parr_ty_help ty
 828
 829 unify_parr_ty_help ty   -- Revert to ordinary unification
 830   = newTyVarTy liftedTypeKind           `thenNF_Tc` \ elt_ty ->
 831     unifyTauTy ty (mkPArrTy elt_ty)     `thenTc_`
 832     returnTc elt_ty
 833 \end{code}
 834
 835 \begin{code}
 836 unifyTupleTy :: Boxity -> Arity -> TcType -> TcM [TcType]
 837 unifyTupleTy boxity arity ty@(TyVarTy tyvar)
 838   = getTcTyVar tyvar    `thenNF_Tc` \ maybe_ty ->
 839     case maybe_ty of
 840         Just ty' -> unifyTupleTy boxity arity ty'
 841         other    -> unify_tuple_ty_help boxity arity ty
 842
 843 unifyTupleTy boxity arity ty
 844   = case tcSplitTyConApp_maybe ty of
 845         Just (tycon, arg_tys)
 846                 |  isTupleTyCon tycon
 847                 && tyConArity tycon == arity
 848                 && tupleTyConBoxity tycon == boxity
 849                 -> returnTc arg_tys
 850         other -> unify_tuple_ty_help boxity arity ty
 851
 852 unify_tuple_ty_help boxity arity ty
 853   = newTyVarTys arity kind                              `thenNF_Tc` \ arg_tys ->
 854     unifyTauTy ty (mkTupleTy boxity arity arg_tys)      `thenTc_`
 855     returnTc arg_tys
 856   where
 857     kind | isBoxed boxity = liftedTypeKind
 858          | otherwise      = openTypeKind
 859 \end{code}
 860
 861
 862 %************************************************************************
 863 %*                                                                      *
 864 \subsection{Kind unification}
 865 %*                                                                      *
 866 %************************************************************************
 867
 868 \begin{code}
 869 unifyKind :: TcKind                 -- Expected
 870           -> TcKind                 -- Actual
 871           -> TcM ()
 872 unifyKind k1 k2
 873   = tcAddErrCtxtM (unifyCtxt "kind" k1 k2) $
 874     uTys k1 k1 k2 k2
 875
 876 unifyKinds :: [TcKind] -> [TcKind] -> TcM ()
 877 unifyKinds []       []       = returnTc ()
 878 unifyKinds (k1:ks1) (k2:ks2) = unifyKind k1 k2  `thenTc_`
 879                                unifyKinds ks1 ks2
 880 unifyKinds _ _ = panic "unifyKinds: length mis-match"
 881 \end{code}
 882
 883 \begin{code}
 884 unifyOpenTypeKind :: TcKind -> TcM ()
 885 -- Ensures that the argument kind is of the form (Type bx)
 886 -- for some boxity bx
 887
 888 unifyOpenTypeKind ty@(TyVarTy tyvar)
 889   = getTcTyVar tyvar    `thenNF_Tc` \ maybe_ty ->
 890     case maybe_ty of
 891         Just ty' -> unifyOpenTypeKind ty'
 892         other    -> unify_open_kind_help ty
 893
 894 unifyOpenTypeKind ty
 895   | isTypeKind ty = returnTc ()
 896   | otherwise     = unify_open_kind_help ty
 897
 898 unify_open_kind_help ty -- Revert to ordinary unification
 899   = newBoxityVar        `thenNF_Tc` \ boxity ->
 900     unifyKind ty (mkTyConApp typeCon [boxity])
 901 \end{code}
 902
 903
 904 %************************************************************************
 905 %*                                                                      *
 906 \subsection[Unify-context]{Errors and contexts}
 907 %*                                                                      *
 908 %************************************************************************
 909
 910 Errors
 911 ~~~~~~
 912
 913 \begin{code}
 914 unifyCtxt s ty1 ty2 tidy_env    -- ty1 expected, ty2 inferred
 915   = zonkTcType ty1      `thenNF_Tc` \ ty1' ->
 916     zonkTcType ty2      `thenNF_Tc` \ ty2' ->
 917     returnNF_Tc (err ty1' ty2')
 918   where
 919     err ty1 ty2 = (env1,
 920                    nest 4
 921                         (vcat [
 922                            text "Expected" <+> text s <> colon <+> ppr tidy_ty1,
 923                            text "Inferred" <+> text s <> colon <+> ppr tidy_ty2
 924                         ]))
 925                   where
 926                     (env1, [tidy_ty1,tidy_ty2]) = tidyOpenTypes tidy_env [ty1,ty2]
 927
 928 unifyKindCtxt swapped tv1 ty2 tidy_env  -- not swapped => tv1 expected, ty2 inferred
 929         -- tv1 is zonked already
 930   = zonkTcType ty2      `thenNF_Tc` \ ty2' ->
 931     returnNF_Tc (err ty2')
 932   where
 933     err ty2 = (env2, ptext SLIT("When matching types") <+>
 934                      sep [quotes pp_expected, ptext SLIT("and"), quotes pp_actual])
 935             where
 936               (pp_expected, pp_actual) | swapped   = (pp2, pp1)
 937                                        | otherwise = (pp1, pp2)
 938               (env1, tv1') = tidyOpenTyVar tidy_env tv1
 939               (env2, ty2') = tidyOpenType  env1 ty2
 940               pp1 = ppr tv1'
 941               pp2 = ppr ty2'
 942
 943 unifyMisMatch ty1 ty2
 944   = zonkTcType ty1      `thenNF_Tc` \ ty1' ->
 945     zonkTcType ty2      `thenNF_Tc` \ ty2' ->
 946     let
 947         (env, [tidy_ty1, tidy_ty2]) = tidyOpenTypes emptyTidyEnv [ty1',ty2']
 948         msg = hang (ptext SLIT("Couldn't match"))
 949                    4 (sep [quotes (ppr tidy_ty1),
 950                            ptext SLIT("against"),
 951                            quotes (ppr tidy_ty2)])
 952     in
 953     failWithTcM (env, msg)
 954
 955 unifyWithSigErr tyvar ty
 956   = (env2, hang (ptext SLIT("Cannot unify the type-signature variable") <+> quotes (ppr tidy_tyvar))
 957               4 (ptext SLIT("with the type") <+> quotes (ppr tidy_ty)))
 958   where
 959     (env1, tidy_tyvar) = tidyOpenTyVar emptyTidyEnv tyvar
 960     (env2, tidy_ty)    = tidyOpenType  env1         ty
 961
 962 unifyCheck problem tyvar ty
 963   = (env2, hang msg
 964               4 (sep [ppr tidy_tyvar, char '=', ppr tidy_ty]))
 965   where
 966     (env1, tidy_tyvar) = tidyOpenTyVar emptyTidyEnv tyvar
 967     (env2, tidy_ty)    = tidyOpenType  env1         ty
 968
 969     msg = case problem of
 970             OccurCheck  -> ptext SLIT("Occurs check: cannot construct the infinite type:")
 971             NotMonoType -> ptext SLIT("Cannot unify a type variable with a type scheme:")
 972 \end{code}
 973
 974
 975
 976 %************************************************************************
 977 %*                                                                      *
 978 \subsection{Checking signature type variables}
 979 %*                                                                      *
 980 %************************************************************************
 981
 982 @checkSigTyVars@ is used after the type in a type signature has been unified with
 983 the actual type found.  It then checks that the type variables of the type signature
 984 are
 985         (a) Still all type variables
 986                 eg matching signature [a] against inferred type [(p,q)]
 987                 [then a will be unified to a non-type variable]
 988
 989         (b) Still all distinct
 990                 eg matching signature [(a,b)] against inferred type [(p,p)]
 991                 [then a and b will be unified together]
 992
 993         (c) Not mentioned in the environment
 994                 eg the signature for f in this:
 995
 996                         g x = ... where
 997                                         f :: a->[a]
 998                                         f y = [x,y]
 999
1000                 Here, f is forced to be monorphic by the free occurence of x.
1001
1002         (d) Not (unified with another type variable that is) in scope.
1003                 eg f x :: (r->r) = (\y->y) :: forall a. a->r
1004             when checking the expression type signature, we find that
1005             even though there is nothing in scope whose type mentions r,
1006             nevertheless the type signature for the expression isn't right.
1007
1008             Another example is in a class or instance declaration:
1009                 class C a where
1010                    op :: forall b. a -> b
1011                    op x = x
1012             Here, b gets unified with a
1013
1014 Before doing this, the substitution is applied to the signature type variable.
1015
1016 We used to have the notion of a "DontBind" type variable, which would
1017 only be bound to itself or nothing.  Then points (a) and (b) were
1018 self-checking.  But it gave rise to bogus consequential error messages.
1019 For example:
1020
1021    f = (*)      -- Monomorphic
1022
1023    g :: Num a => a -> a
1024    g x = f x x
1025
1026 Here, we get a complaint when checking the type signature for g,
1027 that g isn't polymorphic enough; but then we get another one when
1028 dealing with the (Num x) context arising from f's definition;
1029 we try to unify x with Int (to default it), but find that x has already
1030 been unified with the DontBind variable "a" from g's signature.
1031 This is really a problem with side-effecting unification; we'd like to
1032 undo g's effects when its type signature fails, but unification is done
1033 by side effect, so we can't (easily).
1034
1035 So we revert to ordinary type variables for signatures, and try to
1036 give a helpful message in checkSigTyVars.
1037
1038 \begin{code}
1039 checkSigTyVars :: [TcTyVar] -> TcM [TcTyVar]
1040 checkSigTyVars sig_tvs = check_sig_tyvars emptyVarSet sig_tvs
1041
1042 checkSigTyVarsWrt :: TcTyVarSet -> [TcTyVar] -> TcM [TcTyVar]
1043 checkSigTyVarsWrt extra_tvs sig_tvs
1044   = zonkTcTyVarsAndFV (varSetElems extra_tvs)   `thenNF_Tc` \ extra_tvs' ->
1045     check_sig_tyvars extra_tvs' sig_tvs
1046
1047 check_sig_tyvars
1048         :: TcTyVarSet           -- Global type variables. The universally quantified
1049                                 --      tyvars should not mention any of these
1050                                 --      Guaranteed already zonked.
1051         -> [TcTyVar]            -- Universally-quantified type variables in the signature
1052                                 --      Not guaranteed zonked.
1053         -> TcM [TcTyVar]        -- Zonked signature type variables
1054
1055 check_sig_tyvars extra_tvs []
1056   = returnTc []
1057 check_sig_tyvars extra_tvs sig_tvs
1058   = zonkTcTyVars sig_tvs        `thenNF_Tc` \ sig_tys ->
1059     tcGetGlobalTyVars           `thenNF_Tc` \ gbl_tvs ->
1060     let
1061         env_tvs = gbl_tvs `unionVarSet` extra_tvs
1062     in
1063     checkTcM (allDistinctTyVars sig_tys env_tvs)
1064              (complain sig_tys env_tvs)         `thenTc_`
1065
1066     returnTc (map (tcGetTyVar "checkSigTyVars") sig_tys)
1067
1068   where
1069     complain sig_tys globals
1070       = -- "check" checks each sig tyvar in turn
1071         foldlNF_Tc check
1072                    (env2, emptyVarEnv, [])
1073                    (tidy_tvs `zip` tidy_tys)    `thenNF_Tc` \ (env3, _, msgs) ->
1074
1075         failWithTcM (env3, main_msg $$ nest 4 (vcat msgs))
1076       where
1077         (env1, tidy_tvs) = tidyOpenTyVars emptyTidyEnv sig_tvs
1078         (env2, tidy_tys) = tidyOpenTypes  env1         sig_tys
1079
1080         main_msg = ptext SLIT("Inferred type is less polymorphic than expected")
1081
1082         check (tidy_env, acc, msgs) (sig_tyvar,ty)
1083                 -- sig_tyvar is from the signature;
1084                 -- ty is what you get if you zonk sig_tyvar and then tidy it
1085                 --
1086                 -- acc maps a zonked type variable back to a signature type variable
1087           = case tcGetTyVar_maybe ty of {
1088               Nothing ->                        -- Error (a)!
1089                         returnNF_Tc (tidy_env, acc, unify_msg sig_tyvar (quotes (ppr ty)) : msgs) ;
1090
1091               Just tv ->
1092
1093             case lookupVarEnv acc tv of {
1094                 Just sig_tyvar' ->      -- Error (b)!
1095                         returnNF_Tc (tidy_env, acc, unify_msg sig_tyvar thing : msgs)
1096                     where
1097                         thing = ptext SLIT("another quantified type variable") <+> quotes (ppr sig_tyvar')
1098
1099               ; Nothing ->
1100
1101             if tv `elemVarSet` globals  -- Error (c) or (d)! Type variable escapes
1102                                         -- The least comprehensible, so put it last
1103                         -- Game plan:
1104                         --       get the local TcIds and TyVars from the environment,
1105                         --       and pass them to find_globals (they might have tv free)
1106             then   tcGetEnv                                     `thenNF_Tc` \ ve ->
1107                    find_globals tv tidy_env  (tcLEnvElts ve)    `thenNF_Tc` \ (tidy_env1, globs) ->
1108                    returnNF_Tc (tidy_env1, acc, escape_msg sig_tyvar tv globs : msgs)
1109
1110             else        -- All OK
1111             returnNF_Tc (tidy_env, extendVarEnv acc tv sig_tyvar, msgs)
1112             }}
1113 \end{code}
1114
1115
1116 \begin{code}
1117 -----------------------
1118 -- find_globals looks at the value environment and finds values
1119 -- whose types mention the offending type variable.  It has to be
1120 -- careful to zonk the Id's type first, so it has to be in the monad.
1121 -- We must be careful to pass it a zonked type variable, too.
1122
1123 find_globals :: Var
1124              -> TidyEnv
1125              -> [TcTyThing]
1126              -> NF_TcM (TidyEnv, [SDoc])
1127
1128 find_globals tv tidy_env things
1129   = go tidy_env [] things
1130   where
1131     go tidy_env acc [] = returnNF_Tc (tidy_env, acc)
1132     go tidy_env acc (thing : things)
1133       = find_thing ignore_it tidy_env thing     `thenNF_Tc` \ (tidy_env1, maybe_doc) ->
1134         case maybe_doc of
1135           Just d  -> go tidy_env1 (d:acc) things
1136           Nothing -> go tidy_env1 acc     things
1137
1138     ignore_it ty = not (tv `elemVarSet` tyVarsOfType ty)
1139
1140 -----------------------
1141 find_thing ignore_it tidy_env (ATcId id)
1142   = zonkTcType  (idType id)     `thenNF_Tc` \ id_ty ->
1143     if ignore_it id_ty then
1144         returnNF_Tc (tidy_env, Nothing)
1145     else let
1146         (tidy_env', tidy_ty) = tidyOpenType tidy_env id_ty
1147         msg = sep [ppr id <+> dcolon <+> ppr tidy_ty,
1148                    nest 2 (parens (ptext SLIT("bound at") <+>
1149                                    ppr (getSrcLoc id)))]
1150     in
1151     returnNF_Tc (tidy_env', Just msg)
1152
1153 find_thing ignore_it tidy_env (ATyVar tv)
1154   = zonkTcTyVar tv              `thenNF_Tc` \ tv_ty ->
1155     if ignore_it tv_ty then
1156         returnNF_Tc (tidy_env, Nothing)
1157     else let
1158         (tidy_env1, tv1)     = tidyOpenTyVar tidy_env  tv
1159         (tidy_env2, tidy_ty) = tidyOpenType  tidy_env1 tv_ty
1160         msg = sep [ppr tv1 <+> eq_stuff, nest 2 bound_at]
1161
1162         eq_stuff | Just tv' <- Type.getTyVar_maybe tv_ty, tv == tv' = empty
1163                  | otherwise                                        = equals <+> ppr tv_ty
1164                 -- It's ok to use Type.getTyVar_maybe because ty is zonked by now
1165
1166         bound_at = tyVarBindingInfo tv
1167     in
1168     returnNF_Tc (tidy_env2, Just msg)
1169
1170 -----------------------
1171 escape_msg sig_tv tv globs
1172   = mk_msg sig_tv <+> ptext SLIT("escapes") $$
1173     if not (null globs) then
1174         vcat [pp_it <+> ptext SLIT("is mentioned in the environment:"),
1175               nest 2 (vcat globs)]
1176      else
1177         empty   -- Sigh.  It's really hard to give a good error message
1178                 -- all the time.   One bad case is an existential pattern match.
1179                 -- We rely on the "When..." context to help.
1180   where
1181     pp_it | sig_tv /= tv = ptext SLIT("It unifies with") <+> quotes (ppr tv) <> comma <+> ptext SLIT("which")
1182           | otherwise    = ptext SLIT("It")
1183
1184
1185 unify_msg tv thing = mk_msg tv <+> ptext SLIT("is unified with") <+> thing
1186 mk_msg tv          = ptext SLIT("Quantified type variable") <+> quotes (ppr tv)
1187 \end{code}
1188
1189 These two context are used with checkSigTyVars
1190
1191 \begin{code}
1192 sigCtxt :: Id -> [TcTyVar] -> TcThetaType -> TcTauType
1193         -> TidyEnv -> NF_TcM (TidyEnv, Message)
1194 sigCtxt id sig_tvs sig_theta sig_tau tidy_env
1195   = zonkTcType sig_tau          `thenNF_Tc` \ actual_tau ->
1196     let
1197         (env1, tidy_sig_tvs)    = tidyOpenTyVars tidy_env sig_tvs
1198         (env2, tidy_sig_rho)    = tidyOpenType env1 (mkPhiTy sig_theta sig_tau)
1199         (env3, tidy_actual_tau) = tidyOpenType env2 actual_tau
1200         sub_msg = vcat [ptext SLIT("Signature type:    ") <+> pprType (mkForAllTys tidy_sig_tvs tidy_sig_rho),
1201                         ptext SLIT("Type to generalise:") <+> pprType tidy_actual_tau
1202                    ]
1203         msg = vcat [ptext SLIT("When trying to generalise the type inferred for") <+> quotes (ppr id),
1204                     nest 4 sub_msg]
1205     in
1206     returnNF_Tc (env3, msg)
1207 \end{code}