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