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