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