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