compiler/typecheck/TcUnify.lhs

   1 %
   2 % (c) The University of Glasgow 2006
   3 % (c) The GRASP/AQUA Project, Glasgow University, 1992-1998
   4 %
   5
   6 Type subsumption and unification
   7
   8 \begin{code}
   9 {-# OPTIONS -w #-}
  10 -- The above warning supression flag is a temporary kludge.
  11 -- While working on this module you are encouraged to remove it and fix
  12 -- any warnings in the module. See
  13 --     http://hackage.haskell.org/trac/ghc/wiki/Commentary/CodingStyle#Warnings
  14 -- for details
  15
  16 module TcUnify (
  17         -- Full-blown subsumption
  18   tcSubExp, tcGen,
  19   checkSigTyVars, checkSigTyVarsWrt, bleatEscapedTvs, sigCtxt,
  20
  21         -- Various unifications
  22   unifyType, unifyTypeList, unifyTheta,
  23   unifyKind, unifyKinds, unifyFunKind,
  24   checkExpectedKind,
  25   preSubType, boxyMatchTypes,
  26
  27   --------------------------------
  28   -- Holes
  29   tcInfer, subFunTys, unBox, refineBox, refineBoxToTau, withBox,
  30   boxyUnify, boxyUnifyList, zapToMonotype,
  31   boxySplitListTy, boxySplitPArrTy, boxySplitTyConApp, boxySplitAppTy,
  32   wrapFunResCoercion
  33   ) where
  34
  35 #include "HsVersions.h"
  36
  37 import HsSyn
  38 import TypeRep
  39
  40 import TcMType
  41 import TcSimplify
  42 import TcEnv
  43 import TcTyFuns
  44 import TcIface
  45 import TcRnMonad         -- TcType, amongst others
  46 import TcType
  47 import Type
  48 import Coercion
  49 import TysPrim
  50 import Inst
  51 import TyCon
  52 import TysWiredIn
  53 import Var
  54 import VarSet
  55 import VarEnv
  56 import Name
  57 import ErrUtils
  58 import Maybes
  59 import BasicTypes
  60 import Util
  61 import Outputable
  62 import Unique
  63 \end{code}
  64
  65 %************************************************************************
  66 %*                                                                      *
  67 \subsection{'hole' type variables}
  68 %*                                                                      *
  69 %************************************************************************
  70
  71 \begin{code}
  72 tcInfer :: (BoxyType -> TcM a) -> TcM (a, TcType)
  73 tcInfer tc_infer = withBox openTypeKind tc_infer
  74 \end{code}
  75
  76
  77 %************************************************************************
  78 %*                                                                      *
  79         subFunTys
  80 %*                                                                      *
  81 %************************************************************************
  82
  83 \begin{code}
  84 subFunTys :: SDoc  -- Somthing like "The function f has 3 arguments"
  85                    -- or "The abstraction (\x.e) takes 1 argument"
  86           -> Arity              -- Expected # of args
  87           -> BoxyRhoType        -- res_ty
  88           -> ([BoxySigmaType] -> BoxyRhoType -> TcM a)
  89           -> TcM (HsWrapper, a)
  90 -- Attempt to decompse res_ty to have enough top-level arrows to
  91 -- match the number of patterns in the match group
  92 --
  93 -- If (subFunTys n_args res_ty thing_inside) = (co_fn, res)
  94 -- and the inner call to thing_inside passes args: [a1,...,an], b
  95 -- then co_fn :: (a1 -> ... -> an -> b) ~ res_ty
  96 --
  97 -- Note that it takes a BoxyRho type, and guarantees to return a BoxyRhoType
  98
  99
 100 {-      Error messages from subFunTys
 101
 102    The abstraction `\Just 1 -> ...' has two arguments
 103    but its type `Maybe a -> a' has only one
 104
 105    The equation(s) for `f' have two arguments
 106    but its type `Maybe a -> a' has only one
 107
 108    The section `(f 3)' requires 'f' to take two arguments
 109    but its type `Int -> Int' has only one
 110
 111    The function 'f' is applied to two arguments
 112    but its type `Int -> Int' has only one
 113 -}
 114
 115
 116 subFunTys error_herald n_pats res_ty thing_inside
 117   = loop n_pats [] res_ty
 118   where
 119         -- In 'loop', the parameter 'arg_tys' accumulates
 120         -- the arg types so far, in *reverse order*
 121         -- INVARIANT:   res_ty :: *
 122     loop n args_so_far res_ty
 123         | Just res_ty' <- tcView res_ty  = loop n args_so_far res_ty'
 124
 125     loop n args_so_far res_ty
 126         | isSigmaTy res_ty      -- Do this before checking n==0, because we
 127                                 -- guarantee to return a BoxyRhoType, not a
 128                                 -- BoxySigmaType
 129         = do { (gen_fn, (co_fn, res)) <- tcGen res_ty emptyVarSet $ \ _ res_ty' ->
 130                                          loop n args_so_far res_ty'
 131              ; return (gen_fn <.> co_fn, res) }
 132
 133     loop 0 args_so_far res_ty
 134         = do { res <- thing_inside (reverse args_so_far) res_ty
 135              ; return (idHsWrapper, res) }
 136
 137     loop n args_so_far (FunTy arg_ty res_ty)
 138         = do { (co_fn, res) <- loop (n-1) (arg_ty:args_so_far) res_ty
 139              ; co_fn' <- wrapFunResCoercion [arg_ty] co_fn
 140              ; return (co_fn', res) }
 141
 142         -- Try to normalise synonym families and defer if that's not possible
 143     loop n args_so_far ty@(TyConApp tc tys)
 144         | isOpenSynTyCon tc
 145         = do { (coi1, ty') <- tcNormaliseFamInst ty
 146              ; case coi1 of
 147                  IdCo   -> defer n args_so_far ty
 148                                     -- no progress, but maybe solvable => defer
 149                  ACo _  ->          -- progress: so lets try again
 150                    do { (co_fn, res) <- loop n args_so_far ty'
 151                       ; return $ (co_fn <.> coiToHsWrapper (mkSymCoI coi1), res)
 152                       }
 153              }
 154
 155         -- res_ty might have a type variable at the head, such as (a b c),
 156         -- in which case we must fill in with (->).  Simplest thing to do
 157         -- is to use boxyUnify, but we catch failure and generate our own
 158         -- error message on failure
 159     loop n args_so_far res_ty@(AppTy _ _)
 160         = do { [arg_ty',res_ty'] <- newBoxyTyVarTys [argTypeKind, openTypeKind]
 161              ; (_, mb_coi) <- tryTcErrs $
 162                                 boxyUnify res_ty (FunTy arg_ty' res_ty')
 163              ; if isNothing mb_coi then bale_out args_so_far
 164                else do { let coi = expectJust "subFunTys" mb_coi
 165                        ; (co_fn, res) <- loop n args_so_far (FunTy arg_ty'
 166                                                                    res_ty')
 167                        ; return (co_fn <.> coiToHsWrapper coi, res)
 168                        }
 169              }
 170
 171     loop n args_so_far ty@(TyVarTy tv)
 172         | isTyConableTyVar tv
 173         = do { cts <- readMetaTyVar tv
 174              ; case cts of
 175                  Indirect ty -> loop n args_so_far ty
 176                  Flexi ->
 177                    do { (res_ty:arg_tys) <- withMetaTvs tv kinds mk_res_ty
 178                       ; res <- thing_inside (reverse args_so_far ++ arg_tys)
 179                                             res_ty
 180                       ; return (idHsWrapper, res) } }
 181         | otherwise             -- defer as tyvar may be refined by equalities
 182         = defer n args_so_far ty
 183         where
 184           mk_res_ty (res_ty' : arg_tys') = mkFunTys arg_tys' res_ty'
 185           mk_res_ty [] = panic "TcUnify.mk_res_ty1"
 186           kinds = openTypeKind : take n (repeat argTypeKind)
 187                 -- Note argTypeKind: the args can have an unboxed type,
 188                 -- but not an unboxed tuple.
 189
 190     loop n args_so_far res_ty = bale_out args_so_far
 191
 192          -- build a template type a1 -> ... -> an -> b and defer an equality
 193          -- between that template and the expected result type res_ty; then,
 194          -- use the template to type the thing_inside
 195     defer n args_so_far ty
 196       = do { arg_tys <- newFlexiTyVarTys n argTypeKind
 197            ; res_ty' <- newFlexiTyVarTy openTypeKind
 198            ; let fun_ty = mkFunTys arg_tys res_ty'
 199                  err    = error_herald <> comma $$
 200                           text "which does not match its type"
 201            ; coi <- addErrCtxt err $
 202                       defer_unification False False fun_ty ty
 203            ; res <- thing_inside (reverse args_so_far ++ arg_tys) res_ty'
 204            ; return (coiToHsWrapper coi, res)
 205            }
 206
 207     bale_out args_so_far
 208         = do { env0 <- tcInitTidyEnv
 209              ; res_ty' <- zonkTcType res_ty
 210              ; let (env1, res_ty'') = tidyOpenType env0 res_ty'
 211              ; failWithTcM (env1, mk_msg res_ty'' (length args_so_far)) }
 212
 213     mk_msg res_ty n_actual
 214       = error_herald <> comma $$
 215         sep [ptext SLIT("but its type") <+> quotes (pprType res_ty),
 216              if n_actual == 0 then ptext SLIT("has none")
 217              else ptext SLIT("has only") <+> speakN n_actual]
 218 \end{code}
 219
 220 \begin{code}
 221 ----------------------
 222 boxySplitTyConApp :: TyCon                      -- T :: k1 -> ... -> kn -> *
 223                   -> BoxyRhoType                -- Expected type (T a b c)
 224                   -> TcM ([BoxySigmaType],      -- Element types, a b c
 225                           CoercionI)            -- T a b c ~ orig_ty
 226   -- It's used for wired-in tycons, so we call checkWiredInTyCon
 227   -- Precondition: never called with FunTyCon
 228   -- Precondition: input type :: *
 229
 230 boxySplitTyConApp tc orig_ty
 231   = do  { checkWiredInTyCon tc
 232         ; loop (tyConArity tc) [] orig_ty }
 233   where
 234     loop n_req args_so_far ty
 235       | Just ty' <- tcView ty = loop n_req args_so_far ty'
 236
 237     loop n_req args_so_far ty@(TyConApp tycon args)
 238       | tc == tycon
 239       = ASSERT( n_req == length args)   -- ty::*
 240         return (args ++ args_so_far, IdCo)
 241
 242       | isOpenSynTyCon tycon        -- try to normalise type family application
 243       = do { (coi1, ty') <- tcNormaliseFamInst ty
 244            ; traceTc $ text "boxySplitTyConApp:" <+>
 245                        ppr ty <+> text "==>" <+> ppr ty'
 246            ; case coi1 of
 247                IdCo   -> defer    -- no progress, but maybe solvable => defer
 248                ACo _  ->          -- progress: so lets try again
 249                  do { (args, coi2) <- loop n_req args_so_far ty'
 250                     ; return $ (args, coi2 `mkTransCoI` mkSymCoI coi1)
 251                     }
 252            }
 253
 254     loop n_req args_so_far (AppTy fun arg)
 255       | n_req > 0
 256       = do { (args, coi) <- loop (n_req - 1) (arg:args_so_far) fun
 257            ; return (args, mkAppTyCoI fun coi arg IdCo)
 258            }
 259
 260     loop n_req args_so_far (TyVarTy tv)
 261       | isTyConableTyVar tv
 262       , res_kind `isSubKind` tyVarKind tv
 263       = do { cts <- readMetaTyVar tv
 264            ; case cts of
 265                Indirect ty -> loop n_req args_so_far ty
 266                Flexi       -> do { arg_tys <- withMetaTvs tv arg_kinds mk_res_ty
 267                                  ; return (arg_tys ++ args_so_far, IdCo) }
 268            }
 269       | otherwise             -- defer as tyvar may be refined by equalities
 270       = defer
 271       where
 272         (arg_kinds, res_kind) = splitKindFunTysN n_req (tyConKind tc)
 273
 274     loop _ _ _ = boxySplitFailure (mkTyConApp tc (mkTyVarTys (tyConTyVars tc)))
 275                                   orig_ty
 276
 277     -- defer splitting by generating an equality constraint
 278     defer = boxySplitDefer arg_kinds mk_res_ty orig_ty
 279       where
 280         (arg_kinds, _) = splitKindFunTys (tyConKind tc)
 281
 282     -- apply splitted tycon to arguments
 283     mk_res_ty = mkTyConApp tc
 284
 285 ----------------------
 286 boxySplitListTy :: BoxyRhoType -> TcM (BoxySigmaType, CoercionI)
 287 -- Special case for lists
 288 boxySplitListTy exp_ty
 289  = do { ([elt_ty], coi) <- boxySplitTyConApp listTyCon exp_ty
 290       ; return (elt_ty, coi) }
 291
 292 ----------------------
 293 boxySplitPArrTy :: BoxyRhoType -> TcM (BoxySigmaType, CoercionI)
 294 -- Special case for parrs
 295 boxySplitPArrTy exp_ty
 296   = do { ([elt_ty], coi) <- boxySplitTyConApp parrTyCon exp_ty
 297        ; return (elt_ty, coi) }
 298
 299 ----------------------
 300 boxySplitAppTy :: BoxyRhoType                           -- Type to split: m a
 301                -> TcM ((BoxySigmaType, BoxySigmaType),  -- Returns m, a
 302                        CoercionI)
 303 -- If the incoming type is a mutable type variable of kind k, then
 304 -- boxySplitAppTy returns a new type variable (m: * -> k); note the *.
 305 -- If the incoming type is boxy, then so are the result types; and vice versa
 306
 307 boxySplitAppTy orig_ty
 308   = loop orig_ty
 309   where
 310     loop ty
 311       | Just ty' <- tcView ty = loop ty'
 312
 313     loop ty
 314       | Just (fun_ty, arg_ty) <- tcSplitAppTy_maybe ty
 315       = return ((fun_ty, arg_ty), IdCo)
 316
 317     loop ty@(TyConApp tycon _args)
 318       | isOpenSynTyCon tycon        -- try to normalise type family application
 319       = do { (coi1, ty') <- tcNormaliseFamInst ty
 320            ; case coi1 of
 321                IdCo   -> defer    -- no progress, but maybe solvable => defer
 322                ACo co ->          -- progress: so lets try again
 323                  do { (args, coi2) <- loop ty'
 324                     ; return $ (args, coi2 `mkTransCoI` mkSymCoI coi1)
 325                     }
 326            }
 327
 328     loop (TyVarTy tv)
 329       | isTyConableTyVar tv
 330       = do { cts <- readMetaTyVar tv
 331            ; case cts of
 332                Indirect ty -> loop ty
 333                Flexi -> do { [fun_ty, arg_ty] <- withMetaTvs tv kinds mk_res_ty
 334                            ; return ((fun_ty, arg_ty), IdCo) } }
 335       | otherwise             -- defer as tyvar may be refined by equalities
 336       = defer
 337       where
 338         tv_kind = tyVarKind tv
 339         kinds = [mkArrowKind liftedTypeKind (defaultKind tv_kind),
 340                                                 -- m :: * -> k
 341                  liftedTypeKind]                -- arg type :: *
 342         -- The defaultKind is a bit smelly.  If you remove it,
 343         -- try compiling        f x = do { x }
 344         -- and you'll get a kind mis-match.  It smells, but
 345         -- not enough to lose sleep over.
 346
 347     loop _ = boxySplitFailure (mkAppTy alphaTy betaTy) orig_ty
 348
 349     -- defer splitting by generating an equality constraint
 350     defer = do { ([ty1, ty2], coi) <- boxySplitDefer arg_kinds mk_res_ty orig_ty
 351                ; return ((ty1, ty2), coi)
 352                }
 353       where
 354         orig_kind = typeKind orig_ty
 355         arg_kinds = [mkArrowKind liftedTypeKind (defaultKind orig_kind),
 356                                                 -- m :: * -> k
 357                      liftedTypeKind]            -- arg type :: *
 358
 359     -- build type application
 360     mk_res_ty [fun_ty', arg_ty'] = mkAppTy fun_ty' arg_ty'
 361     mk_res_ty _other             = panic "TcUnify.mk_res_ty2"
 362
 363 ------------------
 364 boxySplitFailure actual_ty expected_ty
 365   = unifyMisMatch False False actual_ty expected_ty
 366         -- "outer" is False, so we don't pop the context
 367         -- which is what we want since we have not pushed one!
 368
 369 ------------------
 370 boxySplitDefer :: [Kind]                   -- kinds of required arguments
 371                -> ([TcType] -> TcTauType)  -- construct lhs from argument tyvars
 372                -> BoxyRhoType              -- type to split
 373                -> TcM ([TcType], CoercionI)
 374 boxySplitDefer kinds mkTy orig_ty
 375   = do { tau_tys <- mapM newFlexiTyVarTy kinds
 376        ; coi <- defer_unification False False (mkTy tau_tys) orig_ty
 377        ; return (tau_tys, coi)
 378        }
 379 \end{code}
 380
 381
 382 --------------------------------
 383 -- withBoxes: the key utility function
 384 --------------------------------
 385
 386 \begin{code}
 387 withMetaTvs :: TcTyVar  -- An unfilled-in, non-skolem, meta type variable
 388             -> [Kind]   -- Make fresh boxes (with the same BoxTv/TauTv setting as tv)
 389             -> ([BoxySigmaType] -> BoxySigmaType)
 390                                         -- Constructs the type to assign
 391                                         -- to the original var
 392             -> TcM [BoxySigmaType]      -- Return the fresh boxes
 393
 394 -- It's entirely possible for the [kind] to be empty.
 395 -- For example, when pattern-matching on True,
 396 -- we call boxySplitTyConApp passing a boolTyCon
 397
 398 -- Invariant: tv is still Flexi
 399
 400 withMetaTvs tv kinds mk_res_ty
 401   | isBoxyTyVar tv
 402   = do  { box_tvs <- mapM (newMetaTyVar BoxTv) kinds
 403         ; let box_tys = mkTyVarTys box_tvs
 404         ; writeMetaTyVar tv (mk_res_ty box_tys)
 405         ; return box_tys }
 406
 407   | otherwise                   -- Non-boxy meta type variable
 408   = do  { tau_tys <- mapM newFlexiTyVarTy kinds
 409         ; writeMetaTyVar tv (mk_res_ty tau_tys) -- Write it *first*
 410                                                 -- Sure to be a tau-type
 411         ; return tau_tys }
 412
 413 withBox :: Kind -> (BoxySigmaType -> TcM a) -> TcM (a, TcType)
 414 -- Allocate a *boxy* tyvar
 415 withBox kind thing_inside
 416   = do  { box_tv <- newBoxyTyVar kind
 417         ; res <- thing_inside (mkTyVarTy box_tv)
 418         ; ty  <- {- pprTrace "with_box" (ppr (mkTyVarTy box_tv)) $ -} readFilledBox box_tv
 419         ; return (res, ty) }
 420 \end{code}
 421
 422
 423 %************************************************************************
 424 %*                                                                      *
 425                 Approximate boxy matching
 426 %*                                                                      *
 427 %************************************************************************
 428
 429 \begin{code}
 430 preSubType :: [TcTyVar]         -- Quantified type variables
 431            -> TcTyVarSet        -- Subset of quantified type variables
 432                                 --   see Note [Pre-sub boxy]
 433             -> TcType           -- The rho-type part; quantified tyvars scopes over this
 434             -> BoxySigmaType    -- Matching type from the context
 435             -> TcM [TcType]     -- Types to instantiate the tyvars
 436 -- Perform pre-subsumption, and return suitable types
 437 -- to instantiate the quantified type varibles:
 438 --      info from the pre-subsumption, if there is any
 439 --      a boxy type variable otherwise
 440 --
 441 -- Note [Pre-sub boxy]
 442 --   The 'btvs' are a subset of 'qtvs'.  They are the ones we can
 443 --   instantiate to a boxy type variable, because they'll definitely be
 444 --   filled in later.  This isn't always the case; sometimes we have type
 445 --   variables mentioned in the context of the type, but not the body;
 446 --                f :: forall a b. C a b => a -> a
 447 --   Then we may land up with an unconstrained 'b', so we want to
 448 --   instantiate it to a monotype (non-boxy) type variable
 449 --
 450 -- The 'qtvs' that are *neither* fixed by the pre-subsumption, *nor* are in 'btvs',
 451 -- are instantiated to TauTv meta variables.
 452
 453 preSubType qtvs btvs qty expected_ty
 454   = do { tys <- mapM inst_tv qtvs
 455         ; traceTc (text "preSubType" <+> (ppr qtvs $$ ppr btvs $$ ppr qty $$ ppr expected_ty $$ ppr pre_subst $$ ppr tys))
 456         ; return tys }
 457   where
 458     pre_subst = boxySubMatchType (mkVarSet qtvs) qty expected_ty
 459     inst_tv tv
 460         | Just boxy_ty <- lookupTyVar pre_subst tv = return boxy_ty
 461         | tv `elemVarSet` btvs = do { tv' <- tcInstBoxyTyVar tv
 462                                     ; return (mkTyVarTy tv') }
 463         | otherwise            = do { tv' <- tcInstTyVar tv
 464                                     ; return (mkTyVarTy tv') }
 465
 466 boxySubMatchType
 467         :: TcTyVarSet -> TcType -- The "template"; the tyvars are skolems
 468         -> BoxyRhoType          -- Type to match (note a *Rho* type)
 469         -> TvSubst              -- Substitution of the [TcTyVar] to BoxySigmaTypes
 470
 471 -- boxySubMatchType implements the Pre-subsumption judgement, in Fig 5 of the paper
 472 -- "Boxy types: inference for higher rank types and impredicativity"
 473
 474 boxySubMatchType tmpl_tvs tmpl_ty boxy_ty
 475   = go tmpl_tvs tmpl_ty emptyVarSet boxy_ty
 476   where
 477     go t_tvs t_ty b_tvs b_ty
 478         | Just t_ty' <- tcView t_ty = go t_tvs t_ty' b_tvs b_ty
 479         | Just b_ty' <- tcView b_ty = go t_tvs t_ty b_tvs b_ty'
 480
 481     go t_tvs (TyVarTy _) b_tvs b_ty = emptyTvSubst      -- Rule S-ANY; no bindings
 482         -- Rule S-ANY covers (a) type variables and (b) boxy types
 483         -- in the template.  Both look like a TyVarTy.
 484         -- See Note [Sub-match] below
 485
 486     go t_tvs t_ty b_tvs b_ty
 487         | isSigmaTy t_ty, (tvs, _, t_tau) <- tcSplitSigmaTy t_ty
 488         = go (t_tvs `delVarSetList` tvs) t_tau b_tvs b_ty       -- Rule S-SPEC
 489                 -- Under a forall on the left, if there is shadowing,
 490                 -- do not bind! Hence the delVarSetList.
 491         | isSigmaTy b_ty, (tvs, _, b_tau) <- tcSplitSigmaTy b_ty
 492         = go t_tvs t_ty (extendVarSetList b_tvs tvs) b_tau      -- Rule S-SKOL
 493                 -- Add to the variables we must not bind to
 494         -- NB: it's *important* to discard the theta part. Otherwise
 495         -- consider (forall a. Eq a => a -> b) ~<~ (Int -> Int -> Bool)
 496         -- and end up with a completely bogus binding (b |-> Bool), by lining
 497         -- up the (Eq a) with the Int, whereas it should be (b |-> (Int->Bool)).
 498         -- This pre-subsumption stuff can return too few bindings, but it
 499         -- must *never* return bogus info.
 500
 501     go t_tvs (FunTy arg1 res1) b_tvs (FunTy arg2 res2)  -- Rule S-FUN
 502         = boxy_match t_tvs arg1 b_tvs arg2 (go t_tvs res1 b_tvs res2)
 503         -- Match the args, and sub-match the results
 504
 505     go t_tvs t_ty b_tvs b_ty = boxy_match t_tvs t_ty b_tvs b_ty emptyTvSubst
 506         -- Otherwise defer to boxy matching
 507         -- This covers TyConApp, AppTy, PredTy
 508 \end{code}
 509
 510 Note [Sub-match]
 511 ~~~~~~~~~~~~~~~~
 512 Consider this
 513         head :: [a] -> a
 514         |- head xs : <rhobox>
 515 We will do a boxySubMatchType between   a ~ <rhobox>
 516 But we *don't* want to match [a |-> <rhobox>] because
 517     (a) The box should be filled in with a rho-type, but
 518            but the returned substitution maps TyVars to boxy
 519            *sigma* types
 520     (b) In any case, the right final answer might be *either*
 521            instantiate 'a' with a rho-type or a sigma type
 522            head xs : Int   vs   head xs : forall b. b->b
 523 So the matcher MUST NOT make a choice here.   In general, we only
 524 bind a template type variable in boxyMatchType, not in boxySubMatchType.
 525
 526
 527 \begin{code}
 528 boxyMatchTypes
 529         :: TcTyVarSet -> [TcType] -- The "template"; the tyvars are skolems
 530         -> [BoxySigmaType]        -- Type to match
 531         -> TvSubst                -- Substitution of the [TcTyVar] to BoxySigmaTypes
 532
 533 -- boxyMatchTypes implements the Pre-matching judgement, in Fig 5 of the paper
 534 -- "Boxy types: inference for higher rank types and impredicativity"
 535
 536 -- Find a *boxy* substitution that makes the template look as much
 537 --      like the BoxySigmaType as possible.
 538 -- It's always ok to return an empty substitution;
 539 --      anything more is jam on the pudding
 540 --
 541 -- NB1: This is a pure, non-monadic function.
 542 --      It does no unification, and cannot fail
 543 --
 544 -- Precondition: the arg lengths are equal
 545 -- Precondition: none of the template type variables appear anywhere in the [BoxySigmaType]
 546 --
 547
 548 ------------
 549 boxyMatchTypes tmpl_tvs tmpl_tys boxy_tys
 550   = ASSERT( length tmpl_tys == length boxy_tys )
 551     boxy_match_s tmpl_tvs tmpl_tys emptyVarSet boxy_tys emptyTvSubst
 552         -- ToDo: add error context?
 553
 554 boxy_match_s tmpl_tvs [] boxy_tvs [] subst
 555   = subst
 556 boxy_match_s tmpl_tvs (t_ty:t_tys) boxy_tvs (b_ty:b_tys) subst
 557   = boxy_match tmpl_tvs t_ty boxy_tvs b_ty $
 558     boxy_match_s tmpl_tvs t_tys boxy_tvs b_tys subst
 559 boxy_match_s tmpl_tvs _ boxy_tvs _ subst
 560   = panic "boxy_match_s"        -- Lengths do not match
 561
 562
 563 ------------
 564 boxy_match :: TcTyVarSet -> TcType      -- Template
 565            -> TcTyVarSet                -- boxy_tvs: do not bind template tyvars to any of these
 566            -> BoxySigmaType             -- Match against this type
 567            -> TvSubst
 568            -> TvSubst
 569
 570 -- The boxy_tvs argument prevents this match:
 571 --      [a]  forall b. a  ~  forall b. b
 572 -- We don't want to bind the template variable 'a'
 573 -- to the quantified type variable 'b'!
 574
 575 boxy_match tmpl_tvs orig_tmpl_ty boxy_tvs orig_boxy_ty subst
 576   = go orig_tmpl_ty orig_boxy_ty
 577   where
 578     go t_ty b_ty
 579         | Just t_ty' <- tcView t_ty = go t_ty' b_ty
 580         | Just b_ty' <- tcView b_ty = go t_ty b_ty'
 581
 582     go ty1 ty2          -- C.f. the isSigmaTy case for boxySubMatchType
 583         | isSigmaTy ty1
 584         , (tvs1, _, tau1) <- tcSplitSigmaTy ty1
 585         , (tvs2, _, tau2) <- tcSplitSigmaTy ty2
 586         , equalLength tvs1 tvs2
 587         = boxy_match (tmpl_tvs `delVarSetList` tvs1)    tau1
 588                      (boxy_tvs `extendVarSetList` tvs2) tau2 subst
 589
 590     go (TyConApp tc1 tys1) (TyConApp tc2 tys2)
 591         | tc1 == tc2
 592         , not $ isOpenSynTyCon tc1
 593         = go_s tys1 tys2
 594
 595     go (FunTy arg1 res1) (FunTy arg2 res2)
 596         = go_s [arg1,res1] [arg2,res2]
 597
 598     go t_ty b_ty
 599         | Just (s1,t1) <- tcSplitAppTy_maybe t_ty,
 600           Just (s2,t2) <- tcSplitAppTy_maybe b_ty,
 601           typeKind t2 `isSubKind` typeKind t1   -- Maintain invariant
 602         = go_s [s1,t1] [s2,t2]
 603
 604     go (TyVarTy tv) b_ty
 605         | tv `elemVarSet` tmpl_tvs      -- Template type variable in the template
 606         , boxy_tvs `disjointVarSet` tyVarsOfType orig_boxy_ty
 607         , typeKind b_ty `isSubKind` tyVarKind tv  -- See Note [Matching kinds]
 608         = extendTvSubst subst tv boxy_ty'
 609         | otherwise
 610         = subst                         -- Ignore others
 611         where
 612           boxy_ty' = case lookupTyVar subst tv of
 613                         Nothing -> orig_boxy_ty
 614                         Just ty -> ty `boxyLub` orig_boxy_ty
 615
 616     go _ _ = emptyTvSubst       -- It's important to *fail* by returning the empty substitution
 617         -- Example:  Tree a ~ Maybe Int
 618         -- We do not want to bind (a |-> Int) in pre-matching, because that can give very
 619         -- misleading error messages.  An even more confusing case is
 620         --           a -> b ~ Maybe Int
 621         -- Then we do not want to bind (b |-> Int)!  It's always safe to discard bindings
 622         -- from this pre-matching phase.
 623
 624     --------
 625     go_s tys1 tys2 = boxy_match_s tmpl_tvs tys1 boxy_tvs tys2 subst
 626
 627
 628 boxyLub :: BoxySigmaType -> BoxySigmaType -> BoxySigmaType
 629 -- Combine boxy information from the two types
 630 -- If there is a conflict, return the first
 631 boxyLub orig_ty1 orig_ty2
 632   = go orig_ty1 orig_ty2
 633   where
 634     go (AppTy f1 a1) (AppTy f2 a2) = AppTy (boxyLub f1 f2) (boxyLub a1 a2)
 635     go (FunTy f1 a1) (FunTy f2 a2) = FunTy (boxyLub f1 f2) (boxyLub a1 a2)
 636     go (TyConApp tc1 ts1) (TyConApp tc2 ts2)
 637       | tc1 == tc2, length ts1 == length ts2
 638       = TyConApp tc1 (zipWith boxyLub ts1 ts2)
 639
 640     go (TyVarTy tv1) ty2                -- This is the whole point;
 641       | isTcTyVar tv1, isBoxyTyVar tv1  -- choose ty2 if ty2 is a box
 642       = orig_ty2
 643
 644         -- Look inside type synonyms, but only if the naive version fails
 645     go ty1 ty2 | Just ty1' <- tcView ty1 = go ty1' ty2
 646                | Just ty2' <- tcView ty1 = go ty1 ty2'
 647
 648     -- For now, we don't look inside ForAlls, PredTys
 649     go ty1 ty2 = orig_ty1       -- Default
 650 \end{code}
 651
 652 Note [Matching kinds]
 653 ~~~~~~~~~~~~~~~~~~~~~
 654 The target type might legitimately not be a sub-kind of template.
 655 For example, suppose the target is simply a box with an OpenTypeKind,
 656 and the template is a type variable with LiftedTypeKind.
 657 Then it's ok (because the target type will later be refined).
 658 We simply don't bind the template type variable.
 659
 660 It might also be that the kind mis-match is an error. For example,
 661 suppose we match the template (a -> Int) against (Int# -> Int),
 662 where the template type variable 'a' has LiftedTypeKind.  This
 663 matching function does not fail; it simply doesn't bind the template.
 664 Later stuff will fail.
 665
 666 %************************************************************************
 667 %*                                                                      *
 668                 Subsumption checking
 669 %*                                                                      *
 670 %************************************************************************
 671
 672 All the tcSub calls have the form
 673
 674                 tcSub actual_ty expected_ty
 675 which checks
 676                 actual_ty <= expected_ty
 677
 678 That is, that a value of type actual_ty is acceptable in
 679 a place expecting a value of type expected_ty.
 680
 681 It returns a coercion function
 682         co_fn :: actual_ty ~ expected_ty
 683 which takes an HsExpr of type actual_ty into one of type
 684 expected_ty.
 685
 686 \begin{code}
 687 -----------------
 688 tcSubExp :: InstOrigin -> BoxySigmaType -> BoxySigmaType -> TcM HsWrapper
 689         -- (tcSub act exp) checks that
 690         --      act <= exp
 691 tcSubExp orig actual_ty expected_ty
 692   = -- addErrCtxtM (unifyCtxt actual_ty expected_ty) $
 693     -- Adding the error context here leads to some very confusing error
 694     -- messages, such as "can't match forall a. a->a with forall a. a->a"
 695     -- Example is tcfail165:
 696     --      do var <- newEmptyMVar :: IO (MVar (forall a. Show a => a -> String))
 697     --         putMVar var (show :: forall a. Show a => a -> String)
 698     -- Here the info does not flow from the 'var' arg of putMVar to its 'show' arg
 699     -- but after zonking it looks as if it does!
 700     --
 701     -- So instead I'm adding the error context when moving from tc_sub to u_tys
 702
 703     traceTc (text "tcSubExp" <+> ppr actual_ty <+> ppr expected_ty) >>
 704     tc_sub orig actual_ty actual_ty False expected_ty expected_ty
 705
 706 -----------------
 707 tc_sub :: InstOrigin
 708        -> BoxySigmaType         -- actual_ty, before expanding synonyms
 709        -> BoxySigmaType         --              ..and after
 710        -> InBox                 -- True <=> expected_ty is inside a box
 711        -> BoxySigmaType         -- expected_ty, before
 712        -> BoxySigmaType         --              ..and after
 713        -> TcM HsWrapper
 714                                 -- The acual_ty is never inside a box
 715 -- IMPORTANT pre-condition: if the args contain foralls, the bound type
 716 --                          variables are visible non-monadically
 717 --                          (i.e. tha args are sufficiently zonked)
 718 -- This invariant is needed so that we can "see" the foralls, ad
 719 -- e.g. in the SPEC rule where we just use splitSigmaTy
 720
 721 tc_sub orig act_sty act_ty exp_ib exp_sty exp_ty
 722   = traceTc (text "tc_sub" <+> ppr act_ty $$ ppr exp_ty) >>
 723     tc_sub1 orig act_sty act_ty exp_ib exp_sty exp_ty
 724         -- This indirection is just here to make
 725         -- it easy to insert a debug trace!
 726
 727 tc_sub1 orig act_sty act_ty exp_ib exp_sty exp_ty
 728   | Just exp_ty' <- tcView exp_ty = tc_sub orig act_sty act_ty exp_ib exp_sty exp_ty'
 729 tc_sub1 orig act_sty act_ty exp_ib exp_sty exp_ty
 730   | Just act_ty' <- tcView act_ty = tc_sub orig act_sty act_ty' exp_ib exp_sty exp_ty
 731
 732 -----------------------------------
 733 -- Rule SBOXY, plus other cases when act_ty is a type variable
 734 -- Just defer to boxy matching
 735 -- This rule takes precedence over SKOL!
 736 tc_sub1 orig act_sty (TyVarTy tv) exp_ib exp_sty exp_ty
 737   = do  { traceTc (text "tc_sub1 - case 1")
 738         ; coi <- addSubCtxt orig act_sty exp_sty $
 739                  uVar True False tv exp_ib exp_sty exp_ty
 740         ; traceTc (case coi of
 741                         IdCo   -> text "tc_sub1 (Rule SBOXY) IdCo"
 742                         ACo co -> text "tc_sub1 (Rule SBOXY) ACo" <+> ppr co)
 743         ; return $ coiToHsWrapper coi
 744         }
 745
 746 -----------------------------------
 747 -- Skolemisation case (rule SKOL)
 748 --      actual_ty:   d:Eq b => b->b
 749 --      expected_ty: forall a. Ord a => a->a
 750 --      co_fn e      /\a. \d2:Ord a. let d = eqFromOrd d2 in e
 751
 752 -- It is essential to do this *before* the specialisation case
 753 -- Example:  f :: (Eq a => a->a) -> ...
 754 --           g :: Ord b => b->b
 755 -- Consider  f g !
 756
 757 tc_sub1 orig act_sty act_ty exp_ib exp_sty exp_ty
 758   | isSigmaTy exp_ty
 759   = do { traceTc (text "tc_sub1 - case 2") ;
 760     if exp_ib then      -- SKOL does not apply if exp_ty is inside a box
 761         defer_to_boxy_matching orig act_sty act_ty exp_ib exp_sty exp_ty
 762     else do
 763         { (gen_fn, co_fn) <- tcGen exp_ty act_tvs $ \ _ body_exp_ty ->
 764                              tc_sub orig act_sty act_ty False body_exp_ty body_exp_ty
 765         ; return (gen_fn <.> co_fn) }
 766     }
 767   where
 768     act_tvs = tyVarsOfType act_ty
 769                 -- It's really important to check for escape wrt
 770                 -- the free vars of both expected_ty *and* actual_ty
 771
 772 -----------------------------------
 773 -- Specialisation case (rule ASPEC):
 774 --      actual_ty:   forall a. Ord a => a->a
 775 --      expected_ty: Int -> Int
 776 --      co_fn e =    e Int dOrdInt
 777
 778 tc_sub1 orig act_sty actual_ty exp_ib exp_sty expected_ty
 779 -- Implements the new SPEC rule in the Appendix of the paper
 780 -- "Boxy types: inference for higher rank types and impredicativity"
 781 -- (This appendix isn't in the published version.)
 782 -- The idea is to *first* do pre-subsumption, and then full subsumption
 783 -- Example:     forall a. a->a  <=  Int -> (forall b. Int)
 784 --   Pre-subsumpion finds a|->Int, and that works fine, whereas
 785 --   just running full subsumption would fail.
 786   | isSigmaTy actual_ty
 787   = do  { traceTc (text "tc_sub1 - case 3")
 788         ;       -- Perform pre-subsumption, and instantiate
 789                 -- the type with info from the pre-subsumption;
 790                 -- boxy tyvars if pre-subsumption gives no info
 791           let (tyvars, theta, tau) = tcSplitSigmaTy actual_ty
 792               tau_tvs = exactTyVarsOfType tau
 793         ; inst_tys <- if exp_ib then    -- Inside a box, do not do clever stuff
 794                         do { tyvars' <- mapM tcInstBoxyTyVar tyvars
 795                            ; return (mkTyVarTys tyvars') }
 796                       else              -- Outside, do clever stuff
 797                         preSubType tyvars tau_tvs tau expected_ty
 798         ; let subst' = zipOpenTvSubst tyvars inst_tys
 799               tau'   = substTy subst' tau
 800
 801                 -- Perform a full subsumption check
 802         ; traceTc (text "tc_sub_spec" <+> vcat [ppr actual_ty,
 803                                                 ppr tyvars <+> ppr theta <+> ppr tau,
 804                                                 ppr tau'])
 805         ; co_fn2 <- tc_sub orig tau' tau' exp_ib exp_sty expected_ty
 806
 807                 -- Deal with the dictionaries
 808         ; co_fn1 <- instCall orig inst_tys (substTheta subst' theta)
 809         ; return (co_fn2 <.> co_fn1) }
 810
 811 -----------------------------------
 812 -- Function case (rule F1)
 813 tc_sub1 orig act_sty (FunTy act_arg act_res) exp_ib exp_sty (FunTy exp_arg exp_res)
 814   = do { traceTc (text "tc_sub1 - case 4")
 815        ; tc_sub_funs orig act_arg act_res exp_ib exp_arg exp_res
 816        }
 817
 818 -- Function case (rule F2)
 819 tc_sub1 orig act_sty act_ty@(FunTy act_arg act_res) _ exp_sty (TyVarTy exp_tv)
 820   | isBoxyTyVar exp_tv
 821   = do  { traceTc (text "tc_sub1 - case 5")
 822         ; cts <- readMetaTyVar exp_tv
 823         ; case cts of
 824             Indirect ty -> tc_sub orig act_sty act_ty True exp_sty ty
 825             Flexi -> do { [arg_ty,res_ty] <- withMetaTvs exp_tv fun_kinds mk_res_ty
 826                         ; tc_sub_funs orig act_arg act_res True arg_ty res_ty } }
 827  where
 828     mk_res_ty [arg_ty', res_ty'] = mkFunTy arg_ty' res_ty'
 829     mk_res_ty other = panic "TcUnify.mk_res_ty3"
 830     fun_kinds = [argTypeKind, openTypeKind]
 831
 832 -- Everything else: defer to boxy matching
 833 tc_sub1 orig act_sty actual_ty exp_ib exp_sty expected_ty@(TyVarTy exp_tv)
 834   = do { traceTc (text "tc_sub1 - case 6a" <+> ppr [isBoxyTyVar exp_tv, isMetaTyVar exp_tv, isSkolemTyVar exp_tv, isExistentialTyVar exp_tv,isSigTyVar exp_tv] )
 835        ; defer_to_boxy_matching orig act_sty actual_ty exp_ib exp_sty expected_ty
 836        }
 837
 838 tc_sub1 orig act_sty actual_ty exp_ib exp_sty expected_ty
 839   = do { traceTc (text "tc_sub1 - case 6")
 840        ; defer_to_boxy_matching orig act_sty actual_ty exp_ib exp_sty expected_ty
 841        }
 842
 843 -----------------------------------
 844 defer_to_boxy_matching orig act_sty actual_ty exp_ib exp_sty expected_ty
 845   = do  { coi <- addSubCtxt orig act_sty exp_sty $
 846                  u_tys True False act_sty actual_ty exp_ib exp_sty expected_ty
 847         ; return $ coiToHsWrapper coi }
 848
 849 -----------------------------------
 850 tc_sub_funs orig act_arg act_res exp_ib exp_arg exp_res
 851   = do  { arg_coi   <- addSubCtxt orig act_arg exp_arg $
 852                        uTysOuter False act_arg exp_ib exp_arg
 853         ; co_fn_res <- tc_sub orig act_res act_res exp_ib exp_res exp_res
 854         ; wrapper1  <- wrapFunResCoercion [exp_arg] co_fn_res
 855         ; let wrapper2 = case arg_coi of
 856                                 IdCo   -> idHsWrapper
 857                                 ACo co -> WpCo $ FunTy co act_res
 858         ; return (wrapper1 <.> wrapper2) }
 859
 860 -----------------------------------
 861 wrapFunResCoercion
 862         :: [TcType]     -- Type of args
 863         -> HsWrapper    -- HsExpr a -> HsExpr b
 864         -> TcM HsWrapper        -- HsExpr (arg_tys -> a) -> HsExpr (arg_tys -> b)
 865 wrapFunResCoercion arg_tys co_fn_res
 866   | isIdHsWrapper co_fn_res
 867   = return idHsWrapper
 868   | null arg_tys
 869   = return co_fn_res
 870   | otherwise
 871   = do  { arg_ids <- newSysLocalIds FSLIT("sub") arg_tys
 872         ; return (mkWpLams arg_ids <.> co_fn_res <.> mkWpApps arg_ids) }
 873 \end{code}
 874
 875
 876
 877 %************************************************************************
 878 %*                                                                      *
 879 \subsection{Generalisation}
 880 %*                                                                      *
 881 %************************************************************************
 882
 883 \begin{code}
 884 tcGen :: BoxySigmaType                          -- expected_ty
 885       -> TcTyVarSet                             -- Extra tyvars that the universally
 886                                                 --      quantified tyvars of expected_ty
 887                                                 --      must not be unified
 888       -> ([TcTyVar] -> BoxyRhoType -> TcM result)
 889       -> TcM (HsWrapper, result)
 890         -- The expression has type: spec_ty -> expected_ty
 891
 892 tcGen expected_ty extra_tvs thing_inside        -- We expect expected_ty to be a forall-type
 893                                                 -- If not, the call is a no-op
 894   = do  { traceTc (text "tcGen")
 895                 -- We want the GenSkol info in the skolemised type variables to
 896                 -- mention the *instantiated* tyvar names, so that we get a
 897                 -- good error message "Rigid variable 'a' is bound by (forall a. a->a)"
 898                 -- Hence the tiresome but innocuous fixM
 899         ; ((tvs', theta', rho'), skol_info) <- fixM (\ ~(_, skol_info) ->
 900                 do { (forall_tvs, theta, rho_ty) <- tcInstSkolType skol_info expected_ty
 901                         -- Get loation from monad, not from expected_ty
 902                    ; let skol_info = GenSkol forall_tvs (mkPhiTy theta rho_ty)
 903                    ; return ((forall_tvs, theta, rho_ty), skol_info) })
 904
 905 #ifdef DEBUG
 906         ; traceTc (text "tcGen" <+> vcat [text "extra_tvs" <+> ppr extra_tvs,
 907                                     text "expected_ty" <+> ppr expected_ty,
 908                                     text "inst ty" <+> ppr tvs' <+> ppr theta' <+> ppr rho',
 909                                     text "free_tvs" <+> ppr free_tvs])
 910 #endif
 911
 912         -- Type-check the arg and unify with poly type
 913         ; (result, lie) <- getLIE (thing_inside tvs' rho')
 914
 915         -- Check that the "forall_tvs" havn't been constrained
 916         -- The interesting bit here is that we must include the free variables
 917         -- of the expected_ty.  Here's an example:
 918         --       runST (newVar True)
 919         -- Here, if we don't make a check, we'll get a type (ST s (MutVar s Bool))
 920         -- for (newVar True), with s fresh.  Then we unify with the runST's arg type
 921         -- forall s'. ST s' a. That unifies s' with s, and a with MutVar s Bool.
 922         -- So now s' isn't unconstrained because it's linked to a.
 923         -- Conclusion: include the free vars of the expected_ty in the
 924         -- list of "free vars" for the signature check.
 925
 926         ; loc <- getInstLoc (SigOrigin skol_info)
 927         ; dicts <- newDictBndrs loc theta'
 928         ; inst_binds <- tcSimplifyCheck loc tvs' dicts lie
 929
 930         ; checkSigTyVarsWrt free_tvs tvs'
 931         ; traceTc (text "tcGen:done")
 932
 933         ; let
 934             -- The WpLet binds any Insts which came out of the simplification.
 935             dict_vars = map instToVar dicts
 936             co_fn = mkWpTyLams tvs' <.> mkWpLams dict_vars <.> WpLet inst_binds
 937         ; returnM (co_fn, result) }
 938   where
 939     free_tvs = tyVarsOfType expected_ty `unionVarSet` extra_tvs
 940 \end{code}
 941
 942
 943
 944 %************************************************************************
 945 %*                                                                      *
 946                 Boxy unification
 947 %*                                                                      *
 948 %************************************************************************
 949
 950 The exported functions are all defined as versions of some
 951 non-exported generic functions.
 952
 953 \begin{code}
 954 boxyUnify :: BoxyType -> BoxyType -> TcM CoercionI
 955 -- Acutal and expected, respectively
 956 boxyUnify ty1 ty2
 957   = addErrCtxtM (unifyCtxt ty1 ty2) $
 958     uTysOuter False ty1 False ty2
 959
 960 ---------------
 961 boxyUnifyList :: [BoxyType] -> [BoxyType] -> TcM [CoercionI]
 962 -- Arguments should have equal length
 963 -- Acutal and expected types
 964 boxyUnifyList tys1 tys2 = uList boxyUnify tys1 tys2
 965
 966 ---------------
 967 unifyType :: TcTauType -> TcTauType -> TcM CoercionI
 968 -- No boxes expected inside these types
 969 -- Acutal and expected types
 970 unifyType ty1 ty2       -- ty1 expected, ty2 inferred
 971   = ASSERT2( not (isBoxyTy ty1), ppr ty1 )
 972     ASSERT2( not (isBoxyTy ty2), ppr ty2 )
 973     addErrCtxtM (unifyCtxt ty1 ty2) $
 974     uTysOuter True ty1 True ty2
 975
 976 ---------------
 977 unifyPred :: PredType -> PredType -> TcM CoercionI
 978 -- Acutal and expected types
 979 unifyPred p1 p2 = addErrCtxtM (unifyCtxt (mkPredTy p1) (mkPredTy p2)) $
 980                         uPred True True p1 True p2
 981
 982 unifyTheta :: TcThetaType -> TcThetaType -> TcM [CoercionI]
 983 -- Acutal and expected types
 984 unifyTheta theta1 theta2
 985   = do  { checkTc (equalLength theta1 theta2)
 986                   (vcat [ptext SLIT("Contexts differ in length"),
 987                          nest 2 $ parens $ ptext SLIT("Use -fglasgow-exts to allow this")])
 988         ; uList unifyPred theta1 theta2
 989         }
 990
 991 ---------------
 992 uList :: (a -> a -> TcM b)
 993        -> [a] -> [a] -> TcM [b]
 994 -- Unify corresponding elements of two lists of types, which
 995 -- should be of equal length.  We charge down the list explicitly so that
 996 -- we can complain if their lengths differ.
 997 uList unify []         []         = return []
 998 uList unify (ty1:tys1) (ty2:tys2) = do { x  <- unify ty1 ty2;
 999                                        ; xs <- uList unify tys1 tys2
1000                                        ; return (x:xs)
1001                                        }
1002 uList unify ty1s ty2s = panic "Unify.uList: mismatched type lists!"
1003 \end{code}
1004
1005 @unifyTypeList@ takes a single list of @TauType@s and unifies them
1006 all together.  It is used, for example, when typechecking explicit
1007 lists, when all the elts should be of the same type.
1008
1009 \begin{code}
1010 unifyTypeList :: [TcTauType] -> TcM ()
1011 unifyTypeList []                 = returnM ()
1012 unifyTypeList [ty]               = returnM ()
1013 unifyTypeList (ty1:tys@(ty2:_)) = do { unifyType ty1 ty2
1014                                       ; unifyTypeList tys }
1015 \end{code}
1016
1017 %************************************************************************
1018 %*                                                                      *
1019 \subsection[Unify-uTys]{@uTys@: getting down to business}
1020 %*                                                                      *
1021 %************************************************************************
1022
1023 @uTys@ is the heart of the unifier.  Each arg occurs twice, because
1024 we want to report errors in terms of synomyms if possible.  The first of
1025 the pair is used in error messages only; it is always the same as the
1026 second, except that if the first is a synonym then the second may be a
1027 de-synonym'd version.  This way we get better error messages.
1028
1029 We call the first one \tr{ps_ty1}, \tr{ps_ty2} for ``possible synomym''.
1030
1031 \begin{code}
1032 type SwapFlag = Bool
1033         -- False <=> the two args are (actual, expected) respectively
1034         -- True  <=> the two args are (expected, actual) respectively
1035
1036 type InBox = Bool       -- True  <=> we are inside a box
1037                         -- False <=> we are outside a box
1038         -- The importance of this is that if we get "filled-box meets
1039         -- filled-box", we'll look into the boxes and unify... but
1040         -- we must not allow polytypes.  But if we are in a box on
1041         -- just one side, then we can allow polytypes
1042
1043 type Outer = Bool       -- True <=> this is the outer level of a unification
1044                         --          so that the types being unified are the
1045                         --          very ones we began with, not some sub
1046                         --          component or synonym expansion
1047 -- The idea is that if Outer is true then unifyMisMatch should
1048 -- pop the context to remove the "Expected/Acutal" context
1049
1050 uTysOuter, uTys
1051      :: InBox -> TcType -- ty1 is the *actual*   type
1052      -> InBox -> TcType -- ty2 is the *expected* type
1053      -> TcM CoercionI
1054 uTysOuter nb1 ty1 nb2 ty2
1055         = do { traceTc (text "uTysOuter" <+> ppr ty1 <+> ppr ty2)
1056              ; u_tys True nb1 ty1 ty1 nb2 ty2 ty2 }
1057 uTys nb1 ty1 nb2 ty2
1058         = do { traceTc (text "uTys" <+> ppr ty1 <+> ppr ty2)
1059              ; u_tys False nb1 ty1 ty1 nb2 ty2 ty2 }
1060
1061
1062 --------------
1063 uTys_s :: InBox -> [TcType]     -- tys1 are the *actual*   types
1064        -> InBox -> [TcType]     -- tys2 are the *expected* types
1065        -> TcM [CoercionI]
1066 uTys_s nb1 []         nb2 []         = returnM []
1067 uTys_s nb1 (ty1:tys1) nb2 (ty2:tys2) = do { coi <- uTys nb1 ty1 nb2 ty2
1068                                           ; cois <- uTys_s nb1 tys1 nb2 tys2
1069                                           ; return (coi:cois)
1070                                           }
1071 uTys_s nb1 ty1s nb2 ty2s = panic "Unify.uTys_s: mismatched type lists!"
1072
1073 --------------
1074 u_tys :: Outer
1075       -> InBox -> TcType -> TcType      -- ty1 is the *actual* type
1076       -> InBox -> TcType -> TcType      -- ty2 is the *expected* type
1077       -> TcM CoercionI
1078
1079 u_tys outer nb1 orig_ty1 ty1 nb2 orig_ty2 ty2
1080   = do { traceTc (text "u_tys " <+> ppr ty1 <+> text " " <+> ppr ty2)
1081        ; coi <- go outer ty1 ty2
1082        ; traceTc (case coi of
1083                         ACo co -> text "u_tys yields coercion: " <+> ppr co
1084                         IdCo   -> text "u_tys yields no coercion")
1085        ; return coi
1086        }
1087   where
1088
1089     go :: Outer -> TcType -> TcType -> TcM CoercionI
1090     go outer ty1 ty2 =
1091         do { traceTc (text "go " <+> ppr orig_ty1 <+> text "/" <+> ppr ty1
1092                          <+> ppr orig_ty2 <+> text "/" <+>  ppr ty2)
1093            ; go1 outer ty1 ty2
1094            }
1095
1096     go1 :: Outer -> TcType -> TcType -> TcM CoercionI
1097         -- Always expand synonyms: see Note [Unification and synonyms]
1098         -- (this also throws away FTVs)
1099     go1 outer ty1 ty2
1100       | Just ty1' <- tcView ty1 = go False ty1' ty2
1101       | Just ty2' <- tcView ty2 = go False ty1 ty2'
1102
1103         -- Variables; go for uVar
1104     go1 outer (TyVarTy tyvar1) ty2 = uVar outer False tyvar1 nb2 orig_ty2 ty2
1105     go1 outer ty1 (TyVarTy tyvar2) = uVar outer True  tyvar2 nb1 orig_ty1 ty1
1106                                 -- "True" means args swapped
1107
1108         -- The case for sigma-types must *follow* the variable cases
1109         -- because a boxy variable can be filed with a polytype;
1110         -- but must precede FunTy, because ((?x::Int) => ty) look
1111         -- like a FunTy; there isn't necy a forall at the top
1112     go1 _ ty1 ty2
1113       | isSigmaTy ty1 || isSigmaTy ty2
1114       = do   { traceTc (text "We have sigma types: equalLength" <+> ppr tvs1 <+> ppr tvs2)
1115              ; checkM (equalLength tvs1 tvs2)
1116                       (unifyMisMatch outer False orig_ty1 orig_ty2)
1117              ; traceTc (text "We're past the first length test")
1118              ; tvs <- tcInstSkolTyVars UnkSkol tvs1     -- Not a helpful SkolemInfo
1119                         -- Get location from monad, not from tvs1
1120              ; let tys      = mkTyVarTys tvs
1121                    in_scope = mkInScopeSet (mkVarSet tvs)
1122                    phi1   = substTy (mkTvSubst in_scope (zipTyEnv tvs1 tys)) body1
1123                    phi2   = substTy (mkTvSubst in_scope (zipTyEnv tvs2 tys)) body2
1124                    (theta1,tau1) = tcSplitPhiTy phi1
1125                    (theta2,tau2) = tcSplitPhiTy phi2
1126
1127              ; addErrCtxtM (unifyForAllCtxt tvs phi1 phi2) $ do
1128              { checkM (equalLength theta1 theta2)
1129                       (unifyMisMatch outer False orig_ty1 orig_ty2)
1130
1131              ; cois <- uPreds False nb1 theta1 nb2 theta2 -- TOMDO: do something with these pred_cois
1132              ; traceTc (text "TOMDO!")
1133              ; coi <- uTys nb1 tau1 nb2 tau2
1134
1135                 -- Check for escape; e.g. (forall a. a->b) ~ (forall a. a->a)
1136              ; free_tvs <- zonkTcTyVarsAndFV (varSetElems (tyVarsOfType ty1 `unionVarSet` tyVarsOfType ty2))
1137              ; ifM (any (`elemVarSet` free_tvs) tvs)
1138                    (bleatEscapedTvs free_tvs tvs tvs)
1139
1140                 -- If both sides are inside a box, we are in a "box-meets-box"
1141                 -- situation, and we should not have a polytype at all.
1142                 -- If we get here we have two boxes, already filled with
1143                 -- the same polytype... but it should be a monotype.
1144                 -- This check comes last, because the error message is
1145                 -- extremely unhelpful.
1146              ; ifM (nb1 && nb2) (notMonoType ty1)
1147              ; return coi
1148              }}
1149       where
1150         (tvs1, body1) = tcSplitForAllTys ty1
1151         (tvs2, body2) = tcSplitForAllTys ty2
1152
1153         -- Predicates
1154     go1 outer (PredTy p1) (PredTy p2)
1155         = uPred False nb1 p1 nb2 p2
1156
1157         -- Type constructors must match
1158     go1 _ (TyConApp con1 tys1) (TyConApp con2 tys2)
1159       | con1 == con2 && not (isOpenSynTyCon con1)
1160       = do { cois <- uTys_s nb1 tys1 nb2 tys2
1161            ; return $ mkTyConAppCoI con1 tys1 cois
1162            }
1163         -- See Note [TyCon app]
1164       | con1 == con2 && identicalOpenSynTyConApp
1165       = do { cois <- uTys_s nb1 tys1' nb2 tys2'
1166            ; return $ mkTyConAppCoI con1 tys1 (replicate n IdCo ++ cois)
1167            }
1168       where
1169         n                        = tyConArity con1
1170         (idxTys1, tys1')         = splitAt n tys1
1171         (idxTys2, tys2')         = splitAt n tys2
1172         identicalOpenSynTyConApp = idxTys1 `tcEqTypes` idxTys2
1173         -- See Note [OpenSynTyCon app]
1174
1175         -- Functions; just check the two parts
1176     go1 _ (FunTy fun1 arg1) (FunTy fun2 arg2)
1177       = do { coi_l <- uTys nb1 fun1 nb2 fun2
1178            ; coi_r <- uTys nb1 arg1 nb2 arg2
1179            ; return $ mkFunTyCoI fun1 coi_l arg1 coi_r
1180            }
1181
1182         -- Applications need a bit of care!
1183         -- They can match FunTy and TyConApp, so use splitAppTy_maybe
1184         -- NB: we've already dealt with type variables and Notes,
1185         -- so if one type is an App the other one jolly well better be too
1186     go1 outer (AppTy s1 t1) ty2
1187       | Just (s2,t2) <- tcSplitAppTy_maybe ty2
1188       = do { coi_s <- uTys nb1 s1 nb2 s2; coi_t <- uTys nb1 t1 nb2 t2
1189            ; return $ mkAppTyCoI s1 coi_s t1 coi_t }
1190
1191         -- Now the same, but the other way round
1192         -- Don't swap the types, because the error messages get worse
1193     go1 outer ty1 (AppTy s2 t2)
1194       | Just (s1,t1) <- tcSplitAppTy_maybe ty1
1195       = do { coi_s <- uTys nb1 s1 nb2 s2; coi_t <- uTys nb1 t1 nb2 t2
1196            ; return $ mkAppTyCoI s1 coi_s t1 coi_t }
1197
1198         -- One or both outermost constructors are type family applications.
1199         -- If we can normalise them away, proceed as usual; otherwise, we
1200         -- need to defer unification by generating a wanted equality constraint.
1201     go1 outer ty1 ty2
1202       | ty1_is_fun || ty2_is_fun
1203       = do { (coi1, ty1') <- if ty1_is_fun then tcNormaliseFamInst ty1
1204                                            else return (IdCo, ty1)
1205            ; (coi2, ty2') <- if ty2_is_fun then tcNormaliseFamInst ty2
1206                                            else return (IdCo, ty2)
1207            ; coi <- if isOpenSynTyConApp ty1' || isOpenSynTyConApp ty2'
1208                     then do { -- One type family app can't be reduced yet
1209                               -- => defer
1210                             ; ty1'' <- zonkTcType ty1'
1211                             ; ty2'' <- zonkTcType ty2'
1212                             ; if tcEqType ty1'' ty2''
1213                               then return IdCo
1214                               else -- see [Deferred Unification]
1215                                 defer_unification outer False orig_ty1 orig_ty2
1216                             }
1217                      else -- unification can proceed
1218                           go outer ty1' ty2'
1219            ; return $ coi1 `mkTransCoI` coi `mkTransCoI` (mkSymCoI coi2)
1220            }
1221         where
1222           ty1_is_fun = isOpenSynTyConApp ty1
1223           ty2_is_fun = isOpenSynTyConApp ty2
1224
1225         -- Anything else fails
1226     go1 outer _ _ = unifyMisMatch outer False orig_ty1 orig_ty2
1227
1228
1229 ----------
1230 uPred outer nb1 (IParam n1 t1) nb2 (IParam n2 t2)
1231   | n1 == n2 =
1232         do { coi <- uTys nb1 t1 nb2 t2
1233            ; return $ mkIParamPredCoI n1 coi
1234            }
1235 uPred outer nb1 (ClassP c1 tys1) nb2 (ClassP c2 tys2)
1236   | c1 == c2 =
1237         do { cois <- uTys_s nb1 tys1 nb2 tys2           -- Guaranteed equal lengths because the kinds check
1238            ; return $ mkClassPPredCoI c1 tys1 cois
1239            }
1240 uPred outer _ p1 _ p2 = unifyMisMatch outer False (mkPredTy p1) (mkPredTy p2)
1241
1242 uPreds outer nb1 []       nb2 []       = return []
1243 uPreds outer nb1 (p1:ps1) nb2 (p2:ps2) =
1244         do { coi  <- uPred outer nb1 p1 nb2 p2
1245            ; cois <- uPreds outer nb1 ps1 nb2 ps2
1246            ; return (coi:cois)
1247            }
1248 uPreds outer nb1 ps1      nb2 ps2      = panic "uPreds"
1249 \end{code}
1250
1251 Note [TyCon app]
1252 ~~~~~~~~~~~~~~~~
1253 When we find two TyConApps, the argument lists are guaranteed equal
1254 length.  Reason: intially the kinds of the two types to be unified is
1255 the same. The only way it can become not the same is when unifying two
1256 AppTys (f1 a1):=:(f2 a2).  In that case there can't be a TyConApp in
1257 the f1,f2 (because it'd absorb the app).  If we unify f1:=:f2 first,
1258 which we do, that ensures that f1,f2 have the same kind; and that
1259 means a1,a2 have the same kind.  And now the argument repeats.
1260
1261 Note [OpenSynTyCon app]
1262 ~~~~~~~~~~~~~~~~~~~~~~~
1263 Given
1264
1265   type family T a :: * -> *
1266
1267 the two types (T () a) and (T () Int) must unify, even if there are
1268 no type instances for T at all.  Should we just turn them into an
1269 equality (T () a ~ T () Int)?  I don't think so.  We currently try to
1270 eagerly unify everything we can before generating equalities; otherwise,
1271 we could turn the unification of [Int] with [a] into an equality, too.
1272
1273 Note [Unification and synonyms]
1274 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1275 If you are tempted to make a short cut on synonyms, as in this
1276 pseudocode...
1277
1278 \begin{verbatim}
1279 -- NO   uTys (SynTy con1 args1 ty1) (SynTy con2 args2 ty2)
1280 -- NO     = if (con1 == con2) then
1281 -- NO   -- Good news!  Same synonym constructors, so we can shortcut
1282 -- NO   -- by unifying their arguments and ignoring their expansions.
1283 -- NO   unifyTypepeLists args1 args2
1284 -- NO    else
1285 -- NO   -- Never mind.  Just expand them and try again
1286 -- NO   uTys ty1 ty2
1287 \end{verbatim}
1288
1289 then THINK AGAIN.  Here is the whole story, as detected and reported
1290 by Chris Okasaki \tr{<Chris_Okasaki@loch.mess.cs.cmu.edu>}:
1291 \begin{quotation}
1292 Here's a test program that should detect the problem:
1293
1294 \begin{verbatim}
1295         type Bogus a = Int
1296         x = (1 :: Bogus Char) :: Bogus Bool
1297 \end{verbatim}
1298
1299 The problem with [the attempted shortcut code] is that
1300 \begin{verbatim}
1301         con1 == con2
1302 \end{verbatim}
1303 is not a sufficient condition to be able to use the shortcut!
1304 You also need to know that the type synonym actually USES all
1305 its arguments.  For example, consider the following type synonym
1306 which does not use all its arguments.
1307 \begin{verbatim}
1308         type Bogus a = Int
1309 \end{verbatim}
1310
1311 If you ever tried unifying, say, \tr{Bogus Char} with \tr{Bogus Bool},
1312 the unifier would blithely try to unify \tr{Char} with \tr{Bool} and
1313 would fail, even though the expanded forms (both \tr{Int}) should
1314 match.
1315
1316 Similarly, unifying \tr{Bogus Char} with \tr{Bogus t} would
1317 unnecessarily bind \tr{t} to \tr{Char}.
1318
1319 ... You could explicitly test for the problem synonyms and mark them
1320 somehow as needing expansion, perhaps also issuing a warning to the
1321 user.
1322 \end{quotation}
1323
1324
1325 %************************************************************************
1326 %*                                                                      *
1327 \subsection[Unify-uVar]{@uVar@: unifying with a type variable}
1328 %*                                                                      *
1329 %************************************************************************
1330
1331 @uVar@ is called when at least one of the types being unified is a
1332 variable.  It does {\em not} assume that the variable is a fixed point
1333 of the substitution; rather, notice that @uVar@ (defined below) nips
1334 back into @uTys@ if it turns out that the variable is already bound.
1335
1336 \begin{code}
1337 uVar :: Outer
1338      -> SwapFlag        -- False => tyvar is the "actual" (ty is "expected")
1339                         -- True  => ty is the "actual" (tyvar is "expected")
1340      -> TcTyVar
1341      -> InBox           -- True <=> definitely no boxes in t2
1342      -> TcTauType -> TcTauType  -- printing and real versions
1343      -> TcM CoercionI
1344
1345 uVar outer swapped tv1 nb2 ps_ty2 ty2
1346   = do  { let expansion | showSDoc (ppr ty2) == showSDoc (ppr ps_ty2) = empty
1347                         | otherwise = brackets (equals <+> ppr ty2)
1348         ; traceTc (text "uVar" <+> ppr swapped <+>
1349                         sep [ppr tv1 <+> dcolon <+> ppr (tyVarKind tv1 ),
1350                                 nest 2 (ptext SLIT(" <-> ")),
1351                              ppr ps_ty2 <+> dcolon <+> ppr (typeKind ty2) <+> expansion])
1352         ; details <- lookupTcTyVar tv1
1353         ; case details of
1354             IndirectTv ty1
1355                 | swapped   -> u_tys outer nb2  ps_ty2 ty2 True ty1    ty1      -- Swap back
1356                 | otherwise -> u_tys outer True ty1    ty1 nb2  ps_ty2 ty2      -- Same order
1357                         -- The 'True' here says that ty1 is now inside a box
1358             DoneTv details1 -> uUnfilledVar outer swapped tv1 details1 ps_ty2 ty2
1359         }
1360
1361 ----------------
1362 uUnfilledVar :: Outer
1363              -> SwapFlag
1364              -> TcTyVar -> TcTyVarDetails       -- Tyvar 1
1365              -> TcTauType -> TcTauType          -- Type 2
1366              -> TcM CoercionI
1367 -- Invariant: tyvar 1 is not unified with anything
1368
1369 uUnfilledVar outer swapped tv1 details1 ps_ty2 ty2
1370   | Just ty2' <- tcView ty2
1371   =     -- Expand synonyms; ignore FTVs
1372     uUnfilledVar False swapped tv1 details1 ps_ty2 ty2'
1373
1374 uUnfilledVar outer swapped tv1 details1 ps_ty2 (TyVarTy tv2)
1375   | tv1 == tv2  -- Same type variable => no-op (but watch out for the boxy case)
1376   = case details1 of
1377         MetaTv BoxTv ref1  -- A boxy type variable meets itself;
1378                            -- this is box-meets-box, so fill in with a tau-type
1379               -> do { tau_tv <- tcInstTyVar tv1
1380                     ; updateMeta tv1 ref1 (mkTyVarTy tau_tv)
1381                     ; return IdCo
1382                     }
1383         other -> returnM IdCo   -- No-op
1384
1385   | otherwise  -- Distinct type variables
1386   = do  { lookup2 <- lookupTcTyVar tv2
1387         ; case lookup2 of
1388             IndirectTv ty2' -> uUnfilledVar outer swapped tv1 details1 ty2' ty2'
1389             DoneTv details2 -> uUnfilledVars outer swapped tv1 details1 tv2 details2
1390         }
1391
1392 uUnfilledVar outer swapped tv1 details1 ps_ty2 non_var_ty2
1393   =     -- ty2 is not a type variable
1394     case details1 of
1395       MetaTv (SigTv _) _ -> rigid_variable
1396       MetaTv info ref1   ->
1397         uMetaVar outer swapped tv1 info ref1 ps_ty2 non_var_ty2
1398       SkolemTv _         -> rigid_variable
1399   where
1400     rigid_variable
1401       | isOpenSynTyConApp non_var_ty2
1402       =           -- 'non_var_ty2's outermost constructor is a type family,
1403                   -- which we may may be able to normalise
1404         do { (coi2, ty2') <- tcNormaliseFamInst non_var_ty2
1405            ; case coi2 of
1406                IdCo   ->   -- no progress, but maybe after other instantiations
1407                          defer_unification outer swapped (TyVarTy tv1) ps_ty2
1408                ACo co ->   -- progress: so lets try again
1409                  do { traceTc $
1410                         ppr co <+> text "::"<+> ppr non_var_ty2 <+> text "~" <+>
1411                         ppr ty2'
1412                     ; coi <- uUnfilledVar outer swapped tv1 details1 ps_ty2 ty2'
1413                     ; let coi2' = (if swapped then id else mkSymCoI) coi2
1414                     ; return $ coi2' `mkTransCoI` coi
1415                     }
1416            }
1417       | SkolemTv RuntimeUnkSkol <- details1
1418                    -- runtime unknown will never match
1419       = unifyMisMatch outer swapped (TyVarTy tv1) ps_ty2
1420       | otherwise  -- defer as a given equality may still resolve this
1421       = defer_unification outer swapped (TyVarTy tv1) ps_ty2
1422 \end{code}
1423
1424 Note [Deferred Unification]
1425 ~~~~~~~~~~~~~~~~~~~~
1426 We may encounter a unification ty1 = ty2 that cannot be performed syntactically,
1427 and yet its consistency is undetermined. Previously, there was no way to still
1428 make it consistent. So a mismatch error was issued.
1429
1430 Now these unfications are deferred until constraint simplification, where type
1431 family instances and given equations may (or may not) establish the consistency.
1432 Deferred unifications are of the form
1433                 F ... ~ ...
1434 or              x ~ ...
1435 where F is a type function and x is a type variable.
1436 E.g.
1437         id :: x ~ y => x -> y
1438         id e = e
1439
1440 involves the unfication x = y. It is deferred until we bring into account the
1441 context x ~ y to establish that it holds.
1442
1443 If available, we defer original types (rather than those where closed type
1444 synonyms have already been expanded via tcCoreView).  This is, as usual, to
1445 improve error messages.
1446
1447 We need to both 'unBox' and zonk deferred types.  We need to unBox as
1448 functions, such as TcExpr.tcMonoExpr promise to fill boxes in the expected
1449 type.  We need to zonk as the types go into the kind of the coercion variable
1450 `cotv' and those are not zonked in Inst.zonkInst.  (Maybe it would be better
1451 to zonk in zonInst instead.  Would that be sufficient?)
1452
1453 \begin{code}
1454 defer_unification :: Bool               -- pop innermost context?
1455                   -> SwapFlag
1456                   -> TcType
1457                   -> TcType
1458                   -> TcM CoercionI
1459 defer_unification outer True ty1 ty2
1460   = defer_unification outer False ty2 ty1
1461 defer_unification outer False ty1 ty2
1462   = do  { ty1' <- unBox ty1 >>= zonkTcType      -- unbox *and* zonk..
1463         ; ty2' <- unBox ty2 >>= zonkTcType      -- ..see preceding note
1464         ; traceTc $ text "deferring:" <+> ppr ty1 <+> text "~" <+> ppr ty2
1465         ; cotv <- newMetaCoVar ty1' ty2'
1466                 -- put ty1 ~ ty2 in LIE
1467                 -- Left means "wanted"
1468         ; inst <- (if outer then popErrCtxt else id) $
1469                   mkEqInst (EqPred ty1' ty2') (Left cotv)
1470         ; extendLIE inst
1471         ; return $ ACo $ TyVarTy cotv  }
1472
1473 ----------------
1474 uMetaVar :: Bool               -- pop innermost context?
1475          -> SwapFlag
1476          -> TcTyVar -> BoxInfo -> IORef MetaDetails
1477          -> TcType -> TcType
1478          -> TcM CoercionI
1479 -- tv1 is an un-filled-in meta type variable (maybe boxy, maybe tau)
1480 -- ty2 is not a type variable
1481
1482 uMetaVar outer swapped tv1 BoxTv ref1 ps_ty2 non_var_ty2
1483   =     -- tv1 is a BoxTv.  So we must unbox ty2, to ensure
1484         -- that any boxes in ty2 are filled with monotypes
1485         --
1486         -- It should not be the case that tv1 occurs in ty2
1487         -- (i.e. no occurs check should be needed), but if perchance
1488         -- it does, the unbox operation will fill it, and the DEBUG
1489         -- checks for that.
1490     do  { final_ty <- unBox ps_ty2
1491 #ifdef DEBUG
1492         ; meta_details <- readMutVar ref1
1493         ; case meta_details of
1494             Indirect ty -> WARN( True, ppr tv1 <+> ppr ty )
1495                            return ()    -- This really should *not* happen
1496             Flexi -> return ()
1497 #endif
1498         ; checkUpdateMeta swapped tv1 ref1 final_ty
1499         ; return IdCo
1500         }
1501
1502 uMetaVar outer swapped tv1 info1 ref1 ps_ty2 non_var_ty2
1503   = do  { -- Occurs check + monotype check
1504         ; mb_final_ty <- checkTauTvUpdate tv1 ps_ty2
1505         ; case mb_final_ty of
1506             Nothing       ->    -- tv1 occured in type family parameter
1507               defer_unification outer swapped (mkTyVarTy tv1) ps_ty2
1508             Just final_ty ->
1509               do { checkUpdateMeta swapped tv1 ref1 final_ty
1510                  ; return IdCo
1511                  }
1512         }
1513
1514 ----------------
1515 uUnfilledVars :: Outer
1516               -> SwapFlag
1517               -> TcTyVar -> TcTyVarDetails      -- Tyvar 1
1518               -> TcTyVar -> TcTyVarDetails      -- Tyvar 2
1519               -> TcM CoercionI
1520 -- Invarant: The type variables are distinct,
1521 --           Neither is filled in yet
1522 --           They might be boxy or not
1523
1524 uUnfilledVars outer swapped tv1 (SkolemTv _) tv2 (SkolemTv _)
1525   = -- see [Deferred Unification]
1526     defer_unification outer swapped (mkTyVarTy tv1) (mkTyVarTy tv2)
1527
1528 uUnfilledVars outer swapped tv1 (MetaTv info1 ref1) tv2 (SkolemTv _)
1529   = checkUpdateMeta swapped tv1 ref1 (mkTyVarTy tv2) >> return IdCo
1530 uUnfilledVars outer swapped tv1 (SkolemTv _) tv2 (MetaTv info2 ref2)
1531   = checkUpdateMeta (not swapped) tv2 ref2 (mkTyVarTy tv1) >> return IdCo
1532
1533 -- ToDo: this function seems too long for what it acutally does!
1534 uUnfilledVars outer swapped tv1 (MetaTv info1 ref1) tv2 (MetaTv info2 ref2)
1535   = case (info1, info2) of
1536         (BoxTv,   BoxTv)   -> box_meets_box >> return IdCo
1537
1538         -- If a box meets a TauTv, but the fomer has the smaller kind
1539         -- then we must create a fresh TauTv with the smaller kind
1540         (_,       BoxTv)   | k1_sub_k2 -> update_tv2 >> return IdCo
1541                            | otherwise -> box_meets_box >> return IdCo
1542         (BoxTv,   _    )   | k2_sub_k1 -> update_tv1 >> return IdCo
1543                            | otherwise -> box_meets_box >> return IdCo
1544
1545         -- Avoid SigTvs if poss
1546         (SigTv _, _      ) | k1_sub_k2 -> update_tv2 >> return IdCo
1547         (_,       SigTv _) | k2_sub_k1 -> update_tv1 >> return IdCo
1548
1549         (_,   _) | k1_sub_k2 -> if k2_sub_k1 && nicer_to_update_tv1
1550                                 then update_tv1 >> return IdCo  -- Same kinds
1551                                 else update_tv2 >> return IdCo
1552                  | k2_sub_k1 -> update_tv1 >> return IdCo
1553                  | otherwise -> kind_err >> return IdCo
1554
1555         -- Update the variable with least kind info
1556         -- See notes on type inference in Kind.lhs
1557         -- The "nicer to" part only applies if the two kinds are the same,
1558         -- so we can choose which to do.
1559   where
1560         -- Kinds should be guaranteed ok at this point
1561     update_tv1 = updateMeta tv1 ref1 (mkTyVarTy tv2)
1562     update_tv2 = updateMeta tv2 ref2 (mkTyVarTy tv1)
1563
1564     box_meets_box | k1_sub_k2 = if k2_sub_k1 && nicer_to_update_tv1
1565                                 then fill_from tv2
1566                                 else fill_from tv1
1567                   | k2_sub_k1 = fill_from tv2
1568                   | otherwise = kind_err
1569
1570         -- Update *both* tyvars with a TauTv whose name and kind
1571         -- are gotten from tv (avoid losing nice names is poss)
1572     fill_from tv = do { tv' <- tcInstTyVar tv
1573                       ; let tau_ty = mkTyVarTy tv'
1574                       ; updateMeta tv1 ref1 tau_ty
1575                       ; updateMeta tv2 ref2 tau_ty }
1576
1577     kind_err = addErrCtxtM (unifyKindCtxt swapped tv1 (mkTyVarTy tv2))  $
1578                unifyKindMisMatch k1 k2
1579
1580     k1 = tyVarKind tv1
1581     k2 = tyVarKind tv2
1582     k1_sub_k2 = k1 `isSubKind` k2
1583     k2_sub_k1 = k2 `isSubKind` k1
1584
1585     nicer_to_update_tv1 = isSystemName (Var.varName tv1)
1586         -- Try to update sys-y type variables in preference to ones
1587         -- gotten (say) by instantiating a polymorphic function with
1588         -- a user-written type sig
1589 \end{code}
1590
1591 \begin{code}
1592 refineBox :: TcType -> TcM TcType
1593 -- Unbox the outer box of a boxy type (if any)
1594 refineBox ty@(TyVarTy box_tv)
1595   | isMetaTyVar box_tv
1596   = do  { cts <- readMetaTyVar box_tv
1597         ; case cts of
1598                 Flexi -> return ty
1599                 Indirect ty -> return ty }
1600 refineBox other_ty = return other_ty
1601
1602 refineBoxToTau :: TcType -> TcM TcType
1603 -- Unbox the outer box of a boxy type, filling with a monotype if it is empty
1604 -- Like refineBox except for the "fill with monotype" part.
1605 refineBoxToTau ty@(TyVarTy box_tv)
1606   | isMetaTyVar box_tv
1607   , MetaTv BoxTv ref <- tcTyVarDetails box_tv
1608   = do  { cts <- readMutVar ref
1609         ; case cts of
1610                 Flexi -> fillBoxWithTau box_tv ref
1611                 Indirect ty -> return ty }
1612 refineBoxToTau other_ty = return other_ty
1613
1614 zapToMonotype :: BoxySigmaType -> TcM TcTauType
1615 -- Subtle... we must zap the boxy res_ty
1616 -- to kind * before using it to instantiate a LitInst
1617 -- Calling unBox instead doesn't do the job, because the box
1618 -- often has an openTypeKind, and we don't want to instantiate
1619 -- with that type.
1620 zapToMonotype res_ty
1621   = do  { res_tau <- newFlexiTyVarTy liftedTypeKind
1622         ; boxyUnify res_tau res_ty
1623         ; return res_tau }
1624
1625 unBox :: BoxyType -> TcM TcType
1626 -- unBox implements the judgement
1627 --      |- s' ~ box(s)
1628 -- with input s', and result s
1629 --
1630 -- It removes all boxes from the input type, returning a non-boxy type.
1631 -- A filled box in the type can only contain a monotype; unBox fails if not
1632 -- The type can have empty boxes, which unBox fills with a monotype
1633 --
1634 -- Compare this wth checkTauTvUpdate
1635 --
1636 -- For once, it's safe to treat synonyms as opaque!
1637
1638 unBox (NoteTy n ty)     = do { ty' <- unBox ty; return (NoteTy n ty') }
1639 unBox (TyConApp tc tys) = do { tys' <- mapM unBox tys; return (TyConApp tc tys') }
1640 unBox (AppTy f a)       = do { f' <- unBox f; a' <- unBox a; return (mkAppTy f' a') }
1641 unBox (FunTy f a)       = do { f' <- unBox f; a' <- unBox a; return (FunTy f' a') }
1642 unBox (PredTy p)        = do { p' <- unBoxPred p; return (PredTy p') }
1643 unBox (ForAllTy tv ty)  = ASSERT( isImmutableTyVar tv )
1644                           do { ty' <- unBox ty; return (ForAllTy tv ty') }
1645 unBox (TyVarTy tv)
1646   | isTcTyVar tv                                -- It's a boxy type variable
1647   , MetaTv BoxTv ref <- tcTyVarDetails tv       -- NB: non-TcTyVars are possible
1648   = do  { cts <- readMutVar ref                 --     under nested quantifiers
1649         ; case cts of
1650             Flexi -> fillBoxWithTau tv ref
1651             Indirect ty -> do { non_boxy_ty <- unBox ty
1652                               ; if isTauTy non_boxy_ty
1653                                 then return non_boxy_ty
1654                                 else notMonoType non_boxy_ty }
1655         }
1656   | otherwise   -- Skolems, and meta-tau-variables
1657   = return (TyVarTy tv)
1658
1659 unBoxPred (ClassP cls tys) = do { tys' <- mapM unBox tys; return (ClassP cls tys') }
1660 unBoxPred (IParam ip ty)   = do { ty' <- unBox ty; return (IParam ip ty') }
1661 unBoxPred (EqPred ty1 ty2) = do { ty1' <- unBox ty1; ty2' <- unBox ty2; return (EqPred ty1' ty2') }
1662 \end{code}
1663
1664
1665
1666 %************************************************************************
1667 %*                                                                      *
1668 \subsection[Unify-context]{Errors and contexts}
1669 %*                                                                      *
1670 %************************************************************************
1671
1672 Errors
1673 ~~~~~~
1674
1675 \begin{code}
1676 unifyCtxt act_ty exp_ty tidy_env
1677   = do  { act_ty' <- zonkTcType act_ty
1678         ; exp_ty' <- zonkTcType exp_ty
1679         ; let (env1, exp_ty'') = tidyOpenType tidy_env exp_ty'
1680               (env2, act_ty'') = tidyOpenType env1     act_ty'
1681         ; return (env2, mkExpectedActualMsg act_ty'' exp_ty'') }
1682
1683 ----------------
1684 mkExpectedActualMsg act_ty exp_ty
1685   = nest 2 (vcat [ text "Expected type" <> colon <+> ppr exp_ty,
1686                    text "Inferred type" <> colon <+> ppr act_ty ])
1687
1688 ----------------
1689 -- If an error happens we try to figure out whether the function
1690 -- function has been given too many or too few arguments, and say so.
1691 addSubCtxt orig actual_res_ty expected_res_ty thing_inside
1692   = addErrCtxtM mk_err thing_inside
1693   where
1694     mk_err tidy_env
1695       = do { exp_ty' <- zonkTcType expected_res_ty
1696            ; act_ty' <- zonkTcType actual_res_ty
1697            ; let (env1, exp_ty'') = tidyOpenType tidy_env exp_ty'
1698                  (env2, act_ty'') = tidyOpenType env1     act_ty'
1699                  (exp_args, _)    = tcSplitFunTys exp_ty''
1700                  (act_args, _)    = tcSplitFunTys act_ty''
1701
1702                  len_act_args     = length act_args
1703                  len_exp_args     = length exp_args
1704
1705                  message = case orig of
1706                              OccurrenceOf fun
1707                                   | len_exp_args < len_act_args -> wrongArgsCtxt "too few"  fun
1708                                   | len_exp_args > len_act_args -> wrongArgsCtxt "too many" fun
1709                              other -> mkExpectedActualMsg act_ty'' exp_ty''
1710            ; return (env2, message) }
1711
1712     wrongArgsCtxt too_many_or_few fun
1713       = ptext SLIT("Probable cause:") <+> quotes (ppr fun)
1714         <+> ptext SLIT("is applied to") <+> text too_many_or_few
1715         <+> ptext SLIT("arguments")
1716
1717 ------------------
1718 unifyForAllCtxt tvs phi1 phi2 env
1719   = returnM (env2, msg)
1720   where
1721     (env', tvs') = tidyOpenTyVars env tvs       -- NB: not tidyTyVarBndrs
1722     (env1, phi1') = tidyOpenType env' phi1
1723     (env2, phi2') = tidyOpenType env1 phi2
1724     msg = vcat [ptext SLIT("When matching") <+> quotes (ppr (mkForAllTys tvs' phi1')),
1725                 ptext SLIT("          and") <+> quotes (ppr (mkForAllTys tvs' phi2'))]
1726
1727 -----------------------
1728 unifyMisMatch outer swapped ty1 ty2
1729   | swapped   = unifyMisMatch outer False ty2 ty1
1730   | outer     = popErrCtxt $ unifyMisMatch False swapped ty1 ty2  -- This is the whole point of the 'outer' stuff
1731   | otherwise = failWithMisMatch ty1 ty2
1732 \end{code}
1733
1734
1735 %************************************************************************
1736 %*                                                                      *
1737                 Kind unification
1738 %*                                                                      *
1739 %************************************************************************
1740
1741 Unifying kinds is much, much simpler than unifying types.
1742
1743 \begin{code}
1744 unifyKind :: TcKind                 -- Expected
1745           -> TcKind                 -- Actual
1746           -> TcM ()
1747 unifyKind (TyConApp kc1 []) (TyConApp kc2 [])
1748   | isSubKindCon kc2 kc1 = returnM ()
1749
1750 unifyKind (FunTy a1 r1) (FunTy a2 r2)
1751   = do { unifyKind a2 a1; unifyKind r1 r2 }
1752                 -- Notice the flip in the argument,
1753                 -- so that the sub-kinding works right
1754 unifyKind (TyVarTy kv1) k2 = uKVar False kv1 k2
1755 unifyKind k1 (TyVarTy kv2) = uKVar True kv2 k1
1756 unifyKind k1 k2 = unifyKindMisMatch k1 k2
1757
1758 unifyKinds :: [TcKind] -> [TcKind] -> TcM ()
1759 unifyKinds []       []       = returnM ()
1760 unifyKinds (k1:ks1) (k2:ks2) = unifyKind k1 k2  `thenM_`
1761                                unifyKinds ks1 ks2
1762 unifyKinds _ _               = panic "unifyKinds: length mis-match"
1763
1764 ----------------
1765 uKVar :: Bool -> KindVar -> TcKind -> TcM ()
1766 uKVar swapped kv1 k2
1767   = do  { mb_k1 <- readKindVar kv1
1768         ; case mb_k1 of
1769             Flexi -> uUnboundKVar swapped kv1 k2
1770             Indirect k1 | swapped   -> unifyKind k2 k1
1771                         | otherwise -> unifyKind k1 k2 }
1772
1773 ----------------
1774 uUnboundKVar :: Bool -> KindVar -> TcKind -> TcM ()
1775 uUnboundKVar swapped kv1 k2@(TyVarTy kv2)
1776   | kv1 == kv2 = returnM ()
1777   | otherwise   -- Distinct kind variables
1778   = do  { mb_k2 <- readKindVar kv2
1779         ; case mb_k2 of
1780             Indirect k2 -> uUnboundKVar swapped kv1 k2
1781             Flexi -> writeKindVar kv1 k2 }
1782
1783 uUnboundKVar swapped kv1 non_var_k2
1784   = do  { k2' <- zonkTcKind non_var_k2
1785         ; kindOccurCheck kv1 k2'
1786         ; k2'' <- kindSimpleKind swapped k2'
1787                 -- KindVars must be bound only to simple kinds
1788                 -- Polarities: (kindSimpleKind True ?) succeeds
1789                 -- returning *, corresponding to unifying
1790                 --      expected: ?
1791                 --      actual:   kind-ver
1792         ; writeKindVar kv1 k2'' }
1793
1794 ----------------
1795 kindOccurCheck kv1 k2   -- k2 is zonked
1796   = checkTc (not_in k2) (kindOccurCheckErr kv1 k2)
1797   where
1798     not_in (TyVarTy kv2)   = kv1 /= kv2
1799     not_in (FunTy a2 r2) = not_in a2 && not_in r2
1800     not_in other         = True
1801
1802 kindSimpleKind :: Bool -> Kind -> TcM SimpleKind
1803 -- (kindSimpleKind True k) returns a simple kind sk such that sk <: k
1804 -- If the flag is False, it requires k <: sk
1805 -- E.g.         kindSimpleKind False ?? = *
1806 -- What about (kv -> *) :=: ?? -> *
1807 kindSimpleKind orig_swapped orig_kind
1808   = go orig_swapped orig_kind
1809   where
1810     go sw (FunTy k1 k2) = do { k1' <- go (not sw) k1
1811                              ; k2' <- go sw k2
1812                              ; return (mkArrowKind k1' k2') }
1813     go True k
1814      | isOpenTypeKind k = return liftedTypeKind
1815      | isArgTypeKind k  = return liftedTypeKind
1816     go sw k
1817      | isLiftedTypeKind k   = return liftedTypeKind
1818      | isUnliftedTypeKind k = return unliftedTypeKind
1819     go sw k@(TyVarTy _)   = return k    -- KindVars are always simple
1820     go swapped kind = failWithTc (ptext SLIT("Unexpected kind unification failure:")
1821                                   <+> ppr orig_swapped <+> ppr orig_kind)
1822         -- I think this can't actually happen
1823
1824 -- T v = MkT v           v must be a type
1825 -- T v w = MkT (v -> w)  v must not be an umboxed tuple
1826
1827 ----------------
1828 kindOccurCheckErr tyvar ty
1829   = hang (ptext SLIT("Occurs check: cannot construct the infinite kind:"))
1830        2 (sep [ppr tyvar, char '=', ppr ty])
1831 \end{code}
1832
1833 \begin{code}
1834 unifyFunKind :: TcKind -> TcM (Maybe (TcKind, TcKind))
1835 -- Like unifyFunTy, but does not fail; instead just returns Nothing
1836
1837 unifyFunKind (TyVarTy kvar)
1838   = readKindVar kvar `thenM` \ maybe_kind ->
1839     case maybe_kind of
1840       Indirect fun_kind -> unifyFunKind fun_kind
1841       Flexi ->
1842           do { arg_kind <- newKindVar
1843              ; res_kind <- newKindVar
1844              ; writeKindVar kvar (mkArrowKind arg_kind res_kind)
1845              ; returnM (Just (arg_kind,res_kind)) }
1846
1847 unifyFunKind (FunTy arg_kind res_kind) = returnM (Just (arg_kind,res_kind))
1848 unifyFunKind other                     = returnM Nothing
1849 \end{code}
1850
1851 %************************************************************************
1852 %*                                                                      *
1853         Checking kinds
1854 %*                                                                      *
1855 %************************************************************************
1856
1857 ---------------------------
1858 -- We would like to get a decent error message from
1859 --   (a) Under-applied type constructors
1860 --              f :: (Maybe, Maybe)
1861 --   (b) Over-applied type constructors
1862 --              f :: Int x -> Int x
1863 --
1864
1865 \begin{code}
1866 checkExpectedKind :: Outputable a => a -> TcKind -> TcKind -> TcM ()
1867 -- A fancy wrapper for 'unifyKind', which tries
1868 -- to give decent error messages.
1869 --      (checkExpectedKind ty act_kind exp_kind)
1870 -- checks that the actual kind act_kind is compatible
1871 --      with the expected kind exp_kind
1872 -- The first argument, ty, is used only in the error message generation
1873 checkExpectedKind ty act_kind exp_kind
1874   | act_kind `isSubKind` exp_kind -- Short cut for a very common case
1875   = returnM ()
1876   | otherwise
1877   = tryTc (unifyKind exp_kind act_kind) `thenM` \ (_errs, mb_r) ->
1878     case mb_r of {
1879         Just r  -> returnM () ; -- Unification succeeded
1880         Nothing ->
1881
1882         -- So there's definitely an error
1883         -- Now to find out what sort
1884     zonkTcKind exp_kind         `thenM` \ exp_kind ->
1885     zonkTcKind act_kind         `thenM` \ act_kind ->
1886
1887     tcInitTidyEnv               `thenM` \ env0 ->
1888     let (exp_as, _) = splitKindFunTys exp_kind
1889         (act_as, _) = splitKindFunTys act_kind
1890         n_exp_as = length exp_as
1891         n_act_as = length act_as
1892
1893         (env1, tidy_exp_kind) = tidyKind env0 exp_kind
1894         (env2, tidy_act_kind) = tidyKind env1 act_kind
1895
1896         err | n_exp_as < n_act_as       -- E.g. [Maybe]
1897             = quotes (ppr ty) <+> ptext SLIT("is not applied to enough type arguments")
1898
1899                 -- Now n_exp_as >= n_act_as. In the next two cases,
1900                 -- n_exp_as == 0, and hence so is n_act_as
1901             | isLiftedTypeKind exp_kind && isUnliftedTypeKind act_kind
1902             = ptext SLIT("Expecting a lifted type, but") <+> quotes (ppr ty)
1903                 <+> ptext SLIT("is unlifted")
1904
1905             | isUnliftedTypeKind exp_kind && isLiftedTypeKind act_kind
1906             = ptext SLIT("Expecting an unlifted type, but") <+> quotes (ppr ty)
1907                 <+> ptext SLIT("is lifted")
1908
1909             | otherwise                 -- E.g. Monad [Int]
1910             = ptext SLIT("Kind mis-match")
1911
1912         more_info = sep [ ptext SLIT("Expected kind") <+>
1913                                 quotes (pprKind tidy_exp_kind) <> comma,
1914                           ptext SLIT("but") <+> quotes (ppr ty) <+>
1915                                 ptext SLIT("has kind") <+> quotes (pprKind tidy_act_kind)]
1916    in
1917    failWithTcM (env2, err $$ more_info)
1918    }
1919 \end{code}
1920
1921 %************************************************************************
1922 %*                                                                      *
1923 \subsection{Checking signature type variables}
1924 %*                                                                      *
1925 %************************************************************************
1926
1927 @checkSigTyVars@ checks that a set of universally quantified type varaibles
1928 are not mentioned in the environment.  In particular:
1929
1930         (a) Not mentioned in the type of a variable in the envt
1931                 eg the signature for f in this:
1932
1933                         g x = ... where
1934                                         f :: a->[a]
1935                                         f y = [x,y]
1936
1937                 Here, f is forced to be monorphic by the free occurence of x.
1938
1939         (d) Not (unified with another type variable that is) in scope.
1940                 eg f x :: (r->r) = (\y->y) :: forall a. a->r
1941             when checking the expression type signature, we find that
1942             even though there is nothing in scope whose type mentions r,
1943             nevertheless the type signature for the expression isn't right.
1944
1945             Another example is in a class or instance declaration:
1946                 class C a where
1947                    op :: forall b. a -> b
1948                    op x = x
1949             Here, b gets unified with a
1950
1951 Before doing this, the substitution is applied to the signature type variable.
1952
1953 \begin{code}
1954 checkSigTyVars :: [TcTyVar] -> TcM ()
1955 checkSigTyVars sig_tvs = check_sig_tyvars emptyVarSet sig_tvs
1956
1957 checkSigTyVarsWrt :: TcTyVarSet -> [TcTyVar] -> TcM ()
1958 -- The extra_tvs can include boxy type variables;
1959 --      e.g. TcMatches.tcCheckExistentialPat
1960 checkSigTyVarsWrt extra_tvs sig_tvs
1961   = do  { extra_tvs' <- zonkTcTyVarsAndFV (varSetElems extra_tvs)
1962         ; check_sig_tyvars extra_tvs' sig_tvs }
1963
1964 check_sig_tyvars
1965         :: TcTyVarSet   -- Global type variables. The universally quantified
1966                         --      tyvars should not mention any of these
1967                         --      Guaranteed already zonked.
1968         -> [TcTyVar]    -- Universally-quantified type variables in the signature
1969                         --      Guaranteed to be skolems
1970         -> TcM ()
1971 check_sig_tyvars extra_tvs []
1972   = returnM ()
1973 check_sig_tyvars extra_tvs sig_tvs
1974   = ASSERT( all isSkolemTyVar sig_tvs )
1975     do  { gbl_tvs <- tcGetGlobalTyVars
1976         ; traceTc (text "check_sig_tyvars" <+> (vcat [text "sig_tys" <+> ppr sig_tvs,
1977                                       text "gbl_tvs" <+> ppr gbl_tvs,
1978                                       text "extra_tvs" <+> ppr extra_tvs]))
1979
1980         ; let env_tvs = gbl_tvs `unionVarSet` extra_tvs
1981         ; ifM (any (`elemVarSet` env_tvs) sig_tvs)
1982               (bleatEscapedTvs env_tvs sig_tvs sig_tvs)
1983         }
1984
1985 bleatEscapedTvs :: TcTyVarSet   -- The global tvs
1986                 -> [TcTyVar]    -- The possibly-escaping type variables
1987                 -> [TcTyVar]    -- The zonked versions thereof
1988                 -> TcM ()
1989 -- Complain about escaping type variables
1990 -- We pass a list of type variables, at least one of which
1991 -- escapes.  The first list contains the original signature type variable,
1992 -- while the second  contains the type variable it is unified to (usually itself)
1993 bleatEscapedTvs globals sig_tvs zonked_tvs
1994   = do  { env0 <- tcInitTidyEnv
1995         ; let (env1, tidy_tvs)        = tidyOpenTyVars env0 sig_tvs
1996               (env2, tidy_zonked_tvs) = tidyOpenTyVars env1 zonked_tvs
1997
1998         ; (env3, msgs) <- foldlM check (env2, []) (tidy_tvs `zip` tidy_zonked_tvs)
1999         ; failWithTcM (env3, main_msg $$ nest 2 (vcat msgs)) }
2000   where
2001     main_msg = ptext SLIT("Inferred type is less polymorphic than expected")
2002
2003     check (tidy_env, msgs) (sig_tv, zonked_tv)
2004       | not (zonked_tv `elemVarSet` globals) = return (tidy_env, msgs)
2005       | otherwise
2006       = do { (tidy_env1, globs) <- findGlobals (unitVarSet zonked_tv) tidy_env
2007            ; returnM (tidy_env1, escape_msg sig_tv zonked_tv globs : msgs) }
2008
2009 -----------------------
2010 escape_msg sig_tv zonked_tv globs
2011   | notNull globs
2012   = vcat [sep [msg, ptext SLIT("is mentioned in the environment:")],
2013           nest 2 (vcat globs)]
2014   | otherwise
2015   = msg <+> ptext SLIT("escapes")
2016         -- Sigh.  It's really hard to give a good error message
2017         -- all the time.   One bad case is an existential pattern match.
2018         -- We rely on the "When..." context to help.
2019   where
2020     msg = ptext SLIT("Quantified type variable") <+> quotes (ppr sig_tv) <+> is_bound_to
2021     is_bound_to
2022         | sig_tv == zonked_tv = empty
2023         | otherwise = ptext SLIT("is unified with") <+> quotes (ppr zonked_tv) <+> ptext SLIT("which")
2024 \end{code}
2025
2026 These two context are used with checkSigTyVars
2027
2028 \begin{code}
2029 sigCtxt :: Id -> [TcTyVar] -> TcThetaType -> TcTauType
2030         -> TidyEnv -> TcM (TidyEnv, Message)
2031 sigCtxt id sig_tvs sig_theta sig_tau tidy_env
2032   = zonkTcType sig_tau          `thenM` \ actual_tau ->
2033     let
2034         (env1, tidy_sig_tvs)    = tidyOpenTyVars tidy_env sig_tvs
2035         (env2, tidy_sig_rho)    = tidyOpenType env1 (mkPhiTy sig_theta sig_tau)
2036         (env3, tidy_actual_tau) = tidyOpenType env2 actual_tau
2037         sub_msg = vcat [ptext SLIT("Signature type:    ") <+> pprType (mkForAllTys tidy_sig_tvs tidy_sig_rho),
2038                         ptext SLIT("Type to generalise:") <+> pprType tidy_actual_tau
2039                    ]
2040         msg = vcat [ptext SLIT("When trying to generalise the type inferred for") <+> quotes (ppr id),
2041                     nest 2 sub_msg]
2042     in
2043     returnM (env3, msg)
2044 \end{code}