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