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