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 -- 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         -- Ignore usage annotations inside typechecker
 424 uTys ps_ty1 (UsageTy _ ty1) ps_ty2 ty2 = uTys ps_ty1 ty1 ps_ty2 ty2
 425 uTys ps_ty1 ty1 ps_ty2 (UsageTy _ ty2) = uTys ps_ty1 ty1 ps_ty2 ty2
 426
 427         -- Variables; go for uVar
 428 uTys ps_ty1 (TyVarTy tyvar1) ps_ty2 ty2 = uVar False tyvar1 ps_ty2 ty2
 429 uTys ps_ty1 ty1 ps_ty2 (TyVarTy tyvar2) = uVar True  tyvar2 ps_ty1 ty1
 430                                         -- "True" means args swapped
 431
 432         -- Predicates
 433 uTys _ (SourceTy (IParam n1 t1)) _ (SourceTy (IParam n2 t2))
 434   | n1 == n2 = uTys t1 t1 t2 t2
 435 uTys _ (SourceTy (ClassP c1 tys1)) _ (SourceTy (ClassP c2 tys2))
 436   | c1 == c2 = unifyTauTyLists tys1 tys2
 437 uTys _ (SourceTy (NType tc1 tys1)) _ (SourceTy (NType tc2 tys2))
 438   | tc1 == tc2 = unifyTauTyLists tys1 tys2
 439
 440         -- Functions; just check the two parts
 441 uTys _ (FunTy fun1 arg1) _ (FunTy fun2 arg2)
 442   = uTys fun1 fun1 fun2 fun2    `thenTc_`    uTys arg1 arg1 arg2 arg2
 443
 444         -- Type constructors must match
 445 uTys ps_ty1 (TyConApp con1 tys1) ps_ty2 (TyConApp con2 tys2)
 446   | con1 == con2 && equalLength tys1 tys2
 447   = unifyTauTyLists tys1 tys2
 448
 449   | con1 == openKindCon
 450         -- When we are doing kind checking, we might match a kind '?'
 451         -- against a kind '*' or '#'.  Notably, CCallable :: ? -> *, and
 452         -- (CCallable Int) and (CCallable Int#) are both OK
 453   = unifyOpenTypeKind ps_ty2
 454
 455         -- Applications need a bit of care!
 456         -- They can match FunTy and TyConApp, so use splitAppTy_maybe
 457         -- NB: we've already dealt with type variables and Notes,
 458         -- so if one type is an App the other one jolly well better be too
 459 uTys ps_ty1 (AppTy s1 t1) ps_ty2 ty2
 460   = case tcSplitAppTy_maybe ty2 of
 461         Just (s2,t2) -> uTys s1 s1 s2 s2        `thenTc_`    uTys t1 t1 t2 t2
 462         Nothing      -> unifyMisMatch ps_ty1 ps_ty2
 463
 464         -- Now the same, but the other way round
 465         -- Don't swap the types, because the error messages get worse
 466 uTys ps_ty1 ty1 ps_ty2 (AppTy s2 t2)
 467   = case tcSplitAppTy_maybe ty1 of
 468         Just (s1,t1) -> uTys s1 s1 s2 s2        `thenTc_`    uTys t1 t1 t2 t2
 469         Nothing      -> unifyMisMatch ps_ty1 ps_ty2
 470
 471         -- Not expecting for-alls in unification
 472         -- ... but the error message from the unifyMisMatch more informative
 473         -- than a panic message!
 474
 475         -- Anything else fails
 476 uTys ps_ty1 ty1 ps_ty2 ty2  = unifyMisMatch ps_ty1 ps_ty2
 477 \end{code}
 478
 479
 480 Notes on synonyms
 481 ~~~~~~~~~~~~~~~~~
 482 If you are tempted to make a short cut on synonyms, as in this
 483 pseudocode...
 484
 485 \begin{verbatim}
 486 -- NO   uTys (SynTy con1 args1 ty1) (SynTy con2 args2 ty2)
 487 -- NO     = if (con1 == con2) then
 488 -- NO   -- Good news!  Same synonym constructors, so we can shortcut
 489 -- NO   -- by unifying their arguments and ignoring their expansions.
 490 -- NO   unifyTauTypeLists args1 args2
 491 -- NO    else
 492 -- NO   -- Never mind.  Just expand them and try again
 493 -- NO   uTys ty1 ty2
 494 \end{verbatim}
 495
 496 then THINK AGAIN.  Here is the whole story, as detected and reported
 497 by Chris Okasaki \tr{<Chris_Okasaki@loch.mess.cs.cmu.edu>}:
 498 \begin{quotation}
 499 Here's a test program that should detect the problem:
 500
 501 \begin{verbatim}
 502         type Bogus a = Int
 503         x = (1 :: Bogus Char) :: Bogus Bool
 504 \end{verbatim}
 505
 506 The problem with [the attempted shortcut code] is that
 507 \begin{verbatim}
 508         con1 == con2
 509 \end{verbatim}
 510 is not a sufficient condition to be able to use the shortcut!
 511 You also need to know that the type synonym actually USES all
 512 its arguments.  For example, consider the following type synonym
 513 which does not use all its arguments.
 514 \begin{verbatim}
 515         type Bogus a = Int
 516 \end{verbatim}
 517
 518 If you ever tried unifying, say, \tr{Bogus Char} with \tr{Bogus Bool},
 519 the unifier would blithely try to unify \tr{Char} with \tr{Bool} and
 520 would fail, even though the expanded forms (both \tr{Int}) should
 521 match.
 522
 523 Similarly, unifying \tr{Bogus Char} with \tr{Bogus t} would
 524 unnecessarily bind \tr{t} to \tr{Char}.
 525
 526 ... You could explicitly test for the problem synonyms and mark them
 527 somehow as needing expansion, perhaps also issuing a warning to the
 528 user.
 529 \end{quotation}
 530
 531
 532 %************************************************************************
 533 %*                                                                      *
 534 \subsection[Unify-uVar]{@uVar@: unifying with a type variable}
 535 %*                                                                      *
 536 %************************************************************************
 537
 538 @uVar@ is called when at least one of the types being unified is a
 539 variable.  It does {\em not} assume that the variable is a fixed point
 540 of the substitution; rather, notice that @uVar@ (defined below) nips
 541 back into @uTys@ if it turns out that the variable is already bound.
 542
 543 \begin{code}
 544 uVar :: Bool            -- False => tyvar is the "expected"
 545                         -- True  => ty    is the "expected" thing
 546      -> TcTyVar
 547      -> TcTauType -> TcTauType  -- printing and real versions
 548      -> TcM ()
 549
 550 uVar swapped tv1 ps_ty2 ty2
 551   = traceTc (text "uVar" <+> ppr swapped <+> ppr tv1 <+> (ppr ps_ty2 $$ ppr ty2))       `thenNF_Tc_`
 552     getTcTyVar tv1      `thenNF_Tc` \ maybe_ty1 ->
 553     case maybe_ty1 of
 554         Just ty1 | swapped   -> uTys ps_ty2 ty2 ty1 ty1 -- Swap back
 555                  | otherwise -> uTys ty1 ty1 ps_ty2 ty2 -- Same order
 556         other       -> uUnboundVar swapped tv1 maybe_ty1 ps_ty2 ty2
 557
 558         -- Expand synonyms; ignore FTVs
 559 uUnboundVar swapped tv1 maybe_ty1 ps_ty2 (NoteTy n2 ty2)
 560   = uUnboundVar swapped tv1 maybe_ty1 ps_ty2 ty2
 561
 562
 563         -- The both-type-variable case
 564 uUnboundVar swapped tv1 maybe_ty1 ps_ty2 ty2@(TyVarTy tv2)
 565
 566         -- Same type variable => no-op
 567   | tv1 == tv2
 568   = returnTc ()
 569
 570         -- Distinct type variables
 571         -- ASSERT maybe_ty1 /= Just
 572   | otherwise
 573   = getTcTyVar tv2      `thenNF_Tc` \ maybe_ty2 ->
 574     case maybe_ty2 of
 575         Just ty2' -> uUnboundVar swapped tv1 maybe_ty1 ty2' ty2'
 576
 577         Nothing | update_tv2
 578
 579                 -> WARN( not (k1 `hasMoreBoxityInfo` k2), (ppr tv1 <+> ppr k1) $$ (ppr tv2 <+> ppr k2) )
 580                    putTcTyVar tv2 (TyVarTy tv1)         `thenNF_Tc_`
 581                    returnTc ()
 582                 |  otherwise
 583
 584                 -> WARN( not (k2 `hasMoreBoxityInfo` k1), (ppr tv2 <+> ppr k2) $$ (ppr tv1 <+> ppr k1) )
 585                    putTcTyVar tv1 ps_ty2                `thenNF_Tc_`
 586                    returnTc ()
 587   where
 588     k1 = tyVarKind tv1
 589     k2 = tyVarKind tv2
 590     update_tv2 = (k2 `eqKind` openTypeKind) || (not (k1 `eqKind` openTypeKind) && nicer_to_update_tv2)
 591                         -- Try to get rid of open type variables as soon as poss
 592
 593     nicer_to_update_tv2 =  isUserTyVar tv1
 594                                 -- Don't unify a signature type variable if poss
 595                         || isSystemName (varName tv2)
 596                                 -- Try to update sys-y type variables in preference to sig-y ones
 597
 598         -- Second one isn't a type variable
 599 uUnboundVar swapped tv1 maybe_ty1 ps_ty2 non_var_ty2
 600   =     -- Check that tv1 isn't a type-signature type variable
 601     checkTcM (not (isSkolemTyVar tv1))
 602              (failWithTcM (unifyWithSigErr tv1 ps_ty2)) `thenTc_`
 603
 604         -- Check that the kinds match
 605     zonkTcType ps_ty2                           `thenNF_Tc` \ ps_ty2' ->
 606     checkKinds swapped tv1 ps_ty2'              `thenTc_`
 607
 608         -- Occurs check
 609         -- Basically we want to update     tv1 := ps_ty2
 610         -- because ps_ty2 has type-synonym info, which improves later error messages
 611         --
 612         -- But consider
 613         --      type A a = ()
 614         --
 615         --      f :: (A a -> a -> ()) -> ()
 616         --      f = \ _ -> ()
 617         --
 618         --      x :: ()
 619         --      x = f (\ x p -> p x)
 620         --
 621         -- In the application (p x), we try to match "t" with "A t".  If we go
 622         -- ahead and bind t to A t (= ps_ty2), we'll lead the type checker into
 623         -- an infinite loop later.
 624         -- But we should not reject the program, because A t = ().
 625         -- Rather, we should bind t to () (= non_var_ty2).
 626         --
 627         -- That's why we have this two-state occurs-check
 628     if not (tv1 `elemVarSet` tyVarsOfType ps_ty2') then
 629         putTcTyVar tv1 ps_ty2'                          `thenNF_Tc_`
 630         returnTc ()
 631     else
 632     zonkTcType non_var_ty2                              `thenNF_Tc` \ non_var_ty2' ->
 633     if not (tv1 `elemVarSet` tyVarsOfType non_var_ty2') then
 634         -- This branch rarely succeeds, except in strange cases
 635         -- like that in the example above
 636         putTcTyVar tv1 non_var_ty2'                     `thenNF_Tc_`
 637         returnTc ()
 638     else
 639     failWithTcM (unifyOccurCheck tv1 ps_ty2')
 640
 641
 642 checkKinds swapped tv1 ty2
 643 -- We're about to unify a type variable tv1 with a non-tyvar-type ty2.
 644 -- ty2 has been zonked at this stage
 645
 646   | tk1 `eqKind` liftedTypeKind && tk2 `eqKind` unliftedTypeKind
 647         -- Check that we don't unify a lifted type variable with an
 648         -- unlifted type: e.g.  (id 3#) is illegal
 649   = tcAddErrCtxtM (unifyKindCtxt swapped tv1 ty2)       $
 650     unifyMisMatch k1 k2
 651
 652   | otherwise
 653   =     -- Check that we aren't losing boxity info (shouldn't happen)
 654     WARN (not (tk2 `hasMoreBoxityInfo` tk1),
 655           (ppr tv1 <+> ppr tk1) $$ (ppr ty2 <+> ppr tk2))
 656     returnTc ()
 657   where
 658     (k1,k2) | swapped   = (tk2,tk1)
 659             | otherwise = (tk1,tk2)
 660     tk1 = tyVarKind tv1
 661     tk2 = typeKind ty2
 662 \end{code}
 663
 664
 665 %************************************************************************
 666 %*                                                                      *
 667 \subsection[Unify-fun]{@unifyFunTy@}
 668 %*                                                                      *
 669 %************************************************************************
 670
 671 @subFunTy@ and @unifyFunTy@ is used to avoid the fruitless
 672 creation of type variables.
 673
 674 * subFunTy is used when we might be faced with a "hole" type variable,
 675   in which case we should create two new holes.
 676
 677 * unifyFunTy is used when we expect to encounter only "ordinary"
 678   type variables, so we should create new ordinary type variables
 679
 680 \begin{code}
 681 subFunTy :: TcSigmaType                 -- Fail if ty isn't a function type
 682          -> TcM (TcType, TcType)        -- otherwise return arg and result types
 683 subFunTy ty@(TyVarTy tyvar)
 684
 685   = getTcTyVar tyvar    `thenNF_Tc` \ maybe_ty ->
 686     case maybe_ty of
 687         Just ty -> subFunTy ty
 688         Nothing | isHoleTyVar tyvar
 689                 -> newHoleTyVarTy       `thenNF_Tc` \ arg ->
 690                    newHoleTyVarTy       `thenNF_Tc` \ res ->
 691                    putTcTyVar tyvar (mkFunTy arg res)   `thenNF_Tc_`
 692                    returnTc (arg,res)
 693                 | otherwise
 694                 -> unify_fun_ty_help ty
 695
 696 subFunTy ty
 697   = case tcSplitFunTy_maybe ty of
 698         Just arg_and_res -> returnTc arg_and_res
 699         Nothing          -> unify_fun_ty_help ty
 700
 701
 702 unifyFunTy :: TcPhiType                 -- Fail if ty isn't a function type
 703            -> TcM (TcType, TcType)      -- otherwise return arg and result types
 704
 705 unifyFunTy ty@(TyVarTy tyvar)
 706   = getTcTyVar tyvar    `thenNF_Tc` \ maybe_ty ->
 707     case maybe_ty of
 708         Just ty' -> unifyFunTy ty'
 709         Nothing  -> unify_fun_ty_help ty
 710
 711 unifyFunTy ty
 712   = case tcSplitFunTy_maybe ty of
 713         Just arg_and_res -> returnTc arg_and_res
 714         Nothing          -> unify_fun_ty_help ty
 715
 716 unify_fun_ty_help ty    -- Special cases failed, so revert to ordinary unification
 717   = newTyVarTy openTypeKind     `thenNF_Tc` \ arg ->
 718     newTyVarTy openTypeKind     `thenNF_Tc` \ res ->
 719     unifyTauTy ty (mkFunTy arg res)     `thenTc_`
 720     returnTc (arg,res)
 721 \end{code}
 722
 723 \begin{code}
 724 unifyListTy :: TcType              -- expected list type
 725             -> TcM TcType      -- list element type
 726
 727 unifyListTy ty@(TyVarTy tyvar)
 728   = getTcTyVar tyvar    `thenNF_Tc` \ maybe_ty ->
 729     case maybe_ty of
 730         Just ty' -> unifyListTy ty'
 731         other    -> unify_list_ty_help ty
 732
 733 unifyListTy ty
 734   = case tcSplitTyConApp_maybe ty of
 735         Just (tycon, [arg_ty]) | tycon == listTyCon -> returnTc arg_ty
 736         other                                       -> unify_list_ty_help ty
 737
 738 unify_list_ty_help ty   -- Revert to ordinary unification
 739   = newTyVarTy liftedTypeKind           `thenNF_Tc` \ elt_ty ->
 740     unifyTauTy ty (mkListTy elt_ty)     `thenTc_`
 741     returnTc elt_ty
 742 \end{code}
 743
 744 \begin{code}
 745 unifyTupleTy :: Boxity -> Arity -> TcType -> TcM [TcType]
 746 unifyTupleTy boxity arity ty@(TyVarTy tyvar)
 747   = getTcTyVar tyvar    `thenNF_Tc` \ maybe_ty ->
 748     case maybe_ty of
 749         Just ty' -> unifyTupleTy boxity arity ty'
 750         other    -> unify_tuple_ty_help boxity arity ty
 751
 752 unifyTupleTy boxity arity ty
 753   = case tcSplitTyConApp_maybe ty of
 754         Just (tycon, arg_tys)
 755                 |  isTupleTyCon tycon
 756                 && tyConArity tycon == arity
 757                 && tupleTyConBoxity tycon == boxity
 758                 -> returnTc arg_tys
 759         other -> unify_tuple_ty_help boxity arity ty
 760
 761 unify_tuple_ty_help boxity arity ty
 762   = newTyVarTys arity kind                              `thenNF_Tc` \ arg_tys ->
 763     unifyTauTy ty (mkTupleTy boxity arity arg_tys)      `thenTc_`
 764     returnTc arg_tys
 765   where
 766     kind | isBoxed boxity = liftedTypeKind
 767          | otherwise      = openTypeKind
 768 \end{code}
 769
 770
 771 %************************************************************************
 772 %*                                                                      *
 773 \subsection{Kind unification}
 774 %*                                                                      *
 775 %************************************************************************
 776
 777 \begin{code}
 778 unifyKind :: TcKind                 -- Expected
 779           -> TcKind                 -- Actual
 780           -> TcM ()
 781 unifyKind k1 k2
 782   = tcAddErrCtxtM (unifyCtxt "kind" k1 k2) $
 783     uTys k1 k1 k2 k2
 784
 785 unifyKinds :: [TcKind] -> [TcKind] -> TcM ()
 786 unifyKinds []       []       = returnTc ()
 787 unifyKinds (k1:ks1) (k2:ks2) = unifyKind k1 k2  `thenTc_`
 788                                unifyKinds ks1 ks2
 789 unifyKinds _ _ = panic "unifyKinds: length mis-match"
 790 \end{code}
 791
 792 \begin{code}
 793 unifyOpenTypeKind :: TcKind -> TcM ()
 794 -- Ensures that the argument kind is of the form (Type bx)
 795 -- for some boxity bx
 796
 797 unifyOpenTypeKind ty@(TyVarTy tyvar)
 798   = getTcTyVar tyvar    `thenNF_Tc` \ maybe_ty ->
 799     case maybe_ty of
 800         Just ty' -> unifyOpenTypeKind ty'
 801         other    -> unify_open_kind_help ty
 802
 803 unifyOpenTypeKind ty
 804   | isTypeKind ty = returnTc ()
 805   | otherwise     = unify_open_kind_help ty
 806
 807 unify_open_kind_help ty -- Revert to ordinary unification
 808   = newBoxityVar        `thenNF_Tc` \ boxity ->
 809     unifyKind ty (mkTyConApp typeCon [boxity])
 810 \end{code}
 811
 812
 813 %************************************************************************
 814 %*                                                                      *
 815 \subsection[Unify-context]{Errors and contexts}
 816 %*                                                                      *
 817 %************************************************************************
 818
 819 Errors
 820 ~~~~~~
 821
 822 \begin{code}
 823 unifyCtxt s ty1 ty2 tidy_env    -- ty1 expected, ty2 inferred
 824   = zonkTcType ty1      `thenNF_Tc` \ ty1' ->
 825     zonkTcType ty2      `thenNF_Tc` \ ty2' ->
 826     returnNF_Tc (err ty1' ty2')
 827   where
 828     err ty1 ty2 = (env1,
 829                    nest 4
 830                         (vcat [
 831                            text "Expected" <+> text s <> colon <+> ppr tidy_ty1,
 832                            text "Inferred" <+> text s <> colon <+> ppr tidy_ty2
 833                         ]))
 834                   where
 835                     (env1, [tidy_ty1,tidy_ty2]) = tidyOpenTypes tidy_env [ty1,ty2]
 836
 837 unifyKindCtxt swapped tv1 ty2 tidy_env  -- not swapped => tv1 expected, ty2 inferred
 838         -- tv1 is zonked already
 839   = zonkTcType ty2      `thenNF_Tc` \ ty2' ->
 840     returnNF_Tc (err ty2')
 841   where
 842     err ty2 = (env2, ptext SLIT("When matching types") <+>
 843                      sep [quotes pp_expected, ptext SLIT("and"), quotes pp_actual])
 844             where
 845               (pp_expected, pp_actual) | swapped   = (pp2, pp1)
 846                                        | otherwise = (pp1, pp2)
 847               (env1, tv1') = tidyOpenTyVar tidy_env tv1
 848               (env2, ty2') = tidyOpenType  env1 ty2
 849               pp1 = ppr tv1'
 850               pp2 = ppr ty2'
 851
 852 unifyMisMatch ty1 ty2
 853   = zonkTcType ty1      `thenNF_Tc` \ ty1' ->
 854     zonkTcType ty2      `thenNF_Tc` \ ty2' ->
 855     let
 856         (env, [tidy_ty1, tidy_ty2]) = tidyOpenTypes emptyTidyEnv [ty1',ty2']
 857         msg = hang (ptext SLIT("Couldn't match"))
 858                    4 (sep [quotes (ppr tidy_ty1),
 859                            ptext SLIT("against"),
 860                            quotes (ppr tidy_ty2)])
 861     in
 862     failWithTcM (env, msg)
 863
 864 unifyWithSigErr tyvar ty
 865   = (env2, hang (ptext SLIT("Cannot unify the type-signature variable") <+> quotes (ppr tidy_tyvar))
 866               4 (ptext SLIT("with the type") <+> quotes (ppr tidy_ty)))
 867   where
 868     (env1, tidy_tyvar) = tidyOpenTyVar emptyTidyEnv tyvar
 869     (env2, tidy_ty)    = tidyOpenType  env1         ty
 870
 871 unifyOccurCheck tyvar ty
 872   = (env2, hang (ptext SLIT("Occurs check: cannot construct the infinite type:"))
 873               4 (sep [ppr tidy_tyvar, char '=', ppr tidy_ty]))
 874   where
 875     (env1, tidy_tyvar) = tidyOpenTyVar emptyTidyEnv tyvar
 876     (env2, tidy_ty)    = tidyOpenType  env1         ty
 877 \end{code}
 878
 879
 880
 881 %************************************************************************
 882 %*                                                                      *
 883 \subsection{Checking signature type variables}
 884 %*                                                                      *
 885 %************************************************************************
 886
 887 @checkSigTyVars@ is used after the type in a type signature has been unified with
 888 the actual type found.  It then checks that the type variables of the type signature
 889 are
 890         (a) Still all type variables
 891                 eg matching signature [a] against inferred type [(p,q)]
 892                 [then a will be unified to a non-type variable]
 893
 894         (b) Still all distinct
 895                 eg matching signature [(a,b)] against inferred type [(p,p)]
 896                 [then a and b will be unified together]
 897
 898         (c) Not mentioned in the environment
 899                 eg the signature for f in this:
 900
 901                         g x = ... where
 902                                         f :: a->[a]
 903                                         f y = [x,y]
 904
 905                 Here, f is forced to be monorphic by the free occurence of x.
 906
 907         (d) Not (unified with another type variable that is) in scope.
 908                 eg f x :: (r->r) = (\y->y) :: forall a. a->r
 909             when checking the expression type signature, we find that
 910             even though there is nothing in scope whose type mentions r,
 911             nevertheless the type signature for the expression isn't right.
 912
 913             Another example is in a class or instance declaration:
 914                 class C a where
 915                    op :: forall b. a -> b
 916                    op x = x
 917             Here, b gets unified with a
 918
 919 Before doing this, the substitution is applied to the signature type variable.
 920
 921 We used to have the notion of a "DontBind" type variable, which would
 922 only be bound to itself or nothing.  Then points (a) and (b) were
 923 self-checking.  But it gave rise to bogus consequential error messages.
 924 For example:
 925
 926    f = (*)      -- Monomorphic
 927
 928    g :: Num a => a -> a
 929    g x = f x x
 930
 931 Here, we get a complaint when checking the type signature for g,
 932 that g isn't polymorphic enough; but then we get another one when
 933 dealing with the (Num x) context arising from f's definition;
 934 we try to unify x with Int (to default it), but find that x has already
 935 been unified with the DontBind variable "a" from g's signature.
 936 This is really a problem with side-effecting unification; we'd like to
 937 undo g's effects when its type signature fails, but unification is done
 938 by side effect, so we can't (easily).
 939
 940 So we revert to ordinary type variables for signatures, and try to
 941 give a helpful message in checkSigTyVars.
 942
 943 \begin{code}
 944 checkSigTyVars :: [TcTyVar]             -- Universally-quantified type variables in the signature
 945                -> TcTyVarSet            -- Tyvars that are free in the type signature
 946                                         --      Not necessarily zonked
 947                                         --      These should *already* be in the free-in-env set,
 948                                         --      and are used here only to improve the error message
 949                -> TcM [TcTyVar]         -- Zonked signature type variables
 950
 951 checkSigTyVars [] free = returnTc []
 952 checkSigTyVars sig_tyvars free_tyvars
 953   = zonkTcTyVars sig_tyvars             `thenNF_Tc` \ sig_tys ->
 954     tcGetGlobalTyVars                   `thenNF_Tc` \ globals ->
 955
 956     checkTcM (allDistinctTyVars sig_tys globals)
 957              (complain sig_tys globals) `thenTc_`
 958
 959     returnTc (map (tcGetTyVar "checkSigTyVars") sig_tys)
 960
 961   where
 962     complain sig_tys globals
 963       = -- "check" checks each sig tyvar in turn
 964         foldlNF_Tc check
 965                    (env2, emptyVarEnv, [])
 966                    (tidy_tvs `zip` tidy_tys)    `thenNF_Tc` \ (env3, _, msgs) ->
 967
 968         failWithTcM (env3, main_msg $$ vcat msgs)
 969       where
 970         (env1, tidy_tvs) = tidyOpenTyVars emptyTidyEnv sig_tyvars
 971         (env2, tidy_tys) = tidyOpenTypes  env1         sig_tys
 972
 973         main_msg = ptext SLIT("Inferred type is less polymorphic than expected")
 974
 975         check (tidy_env, acc, msgs) (sig_tyvar,ty)
 976                 -- sig_tyvar is from the signature;
 977                 -- ty is what you get if you zonk sig_tyvar and then tidy it
 978                 --
 979                 -- acc maps a zonked type variable back to a signature type variable
 980           = case tcGetTyVar_maybe ty of {
 981               Nothing ->                        -- Error (a)!
 982                         returnNF_Tc (tidy_env, acc, unify_msg sig_tyvar (quotes (ppr ty)) : msgs) ;
 983
 984               Just tv ->
 985
 986             case lookupVarEnv acc tv of {
 987                 Just sig_tyvar' ->      -- Error (b)!
 988                         returnNF_Tc (tidy_env, acc, unify_msg sig_tyvar thing : msgs)
 989                     where
 990                         thing = ptext SLIT("another quantified type variable") <+> quotes (ppr sig_tyvar')
 991
 992               ; Nothing ->
 993
 994             if tv `elemVarSet` globals  -- Error (c) or (d)! Type variable escapes
 995                                         -- The least comprehensible, so put it last
 996                         -- Game plan:
 997                         --    a) get the local TcIds and TyVars from the environment,
 998                         --       and pass them to find_globals (they might have tv free)
 999                         --    b) similarly, find any free_tyvars that mention tv
1000             then   tcGetEnv                                                     `thenNF_Tc` \ ve ->
1001                    find_globals tv tidy_env  (tcLEnvElts ve)                    `thenNF_Tc` \ (tidy_env1, globs) ->
1002                    find_frees   tv tidy_env1 [] (varSetElems free_tyvars)       `thenNF_Tc` \ (tidy_env2, frees) ->
1003                    returnNF_Tc (tidy_env2, acc, escape_msg sig_tyvar tv globs frees : msgs)
1004
1005             else        -- All OK
1006             returnNF_Tc (tidy_env, extendVarEnv acc tv sig_tyvar, msgs)
1007             }}
1008
1009 -----------------------
1010 -- find_globals looks at the value environment and finds values
1011 -- whose types mention the offending type variable.  It has to be
1012 -- careful to zonk the Id's type first, so it has to be in the monad.
1013 -- We must be careful to pass it a zonked type variable, too.
1014
1015 find_globals :: Var
1016              -> TidyEnv
1017              -> [TcTyThing]
1018              -> NF_TcM (TidyEnv, [SDoc])
1019
1020 find_globals tv tidy_env things
1021   = go tidy_env [] things
1022   where
1023     go tidy_env acc [] = returnNF_Tc (tidy_env, acc)
1024     go tidy_env acc (thing : things)
1025       = find_thing ignore_it tidy_env thing     `thenNF_Tc` \ (tidy_env1, maybe_doc) ->
1026         case maybe_doc of
1027           Just d  -> go tidy_env1 (d:acc) things
1028           Nothing -> go tidy_env1 acc     things
1029
1030     ignore_it ty = not (tv `elemVarSet` tyVarsOfType ty)
1031
1032 -----------------------
1033 find_thing ignore_it tidy_env (ATcId id)
1034   = zonkTcType  (idType id)     `thenNF_Tc` \ id_ty ->
1035     if ignore_it id_ty then
1036         returnNF_Tc (tidy_env, Nothing)
1037     else let
1038         (tidy_env', tidy_ty) = tidyOpenType tidy_env id_ty
1039         msg = sep [ppr id <+> dcolon <+> ppr tidy_ty,
1040                    nest 2 (parens (ptext SLIT("bound at") <+>
1041                                    ppr (getSrcLoc id)))]
1042     in
1043     returnNF_Tc (tidy_env', Just msg)
1044
1045 find_thing ignore_it tidy_env (ATyVar tv)
1046   = zonkTcTyVar tv              `thenNF_Tc` \ tv_ty ->
1047     if ignore_it tv_ty then
1048         returnNF_Tc (tidy_env, Nothing)
1049     else let
1050         (tidy_env1, tv1)     = tidyOpenTyVar tidy_env  tv
1051         (tidy_env2, tidy_ty) = tidyOpenType  tidy_env1 tv_ty
1052         msg = sep [ptext SLIT("Type variable") <+> quotes (ppr tv1) <+> eq_stuff, nest 2 bound_at]
1053
1054         eq_stuff | Just tv' <- Type.getTyVar_maybe tv_ty, tv == tv' = empty
1055                  | otherwise                                        = equals <+> ppr tv_ty
1056                 -- It's ok to use Type.getTyVar_maybe because ty is zonked by now
1057
1058         bound_at = tyVarBindingInfo tv
1059     in
1060     returnNF_Tc (tidy_env2, Just msg)
1061
1062 -----------------------
1063 find_frees tv tidy_env acc []
1064   = returnNF_Tc (tidy_env, acc)
1065 find_frees tv tidy_env acc (ftv:ftvs)
1066   = zonkTcTyVar ftv     `thenNF_Tc` \ ty ->
1067     if tv `elemVarSet` tyVarsOfType ty then
1068         let
1069             (tidy_env', ftv') = tidyOpenTyVar tidy_env ftv
1070         in
1071         find_frees tv tidy_env' (ftv':acc) ftvs
1072     else
1073         find_frees tv tidy_env  acc        ftvs
1074
1075
1076 escape_msg sig_tv tv globs frees
1077   = mk_msg sig_tv <+> ptext SLIT("escapes") $$
1078     if not (null globs) then
1079         vcat [pp_it <+> ptext SLIT("is mentioned in the environment:"),
1080               nest 2 (vcat globs)]
1081      else if not (null frees) then
1082         vcat [ptext SLIT("It is reachable from the type variable(s)") <+> pprQuotedList frees,
1083               nest 2 (ptext SLIT("which") <+> is_are <+> ptext SLIT("free in the signature"))
1084         ]
1085      else
1086         empty   -- Sigh.  It's really hard to give a good error message
1087                 -- all the time.   One bad case is an existential pattern match
1088   where
1089     is_are | isSingleton frees = ptext SLIT("is")
1090            | otherwise         = ptext SLIT("are")
1091     pp_it | sig_tv /= tv = ptext SLIT("It unifies with") <+> quotes (ppr tv) <> comma <+> ptext SLIT("which")
1092           | otherwise    = ptext SLIT("It")
1093
1094     vcat_first :: Int -> [SDoc] -> SDoc
1095     vcat_first n []     = empty
1096     vcat_first 0 (x:xs) = text "...others omitted..."
1097     vcat_first n (x:xs) = x $$ vcat_first (n-1) xs
1098
1099
1100 unify_msg tv thing = mk_msg tv <+> ptext SLIT("is unified with") <+> thing
1101 mk_msg tv          = ptext SLIT("Quantified type variable") <+> quotes (ppr tv)
1102 \end{code}
1103
1104 These two context are used with checkSigTyVars
1105
1106 \begin{code}
1107 sigCtxt :: [TcTyVar] -> TcThetaType -> TcTauType
1108         -> TidyEnv -> NF_TcM (TidyEnv, Message)
1109 sigCtxt sig_tyvars sig_theta sig_tau tidy_env
1110   = zonkTcType sig_tau          `thenNF_Tc` \ actual_tau ->
1111     let
1112         (env1, tidy_sig_tyvars)  = tidyOpenTyVars tidy_env sig_tyvars
1113         (env2, tidy_sig_rho)     = tidyOpenType env1 (mkRhoTy sig_theta sig_tau)
1114         (env3, tidy_actual_tau)  = tidyOpenType env2 actual_tau
1115         msg = vcat [ptext SLIT("Signature type:    ") <+> pprType (mkForAllTys tidy_sig_tyvars tidy_sig_rho),
1116                     ptext SLIT("Type to generalise:") <+> pprType tidy_actual_tau
1117                    ]
1118     in
1119     returnNF_Tc (env3, msg)
1120
1121 sigPatCtxt bound_tvs bound_ids tidy_env
1122   = returnNF_Tc (env1,
1123                  sep [ptext SLIT("When checking a pattern that binds"),
1124                       nest 4 (vcat (zipWith ppr_id show_ids tidy_tys))])
1125   where
1126     show_ids = filter is_interesting bound_ids
1127     is_interesting id = any (`elemVarSet` idFreeTyVars id) bound_tvs
1128
1129     (env1, tidy_tys) = tidyOpenTypes tidy_env (map idType show_ids)
1130     ppr_id id ty     = ppr id <+> dcolon <+> ppr ty
1131         -- Don't zonk the types so we get the separate, un-unified versions
1132 \end{code}
1133
1134