2 % (c) The University of Glasgow 2006
3 % (c) The GRASP/AQUA Project, Glasgow University, 1992-1998
6 Type subsumption and unification
10 -- Full-blown subsumption
12 checkSigTyVars, checkSigTyVarsWrt, bleatEscapedTvs, sigCtxt,
14 -- Various unifications
15 unifyType, unifyTypeList, unifyTheta,
16 unifyKind, unifyKinds, unifyFunKind,
17 preSubType, boxyMatchTypes,
19 --------------------------------
21 tcInfer, subFunTys, unBox, refineBox, refineBoxToTau, withBox,
22 boxyUnify, boxyUnifyList, zapToMonotype,
23 boxySplitListTy, boxySplitPArrTy, boxySplitTyConApp, boxySplitAppTy,
27 #include "HsVersions.h"
37 import TcRnMonad -- TcType, amongst others
59 %************************************************************************
61 \subsection{'hole' type variables}
63 %************************************************************************
66 tcInfer :: (BoxyType -> TcM a) -> TcM (a, TcType)
67 tcInfer tc_infer = withBox openTypeKind tc_infer
71 %************************************************************************
75 %************************************************************************
78 subFunTys :: SDoc -- Something like "The function f has 3 arguments"
79 -- or "The abstraction (\x.e) takes 1 argument"
80 -> Arity -- Expected # of args
81 -> BoxySigmaType -- res_ty
82 -> Maybe UserTypeCtxt -- Whether res_ty arises from a user signature
83 -- Only relevant if we encounter a sigma-type
84 -> ([BoxySigmaType] -> BoxyRhoType -> TcM a)
86 -- Attempt to decompse res_ty to have enough top-level arrows to
87 -- match the number of patterns in the match group
89 -- If (subFunTys n_args res_ty thing_inside) = (co_fn, res)
90 -- and the inner call to thing_inside passes args: [a1,...,an], b
91 -- then co_fn :: (a1 -> ... -> an -> b) ~ res_ty
93 -- Note that it takes a BoxyRho type, and guarantees to return a BoxyRhoType
96 {- Error messages from subFunTys
98 The abstraction `\Just 1 -> ...' has two arguments
99 but its type `Maybe a -> a' has only one
101 The equation(s) for `f' have two arguments
102 but its type `Maybe a -> a' has only one
104 The section `(f 3)' requires 'f' to take two arguments
105 but its type `Int -> Int' has only one
107 The function 'f' is applied to two arguments
108 but its type `Int -> Int' has only one
112 subFunTys error_herald n_pats res_ty mb_ctxt thing_inside
113 = loop n_pats [] res_ty
115 -- In 'loop', the parameter 'arg_tys' accumulates
116 -- the arg types so far, in *reverse order*
117 -- INVARIANT: res_ty :: *
118 loop n args_so_far res_ty
119 | Just res_ty' <- tcView res_ty = loop n args_so_far res_ty'
121 loop n args_so_far res_ty
122 | isSigmaTy res_ty -- Do this before checking n==0, because we
123 -- guarantee to return a BoxyRhoType, not a
125 = do { (gen_fn, (co_fn, res)) <- tcGen res_ty emptyVarSet mb_ctxt $ \ _ res_ty ->
126 loop n args_so_far res_ty
127 ; return (gen_fn <.> co_fn, res) }
129 loop 0 args_so_far res_ty
130 = do { res <- thing_inside (reverse args_so_far) res_ty
131 ; return (idHsWrapper, res) }
133 loop n args_so_far (FunTy arg_ty res_ty)
134 = do { (co_fn, res) <- loop (n-1) (arg_ty:args_so_far) res_ty
135 ; co_fn' <- wrapFunResCoercion [arg_ty] co_fn
136 ; return (co_fn', res) }
138 -- Try to normalise synonym families and defer if that's not possible
139 loop n args_so_far ty@(TyConApp tc _)
141 = do { (coi1, ty') <- tcNormaliseFamInst ty
143 IdCo -> defer n args_so_far ty
144 -- no progress, but maybe solvable => defer
145 ACo _ -> -- progress: so lets try again
146 do { (co_fn, res) <- loop n args_so_far ty'
147 ; return $ (co_fn <.> coiToHsWrapper (mkSymCoI coi1), res)
151 -- res_ty might have a type variable at the head, such as (a b c),
152 -- in which case we must fill in with (->). Simplest thing to do
153 -- is to use boxyUnify, but we catch failure and generate our own
154 -- error message on failure
155 loop n args_so_far res_ty@(AppTy _ _)
156 = do { [arg_ty',res_ty'] <- newBoxyTyVarTys [argTypeKind, openTypeKind]
157 ; (_, mb_coi) <- tryTcErrs $
158 boxyUnify res_ty (FunTy arg_ty' res_ty')
159 ; if isNothing mb_coi then bale_out args_so_far
160 else do { let coi = expectJust "subFunTys" mb_coi
161 ; (co_fn, res) <- loop n args_so_far (FunTy arg_ty'
163 ; return (co_fn <.> coiToHsWrapper coi, res)
167 loop n args_so_far ty@(TyVarTy tv)
168 | isTyConableTyVar tv
169 = do { cts <- readMetaTyVar tv
171 Indirect ty -> loop n args_so_far ty
173 do { (res_ty:arg_tys) <- withMetaTvs tv kinds mk_res_ty
174 ; res <- thing_inside (reverse args_so_far ++ arg_tys)
176 ; return (idHsWrapper, res) } }
177 | otherwise -- defer as tyvar may be refined by equalities
178 = defer n args_so_far ty
180 mk_res_ty (res_ty' : arg_tys') = mkFunTys arg_tys' res_ty'
181 mk_res_ty [] = panic "TcUnify.mk_res_ty1"
182 kinds = openTypeKind : take n (repeat argTypeKind)
183 -- Note argTypeKind: the args can have an unboxed type,
184 -- but not an unboxed tuple.
186 loop _ args_so_far _ = bale_out args_so_far
188 -- Build a template type a1 -> ... -> an -> b and defer an equality
189 -- between that template and the expected result type res_ty; then,
190 -- use the template to type the thing_inside
191 defer n args_so_far ty
192 = do { arg_tys <- newFlexiTyVarTys n argTypeKind
193 ; res_ty' <- newFlexiTyVarTy openTypeKind
194 ; let fun_ty = mkFunTys arg_tys res_ty'
195 err = error_herald <> comma $$
196 text "which does not match its type"
197 ; coi <- addErrCtxt err $
198 defer_unification (Unify False fun_ty ty) False fun_ty ty
199 ; res <- thing_inside (reverse args_so_far ++ arg_tys) res_ty'
200 ; return (coiToHsWrapper coi, res)
204 = do { env0 <- tcInitTidyEnv
205 ; res_ty' <- zonkTcType res_ty
206 ; let (env1, res_ty'') = tidyOpenType env0 res_ty'
207 ; failWithTcM (env1, mk_msg res_ty'' (length args_so_far)) }
209 mk_msg res_ty n_actual
210 = error_herald <> comma $$
211 sep [ptext (sLit "but its type") <+> quotes (pprType res_ty),
212 if n_actual == 0 then ptext (sLit "has none")
213 else ptext (sLit "has only") <+> speakN n_actual]
217 ----------------------
218 boxySplitTyConApp :: TyCon -- T :: k1 -> ... -> kn -> *
219 -> BoxyRhoType -- Expected type (T a b c)
220 -> TcM ([BoxySigmaType], -- Element types, a b c
221 CoercionI) -- T a b c ~ orig_ty
222 -- It's used for wired-in tycons, so we call checkWiredInTyCon
223 -- Precondition: never called with FunTyCon
224 -- Precondition: input type :: *
226 boxySplitTyConApp tc orig_ty
227 = do { checkWiredInTyCon tc
228 ; loop (tyConArity tc) [] orig_ty }
230 loop n_req args_so_far ty
231 | Just ty' <- tcView ty = loop n_req args_so_far ty'
233 loop n_req args_so_far ty@(TyConApp tycon args)
235 = ASSERT( n_req == length args) -- ty::*
236 return (args ++ args_so_far, IdCo)
238 | isOpenSynTyCon tycon -- try to normalise type family application
239 = do { (coi1, ty') <- tcNormaliseFamInst ty
240 ; traceTc $ text "boxySplitTyConApp:" <+>
241 ppr ty <+> text "==>" <+> ppr ty'
243 IdCo -> defer -- no progress, but maybe solvable => defer
244 ACo _ -> -- progress: so lets try again
245 do { (args, coi2) <- loop n_req args_so_far ty'
246 ; return $ (args, coi2 `mkTransCoI` mkSymCoI coi1)
250 loop n_req args_so_far (AppTy fun arg)
252 = do { (args, coi) <- loop (n_req - 1) (arg:args_so_far) fun
253 ; return (args, mkAppTyCoI fun coi arg IdCo)
256 loop n_req args_so_far (TyVarTy tv)
257 | isTyConableTyVar tv
258 , res_kind `isSubKind` tyVarKind tv
259 = do { cts <- readMetaTyVar tv
261 Indirect ty -> loop n_req args_so_far ty
262 Flexi -> do { arg_tys <- withMetaTvs tv arg_kinds mk_res_ty
263 ; return (arg_tys ++ args_so_far, IdCo) }
265 | otherwise -- defer as tyvar may be refined by equalities
268 (arg_kinds, res_kind) = splitKindFunTysN n_req (tyConKind tc)
270 loop _ _ _ = boxySplitFailure (mkTyConApp tc (mkTyVarTys (tyConTyVars tc)))
273 -- defer splitting by generating an equality constraint
274 defer = boxySplitDefer arg_kinds mk_res_ty orig_ty
276 (arg_kinds, _) = splitKindFunTys (tyConKind tc)
278 -- apply splitted tycon to arguments
279 mk_res_ty = mkTyConApp tc
281 ----------------------
282 boxySplitListTy :: BoxyRhoType -> TcM (BoxySigmaType, CoercionI)
283 -- Special case for lists
284 boxySplitListTy exp_ty
285 = do { ([elt_ty], coi) <- boxySplitTyConApp listTyCon exp_ty
286 ; return (elt_ty, coi) }
288 ----------------------
289 boxySplitPArrTy :: BoxyRhoType -> TcM (BoxySigmaType, CoercionI)
290 -- Special case for parrs
291 boxySplitPArrTy exp_ty
292 = do { ([elt_ty], coi) <- boxySplitTyConApp parrTyCon exp_ty
293 ; return (elt_ty, coi) }
295 ----------------------
296 boxySplitAppTy :: BoxyRhoType -- Type to split: m a
297 -> TcM ((BoxySigmaType, BoxySigmaType), -- Returns m, a
299 -- If the incoming type is a mutable type variable of kind k, then
300 -- boxySplitAppTy returns a new type variable (m: * -> k); note the *.
301 -- If the incoming type is boxy, then so are the result types; and vice versa
303 boxySplitAppTy orig_ty
307 | Just ty' <- tcView ty = loop ty'
310 | Just (fun_ty, arg_ty) <- tcSplitAppTy_maybe ty
311 = return ((fun_ty, arg_ty), IdCo)
313 loop ty@(TyConApp tycon _args)
314 | isOpenSynTyCon tycon -- try to normalise type family application
315 = do { (coi1, ty') <- tcNormaliseFamInst ty
317 IdCo -> defer -- no progress, but maybe solvable => defer
318 ACo _ -> -- progress: so lets try again
319 do { (args, coi2) <- loop ty'
320 ; return $ (args, coi2 `mkTransCoI` mkSymCoI coi1)
325 | isTyConableTyVar tv
326 = do { cts <- readMetaTyVar tv
328 Indirect ty -> loop ty
329 Flexi -> do { [fun_ty, arg_ty] <- withMetaTvs tv kinds mk_res_ty
330 ; return ((fun_ty, arg_ty), IdCo) } }
331 | otherwise -- defer as tyvar may be refined by equalities
334 tv_kind = tyVarKind tv
335 kinds = [mkArrowKind liftedTypeKind (defaultKind tv_kind),
337 liftedTypeKind] -- arg type :: *
338 -- The defaultKind is a bit smelly. If you remove it,
339 -- try compiling f x = do { x }
340 -- and you'll get a kind mis-match. It smells, but
341 -- not enough to lose sleep over.
343 loop _ = boxySplitFailure (mkAppTy alphaTy betaTy) orig_ty
345 -- defer splitting by generating an equality constraint
346 defer = do { ([ty1, ty2], coi) <- boxySplitDefer arg_kinds mk_res_ty orig_ty
347 ; return ((ty1, ty2), coi)
350 orig_kind = typeKind orig_ty
351 arg_kinds = [mkArrowKind liftedTypeKind (defaultKind orig_kind),
353 liftedTypeKind] -- arg type :: *
355 -- build type application
356 mk_res_ty [fun_ty', arg_ty'] = mkAppTy fun_ty' arg_ty'
357 mk_res_ty _other = panic "TcUnify.mk_res_ty2"
360 boxySplitFailure :: TcType -> TcType -> TcM (a, CoercionI)
361 boxySplitFailure actual_ty expected_ty = failWithMisMatch actual_ty expected_ty
364 boxySplitDefer :: [Kind] -- kinds of required arguments
365 -> ([TcType] -> TcTauType) -- construct lhs from argument tyvars
366 -> BoxyRhoType -- type to split
367 -> TcM ([TcType], CoercionI)
368 boxySplitDefer kinds mk_ty orig_ty
369 = do { tau_tys <- mapM newFlexiTyVarTy kinds
370 ; let ty1 = mk_ty tau_tys
371 ; coi <- defer_unification (Unify False ty1 orig_ty) False ty1 orig_ty
372 ; return (tau_tys, coi)
377 --------------------------------
378 -- withBoxes: the key utility function
379 --------------------------------
382 withMetaTvs :: TcTyVar -- An unfilled-in, non-skolem, meta type variable
383 -> [Kind] -- Make fresh boxes (with the same BoxTv/TauTv setting as tv)
384 -> ([BoxySigmaType] -> BoxySigmaType)
385 -- Constructs the type to assign
386 -- to the original var
387 -> TcM [BoxySigmaType] -- Return the fresh boxes
389 -- It's entirely possible for the [kind] to be empty.
390 -- For example, when pattern-matching on True,
391 -- we call boxySplitTyConApp passing a boolTyCon
393 -- Invariant: tv is still Flexi
395 withMetaTvs tv kinds mk_res_ty
397 = do { box_tvs <- mapM (newMetaTyVar BoxTv) kinds
398 ; let box_tys = mkTyVarTys box_tvs
399 ; writeMetaTyVar tv (mk_res_ty box_tys)
402 | otherwise -- Non-boxy meta type variable
403 = do { tau_tys <- mapM newFlexiTyVarTy kinds
404 ; writeMetaTyVar tv (mk_res_ty tau_tys) -- Write it *first*
405 -- Sure to be a tau-type
408 withBox :: Kind -> (BoxySigmaType -> TcM a) -> TcM (a, TcType)
409 -- Allocate a *boxy* tyvar
410 withBox kind thing_inside
411 = do { box_tv <- newBoxyTyVar kind
412 ; res <- thing_inside (mkTyVarTy box_tv)
413 ; ty <- {- pprTrace "with_box" (ppr (mkTyVarTy box_tv)) $ -} readFilledBox box_tv
418 %************************************************************************
420 Approximate boxy matching
422 %************************************************************************
425 preSubType :: [TcTyVar] -- Quantified type variables
426 -> TcTyVarSet -- Subset of quantified type variables
427 -- see Note [Pre-sub boxy]
428 -> TcType -- The rho-type part; quantified tyvars scopes over this
429 -> BoxySigmaType -- Matching type from the context
430 -> TcM [TcType] -- Types to instantiate the tyvars
431 -- Perform pre-subsumption, and return suitable types
432 -- to instantiate the quantified type varibles:
433 -- info from the pre-subsumption, if there is any
434 -- a boxy type variable otherwise
436 -- Note [Pre-sub boxy]
437 -- The 'btvs' are a subset of 'qtvs'. They are the ones we can
438 -- instantiate to a boxy type variable, because they'll definitely be
439 -- filled in later. This isn't always the case; sometimes we have type
440 -- variables mentioned in the context of the type, but not the body;
441 -- f :: forall a b. C a b => a -> a
442 -- Then we may land up with an unconstrained 'b', so we want to
443 -- instantiate it to a monotype (non-boxy) type variable
445 -- The 'qtvs' that are *neither* fixed by the pre-subsumption, *nor* are in 'btvs',
446 -- are instantiated to TauTv meta variables.
448 preSubType qtvs btvs qty expected_ty
449 = do { tys <- mapM inst_tv qtvs
450 ; traceTc (text "preSubType" <+> (ppr qtvs $$ ppr btvs $$ ppr qty $$ ppr expected_ty $$ ppr pre_subst $$ ppr tys))
453 pre_subst = boxySubMatchType (mkVarSet qtvs) qty expected_ty
455 | Just boxy_ty <- lookupTyVar pre_subst tv = return boxy_ty
456 | tv `elemVarSet` btvs = do { tv' <- tcInstBoxyTyVar tv
457 ; return (mkTyVarTy tv') }
458 | otherwise = do { tv' <- tcInstTyVar tv
459 ; return (mkTyVarTy tv') }
462 :: TcTyVarSet -> TcType -- The "template"; the tyvars are skolems
463 -> BoxyRhoType -- Type to match (note a *Rho* type)
464 -> TvSubst -- Substitution of the [TcTyVar] to BoxySigmaTypes
466 -- boxySubMatchType implements the Pre-subsumption judgement, in Fig 5 of the paper
467 -- "Boxy types: inference for higher rank types and impredicativity"
469 boxySubMatchType tmpl_tvs tmpl_ty boxy_ty
470 = go tmpl_tvs tmpl_ty emptyVarSet boxy_ty
472 go t_tvs t_ty b_tvs b_ty
473 | Just t_ty' <- tcView t_ty = go t_tvs t_ty' b_tvs b_ty
474 | Just b_ty' <- tcView b_ty = go t_tvs t_ty b_tvs b_ty'
476 go _ (TyVarTy _) _ _ = emptyTvSubst -- Rule S-ANY; no bindings
477 -- Rule S-ANY covers (a) type variables and (b) boxy types
478 -- in the template. Both look like a TyVarTy.
479 -- See Note [Sub-match] below
481 go t_tvs t_ty b_tvs b_ty
482 | isSigmaTy t_ty, (tvs, _, t_tau) <- tcSplitSigmaTy t_ty
483 = go (t_tvs `delVarSetList` tvs) t_tau b_tvs b_ty -- Rule S-SPEC
484 -- Under a forall on the left, if there is shadowing,
485 -- do not bind! Hence the delVarSetList.
486 | isSigmaTy b_ty, (tvs, _, b_tau) <- tcSplitSigmaTy b_ty
487 = go t_tvs t_ty (extendVarSetList b_tvs tvs) b_tau -- Rule S-SKOL
488 -- Add to the variables we must not bind to
489 -- NB: it's *important* to discard the theta part. Otherwise
490 -- consider (forall a. Eq a => a -> b) ~<~ (Int -> Int -> Bool)
491 -- and end up with a completely bogus binding (b |-> Bool), by lining
492 -- up the (Eq a) with the Int, whereas it should be (b |-> (Int->Bool)).
493 -- This pre-subsumption stuff can return too few bindings, but it
494 -- must *never* return bogus info.
496 go t_tvs (FunTy arg1 res1) b_tvs (FunTy arg2 res2) -- Rule S-FUN
497 = boxy_match t_tvs arg1 b_tvs arg2 (go t_tvs res1 b_tvs res2)
498 -- Match the args, and sub-match the results
500 go t_tvs t_ty b_tvs b_ty = boxy_match t_tvs t_ty b_tvs b_ty emptyTvSubst
501 -- Otherwise defer to boxy matching
502 -- This covers TyConApp, AppTy, PredTy
509 |- head xs : <rhobox>
510 We will do a boxySubMatchType between a ~ <rhobox>
511 But we *don't* want to match [a |-> <rhobox>] because
512 (a) The box should be filled in with a rho-type, but
513 but the returned substitution maps TyVars to boxy
515 (b) In any case, the right final answer might be *either*
516 instantiate 'a' with a rho-type or a sigma type
517 head xs : Int vs head xs : forall b. b->b
518 So the matcher MUST NOT make a choice here. In general, we only
519 bind a template type variable in boxyMatchType, not in boxySubMatchType.
524 :: TcTyVarSet -> [TcType] -- The "template"; the tyvars are skolems
525 -> [BoxySigmaType] -- Type to match
526 -> TvSubst -- Substitution of the [TcTyVar] to BoxySigmaTypes
528 -- boxyMatchTypes implements the Pre-matching judgement, in Fig 5 of the paper
529 -- "Boxy types: inference for higher rank types and impredicativity"
531 -- Find a *boxy* substitution that makes the template look as much
532 -- like the BoxySigmaType as possible.
533 -- It's always ok to return an empty substitution;
534 -- anything more is jam on the pudding
536 -- NB1: This is a pure, non-monadic function.
537 -- It does no unification, and cannot fail
539 -- Precondition: the arg lengths are equal
540 -- Precondition: none of the template type variables appear anywhere in the [BoxySigmaType]
544 boxyMatchTypes tmpl_tvs tmpl_tys boxy_tys
545 = ASSERT( length tmpl_tys == length boxy_tys )
546 boxy_match_s tmpl_tvs tmpl_tys emptyVarSet boxy_tys emptyTvSubst
547 -- ToDo: add error context?
549 boxy_match_s :: TcTyVarSet -> [TcType] -> TcTyVarSet -> [BoxySigmaType]
550 -> TvSubst -> TvSubst
551 boxy_match_s _ [] _ [] subst
553 boxy_match_s tmpl_tvs (t_ty:t_tys) boxy_tvs (b_ty:b_tys) subst
554 = boxy_match tmpl_tvs t_ty boxy_tvs b_ty $
555 boxy_match_s tmpl_tvs t_tys boxy_tvs b_tys subst
556 boxy_match_s _ _ _ _ _
557 = panic "boxy_match_s" -- Lengths do not match
561 boxy_match :: TcTyVarSet -> TcType -- Template
562 -> TcTyVarSet -- boxy_tvs: do not bind template tyvars to any of these
563 -> BoxySigmaType -- Match against this type
567 -- The boxy_tvs argument prevents this match:
568 -- [a] forall b. a ~ forall b. b
569 -- We don't want to bind the template variable 'a'
570 -- to the quantified type variable 'b'!
572 boxy_match tmpl_tvs orig_tmpl_ty boxy_tvs orig_boxy_ty subst
573 = go orig_tmpl_ty orig_boxy_ty
576 | Just t_ty' <- tcView t_ty = go t_ty' b_ty
577 | Just b_ty' <- tcView b_ty = go t_ty b_ty'
579 go ty1 ty2 -- C.f. the isSigmaTy case for boxySubMatchType
581 , (tvs1, _, tau1) <- tcSplitSigmaTy ty1
582 , (tvs2, _, tau2) <- tcSplitSigmaTy ty2
583 , equalLength tvs1 tvs2
584 = boxy_match (tmpl_tvs `delVarSetList` tvs1) tau1
585 (boxy_tvs `extendVarSetList` tvs2) tau2 subst
587 go (TyConApp tc1 tys1) (TyConApp tc2 tys2)
589 , not $ isOpenSynTyCon tc1
592 go (FunTy arg1 res1) (FunTy arg2 res2)
593 = go_s [arg1,res1] [arg2,res2]
596 | Just (s1,t1) <- tcSplitAppTy_maybe t_ty,
597 Just (s2,t2) <- tcSplitAppTy_maybe b_ty,
598 typeKind t2 `isSubKind` typeKind t1 -- Maintain invariant
599 = go_s [s1,t1] [s2,t2]
602 | tv `elemVarSet` tmpl_tvs -- Template type variable in the template
603 , boxy_tvs `disjointVarSet` tyVarsOfType orig_boxy_ty
604 , typeKind b_ty `isSubKind` tyVarKind tv -- See Note [Matching kinds]
605 = extendTvSubst subst tv boxy_ty'
607 = subst -- Ignore others
609 boxy_ty' = case lookupTyVar subst tv of
610 Nothing -> orig_boxy_ty
611 Just ty -> ty `boxyLub` orig_boxy_ty
613 go _ (TyVarTy tv) | isTcTyVar tv && isMetaTyVar tv
614 -- NB: A TyVar (not TcTyVar) is possible here, representing
615 -- a skolem, because in this pure boxy_match function
616 -- we don't instantiate foralls to TcTyVars; cf Trac #2714
617 = subst -- Don't fail if the template has more info than the target!
618 -- Otherwise, with tmpl_tvs = [a], matching (a -> Int) ~ (Bool -> beta)
619 -- would fail to instantiate 'a', because the meta-type-variable
620 -- beta is as yet un-filled-in
622 go _ _ = emptyTvSubst -- It's important to *fail* by returning the empty substitution
623 -- Example: Tree a ~ Maybe Int
624 -- We do not want to bind (a |-> Int) in pre-matching, because that can give very
625 -- misleading error messages. An even more confusing case is
626 -- a -> b ~ Maybe Int
627 -- Then we do not want to bind (b |-> Int)! It's always safe to discard bindings
628 -- from this pre-matching phase.
631 go_s tys1 tys2 = boxy_match_s tmpl_tvs tys1 boxy_tvs tys2 subst
634 boxyLub :: BoxySigmaType -> BoxySigmaType -> BoxySigmaType
635 -- Combine boxy information from the two types
636 -- If there is a conflict, return the first
637 boxyLub orig_ty1 orig_ty2
638 = go orig_ty1 orig_ty2
640 go (AppTy f1 a1) (AppTy f2 a2) = AppTy (boxyLub f1 f2) (boxyLub a1 a2)
641 go (FunTy f1 a1) (FunTy f2 a2) = FunTy (boxyLub f1 f2) (boxyLub a1 a2)
642 go (TyConApp tc1 ts1) (TyConApp tc2 ts2)
643 | tc1 == tc2, length ts1 == length ts2
644 = TyConApp tc1 (zipWith boxyLub ts1 ts2)
646 go (TyVarTy tv1) _ -- This is the whole point;
647 | isTcTyVar tv1, isBoxyTyVar tv1 -- choose ty2 if ty2 is a box
650 go _ (TyVarTy tv2) -- Symmetrical case
651 | isTcTyVar tv2, isBoxyTyVar tv2
654 -- Look inside type synonyms, but only if the naive version fails
655 go ty1 ty2 | Just ty1' <- tcView ty1 = go ty1' ty2
656 | Just ty2' <- tcView ty1 = go ty1 ty2'
658 -- For now, we don't look inside ForAlls, PredTys
659 go _ _ = orig_ty1 -- Default
662 Note [Matching kinds]
663 ~~~~~~~~~~~~~~~~~~~~~
664 The target type might legitimately not be a sub-kind of template.
665 For example, suppose the target is simply a box with an OpenTypeKind,
666 and the template is a type variable with LiftedTypeKind.
667 Then it's ok (because the target type will later be refined).
668 We simply don't bind the template type variable.
670 It might also be that the kind mis-match is an error. For example,
671 suppose we match the template (a -> Int) against (Int# -> Int),
672 where the template type variable 'a' has LiftedTypeKind. This
673 matching function does not fail; it simply doesn't bind the template.
674 Later stuff will fail.
676 %************************************************************************
680 %************************************************************************
682 All the tcSub calls have the form
684 tcSub actual_ty expected_ty
686 actual_ty <= expected_ty
688 That is, that a value of type actual_ty is acceptable in
689 a place expecting a value of type expected_ty.
691 It returns a coercion function
692 co_fn :: actual_ty ~ expected_ty
693 which takes an HsExpr of type actual_ty into one of type
698 tcSubExp :: InstOrigin -> BoxySigmaType -> BoxySigmaType -> TcM HsWrapper
699 -- (tcSub act exp) checks that
701 tcSubExp orig actual_ty expected_ty
702 = -- addErrCtxtM (unifyCtxt actual_ty expected_ty) $
703 -- Adding the error context here leads to some very confusing error
704 -- messages, such as "can't match forall a. a->a with forall a. a->a"
705 -- Example is tcfail165:
706 -- do var <- newEmptyMVar :: IO (MVar (forall a. Show a => a -> String))
707 -- putMVar var (show :: forall a. Show a => a -> String)
708 -- Here the info does not flow from the 'var' arg of putMVar to its 'show' arg
709 -- but after zonking it looks as if it does!
711 -- So instead I'm adding the error context when moving from tc_sub to u_tys
713 traceTc (text "tcSubExp" <+> ppr actual_ty <+> ppr expected_ty) >>
714 tc_sub orig actual_ty actual_ty False expected_ty expected_ty
718 -> BoxySigmaType -- actual_ty, before expanding synonyms
719 -> BoxySigmaType -- ..and after
720 -> InBox -- True <=> expected_ty is inside a box
721 -> BoxySigmaType -- expected_ty, before
722 -> BoxySigmaType -- ..and after
724 -- The acual_ty is never inside a box
725 -- IMPORTANT pre-condition: if the args contain foralls, the bound type
726 -- variables are visible non-monadically
727 -- (i.e. tha args are sufficiently zonked)
728 -- This invariant is needed so that we can "see" the foralls, ad
729 -- e.g. in the SPEC rule where we just use splitSigmaTy
731 tc_sub orig act_sty act_ty exp_ib exp_sty exp_ty
732 = traceTc (text "tc_sub" <+> ppr act_ty $$ ppr exp_ty) >>
733 tc_sub1 orig act_sty act_ty exp_ib exp_sty exp_ty
734 -- This indirection is just here to make
735 -- it easy to insert a debug trace!
737 tc_sub1 :: InstOrigin -> BoxySigmaType -> BoxySigmaType -> InBox
738 -> BoxySigmaType -> Type -> TcM HsWrapper
739 tc_sub1 orig act_sty act_ty exp_ib exp_sty exp_ty
740 | Just exp_ty' <- tcView exp_ty = tc_sub orig act_sty act_ty exp_ib exp_sty exp_ty'
741 tc_sub1 orig act_sty act_ty exp_ib exp_sty exp_ty
742 | Just act_ty' <- tcView act_ty = tc_sub orig act_sty act_ty' exp_ib exp_sty exp_ty
744 -----------------------------------
745 -- Rule SBOXY, plus other cases when act_ty is a type variable
746 -- Just defer to boxy matching
747 -- This rule takes precedence over SKOL!
748 tc_sub1 orig act_sty (TyVarTy tv) exp_ib exp_sty exp_ty
749 = do { traceTc (text "tc_sub1 - case 1")
750 ; coi <- addSubCtxt orig act_sty exp_sty $
751 uVar (Unify True act_sty exp_sty) False tv exp_ib exp_sty exp_ty
752 ; traceTc (case coi of
753 IdCo -> text "tc_sub1 (Rule SBOXY) IdCo"
754 ACo co -> text "tc_sub1 (Rule SBOXY) ACo" <+> ppr co)
755 ; return $ coiToHsWrapper coi
758 -----------------------------------
759 -- Skolemisation case (rule SKOL)
760 -- actual_ty: d:Eq b => b->b
761 -- expected_ty: forall a. Ord a => a->a
762 -- co_fn e /\a. \d2:Ord a. let d = eqFromOrd d2 in e
764 -- It is essential to do this *before* the specialisation case
765 -- Example: f :: (Eq a => a->a) -> ...
766 -- g :: Ord b => b->b
769 tc_sub1 orig act_sty act_ty exp_ib exp_sty exp_ty
770 | isSigmaTy exp_ty = do
771 { traceTc (text "tc_sub1 - case 2") ;
772 if exp_ib then -- SKOL does not apply if exp_ty is inside a box
773 defer_to_boxy_matching orig act_sty act_ty exp_ib exp_sty exp_ty
775 { (gen_fn, co_fn) <- tcGen exp_ty act_tvs Nothing $ \ _ body_exp_ty ->
776 tc_sub orig act_sty act_ty False body_exp_ty body_exp_ty
777 ; return (gen_fn <.> co_fn) }
780 act_tvs = tyVarsOfType act_ty
781 -- It's really important to check for escape wrt
782 -- the free vars of both expected_ty *and* actual_ty
784 -----------------------------------
785 -- Specialisation case (rule ASPEC):
786 -- actual_ty: forall a. Ord a => a->a
787 -- expected_ty: Int -> Int
788 -- co_fn e = e Int dOrdInt
790 tc_sub1 orig _ actual_ty exp_ib exp_sty expected_ty
791 -- Implements the new SPEC rule in the Appendix of the paper
792 -- "Boxy types: inference for higher rank types and impredicativity"
793 -- (This appendix isn't in the published version.)
794 -- The idea is to *first* do pre-subsumption, and then full subsumption
795 -- Example: forall a. a->a <= Int -> (forall b. Int)
796 -- Pre-subsumpion finds a|->Int, and that works fine, whereas
797 -- just running full subsumption would fail.
798 | isSigmaTy actual_ty
799 = do { traceTc (text "tc_sub1 - case 3")
800 ; -- Perform pre-subsumption, and instantiate
801 -- the type with info from the pre-subsumption;
802 -- boxy tyvars if pre-subsumption gives no info
803 let (tyvars, theta, tau) = tcSplitSigmaTy actual_ty
804 tau_tvs = exactTyVarsOfType tau
805 ; inst_tys <- if exp_ib then -- Inside a box, do not do clever stuff
806 do { tyvars' <- mapM tcInstBoxyTyVar tyvars
807 ; return (mkTyVarTys tyvars') }
808 else -- Outside, do clever stuff
809 preSubType tyvars tau_tvs tau expected_ty
810 ; let subst' = zipOpenTvSubst tyvars inst_tys
811 tau' = substTy subst' tau
813 -- Perform a full subsumption check
814 ; traceTc (text "tc_sub_spec" <+> vcat [ppr actual_ty,
815 ppr tyvars <+> ppr theta <+> ppr tau,
817 ; co_fn2 <- tc_sub orig tau' tau' exp_ib exp_sty expected_ty
819 -- Deal with the dictionaries
820 ; co_fn1 <- instCall orig inst_tys (substTheta subst' theta)
821 ; return (co_fn2 <.> co_fn1) }
823 -----------------------------------
824 -- Function case (rule F1)
825 tc_sub1 orig _ (FunTy act_arg act_res) exp_ib _ (FunTy exp_arg exp_res)
826 = do { traceTc (text "tc_sub1 - case 4")
827 ; tc_sub_funs orig act_arg act_res exp_ib exp_arg exp_res
830 -- Function case (rule F2)
831 tc_sub1 orig act_sty act_ty@(FunTy act_arg act_res) _ exp_sty (TyVarTy exp_tv)
833 = do { traceTc (text "tc_sub1 - case 5")
834 ; cts <- readMetaTyVar exp_tv
836 Indirect ty -> tc_sub orig act_sty act_ty True exp_sty ty
837 Flexi -> do { [arg_ty,res_ty] <- withMetaTvs exp_tv fun_kinds mk_res_ty
838 ; tc_sub_funs orig act_arg act_res True arg_ty res_ty } }
840 mk_res_ty [arg_ty', res_ty'] = mkFunTy arg_ty' res_ty'
841 mk_res_ty _ = panic "TcUnify.mk_res_ty3"
842 fun_kinds = [argTypeKind, openTypeKind]
844 -- Everything else: defer to boxy matching
845 tc_sub1 orig act_sty actual_ty exp_ib exp_sty expected_ty@(TyVarTy exp_tv)
846 = do { traceTc (text "tc_sub1 - case 6a" <+> ppr [isBoxyTyVar exp_tv, isMetaTyVar exp_tv, isSkolemTyVar exp_tv, isExistentialTyVar exp_tv,isSigTyVar exp_tv] )
847 ; defer_to_boxy_matching orig act_sty actual_ty exp_ib exp_sty expected_ty
850 tc_sub1 orig act_sty actual_ty exp_ib exp_sty expected_ty
851 = do { traceTc (text "tc_sub1 - case 6")
852 ; defer_to_boxy_matching orig act_sty actual_ty exp_ib exp_sty expected_ty
855 -----------------------------------
856 defer_to_boxy_matching :: InstOrigin -> TcType -> TcType -> InBox
857 -> TcType -> TcType -> TcM HsWrapper
858 defer_to_boxy_matching orig act_sty actual_ty exp_ib exp_sty expected_ty
859 = do { coi <- addSubCtxt orig act_sty exp_sty $
860 u_tys (Unify True act_sty exp_sty)
861 False act_sty actual_ty exp_ib exp_sty expected_ty
862 ; return $ coiToHsWrapper coi }
864 -----------------------------------
865 tc_sub_funs :: InstOrigin -> TcType -> BoxySigmaType -> InBox
866 -> TcType -> BoxySigmaType -> TcM HsWrapper
867 tc_sub_funs orig act_arg act_res exp_ib exp_arg exp_res
868 = do { arg_coi <- addSubCtxt orig act_arg exp_arg $
869 uTysOuter False act_arg exp_ib exp_arg
870 ; co_fn_res <- tc_sub orig act_res act_res exp_ib exp_res exp_res
871 ; wrapper1 <- wrapFunResCoercion [exp_arg] co_fn_res
872 ; let wrapper2 = case arg_coi of
874 ACo co -> WpCast $ FunTy co act_res
875 ; return (wrapper1 <.> wrapper2) }
877 -----------------------------------
879 :: [TcType] -- Type of args
880 -> HsWrapper -- HsExpr a -> HsExpr b
881 -> TcM HsWrapper -- HsExpr (arg_tys -> a) -> HsExpr (arg_tys -> b)
882 wrapFunResCoercion arg_tys co_fn_res
883 | isIdHsWrapper co_fn_res
888 = do { arg_ids <- newSysLocalIds (fsLit "sub") arg_tys
889 ; return (mkWpLams arg_ids <.> co_fn_res <.> mkWpApps arg_ids) }
894 %************************************************************************
896 \subsection{Generalisation}
898 %************************************************************************
901 tcGen :: BoxySigmaType -- expected_ty
902 -> TcTyVarSet -- Extra tyvars that the universally
903 -- quantified tyvars of expected_ty
904 -- must not be unified
905 -> Maybe UserTypeCtxt -- Just ctxt => this polytype arose directly
906 -- from a user type sig
907 -- Nothing => a higher order situation
908 -> ([TcTyVar] -> BoxyRhoType -> TcM result)
909 -> TcM (HsWrapper, result)
910 -- The expression has type: spec_ty -> expected_ty
912 tcGen expected_ty extra_tvs mb_ctxt thing_inside -- We expect expected_ty to be a forall-type
913 -- If not, the call is a no-op
914 = do { traceTc (text "tcGen")
915 ; ((tvs', theta', rho'), skol_info) <- instantiate expected_ty
918 traceTc (text "tcGen" <+> vcat [
919 text "extra_tvs" <+> ppr extra_tvs,
920 text "expected_ty" <+> ppr expected_ty,
921 text "inst ty" <+> ppr tvs' <+> ppr theta'
923 text "free_tvs" <+> ppr free_tvs])
925 -- Type-check the arg and unify with poly type
926 ; (result, lie) <- getLIE $
927 thing_inside tvs' rho'
929 -- Check that the "forall_tvs" havn't been constrained
930 -- The interesting bit here is that we must include the free variables
931 -- of the expected_ty. Here's an example:
932 -- runST (newVar True)
933 -- Here, if we don't make a check, we'll get a type (ST s (MutVar s Bool))
934 -- for (newVar True), with s fresh. Then we unify with the runST's arg type
935 -- forall s'. ST s' a. That unifies s' with s, and a with MutVar s Bool.
936 -- So now s' isn't unconstrained because it's linked to a.
937 -- Conclusion: include the free vars of the expected_ty in the
938 -- list of "free vars" for the signature check.
940 ; loc <- getInstLoc (SigOrigin skol_info)
941 ; dicts <- newDictBndrs loc theta' -- Includes equalities
942 ; inst_binds <- tcSimplifyCheck loc tvs' dicts lie
944 ; checkSigTyVarsWrt free_tvs tvs'
945 ; traceTc (text "tcGen:done")
948 -- The WpLet binds any Insts which came out of the simplification.
949 dict_vars = map instToVar dicts
950 co_fn = mkWpTyLams tvs' <.> mkWpLams dict_vars <.> WpLet inst_binds
951 ; return (co_fn, result) }
953 free_tvs = tyVarsOfType expected_ty `unionVarSet` extra_tvs
955 instantiate :: TcType -> TcM (([TcTyVar],ThetaType,TcRhoType), SkolemInfo)
956 instantiate expected_ty
957 | Just ctxt <- mb_ctxt -- This case split is the wohle reason for mb_ctxt
958 = do { let skol_info = SigSkol ctxt
959 ; stuff <- tcInstSigType True skol_info expected_ty
960 ; return (stuff, skol_info) }
962 | otherwise -- We want the GenSkol info in the skolemised type variables to
963 -- mention the *instantiated* tyvar names, so that we get a
964 -- good error message "Rigid variable 'a' is bound by (forall a. a->a)"
965 -- Hence the tiresome but innocuous fixM
966 = fixM $ \ ~(_, skol_info) ->
967 do { stuff@(forall_tvs, theta, rho_ty) <- tcInstSkolType skol_info expected_ty
968 -- Get loation from *monad*, not from expected_ty
969 ; let skol_info = GenSkol forall_tvs (mkPhiTy theta rho_ty)
970 ; return (stuff, skol_info) }
975 %************************************************************************
979 %************************************************************************
981 The exported functions are all defined as versions of some
982 non-exported generic functions.
985 boxyUnify :: BoxyType -> BoxyType -> TcM CoercionI
986 -- Acutal and expected, respectively
987 boxyUnify ty1 ty2 = addErrCtxtM (unifyCtxt ty1 ty2) $
988 uTysOuter False ty1 False ty2
991 boxyUnifyList :: [BoxyType] -> [BoxyType] -> TcM [CoercionI]
992 -- Arguments should have equal length
993 -- Acutal and expected types
994 boxyUnifyList tys1 tys2 = uList boxyUnify tys1 tys2
997 unifyType :: TcTauType -> TcTauType -> TcM CoercionI
998 -- No boxes expected inside these types
999 -- Acutal and expected types
1000 unifyType ty1 ty2 -- ty1 expected, ty2 inferred
1001 = ASSERT2( not (isBoxyTy ty1), ppr ty1 )
1002 ASSERT2( not (isBoxyTy ty2), ppr ty2 )
1003 addErrCtxtM (unifyCtxt ty1 ty2) $
1004 uTysOuter True ty1 True ty2
1007 unifyPred :: PredType -> PredType -> TcM CoercionI
1008 -- Acutal and expected types
1009 unifyPred p1 p2 = uPred (Unify False (mkPredTy p1) (mkPredTy p2)) True p1 True p2
1011 unifyTheta :: TcThetaType -> TcThetaType -> TcM [CoercionI]
1012 -- Acutal and expected types
1013 unifyTheta theta1 theta2
1014 = do { checkTc (equalLength theta1 theta2)
1015 (vcat [ptext (sLit "Contexts differ in length"),
1016 nest 2 $ parens $ ptext (sLit "Use -XRelaxedPolyRec to allow this")])
1017 ; uList unifyPred theta1 theta2
1021 uList :: (a -> a -> TcM b)
1022 -> [a] -> [a] -> TcM [b]
1023 -- Unify corresponding elements of two lists of types, which
1024 -- should be of equal length. We charge down the list explicitly so that
1025 -- we can complain if their lengths differ.
1026 uList _ [] [] = return []
1027 uList unify (ty1:tys1) (ty2:tys2) = do { x <- unify ty1 ty2;
1028 ; xs <- uList unify tys1 tys2
1031 uList _ _ _ = panic "Unify.uList: mismatched type lists!"
1034 @unifyTypeList@ takes a single list of @TauType@s and unifies them
1035 all together. It is used, for example, when typechecking explicit
1036 lists, when all the elts should be of the same type.
1039 unifyTypeList :: [TcTauType] -> TcM ()
1040 unifyTypeList [] = return ()
1041 unifyTypeList [_] = return ()
1042 unifyTypeList (ty1:tys@(ty2:_)) = do { unifyType ty1 ty2
1043 ; unifyTypeList tys }
1046 %************************************************************************
1048 \subsection[Unify-uTys]{@uTys@: getting down to business}
1050 %************************************************************************
1052 @uTys@ is the heart of the unifier. Each arg occurs twice, because
1053 we want to report errors in terms of synomyms if possible. The first of
1054 the pair is used in error messages only; it is always the same as the
1055 second, except that if the first is a synonym then the second may be a
1056 de-synonym'd version. This way we get better error messages.
1058 We call the first one \tr{ps_ty1}, \tr{ps_ty2} for ``possible synomym''.
1061 type SwapFlag = Bool
1062 -- False <=> the two args are (actual, expected) respectively
1063 -- True <=> the two args are (expected, actual) respectively
1065 type InBox = Bool -- True <=> we are inside a box
1066 -- False <=> we are outside a box
1067 -- The importance of this is that if we get "filled-box meets
1068 -- filled-box", we'll look into the boxes and unify... but
1069 -- we must not allow polytypes. But if we are in a box on
1070 -- just one side, then we can allow polytypes
1072 data Outer = Unify Bool TcType TcType
1073 -- If there is a unification error, report these types as mis-matching
1074 -- Bool = True <=> the context says "Expected = ty1, Acutal = ty2"
1075 -- for this particular ty1,ty2
1077 instance Outputable Outer where
1078 ppr (Unify c ty1 ty2) = pp_c <+> pprParendType ty1 <+> ptext (sLit "~")
1079 <+> pprParendType ty2
1081 pp_c = if c then ptext (sLit "Top") else ptext (sLit "NonTop")
1084 -------------------------
1085 uTysOuter :: InBox -> TcType -- ty1 is the *actual* type
1086 -> InBox -> TcType -- ty2 is the *expected* type
1088 -- We've just pushed a context describing ty1,ty2
1089 uTysOuter nb1 ty1 nb2 ty2
1090 = do { traceTc (text "uTysOuter" <+> ppr ty1 <+> ppr ty2)
1091 ; u_tys (Unify True ty1 ty2) nb1 ty1 ty1 nb2 ty2 ty2 }
1093 uTys :: InBox -> TcType -> InBox -> TcType -> TcM CoercionI
1094 -- The context does not describe ty1,ty2
1095 uTys nb1 ty1 nb2 ty2
1096 = do { traceTc (text "uTys" <+> ppr ty1 <+> ppr ty2)
1097 ; u_tys (Unify False ty1 ty2) nb1 ty1 ty1 nb2 ty2 ty2 }
1101 uTys_s :: InBox -> [TcType] -- tys1 are the *actual* types
1102 -> InBox -> [TcType] -- tys2 are the *expected* types
1104 uTys_s _ [] _ [] = return []
1105 uTys_s nb1 (ty1:tys1) nb2 (ty2:tys2) = do { coi <- uTys nb1 ty1 nb2 ty2
1106 ; cois <- uTys_s nb1 tys1 nb2 tys2
1107 ; return (coi:cois) }
1108 uTys_s _ _ _ _ = panic "Unify.uTys_s: mismatched type lists!"
1112 -> InBox -> TcType -> TcType -- ty1 is the *actual* type
1113 -> InBox -> TcType -> TcType -- ty2 is the *expected* type
1116 u_tys outer nb1 orig_ty1 ty1 nb2 orig_ty2 ty2
1117 = do { traceTc (text "u_tys " <+> vcat [sep [ braces (ppr orig_ty1 <+> text "/" <+> ppr ty1),
1119 braces (ppr orig_ty2 <+> text "/" <+> ppr ty2)],
1121 ; coi <- go outer orig_ty1 ty1 orig_ty2 ty2
1122 ; traceTc (case coi of
1123 ACo co -> text "u_tys yields coercion:" <+> ppr co
1124 IdCo -> text "u_tys yields no coercion")
1128 bale_out :: Outer -> TcM a
1129 bale_out outer = unifyMisMatch outer
1130 -- We report a mis-match in terms of the original arugments to
1131 -- u_tys, even though 'go' has recursed inwards somewhat
1133 -- Note [Unifying AppTy]
1134 -- A case in point is unifying (m Int) ~ (IO Int)
1135 -- where m is a unification variable that is now bound to (say) (Bool ->)
1136 -- Then we want to report "Can't unify (Bool -> Int) with (IO Int)
1137 -- and not "Can't unify ((->) Bool) with IO"
1139 go :: Outer -> TcType -> TcType -> TcType -> TcType -> TcM CoercionI
1140 -- Always expand synonyms: see Note [Unification and synonyms]
1141 -- (this also throws away FTVs)
1142 go _ sty1 ty1 sty2 ty2
1143 | Just ty1' <- tcView ty1 = go (Unify False ty1' ty2 ) sty1 ty1' sty2 ty2
1144 | Just ty2' <- tcView ty2 = go (Unify False ty1 ty2') sty1 ty1 sty2 ty2'
1146 -- Variables; go for uVar
1147 go outer _ (TyVarTy tyvar1) sty2 ty2 = uVar outer False tyvar1 nb2 sty2 ty2
1148 go outer sty1 ty1 _ (TyVarTy tyvar2) = uVar outer True tyvar2 nb1 sty1 ty1
1149 -- "True" means args swapped
1151 -- The case for sigma-types must *follow* the variable cases
1152 -- because a boxy variable can be filed with a polytype;
1153 -- but must precede FunTy, because ((?x::Int) => ty) look
1154 -- like a FunTy; there isn't necy a forall at the top
1156 | isSigmaTy ty1 || isSigmaTy ty2
1157 = do { traceTc (text "We have sigma types: equalLength" <+> ppr tvs1 <+> ppr tvs2)
1158 ; unless (equalLength tvs1 tvs2) (bale_out outer)
1159 ; traceTc (text "We're past the first length test")
1160 ; tvs <- tcInstSkolTyVars UnkSkol tvs1 -- Not a helpful SkolemInfo
1161 -- Get location from monad, not from tvs1
1162 ; let tys = mkTyVarTys tvs
1163 in_scope = mkInScopeSet (mkVarSet tvs)
1164 phi1 = substTy (mkTvSubst in_scope (zipTyEnv tvs1 tys)) body1
1165 phi2 = substTy (mkTvSubst in_scope (zipTyEnv tvs2 tys)) body2
1166 (theta1,tau1) = tcSplitPhiTy phi1
1167 (theta2,tau2) = tcSplitPhiTy phi2
1169 ; addErrCtxtM (unifyForAllCtxt tvs phi1 phi2) $ do
1170 { unless (equalLength theta1 theta2) (bale_out outer)
1171 ; _cois <- uPreds outer nb1 theta1 nb2 theta2 -- TOMDO: do something with these pred_cois
1172 ; traceTc (text "TOMDO!")
1173 ; coi <- uTys nb1 tau1 nb2 tau2
1175 -- Check for escape; e.g. (forall a. a->b) ~ (forall a. a->a)
1176 ; free_tvs <- zonkTcTyVarsAndFV (varSetElems (tyVarsOfType ty1 `unionVarSet` tyVarsOfType ty2))
1177 ; when (any (`elemVarSet` free_tvs) tvs)
1178 (bleatEscapedTvs free_tvs tvs tvs)
1180 -- If both sides are inside a box, we are in a "box-meets-box"
1181 -- situation, and we should not have a polytype at all.
1182 -- If we get here we have two boxes, already filled with
1183 -- the same polytype... but it should be a monotype.
1184 -- This check comes last, because the error message is
1185 -- extremely unhelpful.
1186 ; when (nb1 && nb2) (notMonoType ty1)
1190 (tvs1, body1) = tcSplitForAllTys ty1
1191 (tvs2, body2) = tcSplitForAllTys ty2
1194 go outer _ (PredTy p1) _ (PredTy p2)
1195 = uPred outer nb1 p1 nb2 p2
1197 -- Non-synonym type constructors must match
1198 go _ _ (TyConApp con1 tys1) _ (TyConApp con2 tys2)
1199 | con1 == con2 && not (isOpenSynTyCon con1)
1200 = do { cois <- uTys_s nb1 tys1 nb2 tys2
1201 ; return $ mkTyConAppCoI con1 tys1 cois
1203 -- Family synonyms See Note [TyCon app]
1204 | con1 == con2 && identicalOpenSynTyConApp
1205 = do { cois <- uTys_s nb1 tys1' nb2 tys2'
1206 ; return $ mkTyConAppCoI con1 tys1 (replicate n IdCo ++ cois)
1210 (idxTys1, tys1') = splitAt n tys1
1211 (idxTys2, tys2') = splitAt n tys2
1212 identicalOpenSynTyConApp = idxTys1 `tcEqTypes` idxTys2
1213 -- See Note [OpenSynTyCon app]
1215 -- If we can reduce a family app => proceed with reduct
1216 -- NB: We use isOpenSynTyCon, not isOpenSynTyConApp as we also must
1217 -- defer oversaturated applications!
1218 go outer sty1 ty1@(TyConApp con1 _) sty2 ty2
1219 | isOpenSynTyCon con1
1220 = do { (coi1, ty1') <- tcNormaliseFamInst ty1
1222 IdCo -> defer -- no reduction, see [Deferred Unification]
1223 _ -> liftM (coi1 `mkTransCoI`) $ go outer sty1 ty1' sty2 ty2
1226 -- If we can reduce a family app => proceed with reduct
1227 -- NB: We use isOpenSynTyCon, not isOpenSynTyConApp as we also must
1228 -- defer oversaturated applications!
1229 go outer sty1 ty1 sty2 ty2@(TyConApp con2 _)
1230 | isOpenSynTyCon con2
1231 = do { (coi2, ty2') <- tcNormaliseFamInst ty2
1233 IdCo -> defer -- no reduction, see [Deferred Unification]
1234 _ -> liftM (`mkTransCoI` mkSymCoI coi2) $
1235 go outer sty1 ty1 sty2 ty2'
1238 -- Functions; just check the two parts
1239 go _ _ (FunTy fun1 arg1) _ (FunTy fun2 arg2)
1240 = do { coi_l <- uTys nb1 fun1 nb2 fun2
1241 ; coi_r <- uTys nb1 arg1 nb2 arg2
1242 ; return $ mkFunTyCoI fun1 coi_l arg1 coi_r
1245 -- Applications need a bit of care!
1246 -- They can match FunTy and TyConApp, so use splitAppTy_maybe
1247 -- NB: we've already dealt with type variables and Notes,
1248 -- so if one type is an App the other one jolly well better be too
1249 go outer _ (AppTy s1 t1) _ ty2
1250 | Just (s2,t2) <- tcSplitAppTy_maybe ty2
1251 = do { coi_s <- go outer s1 s1 s2 s2 -- NB recurse into go
1252 ; coi_t <- uTys nb1 t1 nb2 t2 -- See Note [Unifying AppTy]
1253 ; return $ mkAppTyCoI s1 coi_s t1 coi_t }
1255 -- Now the same, but the other way round
1256 -- Don't swap the types, because the error messages get worse
1257 go outer _ ty1 _ (AppTy s2 t2)
1258 | Just (s1,t1) <- tcSplitAppTy_maybe ty1
1259 = do { coi_s <- go outer s1 s1 s2 s2
1260 ; coi_t <- uTys nb1 t1 nb2 t2
1261 ; return $ mkAppTyCoI s1 coi_s t1 coi_t }
1263 -- Anything else fails
1264 go outer _ _ _ _ = bale_out outer
1266 defer = defer_unification outer False orig_ty1 orig_ty2
1270 uPred :: Outer -> InBox -> PredType -> InBox -> PredType -> TcM CoercionI
1271 uPred _ nb1 (IParam n1 t1) nb2 (IParam n2 t2)
1273 do { coi <- uTys nb1 t1 nb2 t2
1274 ; return $ mkIParamPredCoI n1 coi
1276 uPred _ nb1 (ClassP c1 tys1) nb2 (ClassP c2 tys2)
1278 do { cois <- uTys_s nb1 tys1 nb2 tys2 -- Guaranteed equal lengths because the kinds check
1279 ; return $ mkClassPPredCoI c1 tys1 cois
1281 uPred outer _ _ _ _ = unifyMisMatch outer
1283 uPreds :: Outer -> InBox -> [PredType] -> InBox -> [PredType]
1285 uPreds _ _ [] _ [] = return []
1286 uPreds outer nb1 (p1:ps1) nb2 (p2:ps2) =
1287 do { coi <- uPred outer nb1 p1 nb2 p2
1288 ; cois <- uPreds outer nb1 ps1 nb2 ps2
1291 uPreds _ _ _ _ _ = panic "uPreds"
1296 When we find two TyConApps, the argument lists are guaranteed equal
1297 length. Reason: intially the kinds of the two types to be unified is
1298 the same. The only way it can become not the same is when unifying two
1299 AppTys (f1 a1)~(f2 a2). In that case there can't be a TyConApp in
1300 the f1,f2 (because it'd absorb the app). If we unify f1~f2 first,
1301 which we do, that ensures that f1,f2 have the same kind; and that
1302 means a1,a2 have the same kind. And now the argument repeats.
1304 Note [OpenSynTyCon app]
1305 ~~~~~~~~~~~~~~~~~~~~~~~
1308 type family T a :: * -> *
1310 the two types (T () a) and (T () Int) must unify, even if there are
1311 no type instances for T at all. Should we just turn them into an
1312 equality (T () a ~ T () Int)? I don't think so. We currently try to
1313 eagerly unify everything we can before generating equalities; otherwise,
1314 we could turn the unification of [Int] with [a] into an equality, too.
1316 Note [Unification and synonyms]
1317 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1318 If you are tempted to make a short cut on synonyms, as in this
1322 -- NO uTys (SynTy con1 args1 ty1) (SynTy con2 args2 ty2)
1323 -- NO = if (con1 == con2) then
1324 -- NO -- Good news! Same synonym constructors, so we can shortcut
1325 -- NO -- by unifying their arguments and ignoring their expansions.
1326 -- NO unifyTypepeLists args1 args2
1328 -- NO -- Never mind. Just expand them and try again
1332 then THINK AGAIN. Here is the whole story, as detected and reported
1333 by Chris Okasaki \tr{<Chris_Okasaki@loch.mess.cs.cmu.edu>}:
1335 Here's a test program that should detect the problem:
1339 x = (1 :: Bogus Char) :: Bogus Bool
1342 The problem with [the attempted shortcut code] is that
1346 is not a sufficient condition to be able to use the shortcut!
1347 You also need to know that the type synonym actually USES all
1348 its arguments. For example, consider the following type synonym
1349 which does not use all its arguments.
1354 If you ever tried unifying, say, \tr{Bogus Char} with \tr{Bogus Bool},
1355 the unifier would blithely try to unify \tr{Char} with \tr{Bool} and
1356 would fail, even though the expanded forms (both \tr{Int}) should
1359 Similarly, unifying \tr{Bogus Char} with \tr{Bogus t} would
1360 unnecessarily bind \tr{t} to \tr{Char}.
1362 ... You could explicitly test for the problem synonyms and mark them
1363 somehow as needing expansion, perhaps also issuing a warning to the
1368 %************************************************************************
1370 \subsection[Unify-uVar]{@uVar@: unifying with a type variable}
1372 %************************************************************************
1374 @uVar@ is called when at least one of the types being unified is a
1375 variable. It does {\em not} assume that the variable is a fixed point
1376 of the substitution; rather, notice that @uVar@ (defined below) nips
1377 back into @uTys@ if it turns out that the variable is already bound.
1381 -> SwapFlag -- False => tyvar is the "actual" (ty is "expected")
1382 -- True => ty is the "actual" (tyvar is "expected")
1384 -> InBox -- True <=> definitely no boxes in t2
1385 -> TcTauType -> TcTauType -- printing and real versions
1388 uVar outer swapped tv1 nb2 ps_ty2 ty2
1389 = do { let expansion | showSDoc (ppr ty2) == showSDoc (ppr ps_ty2) = empty
1390 | otherwise = brackets (equals <+> ppr ty2)
1391 ; traceTc (text "uVar" <+> ppr outer <+> ppr swapped <+>
1392 sep [ppr tv1 <+> dcolon <+> ppr (tyVarKind tv1 ),
1393 nest 2 (ptext (sLit " <-> ")),
1394 ppr ps_ty2 <+> dcolon <+> ppr (typeKind ty2) <+> expansion])
1395 ; details <- lookupTcTyVar tv1
1398 | swapped -> u_tys outer nb2 ps_ty2 ty2 True ty1 ty1 -- Swap back
1399 | otherwise -> u_tys outer True ty1 ty1 nb2 ps_ty2 ty2 -- Same order
1400 -- The 'True' here says that ty1 is now inside a box
1401 DoneTv details1 -> uUnfilledVar outer swapped tv1 details1 ps_ty2 ty2
1405 uUnfilledVar :: Outer
1407 -> TcTyVar -> TcTyVarDetails -- Tyvar 1
1408 -> TcTauType -> TcTauType -- Type 2
1410 -- Invariant: tyvar 1 is not unified with anything
1412 uUnfilledVar _ swapped tv1 details1 ps_ty2 ty2
1413 | Just ty2' <- tcView ty2
1414 = -- Expand synonyms; ignore FTVs
1415 let outer' | swapped = Unify False ty2' (mkTyVarTy tv1)
1416 | otherwise = Unify False (mkTyVarTy tv1) ty2'
1417 in uUnfilledVar outer' swapped tv1 details1 ps_ty2 ty2'
1419 uUnfilledVar outer swapped tv1 details1 _ (TyVarTy tv2)
1420 | tv1 == tv2 -- Same type variable => no-op (but watch out for the boxy case)
1422 MetaTv BoxTv ref1 -- A boxy type variable meets itself;
1423 -- this is box-meets-box, so fill in with a tau-type
1424 -> do { tau_tv <- tcInstTyVar tv1
1425 ; updateMeta tv1 ref1 (mkTyVarTy tau_tv)
1428 _ -> return IdCo -- No-op
1430 | otherwise -- Distinct type variables
1431 = do { lookup2 <- lookupTcTyVar tv2
1433 IndirectTv ty2' -> uUnfilledVar outer swapped tv1 details1 ty2' ty2'
1434 DoneTv details2 -> uUnfilledVars outer swapped tv1 details1 tv2 details2
1437 uUnfilledVar outer swapped tv1 details1 ps_ty2 non_var_ty2
1438 = -- ty2 is not a type variable
1440 MetaTv (SigTv _) _ -> rigid_variable
1441 MetaTv info ref1 -> uMetaVar outer swapped tv1 info ref1 ps_ty2 non_var_ty2
1442 SkolemTv _ -> rigid_variable
1445 | isOpenSynTyConApp non_var_ty2
1446 = -- 'non_var_ty2's outermost constructor is a type family,
1447 -- which we may may be able to normalise
1448 do { (coi2, ty2') <- tcNormaliseFamInst non_var_ty2
1450 IdCo -> -- no progress, but maybe after other instantiations
1451 defer_unification outer swapped (TyVarTy tv1) ps_ty2
1452 ACo co -> -- progress: so lets try again
1454 ppr co <+> text "::"<+> ppr non_var_ty2 <+> text "~" <+>
1456 ; coi <- uUnfilledVar outer swapped tv1 details1 ps_ty2 ty2'
1457 ; let coi2' = (if swapped then id else mkSymCoI) coi2
1458 ; return $ coi2' `mkTransCoI` coi
1461 | SkolemTv RuntimeUnkSkol <- details1
1462 -- runtime unknown will never match
1463 = unifyMisMatch outer
1464 | otherwise -- defer as a given equality may still resolve this
1465 = defer_unification outer swapped (TyVarTy tv1) ps_ty2
1468 Note [Deferred Unification]
1469 ~~~~~~~~~~~~~~~~~~~~
1470 We may encounter a unification ty1 = ty2 that cannot be performed syntactically,
1471 and yet its consistency is undetermined. Previously, there was no way to still
1472 make it consistent. So a mismatch error was issued.
1474 Now these unfications are deferred until constraint simplification, where type
1475 family instances and given equations may (or may not) establish the consistency.
1476 Deferred unifications are of the form
1479 where F is a type function and x is a type variable.
1481 id :: x ~ y => x -> y
1484 involves the unfication x = y. It is deferred until we bring into account the
1485 context x ~ y to establish that it holds.
1487 If available, we defer original types (rather than those where closed type
1488 synonyms have already been expanded via tcCoreView). This is, as usual, to
1489 improve error messages.
1491 We need to both 'unBox' and zonk deferred types. We need to unBox as
1492 functions, such as TcExpr.tcMonoExpr promise to fill boxes in the expected
1493 type. We need to zonk as the types go into the kind of the coercion variable
1494 `cotv' and those are not zonked in Inst.zonkInst. (Maybe it would be better
1495 to zonk in zonInst instead. Would that be sufficient?)
1498 defer_unification :: Outer
1503 defer_unification outer True ty1 ty2
1504 = defer_unification outer False ty2 ty1
1505 defer_unification outer False ty1 ty2
1506 = do { ty1' <- unBox ty1 >>= zonkTcType -- unbox *and* zonk..
1507 ; ty2' <- unBox ty2 >>= zonkTcType -- ..see preceding note
1508 ; traceTc $ text "deferring:" <+> ppr ty1 <+> text "~" <+> ppr ty2
1509 ; cotv <- newMetaCoVar ty1' ty2'
1510 -- put ty1 ~ ty2 in LIE
1511 -- Left means "wanted"
1512 ; inst <- popUnifyCtxt outer $
1513 mkEqInst (EqPred ty1' ty2') (Left cotv)
1515 ; return $ ACo $ TyVarTy cotv }
1520 -> TcTyVar -> BoxInfo -> IORef MetaDetails
1523 -- tv1 is an un-filled-in meta type variable (maybe boxy, maybe tau)
1524 -- ty2 is not a type variable
1526 uMetaVar outer swapped tv1 BoxTv ref1 ps_ty2 ty2
1527 = -- tv1 is a BoxTv. So we must unbox ty2, to ensure
1528 -- that any boxes in ty2 are filled with monotypes
1530 -- It should not be the case that tv1 occurs in ty2
1531 -- (i.e. no occurs check should be needed), but if perchance
1532 -- it does, the unbox operation will fill it, and the debug code
1534 do { final_ty <- unBox ps_ty2
1535 ; meta_details <- readMutVar ref1
1536 ; case meta_details of
1537 Indirect _ -> -- This *can* happen due to an occurs check,
1538 -- just as it can in checkTauTvUpdate in the next
1539 -- equation of uMetaVar; see Trac #2414
1540 -- Note [Occurs check]
1541 -- Go round again. Probably there's an immediate
1542 -- error, but maybe not (a type function might discard
1543 -- its argument). Next time round we'll end up in the
1544 -- TauTv case of uMetaVar.
1545 uVar outer swapped tv1 False ps_ty2 ty2
1546 -- Setting for nb2::InBox is irrelevant
1548 Flexi -> do { checkUpdateMeta swapped tv1 ref1 final_ty
1552 uMetaVar outer swapped tv1 _ ref1 ps_ty2 _
1553 = do { -- Occurs check + monotype check
1554 ; mb_final_ty <- checkTauTvUpdate tv1 ps_ty2
1555 ; case mb_final_ty of
1556 Nothing -> -- tv1 occured in type family parameter
1557 defer_unification outer swapped (mkTyVarTy tv1) ps_ty2
1559 do { checkUpdateMeta swapped tv1 ref1 final_ty
1564 {- Note [Occurs check]
1566 An eager occurs check is made in checkTauTvUpdate, deferring tricky
1567 cases by calling defer_unification (see notes with
1568 checkTauTvUpdate). An occurs check can also (and does) happen in the
1569 BoxTv case, but unBox doesn't check for occurrences, and in any case
1570 doesn't have the type-function-related complexity that
1571 checkTauTvUpdate has. So we content ourselves with spotting the potential
1572 occur check (by the fact that tv1 is now filled), and going round again.
1573 Next time round we'll get the TauTv case of uMetaVar.
1577 uUnfilledVars :: Outer
1579 -> TcTyVar -> TcTyVarDetails -- Tyvar 1
1580 -> TcTyVar -> TcTyVarDetails -- Tyvar 2
1582 -- Invarant: The type variables are distinct,
1583 -- Neither is filled in yet
1584 -- They might be boxy or not
1586 uUnfilledVars outer swapped tv1 (SkolemTv _) tv2 (SkolemTv _)
1587 = -- see [Deferred Unification]
1588 defer_unification outer swapped (mkTyVarTy tv1) (mkTyVarTy tv2)
1590 uUnfilledVars _ swapped tv1 (MetaTv _ ref1) tv2 (SkolemTv _)
1591 = checkUpdateMeta swapped tv1 ref1 (mkTyVarTy tv2) >> return IdCo
1592 uUnfilledVars _ swapped tv1 (SkolemTv _) tv2 (MetaTv _ ref2)
1593 = checkUpdateMeta (not swapped) tv2 ref2 (mkTyVarTy tv1) >> return IdCo
1595 -- ToDo: this function seems too long for what it acutally does!
1596 uUnfilledVars _ swapped tv1 (MetaTv info1 ref1) tv2 (MetaTv info2 ref2)
1597 = case (info1, info2) of
1598 (BoxTv, BoxTv) -> box_meets_box >> return IdCo
1600 -- If a box meets a TauTv, but the fomer has the smaller kind
1601 -- then we must create a fresh TauTv with the smaller kind
1602 (_, BoxTv) | k1_sub_k2 -> update_tv2 >> return IdCo
1603 | otherwise -> box_meets_box >> return IdCo
1604 (BoxTv, _ ) | k2_sub_k1 -> update_tv1 >> return IdCo
1605 | otherwise -> box_meets_box >> return IdCo
1607 -- Avoid SigTvs if poss
1608 (SigTv _, _ ) | k1_sub_k2 -> update_tv2 >> return IdCo
1609 (_, SigTv _) | k2_sub_k1 -> update_tv1 >> return IdCo
1611 (_, _) | k1_sub_k2 -> if k2_sub_k1 && nicer_to_update_tv1
1612 then update_tv1 >> return IdCo -- Same kinds
1613 else update_tv2 >> return IdCo
1614 | k2_sub_k1 -> update_tv1 >> return IdCo
1615 | otherwise -> kind_err >> return IdCo
1617 -- Update the variable with least kind info
1618 -- See notes on type inference in Kind.lhs
1619 -- The "nicer to" part only applies if the two kinds are the same,
1620 -- so we can choose which to do.
1622 -- Kinds should be guaranteed ok at this point
1623 update_tv1 = updateMeta tv1 ref1 (mkTyVarTy tv2)
1624 update_tv2 = updateMeta tv2 ref2 (mkTyVarTy tv1)
1626 box_meets_box | k1_sub_k2 = if k2_sub_k1 && nicer_to_update_tv1
1629 | k2_sub_k1 = fill_from tv2
1630 | otherwise = kind_err
1632 -- Update *both* tyvars with a TauTv whose name and kind
1633 -- are gotten from tv (avoid losing nice names is poss)
1634 fill_from tv = do { tv' <- tcInstTyVar tv
1635 ; let tau_ty = mkTyVarTy tv'
1636 ; updateMeta tv1 ref1 tau_ty
1637 ; updateMeta tv2 ref2 tau_ty }
1639 kind_err = addErrCtxtM (unifyKindCtxt swapped tv1 (mkTyVarTy tv2)) $
1640 unifyKindMisMatch k1 k2
1644 k1_sub_k2 = k1 `isSubKind` k2
1645 k2_sub_k1 = k2 `isSubKind` k1
1647 nicer_to_update_tv1 = isSystemName (Var.varName tv1)
1648 -- Try to update sys-y type variables in preference to ones
1649 -- gotten (say) by instantiating a polymorphic function with
1650 -- a user-written type sig
1654 refineBox :: TcType -> TcM TcType
1655 -- Unbox the outer box of a boxy type (if any)
1656 refineBox ty@(TyVarTy box_tv)
1657 | isMetaTyVar box_tv
1658 = do { cts <- readMetaTyVar box_tv
1661 Indirect ty -> return ty }
1662 refineBox other_ty = return other_ty
1664 refineBoxToTau :: TcType -> TcM TcType
1665 -- Unbox the outer box of a boxy type, filling with a monotype if it is empty
1666 -- Like refineBox except for the "fill with monotype" part.
1667 refineBoxToTau (TyVarTy box_tv)
1668 | isMetaTyVar box_tv
1669 , MetaTv BoxTv ref <- tcTyVarDetails box_tv
1670 = do { cts <- readMutVar ref
1672 Flexi -> fillBoxWithTau box_tv ref
1673 Indirect ty -> return ty }
1674 refineBoxToTau other_ty = return other_ty
1676 zapToMonotype :: BoxySigmaType -> TcM TcTauType
1677 -- Subtle... we must zap the boxy res_ty
1678 -- to kind * before using it to instantiate a LitInst
1679 -- Calling unBox instead doesn't do the job, because the box
1680 -- often has an openTypeKind, and we don't want to instantiate
1682 zapToMonotype res_ty
1683 = do { res_tau <- newFlexiTyVarTy liftedTypeKind
1684 ; boxyUnify res_tau res_ty
1687 unBox :: BoxyType -> TcM TcType
1688 -- unBox implements the judgement
1690 -- with input s', and result s
1692 -- It removes all boxes from the input type, returning a non-boxy type.
1693 -- A filled box in the type can only contain a monotype; unBox fails if not
1694 -- The type can have empty boxes, which unBox fills with a monotype
1696 -- Compare this wth checkTauTvUpdate
1698 -- For once, it's safe to treat synonyms as opaque!
1700 unBox (TyConApp tc tys) = do { tys' <- mapM unBox tys; return (TyConApp tc tys') }
1701 unBox (AppTy f a) = do { f' <- unBox f; a' <- unBox a; return (mkAppTy f' a') }
1702 unBox (FunTy f a) = do { f' <- unBox f; a' <- unBox a; return (FunTy f' a') }
1703 unBox (PredTy p) = do { p' <- unBoxPred p; return (PredTy p') }
1704 unBox (ForAllTy tv ty) = ASSERT( isImmutableTyVar tv )
1705 do { ty' <- unBox ty; return (ForAllTy tv ty') }
1707 | isTcTyVar tv -- It's a boxy type variable
1708 , MetaTv BoxTv ref <- tcTyVarDetails tv -- NB: non-TcTyVars are possible
1709 = do { cts <- readMutVar ref -- under nested quantifiers
1711 Flexi -> fillBoxWithTau tv ref
1712 Indirect ty -> do { non_boxy_ty <- unBox ty
1713 ; if isTauTy non_boxy_ty
1714 then return non_boxy_ty
1715 else notMonoType non_boxy_ty }
1717 | otherwise -- Skolems, and meta-tau-variables
1718 = return (TyVarTy tv)
1720 unBoxPred :: PredType -> TcM PredType
1721 unBoxPred (ClassP cls tys) = do { tys' <- mapM unBox tys; return (ClassP cls tys') }
1722 unBoxPred (IParam ip ty) = do { ty' <- unBox ty; return (IParam ip ty') }
1723 unBoxPred (EqPred ty1 ty2) = do { ty1' <- unBox ty1; ty2' <- unBox ty2; return (EqPred ty1' ty2') }
1728 %************************************************************************
1732 %************************************************************************
1735 unifyMisMatch :: Outer -> TcM a
1736 unifyMisMatch (Unify is_outer ty1 ty2)
1737 | is_outer = popErrCtxt $ failWithMisMatch ty1 ty2 -- This is the whole point of the 'outer' stuff
1738 | otherwise = failWithMisMatch ty1 ty2
1740 popUnifyCtxt :: Outer -> TcM a -> TcM a
1741 popUnifyCtxt (Unify True _ _) thing = popErrCtxt thing
1742 popUnifyCtxt (Unify False _ _) thing = thing
1744 -----------------------
1745 unifyCtxt :: TcType -> TcType -> TidyEnv -> TcM (TidyEnv, SDoc)
1746 unifyCtxt act_ty exp_ty tidy_env
1747 = do { act_ty' <- zonkTcType act_ty
1748 ; exp_ty' <- zonkTcType exp_ty
1749 ; let (env1, exp_ty'') = tidyOpenType tidy_env exp_ty'
1750 (env2, act_ty'') = tidyOpenType env1 act_ty'
1751 ; return (env2, mkExpectedActualMsg act_ty'' exp_ty'') }
1754 mkExpectedActualMsg :: Type -> Type -> SDoc
1755 mkExpectedActualMsg act_ty exp_ty
1756 = nest 2 (vcat [ text "Expected type" <> colon <+> ppr exp_ty,
1757 text "Inferred type" <> colon <+> ppr act_ty ])
1760 -- If an error happens we try to figure out whether the function
1761 -- function has been given too many or too few arguments, and say so.
1762 addSubCtxt :: InstOrigin -> TcType -> TcType -> TcM a -> TcM a
1763 addSubCtxt orig actual_res_ty expected_res_ty thing_inside
1764 = addErrCtxtM mk_err thing_inside
1767 = do { exp_ty' <- zonkTcType expected_res_ty
1768 ; act_ty' <- zonkTcType actual_res_ty
1769 ; let (env1, exp_ty'') = tidyOpenType tidy_env exp_ty'
1770 (env2, act_ty'') = tidyOpenType env1 act_ty'
1771 (exp_args, _) = tcSplitFunTys exp_ty''
1772 (act_args, _) = tcSplitFunTys act_ty''
1774 len_act_args = length act_args
1775 len_exp_args = length exp_args
1777 message = case orig of
1779 | len_exp_args < len_act_args -> wrongArgsCtxt "too few" fun
1780 | len_exp_args > len_act_args -> wrongArgsCtxt "too many" fun
1781 _ -> mkExpectedActualMsg act_ty'' exp_ty''
1782 ; return (env2, message) }
1784 wrongArgsCtxt too_many_or_few fun
1785 = ptext (sLit "Probable cause:") <+> quotes (ppr fun)
1786 <+> ptext (sLit "is applied to") <+> text too_many_or_few
1787 <+> ptext (sLit "arguments")
1790 unifyForAllCtxt :: [TyVar] -> Type -> Type -> TidyEnv -> TcM (TidyEnv, SDoc)
1791 unifyForAllCtxt tvs phi1 phi2 env
1792 = return (env2, msg)
1794 (env', tvs') = tidyOpenTyVars env tvs -- NB: not tidyTyVarBndrs
1795 (env1, phi1') = tidyOpenType env' phi1
1796 (env2, phi2') = tidyOpenType env1 phi2
1797 msg = vcat [ptext (sLit "When matching") <+> quotes (ppr (mkForAllTys tvs' phi1')),
1798 ptext (sLit " and") <+> quotes (ppr (mkForAllTys tvs' phi2'))]
1803 %************************************************************************
1807 %************************************************************************
1809 Unifying kinds is much, much simpler than unifying types.
1812 unifyKind :: TcKind -- Expected
1815 unifyKind (TyConApp kc1 []) (TyConApp kc2 [])
1816 | isSubKindCon kc2 kc1 = return ()
1818 unifyKind (FunTy a1 r1) (FunTy a2 r2)
1819 = do { unifyKind a2 a1; unifyKind r1 r2 }
1820 -- Notice the flip in the argument,
1821 -- so that the sub-kinding works right
1822 unifyKind (TyVarTy kv1) k2 = uKVar False kv1 k2
1823 unifyKind k1 (TyVarTy kv2) = uKVar True kv2 k1
1824 unifyKind k1 k2 = unifyKindMisMatch k1 k2
1826 unifyKinds :: [TcKind] -> [TcKind] -> TcM ()
1827 unifyKinds [] [] = return ()
1828 unifyKinds (k1:ks1) (k2:ks2) = do unifyKind k1 k2
1830 unifyKinds _ _ = panic "unifyKinds: length mis-match"
1833 uKVar :: Bool -> KindVar -> TcKind -> TcM ()
1834 uKVar swapped kv1 k2
1835 = do { mb_k1 <- readKindVar kv1
1837 Flexi -> uUnboundKVar swapped kv1 k2
1838 Indirect k1 | swapped -> unifyKind k2 k1
1839 | otherwise -> unifyKind k1 k2 }
1842 uUnboundKVar :: Bool -> KindVar -> TcKind -> TcM ()
1843 uUnboundKVar swapped kv1 k2@(TyVarTy kv2)
1844 | kv1 == kv2 = return ()
1845 | otherwise -- Distinct kind variables
1846 = do { mb_k2 <- readKindVar kv2
1848 Indirect k2 -> uUnboundKVar swapped kv1 k2
1849 Flexi -> writeKindVar kv1 k2 }
1851 uUnboundKVar swapped kv1 non_var_k2
1852 = do { k2' <- zonkTcKind non_var_k2
1853 ; kindOccurCheck kv1 k2'
1854 ; k2'' <- kindSimpleKind swapped k2'
1855 -- KindVars must be bound only to simple kinds
1856 -- Polarities: (kindSimpleKind True ?) succeeds
1857 -- returning *, corresponding to unifying
1860 ; writeKindVar kv1 k2'' }
1863 kindOccurCheck :: TyVar -> Type -> TcM ()
1864 kindOccurCheck kv1 k2 -- k2 is zonked
1865 = checkTc (not_in k2) (kindOccurCheckErr kv1 k2)
1867 not_in (TyVarTy kv2) = kv1 /= kv2
1868 not_in (FunTy a2 r2) = not_in a2 && not_in r2
1871 kindSimpleKind :: Bool -> Kind -> TcM SimpleKind
1872 -- (kindSimpleKind True k) returns a simple kind sk such that sk <: k
1873 -- If the flag is False, it requires k <: sk
1874 -- E.g. kindSimpleKind False ?? = *
1875 -- What about (kv -> *) ~ ?? -> *
1876 kindSimpleKind orig_swapped orig_kind
1877 = go orig_swapped orig_kind
1879 go sw (FunTy k1 k2) = do { k1' <- go (not sw) k1
1881 ; return (mkArrowKind k1' k2') }
1883 | isOpenTypeKind k = return liftedTypeKind
1884 | isArgTypeKind k = return liftedTypeKind
1886 | isLiftedTypeKind k = return liftedTypeKind
1887 | isUnliftedTypeKind k = return unliftedTypeKind
1888 go _ k@(TyVarTy _) = return k -- KindVars are always simple
1889 go _ _ = failWithTc (ptext (sLit "Unexpected kind unification failure:")
1890 <+> ppr orig_swapped <+> ppr orig_kind)
1891 -- I think this can't actually happen
1893 -- T v = MkT v v must be a type
1894 -- T v w = MkT (v -> w) v must not be an umboxed tuple
1897 kindOccurCheckErr :: Var -> Type -> SDoc
1898 kindOccurCheckErr tyvar ty
1899 = hang (ptext (sLit "Occurs check: cannot construct the infinite kind:"))
1900 2 (sep [ppr tyvar, char '=', ppr ty])
1904 unifyFunKind :: TcKind -> TcM (Maybe (TcKind, TcKind))
1905 -- Like unifyFunTy, but does not fail; instead just returns Nothing
1907 unifyFunKind (TyVarTy kvar) = do
1908 maybe_kind <- readKindVar kvar
1910 Indirect fun_kind -> unifyFunKind fun_kind
1912 do { arg_kind <- newKindVar
1913 ; res_kind <- newKindVar
1914 ; writeKindVar kvar (mkArrowKind arg_kind res_kind)
1915 ; return (Just (arg_kind,res_kind)) }
1917 unifyFunKind (FunTy arg_kind res_kind) = return (Just (arg_kind,res_kind))
1918 unifyFunKind _ = return Nothing
1921 %************************************************************************
1923 \subsection{Checking signature type variables}
1925 %************************************************************************
1927 @checkSigTyVars@ checks that a set of universally quantified type varaibles
1928 are not mentioned in the environment. In particular:
1930 (a) Not mentioned in the type of a variable in the envt
1931 eg the signature for f in this:
1937 Here, f is forced to be monorphic by the free occurence of x.
1939 (d) Not (unified with another type variable that is) in scope.
1940 eg f x :: (r->r) = (\y->y) :: forall a. a->r
1941 when checking the expression type signature, we find that
1942 even though there is nothing in scope whose type mentions r,
1943 nevertheless the type signature for the expression isn't right.
1945 Another example is in a class or instance declaration:
1947 op :: forall b. a -> b
1949 Here, b gets unified with a
1951 Before doing this, the substitution is applied to the signature type variable.
1954 checkSigTyVars :: [TcTyVar] -> TcM ()
1955 checkSigTyVars sig_tvs = check_sig_tyvars emptyVarSet sig_tvs
1957 checkSigTyVarsWrt :: TcTyVarSet -> [TcTyVar] -> TcM ()
1958 -- The extra_tvs can include boxy type variables;
1959 -- e.g. TcMatches.tcCheckExistentialPat
1960 checkSigTyVarsWrt extra_tvs sig_tvs
1961 = do { extra_tvs' <- zonkTcTyVarsAndFV (varSetElems extra_tvs)
1962 ; check_sig_tyvars extra_tvs' sig_tvs }
1965 :: TcTyVarSet -- Global type variables. The universally quantified
1966 -- tyvars should not mention any of these
1967 -- Guaranteed already zonked.
1968 -> [TcTyVar] -- Universally-quantified type variables in the signature
1969 -- Guaranteed to be skolems
1971 check_sig_tyvars _ []
1973 check_sig_tyvars extra_tvs sig_tvs
1974 = ASSERT( all isTcTyVar sig_tvs && all isSkolemTyVar sig_tvs )
1975 do { gbl_tvs <- tcGetGlobalTyVars
1976 ; traceTc (text "check_sig_tyvars" <+> (vcat [text "sig_tys" <+> ppr sig_tvs,
1977 text "gbl_tvs" <+> ppr gbl_tvs,
1978 text "extra_tvs" <+> ppr extra_tvs]))
1980 ; let env_tvs = gbl_tvs `unionVarSet` extra_tvs
1981 ; when (any (`elemVarSet` env_tvs) sig_tvs)
1982 (bleatEscapedTvs env_tvs sig_tvs sig_tvs)
1985 bleatEscapedTvs :: TcTyVarSet -- The global tvs
1986 -> [TcTyVar] -- The possibly-escaping type variables
1987 -> [TcTyVar] -- The zonked versions thereof
1989 -- Complain about escaping type variables
1990 -- We pass a list of type variables, at least one of which
1991 -- escapes. The first list contains the original signature type variable,
1992 -- while the second contains the type variable it is unified to (usually itself)
1993 bleatEscapedTvs globals sig_tvs zonked_tvs
1994 = do { env0 <- tcInitTidyEnv
1995 ; let (env1, tidy_tvs) = tidyOpenTyVars env0 sig_tvs
1996 (env2, tidy_zonked_tvs) = tidyOpenTyVars env1 zonked_tvs
1998 ; (env3, msgs) <- foldlM check (env2, []) (tidy_tvs `zip` tidy_zonked_tvs)
1999 ; failWithTcM (env3, main_msg $$ nest 2 (vcat msgs)) }
2001 main_msg = ptext (sLit "Inferred type is less polymorphic than expected")
2003 check (tidy_env, msgs) (sig_tv, zonked_tv)
2004 | not (zonked_tv `elemVarSet` globals) = return (tidy_env, msgs)
2006 = do { (tidy_env1, globs) <- findGlobals (unitVarSet zonked_tv) tidy_env
2007 ; return (tidy_env1, escape_msg sig_tv zonked_tv globs : msgs) }
2009 -----------------------
2010 escape_msg :: Var -> Var -> [SDoc] -> SDoc
2011 escape_msg sig_tv zonked_tv globs
2013 = vcat [sep [msg, ptext (sLit "is mentioned in the environment:")],
2014 nest 2 (vcat globs)]
2016 = msg <+> ptext (sLit "escapes")
2017 -- Sigh. It's really hard to give a good error message
2018 -- all the time. One bad case is an existential pattern match.
2019 -- We rely on the "When..." context to help.
2021 msg = ptext (sLit "Quantified type variable") <+> quotes (ppr sig_tv) <+> is_bound_to
2023 | sig_tv == zonked_tv = empty
2024 | otherwise = ptext (sLit "is unified with") <+> quotes (ppr zonked_tv) <+> ptext (sLit "which")
2027 These two context are used with checkSigTyVars
2030 sigCtxt :: Id -> [TcTyVar] -> TcThetaType -> TcTauType
2031 -> TidyEnv -> TcM (TidyEnv, Message)
2032 sigCtxt id sig_tvs sig_theta sig_tau tidy_env = do
2033 actual_tau <- zonkTcType sig_tau
2035 (env1, tidy_sig_tvs) = tidyOpenTyVars tidy_env sig_tvs
2036 (env2, tidy_sig_rho) = tidyOpenType env1 (mkPhiTy sig_theta sig_tau)
2037 (env3, tidy_actual_tau) = tidyOpenType env2 actual_tau
2038 sub_msg = vcat [ptext (sLit "Signature type: ") <+> pprType (mkForAllTys tidy_sig_tvs tidy_sig_rho),
2039 ptext (sLit "Type to generalise:") <+> pprType tidy_actual_tau
2041 msg = vcat [ptext (sLit "When trying to generalise the type inferred for") <+> quotes (ppr id),