ghc/compiler/typecheck/TcUnify.lhs

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