1 Normalisation of type terms relative to type instances as well as
2 normalisation and entailment checking of equality constraints.
8 normaliseGivenEqs, normaliseGivenDicts,
9 normaliseWantedEqs, normaliseWantedDicts,
12 misMatchMsg, failWithMisMatch
16 #include "HsVersions.h"
28 import TypeRep ( Type(..) )
36 import SrcLoc ( Located(..) )
45 %************************************************************************
47 Normalisation of types
49 %************************************************************************
51 Unfold a single synonym family instance and yield the witnessing coercion.
52 Return 'Nothing' if the given type is either not synonym family instance
53 or is a synonym family instance that has no matching instance declaration.
54 (Applies only if the type family application is outermost.)
56 For example, if we have
58 :Co:R42T a :: T [a] ~ :R42T a
60 then 'T [Int]' unfolds to (:R42T Int, :Co:R42T Int).
63 tcUnfoldSynFamInst :: Type -> TcM (Maybe (Type, Coercion))
64 tcUnfoldSynFamInst (TyConApp tycon tys)
65 | not (isOpenSynTyCon tycon) -- unfold *only* _synonym_ family instances
68 = do { -- we only use the indexing arguments for matching,
69 -- not the additional ones
70 ; maybeFamInst <- tcLookupFamInst tycon idxTys
71 ; case maybeFamInst of
72 Nothing -> return Nothing
73 Just (rep_tc, rep_tys) -> return $ Just (mkTyConApp rep_tc tys',
74 mkTyConApp coe_tc tys')
76 tys' = rep_tys ++ restTys
77 coe_tc = expectJust "TcTyFun.tcUnfoldSynFamInst"
78 (tyConFamilyCoercion_maybe rep_tc)
82 (idxTys, restTys) = splitAt n tys
83 tcUnfoldSynFamInst _other = return Nothing
86 Normalise 'Type's and 'PredType's by unfolding type family applications where
87 possible (ie, we treat family instances as a TRS). Also zonk meta variables.
89 tcNormaliseFamInst ty = (co, ty')
93 tcNormaliseFamInst :: TcType -> TcM (CoercionI, TcType)
94 tcNormaliseFamInst = tcGenericNormaliseFamInst tcUnfoldSynFamInst
96 tcNormaliseFamInstPred :: TcPredType -> TcM (CoercionI, TcPredType)
97 tcNormaliseFamInstPred = tcGenericNormaliseFamInstPred tcUnfoldSynFamInst
100 An elementary rewrite is a properly oriented equality with associated coercion
101 that has one of the following two forms:
103 (1) co :: F t1..tn ~ t
104 (2) co :: a ~ t , where t /= F t1..tn and a is a skolem tyvar
106 NB: We do *not* use equalities of the form a ~ t where a is a meta tyvar as a
107 reqrite rule. Instead, such equalities are solved by unification. This is
108 essential; cf Note [skolemOccurs loop].
110 The following functions takes an equality instance and turns it into an
111 elementary rewrite if possible.
114 data Rewrite = Rewrite TcType -- lhs of rewrite rule
115 TcType -- rhs of rewrite rule
116 TcType -- coercion witnessing the rewrite rule
118 eqInstToRewrite :: Inst -> Maybe (Rewrite, Bool)
119 -- True iff rewrite swapped equality
121 = ASSERT( isEqInst inst )
122 go ty1 ty2 (eqInstType inst)
124 (ty1,ty2) = eqInstTys inst
126 -- look through synonyms
127 go ty1 ty2 co | Just ty1' <- tcView ty1 = go ty1' ty2 co
128 go ty1 ty2 co | Just ty2' <- tcView ty2 = go ty1 ty2' co
130 -- left-to-right rule with type family head
131 go ty1@(TyConApp con _) ty2 co
133 = Just (Rewrite ty1 ty2 co, False) -- not swapped
135 -- left-to-right rule with type variable head
136 go ty1@(TyVarTy tv) ty2 co
138 = Just (Rewrite ty1 ty2 co, False) -- not swapped
140 -- right-to-left rule with type family head, only after
141 -- having checked whether we can work left-to-right
142 go ty1 ty2@(TyConApp con _) co
144 = Just (Rewrite ty2 ty1 (mkSymCoercion co), True) -- swapped
146 -- right-to-left rule with type variable head, only after
147 -- having checked whether we can work left-to-right
148 go ty1 ty2@(TyVarTy tv) co
150 = Just (Rewrite ty2 ty1 (mkSymCoercion co), True) -- swapped
152 -- this equality is not a rewrite rule => ignore
156 Normalise a type relative to an elementary rewrite implied by an EqInst or an
157 explicitly given elementary rewrite.
161 -- Precondition: the EqInst passes the occurs check
162 tcEqInstNormaliseFamInst :: Inst -> TcType -> TcM (CoercionI, TcType)
163 tcEqInstNormaliseFamInst inst ty
164 = case eqInstToRewrite inst of
165 Just (rewrite, _) -> tcEqRuleNormaliseFamInst rewrite ty
166 Nothing -> return (IdCo, ty)
168 -- Rewrite by equality rewrite rule
169 tcEqRuleNormaliseFamInst :: Rewrite -- elementary rewrite
170 -> TcType -- type to rewrite
171 -> TcM (CoercionI, -- witnessing coercion
172 TcType) -- rewritten type
173 tcEqRuleNormaliseFamInst (Rewrite pat rhs co) ty
174 = tcGenericNormaliseFamInst matchEqRule ty
176 matchEqRule sty | pat `tcEqType` sty = return $ Just (rhs, co)
177 | otherwise = return $ Nothing
180 Generic normalisation of 'Type's and 'PredType's; ie, walk the type term and
181 apply the normalisation function gives as the first argument to every TyConApp
182 and every TyVarTy subterm.
184 tcGenericNormaliseFamInst fun ty = (co, ty')
187 This function is (by way of using smart constructors) careful to ensure that
188 the returned coercion is exactly IdCo (and not some semantically equivalent,
189 but syntactically different coercion) whenever (ty' `tcEqType` ty). This
190 makes it easy for the caller to determine whether the type changed. BUT
191 even if we return IdCo, ty' may be *syntactically* different from ty due to
192 unfolded closed type synonyms (by way of tcCoreView). In the interest of
193 good error messages, callers should discard ty' in favour of ty in this case.
196 tcGenericNormaliseFamInst :: (TcType -> TcM (Maybe (TcType, Coercion)))
197 -- what to do with type functions and tyvars
198 -> TcType -- old type
199 -> TcM (CoercionI, TcType) -- (coercion, new type)
200 tcGenericNormaliseFamInst fun ty
201 | Just ty' <- tcView ty = tcGenericNormaliseFamInst fun ty'
202 tcGenericNormaliseFamInst fun (TyConApp tyCon tys)
203 = do { (cois, ntys) <- mapAndUnzipM (tcGenericNormaliseFamInst fun) tys
204 ; let tycon_coi = mkTyConAppCoI tyCon ntys cois
205 ; maybe_ty_co <- fun (mkTyConApp tyCon ntys) -- use normalised args!
206 ; case maybe_ty_co of
207 -- a matching family instance exists
209 do { let first_coi = mkTransCoI tycon_coi (ACo co)
210 ; (rest_coi, nty) <- tcGenericNormaliseFamInst fun ty'
211 ; let fix_coi = mkTransCoI first_coi rest_coi
212 ; return (fix_coi, nty)
214 -- no matching family instance exists
215 -- we do not do anything
216 Nothing -> return (tycon_coi, mkTyConApp tyCon ntys)
218 tcGenericNormaliseFamInst fun (AppTy ty1 ty2)
219 = do { (coi1,nty1) <- tcGenericNormaliseFamInst fun ty1
220 ; (coi2,nty2) <- tcGenericNormaliseFamInst fun ty2
221 ; return (mkAppTyCoI nty1 coi1 nty2 coi2, mkAppTy nty1 nty2)
223 tcGenericNormaliseFamInst fun (FunTy ty1 ty2)
224 = do { (coi1,nty1) <- tcGenericNormaliseFamInst fun ty1
225 ; (coi2,nty2) <- tcGenericNormaliseFamInst fun ty2
226 ; return (mkFunTyCoI nty1 coi1 nty2 coi2, mkFunTy nty1 nty2)
228 tcGenericNormaliseFamInst fun (ForAllTy tyvar ty1)
229 = do { (coi,nty1) <- tcGenericNormaliseFamInst fun ty1
230 ; return (mkForAllTyCoI tyvar coi, mkForAllTy tyvar nty1)
232 tcGenericNormaliseFamInst fun ty@(TyVarTy tv)
234 = do { traceTc (text "tcGenericNormaliseFamInst" <+> ppr ty)
235 ; res <- lookupTcTyVar tv
238 do { maybe_ty' <- fun ty
240 Nothing -> return (IdCo, ty)
242 do { (coi2, ty'') <- tcGenericNormaliseFamInst fun ty'
243 ; return (ACo co1 `mkTransCoI` coi2, ty'')
246 IndirectTv ty' -> tcGenericNormaliseFamInst fun ty'
250 tcGenericNormaliseFamInst fun (PredTy predty)
251 = do { (coi, pred') <- tcGenericNormaliseFamInstPred fun predty
252 ; return (coi, PredTy pred') }
254 ---------------------------------
255 tcGenericNormaliseFamInstPred :: (TcType -> TcM (Maybe (TcType,Coercion)))
257 -> TcM (CoercionI, TcPredType)
259 tcGenericNormaliseFamInstPred fun (ClassP cls tys)
260 = do { (cois, tys')<- mapAndUnzipM (tcGenericNormaliseFamInst fun) tys
261 ; return (mkClassPPredCoI cls tys' cois, ClassP cls tys')
263 tcGenericNormaliseFamInstPred fun (IParam ipn ty)
264 = do { (coi, ty') <- tcGenericNormaliseFamInst fun ty
265 ; return $ (mkIParamPredCoI ipn coi, IParam ipn ty')
267 tcGenericNormaliseFamInstPred fun (EqPred ty1 ty2)
268 = do { (coi1, ty1') <- tcGenericNormaliseFamInst fun ty1
269 ; (coi2, ty2') <- tcGenericNormaliseFamInst fun ty2
270 ; return (mkEqPredCoI ty1' coi1 ty2' coi2, EqPred ty1' ty2') }
274 %************************************************************************
276 \section{Normalisation of equality constraints}
278 %************************************************************************
280 Note [Inconsistencies in equality constraints]
281 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
282 We guarantee that we raise an error if we discover any inconsistencies (i.e.,
283 equalities that if presented to the unifer in TcUnify would result in an
284 error) during normalisation of wanted constraints. This is especially so that
285 we don't solve wanted constraints under an inconsistent given set. In
286 particular, we don't want to permit signatures, such as
288 bad :: (Int ~ Bool => Int) -> a -> a
291 normaliseGivenEqs :: [Inst] -> TcM ([Inst], TcM ())
292 normaliseGivenEqs givens
293 = do { traceTc (text "normaliseGivenEqs <-" <+> ppr givens)
294 ; (result, deSkolem) <-
295 rewriteToFixedPoint (Just ("(SkolemOccurs)", skolemOccurs))
296 [ ("(ZONK)", dontRerun $ zonkInsts)
297 , ("(TRIVIAL)", dontRerun $ trivialRule)
298 , ("(DECOMP)", decompRule)
300 , ("(SUBST)", substRule) -- incl. occurs check
302 ; traceTc (text "normaliseGivenEqs ->" <+> ppr result)
303 ; return (result, deSkolem)
308 normaliseWantedEqs :: [Inst] -- givens
310 -> TcM [Inst] -- irreducible wanteds
311 normaliseWantedEqs givens wanteds
312 = do { traceTc $ text "normaliseWantedEqs <-" <+> ppr wanteds
313 <+> text "with" <+> ppr givens
314 ; result <- liftM fst $ rewriteToFixedPoint Nothing
315 [ ("(ZONK)", dontRerun $ zonkInsts)
316 , ("(TRIVIAL)", dontRerun $ trivialRule)
317 , ("(DECOMP)", decompRule)
319 , ("(GIVEN)", substGivens givens) -- incl. occurs check
320 , ("(UNIFY)", unifyMetaRule) -- incl. occurs check
321 , ("(SUBST)", substRule) -- incl. occurs check
323 ; traceTc (text "normaliseWantedEqs ->" <+> ppr result)
327 -- Use `substInst' with every given on all the wanteds.
328 substGivens :: [Inst] -> [Inst] -> TcM ([Inst], Bool)
329 substGivens [] wanteds = return (wanteds, False)
330 substGivens (g:gs) wanteds
331 = do { (wanteds1, changed1) <- substGivens gs wanteds
332 ; (wanteds2, changed2) <- substInst g wanteds1
333 ; return (wanteds2, changed1 || changed2)
338 %************************************************************************
340 \section{Normalisation of non-equality dictionaries}
342 %************************************************************************
345 normaliseGivenDicts, normaliseWantedDicts
346 :: [Inst] -- given equations
347 -> [Inst] -- dictionaries
348 -> TcM ([Inst],TcDictBinds)
350 normaliseGivenDicts eqs dicts = normalise_dicts eqs dicts False
351 normaliseWantedDicts eqs dicts = normalise_dicts eqs dicts True
354 :: [Inst] -- given equations
355 -> [Inst] -- dictionaries
356 -> Bool -- True <=> the dicts are wanted
357 -- Fals <=> they are given
358 -> TcM ([Inst],TcDictBinds)
359 normalise_dicts given_eqs dicts is_wanted
360 = do { traceTc $ let name | is_wanted = "normaliseWantedDicts <-"
361 | otherwise = "normaliseGivenDicts <-"
363 text name <+> ppr dicts <+>
364 text "with" <+> ppr given_eqs
365 ; (dicts0, binds0) <- normaliseInsts is_wanted dicts
366 ; (dicts1, binds1) <- substEqInDictInsts is_wanted given_eqs dicts0
367 ; let binds01 = binds0 `unionBags` binds1
368 ; if isEmptyBag binds1
369 then return (dicts1, binds01)
370 else do { (dicts2, binds2) <-
371 normalise_dicts given_eqs dicts1 is_wanted
372 ; return (dicts2, binds01 `unionBags` binds2) } }
376 %************************************************************************
378 \section{Normalisation rules and iterative rule application}
380 %************************************************************************
382 We have three kinds of normalising rewrite rules:
384 (1) Normalisation rules that rewrite a set of insts and return a flag indicating
385 whether any changes occurred during rewriting that necessitate re-running
386 the current rule set.
388 (2) Precondition rules that rewrite a set of insts and return a monadic action
389 that reverts the effect of preconditioning.
391 (3) Idempotent normalisation rules that never require re-running the rule set.
394 type RewriteRule = [Inst] -> TcM ([Inst], Bool) -- rewrite, maybe re-run
395 type PrecondRule = [Inst] -> TcM ([Inst], TcM ()) -- rewrite, revertable
396 type IdemRewriteRule = [Inst] -> TcM [Inst] -- rewrite, don't re-run
398 type NamedRule = (String, RewriteRule) -- rule with description
399 type NamedPreRule = (String, PrecondRule) -- precond with desc
402 Template lifting idempotent rules to full rules (which can be put into a rule
406 dontRerun :: IdemRewriteRule -> RewriteRule
407 dontRerun rule insts = liftM addFalse $ rule insts
409 addFalse x = (x, False)
412 The following function applies a set of rewrite rules until a fixed point is
413 reached; i.e., none of the `RewriteRule's require re-running the rule set.
414 Optionally, there may be a pre-conditing rule that is applied before any other
415 rules are applied and before the rule set is re-run.
417 The result is the set of rewritten (i.e., normalised) insts and, in case of a
418 pre-conditing rule, a monadic action that reverts the effects of
419 pre-conditioning - specifically, this is removing introduced skolems.
422 rewriteToFixedPoint :: Maybe NamedPreRule -- optional preconditioning rule
423 -> [NamedRule] -- rule set
424 -> [Inst] -- insts to rewrite
425 -> TcM ([Inst], TcM ())
426 rewriteToFixedPoint precondRule rules insts
427 = completeRewrite (return ()) precondRule insts
429 completeRewrite :: TcM () -> Maybe NamedPreRule -> [Inst]
430 -> TcM ([Inst], TcM ())
431 completeRewrite dePrecond (Just (precondName, precond)) insts
432 = do { traceTc $ text precondName <+> text " <- " <+> ppr insts
433 ; (insts', dePrecond') <- precond insts
434 ; traceTc $ text precondName <+> text " -> " <+> ppr insts'
435 ; tryRules (dePrecond >> dePrecond') rules insts'
437 completeRewrite dePrecond Nothing insts
438 = tryRules dePrecond rules insts
440 tryRules dePrecond _ [] = return ([] , dePrecond)
441 tryRules dePrecond [] insts = return (insts, dePrecond)
442 tryRules dePrecond ((name, rule):rules) insts
443 = do { traceTc $ text name <+> text " <- " <+> ppr insts
444 ; (insts', rerun) <- rule insts
445 ; traceTc $ text name <+> text " -> " <+> ppr insts'
446 ; if rerun then completeRewrite dePrecond precondRule insts'
447 else tryRules dePrecond rules insts'
452 %************************************************************************
454 \section{Different forms of Inst rewrite rules}
456 %************************************************************************
458 Splitting of non-terminating given constraints: skolemOccurs
459 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
460 This is a preconditioning rule exclusively applied to given constraints.
461 Moreover, its rewriting is only temporary, as it is undone by way of
462 side-effecting mutable type variables after simplification and constraint
463 entailment has been completed.
465 This version is an (attempt at, yet unproven, an) *unflattened* version of
466 the SubstL-Ev completion rule.
468 The above rule is essential to catch non-terminating rules that cannot be
469 oriented properly, like
473 a ~ [G a] , where a is a skolem tyvar
475 The left-to-right orientiation is not suitable because it does not
476 terminate. The right-to-left orientation is not suitable because it
477 does not have a type-function on the left. This is undesirable because
478 it would hide information. E.g. assume
482 then rewriting C [G (F a)] to C (F a) is bad because we cannot now
483 see that the C [x] instance applies.
485 The rule also caters for badly-oriented rules of the form:
489 for which other solutions are possible, but this one will do too.
493 co : ty1 ~ ty2{F ty1}
496 sym (F co) : F ty2{b} ~ b
497 where b is a fresh skolem variable
499 We also cater for the symmetric situation *if* the rule cannot be used as a
500 left-to-right rewrite rule.
502 We also return an action (b := ty1) which is used to eliminate b
503 after the dust of normalisation with the completed rewrite system
506 A subtle point of this transformation is that both coercions in the results
507 are strictly speaking incorrect. However, they are correct again after the
508 action {B := ty1} has removed the skolem again. This happens immediately
509 after constraint entailment has been checked; ie, code outside of the
510 simplification and entailment checking framework will never see these
511 temporarily incorrect coercions.
513 NB: We perform this transformation for multiple occurences of ty1 under one
514 or multiple family applications on the left-hand side at once (ie, the
515 rule doesn't need to be applied multiple times at a single inst). As a
516 result we can get two or more insts back.
518 Note [skolemOccurs loop]
519 ~~~~~~~~~~~~~~~~~~~~~~~~
520 You might think that under
523 type instance F [a] = [F a]
527 foo :: (F [a] ~ a) => a
529 will get us into a loop. However, this is *not* the case. Here is why:
540 F [b<tau>] ~ b<tau> , with b := F a
545 [F b<tau>] ~ b<tau> , with b := F a
547 At this point (SkolemOccurs) does *not* apply anymore, as
551 is not used as a rewrite rule. The variable b<tau> is not a skolem (cf
554 (The regression test indexed-types/should_compile/Simple20 checks that the
555 described property of the system does not change.)
558 skolemOccurs :: PrecondRule
560 = do { (instss, undoSkolems) <- mapAndUnzipM oneSkolemOccurs insts
561 ; return (concat instss, sequence_ undoSkolems)
565 = ASSERT( isEqInst inst )
566 case eqInstToRewrite inst of
567 Just (rewrite, swapped) -> breakRecursion rewrite swapped
568 Nothing -> return ([inst], return ())
570 -- inst is an elementary rewrite rule, check whether we need to break
572 breakRecursion (Rewrite pat body _) swapped
574 -- skolemOccurs does not apply, leave as is
576 = do { traceTc $ text "oneSkolemOccurs: no tys to lift out"
577 ; return ([inst], return ())
580 -- recursive occurence of pat in body under a type family application
582 = do { traceTc $ text "oneSkolemOccurs[TLO]:" <+> ppr tysToLiftOut
583 ; skTvs <- mapM (newMetaTyVar TauTv . typeKind) tysToLiftOut
584 ; let skTvs_tysTLO = zip skTvs tysToLiftOut
585 insertSkolems = return . replace skTvs_tysTLO
586 ; (_, body') <- tcGenericNormaliseFamInst insertSkolems body
587 ; inst' <- if swapped then mkEqInst (EqPred body' pat) co
588 else mkEqInst (EqPred pat body') co
589 -- ensure to reconstruct the inst in the
590 -- original orientation
591 ; traceTc $ text "oneSkolemOccurs[inst']:" <+> ppr inst'
592 ; (insts, undoSk) <- mapAndUnzipM (mkSkolemInst inst')
594 ; return (inst':insts, sequence_ undoSk)
597 co = eqInstCoercion inst
599 -- all subtypes that are (1) type family instances and (2) contain
600 -- the lhs type as part of the type arguments of the type family
602 tysToLiftOut = [mkTyConApp tc tys | (tc, tys) <- tyFamInsts body
603 , any (pat `tcPartOfType`) tys]
605 replace :: [(TcTyVar, Type)] -> Type -> Maybe (Type, Coercion)
606 replace [] _ = Nothing
607 replace ((skTv, tyTLO):rest) ty
608 | tyTLO `tcEqType` ty = Just (mkTyVarTy skTv, undefined)
609 | otherwise = replace rest ty
611 -- create the EqInst for the equality determining the skolem and a
612 -- TcM action undoing the skolem introduction
613 mkSkolemInst inst' (skTv, tyTLO)
614 = do { (co, tyLiftedOut) <- tcEqInstNormaliseFamInst inst' tyTLO
615 ; inst <- mkEqInst (EqPred tyLiftedOut (mkTyVarTy skTv))
616 (mkGivenCo $ mkSymCoercion (fromACo co))
617 -- co /= IdCo due to construction of inst'
618 ; return (inst, writeMetaTyVar skTv tyTLO)
623 Removal of trivial equalities: trivialRule
624 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
625 The following rules exploits the reflexivity of equality:
633 trivialRule :: IdemRewriteRule
635 = liftM catMaybes $ mapM trivial insts
638 | ASSERT( isEqInst inst )
640 = do { eitherEqInst inst
641 (\cotv -> writeMetaTyVar cotv ty1)
648 (ty1,ty2) = eqInstTys inst
652 Decomposition of data type constructors: decompRule
653 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
654 Whenever, the same *data* constructors occurs on both sides of an equality, we
655 can decompose as in standard unification.
660 g21 : c1 ~ d1, ..., g2n : cn ~ dn
663 Works also for the case where T is actually an application of a type family
664 constructor to a set of types, provided the applications on both sides of the
665 ~ are identical; see also Note [OpenSynTyCon app] in TcUnify.
667 We guarantee to raise an error for any inconsistent equalities;
668 cf Note [Inconsistencies in equality constraints].
671 decompRule :: RewriteRule
673 = do { (insts, changed) <- mapAndUnzipM decomp insts
674 ; return (concat insts, or changed)
678 = ASSERT( isEqInst inst )
681 (ty1,ty2) = eqInstTys inst
683 | Just ty1' <- tcView ty1 = go ty1' ty2
684 | Just ty2' <- tcView ty2 = go ty1 ty2'
686 go (TyConApp con1 tys1) (TyConApp con2 tys2)
687 | con1 == con2 && identicalHead
688 = mkArgInsts (mkTyConApp con1) tys1 tys2
690 | con1 /= con2 && not (isOpenSynTyCon con1 || isOpenSynTyCon con2)
691 -- not matching data constructors (of any flavour) are bad news
692 = eqInstMisMatch inst
695 (idxTys1, _) = splitAt n tys1
696 (idxTys2, _) = splitAt n tys2
697 identicalHead = not (isOpenSynTyCon con1) ||
698 idxTys1 `tcEqTypes` idxTys2
700 go (FunTy fun1 arg1) (FunTy fun2 arg2)
701 = mkArgInsts (\[funCo, argCo] -> mkFunTy funCo argCo) [fun1, arg1]
704 -- Applications need a bit of care!
705 -- They can match FunTy and TyConApp, so use splitAppTy_maybe
707 | Just (s2, t2) <- tcSplitAppTy_maybe ty2
708 = mkArgInsts (\[s, t] -> mkAppTy s t) [s1, t1] [s2, t2]
712 | Just (s1, t1) <- tcSplitAppTy_maybe ty1
713 = mkArgInsts (\[s, t] -> mkAppTy s t) [s1, t1] [s2, t2]
715 -- We already covered all the consistent cases of rigid types on both
716 -- sides; so, if we see two rigid types here, we discovered an
719 | isRigid ty1 && isRigid ty2
720 = eqInstMisMatch inst
722 -- We can neither assert consistency nor inconsistency => defer
723 go _ _ = return ([inst], False)
725 isRigid (TyConApp con _) = not (isOpenSynTyCon con)
726 isRigid (FunTy _ _) = True
727 isRigid (AppTy _ _) = True
730 -- Create insts for matching argument positions (ie, the bit after
731 -- '>-->' in the rule description above)
732 mkArgInsts con tys1 tys2
733 = do { cos <- eitherEqInst inst
734 -- old_co := Con1 cos
736 do { cotvs <- zipWithM newMetaCoVar tys1 tys2
737 ; let cos = map mkTyVarTy cotvs
738 ; writeMetaTyVar old_covar (con cos)
739 ; return $ map mkWantedCo cotvs
741 -- co_i := Con_i old_co
743 return $ map mkGivenCo $
744 mkRightCoercions (length tys1) old_co)
745 ; insts <- zipWithM mkEqInst (zipWith EqPred tys1 tys2) cos
746 ; traceTc (text "decomp identicalHead" <+> ppr insts)
747 ; return (insts, not $ null insts)
752 Rewriting with type instances: topRule
753 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
754 We use (toplevel) type instances to normalise both sides of equalities.
758 >--> co1 :: t ~ t' / co2 :: s ~ s'
760 g1 := co1 * g2 * sym co2
763 topRule :: RewriteRule
765 = do { (insts, changed) <- mapAndUnzipM top insts
766 ; return (insts, or changed)
770 = ASSERT( isEqInst inst )
771 do { (coi1, ty1') <- tcNormaliseFamInst ty1
772 ; (coi2, ty2') <- tcNormaliseFamInst ty2
773 ; case (coi1, coi2) of
774 (IdCo, IdCo) -> return (inst, False)
778 -- old_co = co1 * new_co * sym co2
780 do { new_cotv <- newMetaCoVar ty1' ty2'
781 ; let new_co = mkTyVarTy new_cotv
782 old_coi = coi1 `mkTransCoI`
783 ACo new_co `mkTransCoI`
785 ; writeMetaTyVar old_covar (fromACo old_coi)
786 ; return $ mkWantedCo new_cotv
788 -- new_co = sym co1 * old_co * co2
793 mkSymCoI coi1 `mkTransCoI`
794 ACo old_co `mkTransCoI` coi2)
795 ; new_inst <- mkEqInst (EqPred ty1' ty2') wg_co
796 ; return (new_inst, True)
800 (ty1,ty2) = eqInstTys inst
804 Rewriting with equalities: substRule
805 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
806 From a set of insts, use all insts that can be read as rewrite rules to
807 rewrite the types in all other insts.
811 forall g1 : s1{F c} ~ s2{F c}
814 g1 := s1{g} * g2 * sym s2{g} <=> g2 := sym s1{g} * g1 * s2{g}
816 Alternatively, the rewrite rule may have the form (g : a ~ t).
818 To avoid having to swap rules of the form (g : t ~ F c) and (g : t ~ a),
819 where t is neither a variable nor a type family application, we use them for
820 rewriting from right-to-left. However, it is crucial to only apply rules
821 from right-to-left if they cannot be used left-to-right.
823 The workhorse is substInst, which performs an occurs check before actually
824 using an equality for rewriting. If the type pattern occurs in the type we
825 substitute for the pattern, normalisation would diverge.
828 substRule :: RewriteRule
829 substRule insts = tryAllInsts insts []
831 -- for every inst check whether it can be used to rewrite the others
832 -- (we make an effort to keep the insts in order; it makes debugging
834 tryAllInsts [] triedInsts = return (reverse triedInsts, False)
835 tryAllInsts (inst:insts) triedInsts
836 = do { (insts', changed) <- substInst inst (reverse triedInsts ++ insts)
837 ; if changed then return (insertAt (length triedInsts) inst insts',
839 else tryAllInsts insts (inst:triedInsts)
842 insertAt n x xs = let (xs1, xs2) = splitAt n xs
845 -- Use the given inst as a rewrite rule to normalise the insts in the second
846 -- argument. Don't do anything if the inst cannot be used as a rewrite rule,
847 -- but do apply it right-to-left, if possible, and if it cannot be used
850 substInst :: Inst -> [Inst] -> TcM ([Inst], Bool)
852 = case eqInstToRewrite inst of
853 Just (rewrite, _) -> substEquality rewrite insts
854 Nothing -> return (insts, False)
856 substEquality :: Rewrite -- elementary rewrite
857 -> [Inst] -- insts to rewrite
858 -> TcM ([Inst], Bool)
859 substEquality eqRule@(Rewrite pat rhs _) insts
860 | pat `tcPartOfType` rhs -- occurs check!
861 = occurCheckErr pat rhs
863 = do { (insts', changed) <- mapAndUnzipM substOne insts
864 ; return (insts', or changed)
868 = ASSERT( isEqInst inst )
869 do { (coi1, ty1') <- tcEqRuleNormaliseFamInst eqRule ty1
870 ; (coi2, ty2') <- tcEqRuleNormaliseFamInst eqRule ty2
871 ; case (coi1, coi2) of
872 (IdCo, IdCo) -> return (inst, False)
876 -- old_co := co1 * new_co * sym co2
878 do { new_cotv <- newMetaCoVar ty1' ty2'
879 ; let new_co = mkTyVarTy new_cotv
880 old_coi = coi1 `mkTransCoI`
881 ACo new_co `mkTransCoI`
883 ; writeMetaTyVar old_covar (fromACo old_coi)
884 ; return $ mkWantedCo new_cotv
886 -- new_co := sym co1 * old_co * co2
891 mkSymCoI coi1 `mkTransCoI`
892 ACo old_co `mkTransCoI` coi2)
893 ; new_inst <- mkEqInst (EqPred ty1' ty2') gw_co
894 ; return (new_inst, True)
898 (ty1,ty2) = eqInstTys inst
902 Instantiate meta variables: unifyMetaRule
903 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
904 If an equality equates a meta type variable with a type, we simply instantiate
913 Meta variables can only appear in wanted constraints, and this rule should
914 only be applied to wanted constraints. We also know that t definitely is
915 distinct from alpha (as the trivialRule) has been run on the insts beforehand.
917 NB: We cannot assume that meta tyvars are empty. They may have been updated
918 by another inst in the currently processed wanted list. We need to be very
919 careful when updateing type variables (see TcUnify.uUnfilledVar), but at least
920 we know that we have no boxes. It's unclear that it would be an advantage to
921 common up the code in TcUnify and the code below. Firstly, we don't want
922 calls to TcUnify.defer_unification here, and secondly, TcUnify import the
923 current module, so we would have to move everything here (Yuk!) or to
924 TcMType. Besides, the code here is much simpler due to the lack of boxes.
927 unifyMetaRule :: RewriteRule
929 = do { (insts', changed) <- mapAndUnzipM unifyMeta insts
930 ; return (concat insts', or changed)
934 = ASSERT( isEqInst inst )
936 (fromWantedCo "unifyMetaRule" $ eqInstCoercion inst)
938 (ty1,ty2) = eqInstTys inst
940 | Just ty1' <- tcView ty1 = go ty1' ty2 cotv
941 | Just ty2' <- tcView ty2 = go ty1 ty2' cotv
944 , isMetaTyVar tv1 = do { lookupTV <- lookupTcTyVar tv1
945 ; uMeta False tv1 lookupTV ty2 cotv
948 , isMetaTyVar tv2 = do { lookupTV <- lookupTcTyVar tv2
949 ; uMeta True tv2 lookupTV ty1 cotv
951 | otherwise = return ([inst], False)
953 -- meta variable has been filled already
954 -- => ignore this inst (we'll come around again, after zonking)
955 uMeta _swapped _tv (IndirectTv _) _ty _cotv
956 = return ([inst], False)
958 -- type variable meets type variable
959 -- => check that tv2 hasn't been updated yet and choose which to update
960 uMeta swapped tv1 (DoneTv details1) (TyVarTy tv2) cotv
962 = return ([inst], False) -- The two types are already identical
965 = do { lookupTV2 <- lookupTcTyVar tv2
967 IndirectTv ty -> uMeta swapped tv1 (DoneTv details1) ty cotv
968 DoneTv details2 -> uMetaVar swapped tv1 details1 tv2 details2 cotv
971 ------ Beyond this point we know that ty2 is not a type variable
973 -- signature skolem meets non-variable type
975 uMeta _swapped _tv (DoneTv (MetaTv (SigTv _) _)) _non_tv_ty _cotv
976 = return ([inst], False)
978 -- updatable meta variable meets non-variable type
979 -- => occurs check, monotype check, and kinds match check, then update
980 uMeta swapped tv (DoneTv (MetaTv _ ref)) non_tv_ty cotv
981 = do { mb_ty' <- checkTauTvUpdate tv non_tv_ty -- occurs + monotype check
983 Nothing -> return ([inst], False) -- tv occurs in faminst
985 do { checkUpdateMeta swapped tv ref ty' -- update meta var
986 ; writeMetaTyVar cotv ty' -- update co var
991 uMeta _ _ _ _ _ = panic "uMeta"
993 -- uMetaVar: unify two type variables
994 -- meta variable meets skolem
996 uMetaVar swapped tv1 (MetaTv _ ref) tv2 (SkolemTv _) cotv
997 = do { checkUpdateMeta swapped tv1 ref (mkTyVarTy tv2)
998 ; writeMetaTyVar cotv (mkTyVarTy tv2)
1002 -- meta variable meets meta variable
1003 -- => be clever about which of the two to update
1004 -- (from TcUnify.uUnfilledVars minus boxy stuff)
1005 uMetaVar swapped tv1 (MetaTv info1 ref1) tv2 (MetaTv info2 ref2) cotv
1006 = do { case (info1, info2) of
1007 -- Avoid SigTvs if poss
1008 (SigTv _, _ ) | k1_sub_k2 -> update_tv2
1009 (_, SigTv _) | k2_sub_k1 -> update_tv1
1011 (_, _) | k1_sub_k2 -> if k2_sub_k1 && nicer_to_update_tv1
1012 then update_tv1 -- Same kinds
1014 | k2_sub_k1 -> update_tv1
1015 | otherwise -> kind_err
1016 -- Update the variable with least kind info
1017 -- See notes on type inference in Kind.lhs
1018 -- The "nicer to" part only applies if the two kinds are the same,
1019 -- so we can choose which to do.
1021 ; writeMetaTyVar cotv (mkTyVarTy tv2)
1025 -- Kinds should be guaranteed ok at this point
1026 update_tv1 = updateMeta tv1 ref1 (mkTyVarTy tv2)
1027 update_tv2 = updateMeta tv2 ref2 (mkTyVarTy tv1)
1029 kind_err = addErrCtxtM (unifyKindCtxt swapped tv1 (mkTyVarTy tv2)) $
1030 unifyKindMisMatch k1 k2
1034 k1_sub_k2 = k1 `isSubKind` k2
1035 k2_sub_k1 = k2 `isSubKind` k1
1037 nicer_to_update_tv1 = isSystemName (Var.varName tv1)
1038 -- Try to update sys-y type variables in preference to ones
1039 -- gotten (say) by instantiating a polymorphic function with
1040 -- a user-written type sig
1042 uMetaVar _ _ _ _ _ _ = panic "uMetaVar"
1046 %************************************************************************
1048 \section{Normalisation of Insts}
1050 %************************************************************************
1052 Normalises a set of dictionaries relative to a set of given equalities (which
1053 are interpreted as rewrite rules). We only consider given equalities of the
1058 where F is a type family.
1061 substEqInDictInsts :: Bool -- whether the *dictionaries* are wanted/given
1062 -> [Inst] -- given equalities (used as rewrite rules)
1063 -> [Inst] -- dictinaries to be normalised
1064 -> TcM ([Inst], TcDictBinds)
1065 substEqInDictInsts isWanted eqInsts dictInsts
1066 = do { traceTc (text "substEqInDictInst <-" <+> ppr dictInsts)
1068 foldlM rewriteWithOneEquality (dictInsts, emptyBag) eqInsts
1069 ; traceTc (text "substEqInDictInst ->" <+> ppr dictInsts')
1073 -- (1) Given equality of form 'F ts ~ t' or 'a ~ t': use for rewriting
1074 rewriteWithOneEquality (dictInsts, dictBinds)
1075 eqInst@(EqInst {tci_left = pattern,
1076 tci_right = target})
1077 | isOpenSynTyConApp pattern || isTyVarTy pattern
1078 = do { (dictInsts', moreDictBinds) <-
1079 genericNormaliseInsts isWanted applyThisEq dictInsts
1080 ; return (dictInsts', dictBinds `unionBags` moreDictBinds)
1083 applyThisEq = tcGenericNormaliseFamInstPred (return . matchResult)
1085 -- rewrite in case of an exact match
1086 matchResult ty | tcEqType pattern ty = Just (target, eqInstType eqInst)
1087 | otherwise = Nothing
1089 -- (2) Given equality has the wrong form: ignore
1090 rewriteWithOneEquality (dictInsts, dictBinds) _not_a_rewrite_rule
1091 = return (dictInsts, dictBinds)
1095 Take a bunch of Insts (not EqInsts), and normalise them wrt the top-level
1096 type-function equations, where
1098 (norm_insts, binds) = normaliseInsts is_wanted insts
1101 = True, (binds + norm_insts) defines insts (wanteds)
1102 = False, (binds + insts) defines norm_insts (givens)
1104 Ie, in the case of normalising wanted dictionaries, we use the normalised
1105 dictionaries to define the originally wanted ones. However, in the case of
1106 given dictionaries, we use the originally given ones to define the normalised
1110 normaliseInsts :: Bool -- True <=> wanted insts
1111 -> [Inst] -- wanted or given insts
1112 -> TcM ([Inst], TcDictBinds) -- normalised insts and bindings
1113 normaliseInsts isWanted insts
1114 = genericNormaliseInsts isWanted tcNormaliseFamInstPred insts
1116 genericNormaliseInsts :: Bool -- True <=> wanted insts
1117 -> (TcPredType -> TcM (CoercionI, TcPredType))
1119 -> [Inst] -- wanted or given insts
1120 -> TcM ([Inst], TcDictBinds) -- normalised insts & binds
1121 genericNormaliseInsts isWanted fun insts
1122 = do { (insts', binds) <- mapAndUnzipM (normaliseOneInst isWanted fun) insts
1123 ; return (insts', unionManyBags binds)
1126 normaliseOneInst isWanted fun
1127 dict@(Dict {tci_pred = pred,
1129 = do { traceTc $ text "genericNormaliseInst <-" <+> ppr dict
1130 ; (coi, pred') <- fun pred
1134 do { traceTc $ text "genericNormaliseInst ->" <+> ppr dict
1135 ; return (dict, emptyBag)
1137 -- don't use pred' in this case; otherwise, we get
1138 -- more unfolded closed type synonyms in error messages
1140 do { -- an inst for the new pred
1141 ; dict' <- newDictBndr loc pred'
1142 -- relate the old inst to the new one
1143 -- target_dict = source_dict `cast` st_co
1144 ; let (target_dict, source_dict, st_co)
1145 | isWanted = (dict, dict', mkSymCoercion co)
1146 | otherwise = (dict', dict, co)
1148 -- co :: dict ~ dict'
1149 -- hence, if isWanted
1150 -- dict = dict' `cast` sym co
1152 -- dict' = dict `cast` co
1153 expr = HsVar $ instToId source_dict
1154 cast_expr = HsWrap (WpCo st_co) expr
1155 rhs = L (instLocSpan loc) cast_expr
1156 binds = instToDictBind target_dict rhs
1157 -- return the new inst
1158 ; traceTc $ let name | isWanted
1159 = "genericNormaliseInst (wanted) ->"
1161 = "genericNormaliseInst (given) ->"
1163 text name <+> ppr dict' <+>
1164 text "with" <+> ppr binds
1165 ; return (dict', binds)
1169 -- TOMDO: What do we have to do about ImplicInst, Method, and LitInst??
1170 normaliseOneInst _isWanted _fun inst
1171 = do { inst' <- zonkInst inst
1172 ; traceTc $ text "*** TcTyFuns.normaliseOneInst: Skipping" <+>
1174 ; return (inst', emptyBag)
1179 %************************************************************************
1183 %************************************************************************
1185 The infamous couldn't match expected type soandso against inferred type
1186 somethingdifferent message.
1189 eqInstMisMatch :: Inst -> TcM a
1191 = ASSERT( isEqInst inst )
1192 setErrCtxt ctxt $ failWithMisMatch ty_act ty_exp
1194 (ty_act, ty_exp) = eqInstTys inst
1195 InstLoc _ _ ctxt = instLoc inst
1197 -----------------------
1198 failWithMisMatch :: TcType -> TcType -> TcM a
1199 -- Generate the message when two types fail to match,
1200 -- going to some trouble to make it helpful.
1201 -- The argument order is: actual type, expected type
1202 failWithMisMatch ty_act ty_exp
1203 = do { env0 <- tcInitTidyEnv
1204 ; ty_exp <- zonkTcType ty_exp
1205 ; ty_act <- zonkTcType ty_act
1206 ; failWithTcM (misMatchMsg env0 (ty_act, ty_exp))
1209 misMatchMsg :: TidyEnv -> (TcType, TcType) -> (TidyEnv, SDoc)
1210 misMatchMsg env0 (ty_act, ty_exp)
1211 = let (env1, pp_exp, extra_exp) = ppr_ty env0 ty_exp
1212 (env2, pp_act, extra_act) = ppr_ty env1 ty_act
1213 msg = sep [sep [ptext SLIT("Couldn't match expected type") <+> pp_exp,
1215 ptext SLIT("against inferred type") <+> pp_act],
1216 nest 2 (extra_exp $$ extra_act)]
1221 ppr_ty :: TidyEnv -> TcType -> (TidyEnv, SDoc, SDoc)
1223 = let (env1, tidy_ty) = tidyOpenType env ty
1224 (env2, extra) = ppr_extra env1 tidy_ty
1226 (env2, quotes (ppr tidy_ty), extra)
1228 -- (ppr_extra env ty) shows extra info about 'ty'
1229 ppr_extra :: TidyEnv -> Type -> (TidyEnv, SDoc)
1230 ppr_extra env (TyVarTy tv)
1231 | isTcTyVar tv && (isSkolemTyVar tv || isSigTyVar tv) && not (isUnk tv)
1232 = (env1, pprSkolTvBinding tv1)
1234 (env1, tv1) = tidySkolemTyVar env tv
1236 ppr_extra env _ty = (env, empty) -- Normal case