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