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