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 (NoteTy note ty1)
233 = do { (coi,nty1) <- tcGenericNormaliseFamInst fun ty1
234 ; return (coi, NoteTy note nty1)
236 tcGenericNormaliseFamInst fun ty@(TyVarTy tv)
238 = do { traceTc (text "tcGenericNormaliseFamInst" <+> ppr ty)
239 ; res <- lookupTcTyVar tv
242 do { maybe_ty' <- fun ty
244 Nothing -> return (IdCo, ty)
246 do { (coi2, ty'') <- tcGenericNormaliseFamInst fun ty'
247 ; return (ACo co1 `mkTransCoI` coi2, ty'')
250 IndirectTv ty' -> tcGenericNormaliseFamInst fun ty'
254 tcGenericNormaliseFamInst fun (PredTy predty)
255 = do { (coi, pred') <- tcGenericNormaliseFamInstPred fun predty
256 ; return (coi, PredTy pred') }
258 ---------------------------------
259 tcGenericNormaliseFamInstPred :: (TcType -> TcM (Maybe (TcType,Coercion)))
261 -> TcM (CoercionI, TcPredType)
263 tcGenericNormaliseFamInstPred fun (ClassP cls tys)
264 = do { (cois, tys')<- mapAndUnzipM (tcGenericNormaliseFamInst fun) tys
265 ; return (mkClassPPredCoI cls tys' cois, ClassP cls tys')
267 tcGenericNormaliseFamInstPred fun (IParam ipn ty)
268 = do { (coi, ty') <- tcGenericNormaliseFamInst fun ty
269 ; return $ (mkIParamPredCoI ipn coi, IParam ipn ty')
271 tcGenericNormaliseFamInstPred fun (EqPred ty1 ty2)
272 = do { (coi1, ty1') <- tcGenericNormaliseFamInst fun ty1
273 ; (coi2, ty2') <- tcGenericNormaliseFamInst fun ty2
274 ; return (mkEqPredCoI ty1' coi1 ty2' coi2, EqPred ty1' ty2') }
278 %************************************************************************
280 \section{Normalisation of equality constraints}
282 %************************************************************************
284 Note [Inconsistencies in equality constraints]
285 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
286 We guarantee that we raise an error if we discover any inconsistencies (i.e.,
287 equalities that if presented to the unifer in TcUnify would result in an
288 error) during normalisation of wanted constraints. This is especially so that
289 we don't solve wanted constraints under an inconsistent given set. In
290 particular, we don't want to permit signatures, such as
292 bad :: (Int ~ Bool => Int) -> a -> a
295 normaliseGivenEqs :: [Inst] -> TcM ([Inst], TcM ())
296 normaliseGivenEqs givens
297 = do { traceTc (text "normaliseGivenEqs <-" <+> ppr givens)
298 ; (result, deSkolem) <-
299 rewriteToFixedPoint (Just ("(SkolemOccurs)", skolemOccurs))
300 [ ("(ZONK)", dontRerun $ zonkInsts)
301 , ("(TRIVIAL)", dontRerun $ trivialRule)
302 , ("(DECOMP)", decompRule)
304 , ("(SUBST)", substRule) -- incl. occurs check
306 ; traceTc (text "normaliseGivenEqs ->" <+> ppr result)
307 ; return (result, deSkolem)
312 normaliseWantedEqs :: [Inst] -- givens
314 -> TcM [Inst] -- irreducible wanteds
315 normaliseWantedEqs givens wanteds
316 = do { traceTc $ text "normaliseWantedEqs <-" <+> ppr wanteds
317 <+> text "with" <+> ppr givens
318 ; result <- liftM fst $ rewriteToFixedPoint Nothing
319 [ ("(ZONK)", dontRerun $ zonkInsts)
320 , ("(TRIVIAL)", dontRerun $ trivialRule)
321 , ("(DECOMP)", decompRule)
323 , ("(GIVEN)", substGivens givens) -- incl. occurs check
324 , ("(UNIFY)", unifyMetaRule) -- incl. occurs check
325 , ("(SUBST)", substRule) -- incl. occurs check
327 ; traceTc (text "normaliseWantedEqs ->" <+> ppr result)
331 -- Use `substInst' with every given on all the wanteds.
332 substGivens :: [Inst] -> [Inst] -> TcM ([Inst], Bool)
333 substGivens [] wanteds = return (wanteds, False)
334 substGivens (g:gs) wanteds
335 = do { (wanteds1, changed1) <- substGivens gs wanteds
336 ; (wanteds2, changed2) <- substInst g wanteds1
337 ; return (wanteds2, changed1 || changed2)
342 %************************************************************************
344 \section{Normalisation of non-equality dictionaries}
346 %************************************************************************
349 normaliseGivenDicts, normaliseWantedDicts
350 :: [Inst] -- given equations
351 -> [Inst] -- dictionaries
352 -> TcM ([Inst],TcDictBinds)
354 normaliseGivenDicts eqs dicts = normalise_dicts eqs dicts False
355 normaliseWantedDicts eqs dicts = normalise_dicts eqs dicts True
358 :: [Inst] -- given equations
359 -> [Inst] -- dictionaries
360 -> Bool -- True <=> the dicts are wanted
361 -- Fals <=> they are given
362 -> TcM ([Inst],TcDictBinds)
363 normalise_dicts given_eqs dicts is_wanted
364 = do { traceTc $ let name | is_wanted = "normaliseWantedDicts <-"
365 | otherwise = "normaliseGivenDicts <-"
367 text name <+> ppr dicts <+>
368 text "with" <+> ppr given_eqs
369 ; (dicts0, binds0) <- normaliseInsts is_wanted dicts
370 ; (dicts1, binds1) <- substEqInDictInsts is_wanted given_eqs dicts0
371 ; let binds01 = binds0 `unionBags` binds1
372 ; if isEmptyBag binds1
373 then return (dicts1, binds01)
374 else do { (dicts2, binds2) <-
375 normalise_dicts given_eqs dicts1 is_wanted
376 ; return (dicts2, binds01 `unionBags` binds2) } }
380 %************************************************************************
382 \section{Normalisation rules and iterative rule application}
384 %************************************************************************
386 We have three kinds of normalising rewrite rules:
388 (1) Normalisation rules that rewrite a set of insts and return a flag indicating
389 whether any changes occurred during rewriting that necessitate re-running
390 the current rule set.
392 (2) Precondition rules that rewrite a set of insts and return a monadic action
393 that reverts the effect of preconditioning.
395 (3) Idempotent normalisation rules that never require re-running the rule set.
398 type RewriteRule = [Inst] -> TcM ([Inst], Bool) -- rewrite, maybe re-run
399 type PrecondRule = [Inst] -> TcM ([Inst], TcM ()) -- rewrite, revertable
400 type IdemRewriteRule = [Inst] -> TcM [Inst] -- rewrite, don't re-run
402 type NamedRule = (String, RewriteRule) -- rule with description
403 type NamedPreRule = (String, PrecondRule) -- precond with desc
406 Template lifting idempotent rules to full rules (which can be put into a rule
410 dontRerun :: IdemRewriteRule -> RewriteRule
411 dontRerun rule insts = liftM addFalse $ rule insts
413 addFalse x = (x, False)
416 The following function applies a set of rewrite rules until a fixed point is
417 reached; i.e., none of the `RewriteRule's require re-running the rule set.
418 Optionally, there may be a pre-conditing rule that is applied before any other
419 rules are applied and before the rule set is re-run.
421 The result is the set of rewritten (i.e., normalised) insts and, in case of a
422 pre-conditing rule, a monadic action that reverts the effects of
423 pre-conditioning - specifically, this is removing introduced skolems.
426 rewriteToFixedPoint :: Maybe NamedPreRule -- optional preconditioning rule
427 -> [NamedRule] -- rule set
428 -> [Inst] -- insts to rewrite
429 -> TcM ([Inst], TcM ())
430 rewriteToFixedPoint precondRule rules insts
431 = completeRewrite (return ()) precondRule insts
433 completeRewrite :: TcM () -> Maybe NamedPreRule -> [Inst]
434 -> TcM ([Inst], TcM ())
435 completeRewrite dePrecond (Just (precondName, precond)) insts
436 = do { traceTc $ text precondName <+> text " <- " <+> ppr insts
437 ; (insts', dePrecond') <- precond insts
438 ; traceTc $ text precondName <+> text " -> " <+> ppr insts'
439 ; tryRules (dePrecond >> dePrecond') rules insts'
441 completeRewrite dePrecond Nothing insts
442 = tryRules dePrecond rules insts
444 tryRules dePrecond _ [] = return ([] , dePrecond)
445 tryRules dePrecond [] insts = return (insts, dePrecond)
446 tryRules dePrecond ((name, rule):rules) insts
447 = do { traceTc $ text name <+> text " <- " <+> ppr insts
448 ; (insts', rerun) <- rule insts
449 ; traceTc $ text name <+> text " -> " <+> ppr insts'
450 ; if rerun then completeRewrite dePrecond precondRule insts'
451 else tryRules dePrecond rules insts'
456 %************************************************************************
458 \section{Different forms of Inst rewrite rules}
460 %************************************************************************
462 Splitting of non-terminating given constraints: skolemOccurs
463 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
464 This is a preconditioning rule exclusively applied to given constraints.
465 Moreover, its rewriting is only temporary, as it is undone by way of
466 side-effecting mutable type variables after simplification and constraint
467 entailment has been completed.
469 This version is an (attempt at, yet unproven, an) *unflattened* version of
470 the SubstL-Ev completion rule.
472 The above rule is essential to catch non-terminating rules that cannot be
473 oriented properly, like
477 a ~ [G a] , where a is a skolem tyvar
479 The left-to-right orientiation is not suitable because it does not
480 terminate. The right-to-left orientation is not suitable because it
481 does not have a type-function on the left. This is undesirable because
482 it would hide information. E.g. assume
486 then rewriting C [G (F a)] to C (F a) is bad because we cannot now
487 see that the C [x] instance applies.
489 The rule also caters for badly-oriented rules of the form:
493 for which other solutions are possible, but this one will do too.
497 co : ty1 ~ ty2{F ty1}
500 sym (F co) : F ty2{b} ~ b
501 where b is a fresh skolem variable
503 We also cater for the symmetric situation *if* the rule cannot be used as a
504 left-to-right rewrite rule.
506 We also return an action (b := ty1) which is used to eliminate b
507 after the dust of normalisation with the completed rewrite system
510 A subtle point of this transformation is that both coercions in the results
511 are strictly speaking incorrect. However, they are correct again after the
512 action {B := ty1} has removed the skolem again. This happens immediately
513 after constraint entailment has been checked; ie, code outside of the
514 simplification and entailment checking framework will never see these
515 temporarily incorrect coercions.
517 NB: We perform this transformation for multiple occurences of ty1 under one
518 or multiple family applications on the left-hand side at once (ie, the
519 rule doesn't need to be applied multiple times at a single inst). As a
520 result we can get two or more insts back.
522 Note [skolemOccurs loop]
523 ~~~~~~~~~~~~~~~~~~~~~~~~
524 You might think that under
527 type instance F [a] = [F a]
531 foo :: (F [a] ~ a) => a
533 will get us into a loop. However, this is *not* the case. Here is why:
544 F [b<tau>] ~ b<tau> , with b := F a
549 [F b<tau>] ~ b<tau> , with b := F a
551 At this point (SkolemOccurs) does *not* apply anymore, as
555 is not used as a rewrite rule. The variable b<tau> is not a skolem (cf
558 (The regression test indexed-types/should_compile/Simple20 checks that the
559 described property of the system does not change.)
562 skolemOccurs :: PrecondRule
564 = do { (instss, undoSkolems) <- mapAndUnzipM oneSkolemOccurs insts
565 ; return (concat instss, sequence_ undoSkolems)
569 = ASSERT( isEqInst inst )
570 case eqInstToRewrite inst of
571 Just (rewrite, swapped) -> breakRecursion rewrite swapped
572 Nothing -> return ([inst], return ())
574 -- inst is an elementary rewrite rule, check whether we need to break
576 breakRecursion (Rewrite pat body _) swapped
578 -- skolemOccurs does not apply, leave as is
580 = do { traceTc $ text "oneSkolemOccurs: no tys to lift out"
581 ; return ([inst], return ())
584 -- recursive occurence of pat in body under a type family application
586 = do { traceTc $ text "oneSkolemOccurs[TLO]:" <+> ppr tysToLiftOut
587 ; skTvs <- mapM (newMetaTyVar TauTv . typeKind) tysToLiftOut
588 ; let skTvs_tysTLO = zip skTvs tysToLiftOut
589 insertSkolems = return . replace skTvs_tysTLO
590 ; (_, body') <- tcGenericNormaliseFamInst insertSkolems body
591 ; inst' <- if swapped then mkEqInst (EqPred body' pat) co
592 else mkEqInst (EqPred pat body') co
593 -- ensure to reconstruct the inst in the
594 -- original orientation
595 ; traceTc $ text "oneSkolemOccurs[inst']:" <+> ppr inst'
596 ; (insts, undoSk) <- mapAndUnzipM (mkSkolemInst inst')
598 ; return (inst':insts, sequence_ undoSk)
601 co = eqInstCoercion inst
603 -- all subtypes that are (1) type family instances and (2) contain
604 -- the lhs type as part of the type arguments of the type family
606 tysToLiftOut = [mkTyConApp tc tys | (tc, tys) <- tyFamInsts body
607 , any (pat `tcPartOfType`) tys]
609 replace :: [(TcTyVar, Type)] -> Type -> Maybe (Type, Coercion)
610 replace [] _ = Nothing
611 replace ((skTv, tyTLO):rest) ty
612 | tyTLO `tcEqType` ty = Just (mkTyVarTy skTv, undefined)
613 | otherwise = replace rest ty
615 -- create the EqInst for the equality determining the skolem and a
616 -- TcM action undoing the skolem introduction
617 mkSkolemInst inst' (skTv, tyTLO)
618 = do { (co, tyLiftedOut) <- tcEqInstNormaliseFamInst inst' tyTLO
619 ; inst <- mkEqInst (EqPred tyLiftedOut (mkTyVarTy skTv))
620 (mkGivenCo $ mkSymCoercion (fromACo co))
621 -- co /= IdCo due to construction of inst'
622 ; return (inst, writeMetaTyVar skTv tyTLO)
627 Removal of trivial equalities: trivialRule
628 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
629 The following rules exploits the reflexivity of equality:
637 trivialRule :: IdemRewriteRule
639 = liftM catMaybes $ mapM trivial insts
642 | ASSERT( isEqInst inst )
644 = do { eitherEqInst inst
645 (\cotv -> writeMetaTyVar cotv ty1)
652 (ty1,ty2) = eqInstTys inst
656 Decomposition of data type constructors: decompRule
657 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
658 Whenever, the same *data* constructors occurs on both sides of an equality, we
659 can decompose as in standard unification.
664 g21 : c1 ~ d1, ..., g2n : cn ~ dn
667 Works also for the case where T is actually an application of a type family
668 constructor to a set of types, provided the applications on both sides of the
669 ~ are identical; see also Note [OpenSynTyCon app] in TcUnify.
671 We guarantee to raise an error for any inconsistent equalities;
672 cf Note [Inconsistencies in equality constraints].
675 decompRule :: RewriteRule
677 = do { (insts, changed) <- mapAndUnzipM decomp insts
678 ; return (concat insts, or changed)
682 = ASSERT( isEqInst inst )
685 (ty1,ty2) = eqInstTys inst
687 | Just ty1' <- tcView ty1 = go ty1' ty2
688 | Just ty2' <- tcView ty2 = go ty1 ty2'
690 go (TyConApp con1 tys1) (TyConApp con2 tys2)
691 | con1 == con2 && identicalHead
692 = mkArgInsts (mkTyConApp con1) tys1 tys2
694 | con1 /= con2 && not (isOpenSynTyCon con1 || isOpenSynTyCon con2)
695 -- not matching data constructors (of any flavour) are bad news
696 = eqInstMisMatch inst
699 (idxTys1, _) = splitAt n tys1
700 (idxTys2, _) = splitAt n tys2
701 identicalHead = not (isOpenSynTyCon con1) ||
702 idxTys1 `tcEqTypes` idxTys2
704 go (FunTy fun1 arg1) (FunTy fun2 arg2)
705 = mkArgInsts (\[funCo, argCo] -> mkFunTy funCo argCo) [fun1, arg1]
708 -- Applications need a bit of care!
709 -- They can match FunTy and TyConApp, so use splitAppTy_maybe
711 | Just (s2, t2) <- tcSplitAppTy_maybe ty2
712 = mkArgInsts (\[s, t] -> mkAppTy s t) [s1, t1] [s2, t2]
716 | Just (s1, t1) <- tcSplitAppTy_maybe ty1
717 = mkArgInsts (\[s, t] -> mkAppTy s t) [s1, t1] [s2, t2]
719 -- We already covered all the consistent cases of rigid types on both
720 -- sides; so, if we see two rigid types here, we discovered an
723 | isRigid ty1 && isRigid ty2
724 = eqInstMisMatch inst
726 -- We can neither assert consistency nor inconsistency => defer
727 go _ _ = return ([inst], False)
729 isRigid (TyConApp con _) = not (isOpenSynTyCon con)
730 isRigid (FunTy _ _) = True
731 isRigid (AppTy _ _) = True
734 -- Create insts for matching argument positions (ie, the bit after
735 -- '>-->' in the rule description above)
736 mkArgInsts con tys1 tys2
737 = do { cos <- eitherEqInst inst
738 -- old_co := Con1 cos
740 do { cotvs <- zipWithM newMetaCoVar tys1 tys2
741 ; let cos = map mkTyVarTy cotvs
742 ; writeMetaTyVar old_covar (con cos)
743 ; return $ map mkWantedCo cotvs
745 -- co_i := Con_i old_co
747 return $ map mkGivenCo $
748 mkRightCoercions (length tys1) old_co)
749 ; insts <- zipWithM mkEqInst (zipWith EqPred tys1 tys2) cos
750 ; traceTc (text "decomp identicalHead" <+> ppr insts)
751 ; return (insts, not $ null insts)
756 Rewriting with type instances: topRule
757 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
758 We use (toplevel) type instances to normalise both sides of equalities.
762 >--> co1 :: t ~ t' / co2 :: s ~ s'
764 g1 := co1 * g2 * sym co2
767 topRule :: RewriteRule
769 = do { (insts, changed) <- mapAndUnzipM top insts
770 ; return (insts, or changed)
774 = ASSERT( isEqInst inst )
775 do { (coi1, ty1') <- tcNormaliseFamInst ty1
776 ; (coi2, ty2') <- tcNormaliseFamInst ty2
777 ; case (coi1, coi2) of
778 (IdCo, IdCo) -> return (inst, False)
782 -- old_co = co1 * new_co * sym co2
784 do { new_cotv <- newMetaCoVar ty1' ty2'
785 ; let new_co = mkTyVarTy new_cotv
786 old_coi = coi1 `mkTransCoI`
787 ACo new_co `mkTransCoI`
789 ; writeMetaTyVar old_covar (fromACo old_coi)
790 ; return $ mkWantedCo new_cotv
792 -- new_co = sym co1 * old_co * co2
797 mkSymCoI coi1 `mkTransCoI`
798 ACo old_co `mkTransCoI` coi2)
799 ; new_inst <- mkEqInst (EqPred ty1' ty2') wg_co
800 ; return (new_inst, True)
804 (ty1,ty2) = eqInstTys inst
808 Rewriting with equalities: substRule
809 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
810 From a set of insts, use all insts that can be read as rewrite rules to
811 rewrite the types in all other insts.
815 forall g1 : s1{F c} ~ s2{F c}
818 g1 := s1{g} * g2 * sym s2{g} <=> g2 := sym s1{g} * g1 * s2{g}
820 Alternatively, the rewrite rule may have the form (g : a ~ t).
822 To avoid having to swap rules of the form (g : t ~ F c) and (g : t ~ a),
823 where t is neither a variable nor a type family application, we use them for
824 rewriting from right-to-left. However, it is crucial to only apply rules
825 from right-to-left if they cannot be used left-to-right.
827 The workhorse is substInst, which performs an occurs check before actually
828 using an equality for rewriting. If the type pattern occurs in the type we
829 substitute for the pattern, normalisation would diverge.
832 substRule :: RewriteRule
833 substRule insts = tryAllInsts insts []
835 -- for every inst check whether it can be used to rewrite the others
836 -- (we make an effort to keep the insts in order; it makes debugging
838 tryAllInsts [] triedInsts = return (reverse triedInsts, False)
839 tryAllInsts (inst:insts) triedInsts
840 = do { (insts', changed) <- substInst inst (reverse triedInsts ++ insts)
841 ; if changed then return (insertAt (length triedInsts) inst insts',
843 else tryAllInsts insts (inst:triedInsts)
846 insertAt n x xs = let (xs1, xs2) = splitAt n xs
849 -- Use the given inst as a rewrite rule to normalise the insts in the second
850 -- argument. Don't do anything if the inst cannot be used as a rewrite rule,
851 -- but do apply it right-to-left, if possible, and if it cannot be used
854 substInst :: Inst -> [Inst] -> TcM ([Inst], Bool)
856 = case eqInstToRewrite inst of
857 Just (rewrite, _) -> substEquality rewrite insts
858 Nothing -> return (insts, False)
860 substEquality :: Rewrite -- elementary rewrite
861 -> [Inst] -- insts to rewrite
862 -> TcM ([Inst], Bool)
863 substEquality eqRule@(Rewrite pat rhs _) insts
864 | pat `tcPartOfType` rhs -- occurs check!
865 = occurCheckErr pat rhs
867 = do { (insts', changed) <- mapAndUnzipM substOne insts
868 ; return (insts', or changed)
872 = ASSERT( isEqInst inst )
873 do { (coi1, ty1') <- tcEqRuleNormaliseFamInst eqRule ty1
874 ; (coi2, ty2') <- tcEqRuleNormaliseFamInst eqRule ty2
875 ; case (coi1, coi2) of
876 (IdCo, IdCo) -> return (inst, False)
880 -- old_co := co1 * new_co * sym co2
882 do { new_cotv <- newMetaCoVar ty1' ty2'
883 ; let new_co = mkTyVarTy new_cotv
884 old_coi = coi1 `mkTransCoI`
885 ACo new_co `mkTransCoI`
887 ; writeMetaTyVar old_covar (fromACo old_coi)
888 ; return $ mkWantedCo new_cotv
890 -- new_co := sym co1 * old_co * co2
895 mkSymCoI coi1 `mkTransCoI`
896 ACo old_co `mkTransCoI` coi2)
897 ; new_inst <- mkEqInst (EqPred ty1' ty2') gw_co
898 ; return (new_inst, True)
902 (ty1,ty2) = eqInstTys inst
906 Instantiate meta variables: unifyMetaRule
907 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
908 If an equality equates a meta type variable with a type, we simply instantiate
917 Meta variables can only appear in wanted constraints, and this rule should
918 only be applied to wanted constraints. We also know that t definitely is
919 distinct from alpha (as the trivialRule) has been run on the insts beforehand.
921 NB: We cannot assume that meta tyvars are empty. They may have been updated
922 by another inst in the currently processed wanted list. We need to be very
923 careful when updateing type variables (see TcUnify.uUnfilledVar), but at least
924 we know that we have no boxes. It's unclear that it would be an advantage to
925 common up the code in TcUnify and the code below. Firstly, we don't want
926 calls to TcUnify.defer_unification here, and secondly, TcUnify import the
927 current module, so we would have to move everything here (Yuk!) or to
928 TcMType. Besides, the code here is much simpler due to the lack of boxes.
931 unifyMetaRule :: RewriteRule
933 = do { (insts', changed) <- mapAndUnzipM unifyMeta insts
934 ; return (concat insts', or changed)
938 = ASSERT( isEqInst inst )
940 (fromWantedCo "unifyMetaRule" $ eqInstCoercion inst)
942 (ty1,ty2) = eqInstTys inst
944 | Just ty1' <- tcView ty1 = go ty1' ty2 cotv
945 | Just ty2' <- tcView ty2 = go ty1 ty2' cotv
948 , isMetaTyVar tv1 = do { lookupTV <- lookupTcTyVar tv1
949 ; uMeta False tv1 lookupTV ty2 cotv
952 , isMetaTyVar tv2 = do { lookupTV <- lookupTcTyVar tv2
953 ; uMeta True tv2 lookupTV ty1 cotv
955 | otherwise = return ([inst], False)
957 -- meta variable has been filled already
958 -- => ignore this inst (we'll come around again, after zonking)
959 uMeta _swapped _tv (IndirectTv _) _ty _cotv
960 = return ([inst], False)
962 -- type variable meets type variable
963 -- => check that tv2 hasn't been updated yet and choose which to update
964 uMeta swapped tv1 (DoneTv details1) (TyVarTy tv2) cotv
966 = return ([inst], False) -- The two types are already identical
969 = do { lookupTV2 <- lookupTcTyVar tv2
971 IndirectTv ty -> uMeta swapped tv1 (DoneTv details1) ty cotv
972 DoneTv details2 -> uMetaVar swapped tv1 details1 tv2 details2 cotv
975 ------ Beyond this point we know that ty2 is not a type variable
977 -- signature skolem meets non-variable type
979 uMeta _swapped _tv (DoneTv (MetaTv (SigTv _) _)) _non_tv_ty _cotv
980 = return ([inst], False)
982 -- updatable meta variable meets non-variable type
983 -- => occurs check, monotype check, and kinds match check, then update
984 uMeta swapped tv (DoneTv (MetaTv _ ref)) non_tv_ty cotv
985 = do { mb_ty' <- checkTauTvUpdate tv non_tv_ty -- occurs + monotype check
987 Nothing -> return ([inst], False) -- tv occurs in faminst
989 do { checkUpdateMeta swapped tv ref ty' -- update meta var
990 ; writeMetaTyVar cotv ty' -- update co var
995 uMeta _ _ _ _ _ = panic "uMeta"
997 -- uMetaVar: unify two type variables
998 -- meta variable meets skolem
1000 uMetaVar swapped tv1 (MetaTv _ ref) tv2 (SkolemTv _) cotv
1001 = do { checkUpdateMeta swapped tv1 ref (mkTyVarTy tv2)
1002 ; writeMetaTyVar cotv (mkTyVarTy tv2)
1006 -- meta variable meets meta variable
1007 -- => be clever about which of the two to update
1008 -- (from TcUnify.uUnfilledVars minus boxy stuff)
1009 uMetaVar swapped tv1 (MetaTv info1 ref1) tv2 (MetaTv info2 ref2) cotv
1010 = do { case (info1, info2) of
1011 -- Avoid SigTvs if poss
1012 (SigTv _, _ ) | k1_sub_k2 -> update_tv2
1013 (_, SigTv _) | k2_sub_k1 -> update_tv1
1015 (_, _) | k1_sub_k2 -> if k2_sub_k1 && nicer_to_update_tv1
1016 then update_tv1 -- Same kinds
1018 | k2_sub_k1 -> update_tv1
1019 | otherwise -> kind_err
1020 -- Update the variable with least kind info
1021 -- See notes on type inference in Kind.lhs
1022 -- The "nicer to" part only applies if the two kinds are the same,
1023 -- so we can choose which to do.
1025 ; writeMetaTyVar cotv (mkTyVarTy tv2)
1029 -- Kinds should be guaranteed ok at this point
1030 update_tv1 = updateMeta tv1 ref1 (mkTyVarTy tv2)
1031 update_tv2 = updateMeta tv2 ref2 (mkTyVarTy tv1)
1033 kind_err = addErrCtxtM (unifyKindCtxt swapped tv1 (mkTyVarTy tv2)) $
1034 unifyKindMisMatch k1 k2
1038 k1_sub_k2 = k1 `isSubKind` k2
1039 k2_sub_k1 = k2 `isSubKind` k1
1041 nicer_to_update_tv1 = isSystemName (Var.varName tv1)
1042 -- Try to update sys-y type variables in preference to ones
1043 -- gotten (say) by instantiating a polymorphic function with
1044 -- a user-written type sig
1046 uMetaVar _ _ _ _ _ _ = panic "uMetaVar"
1050 %************************************************************************
1052 \section{Normalisation of Insts}
1054 %************************************************************************
1056 Normalises a set of dictionaries relative to a set of given equalities (which
1057 are interpreted as rewrite rules). We only consider given equalities of the
1062 where F is a type family.
1065 substEqInDictInsts :: Bool -- whether the *dictionaries* are wanted/given
1066 -> [Inst] -- given equalities (used as rewrite rules)
1067 -> [Inst] -- dictinaries to be normalised
1068 -> TcM ([Inst], TcDictBinds)
1069 substEqInDictInsts isWanted eqInsts dictInsts
1070 = do { traceTc (text "substEqInDictInst <-" <+> ppr dictInsts)
1072 foldlM rewriteWithOneEquality (dictInsts, emptyBag) eqInsts
1073 ; traceTc (text "substEqInDictInst ->" <+> ppr dictInsts')
1077 -- (1) Given equality of form 'F ts ~ t' or 'a ~ t': use for rewriting
1078 rewriteWithOneEquality (dictInsts, dictBinds)
1079 eqInst@(EqInst {tci_left = pattern,
1080 tci_right = target})
1081 | isOpenSynTyConApp pattern || isTyVarTy pattern
1082 = do { (dictInsts', moreDictBinds) <-
1083 genericNormaliseInsts isWanted applyThisEq dictInsts
1084 ; return (dictInsts', dictBinds `unionBags` moreDictBinds)
1087 applyThisEq = tcGenericNormaliseFamInstPred (return . matchResult)
1089 -- rewrite in case of an exact match
1090 matchResult ty | tcEqType pattern ty = Just (target, eqInstType eqInst)
1091 | otherwise = Nothing
1093 -- (2) Given equality has the wrong form: ignore
1094 rewriteWithOneEquality (dictInsts, dictBinds) _not_a_rewrite_rule
1095 = return (dictInsts, dictBinds)
1099 Take a bunch of Insts (not EqInsts), and normalise them wrt the top-level
1100 type-function equations, where
1102 (norm_insts, binds) = normaliseInsts is_wanted insts
1105 = True, (binds + norm_insts) defines insts (wanteds)
1106 = False, (binds + insts) defines norm_insts (givens)
1108 Ie, in the case of normalising wanted dictionaries, we use the normalised
1109 dictionaries to define the originally wanted ones. However, in the case of
1110 given dictionaries, we use the originally given ones to define the normalised
1114 normaliseInsts :: Bool -- True <=> wanted insts
1115 -> [Inst] -- wanted or given insts
1116 -> TcM ([Inst], TcDictBinds) -- normalised insts and bindings
1117 normaliseInsts isWanted insts
1118 = genericNormaliseInsts isWanted tcNormaliseFamInstPred insts
1120 genericNormaliseInsts :: Bool -- True <=> wanted insts
1121 -> (TcPredType -> TcM (CoercionI, TcPredType))
1123 -> [Inst] -- wanted or given insts
1124 -> TcM ([Inst], TcDictBinds) -- normalised insts & binds
1125 genericNormaliseInsts isWanted fun insts
1126 = do { (insts', binds) <- mapAndUnzipM (normaliseOneInst isWanted fun) insts
1127 ; return (insts', unionManyBags binds)
1130 normaliseOneInst isWanted fun
1131 dict@(Dict {tci_pred = pred,
1133 = do { traceTc $ text "genericNormaliseInst <-" <+> ppr dict
1134 ; (coi, pred') <- fun pred
1138 do { traceTc $ text "genericNormaliseInst ->" <+> ppr dict
1139 ; return (dict, emptyBag)
1141 -- don't use pred' in this case; otherwise, we get
1142 -- more unfolded closed type synonyms in error messages
1144 do { -- an inst for the new pred
1145 ; dict' <- newDictBndr loc pred'
1146 -- relate the old inst to the new one
1147 -- target_dict = source_dict `cast` st_co
1148 ; let (target_dict, source_dict, st_co)
1149 | isWanted = (dict, dict', mkSymCoercion co)
1150 | otherwise = (dict', dict, co)
1152 -- co :: dict ~ dict'
1153 -- hence, if isWanted
1154 -- dict = dict' `cast` sym co
1156 -- dict' = dict `cast` co
1157 expr = HsVar $ instToId source_dict
1158 cast_expr = HsWrap (WpCo st_co) expr
1159 rhs = L (instLocSpan loc) cast_expr
1160 binds = instToDictBind target_dict rhs
1161 -- return the new inst
1162 ; traceTc $ let name | isWanted
1163 = "genericNormaliseInst (wanted) ->"
1165 = "genericNormaliseInst (given) ->"
1167 text name <+> ppr dict' <+>
1168 text "with" <+> ppr binds
1169 ; return (dict', binds)
1173 -- TOMDO: What do we have to do about ImplicInst, Method, and LitInst??
1174 normaliseOneInst _isWanted _fun inst
1175 = do { inst' <- zonkInst inst
1176 ; traceTc $ text "*** TcTyFuns.normaliseOneInst: Skipping" <+>
1178 ; return (inst', emptyBag)
1183 %************************************************************************
1187 %************************************************************************
1189 The infamous couldn't match expected type soandso against inferred type
1190 somethingdifferent message.
1193 eqInstMisMatch :: Inst -> TcM a
1195 = ASSERT( isEqInst inst )
1196 setErrCtxt ctxt $ failWithMisMatch ty_act ty_exp
1198 (ty_act, ty_exp) = eqInstTys inst
1199 InstLoc _ _ ctxt = instLoc inst
1201 -----------------------
1202 failWithMisMatch :: TcType -> TcType -> TcM a
1203 -- Generate the message when two types fail to match,
1204 -- going to some trouble to make it helpful.
1205 -- The argument order is: actual type, expected type
1206 failWithMisMatch ty_act ty_exp
1207 = do { env0 <- tcInitTidyEnv
1208 ; ty_exp <- zonkTcType ty_exp
1209 ; ty_act <- zonkTcType ty_act
1210 ; failWithTcM (misMatchMsg env0 (ty_act, ty_exp))
1213 misMatchMsg :: TidyEnv -> (TcType, TcType) -> (TidyEnv, SDoc)
1214 misMatchMsg env0 (ty_act, ty_exp)
1215 = let (env1, pp_exp, extra_exp) = ppr_ty env0 ty_exp
1216 (env2, pp_act, extra_act) = ppr_ty env1 ty_act
1217 msg = sep [sep [ptext SLIT("Couldn't match expected type") <+> pp_exp,
1219 ptext SLIT("against inferred type") <+> pp_act],
1220 nest 2 (extra_exp $$ extra_act)]
1225 ppr_ty :: TidyEnv -> TcType -> (TidyEnv, SDoc, SDoc)
1227 = let (env1, tidy_ty) = tidyOpenType env ty
1228 (env2, extra) = ppr_extra env1 tidy_ty
1230 (env2, quotes (ppr tidy_ty), extra)
1232 -- (ppr_extra env ty) shows extra info about 'ty'
1233 ppr_extra :: TidyEnv -> Type -> (TidyEnv, SDoc)
1234 ppr_extra env (TyVarTy tv)
1235 | isTcTyVar tv && (isSkolemTyVar tv || isSigTyVar tv) && not (isUnk tv)
1236 = (env1, pprSkolTvBinding tv1)
1238 (env1, tv1) = tidySkolemTyVar env tv
1240 ppr_extra env _ty = (env, empty) -- Normal case