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