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,
13 misMatchMsg, failWithMisMatch
17 #include "HsVersions.h"
29 import TypeRep ( Type(..) )
37 import SrcLoc ( Located(..) )
46 %************************************************************************
48 Normalisation of types
50 %************************************************************************
52 Unfold a single synonym family instance and yield the witnessing coercion.
53 Return 'Nothing' if the given type is either not synonym family instance
54 or is a synonym family instance that has no matching instance declaration.
55 (Applies only if the type family application is outermost.)
57 For example, if we have
59 :Co:R42T a :: T [a] ~ :R42T a
61 then 'T [Int]' unfolds to (:R42T Int, :Co:R42T Int).
64 tcUnfoldSynFamInst :: Type -> TcM (Maybe (Type, Coercion))
65 tcUnfoldSynFamInst (TyConApp tycon tys)
66 | not (isOpenSynTyCon tycon) -- unfold *only* _synonym_ family instances
69 = do { -- we only use the indexing arguments for matching,
70 -- not the additional ones
71 ; maybeFamInst <- tcLookupFamInst tycon idxTys
72 ; case maybeFamInst of
73 Nothing -> return Nothing
74 Just (rep_tc, rep_tys) -> return $ Just (mkTyConApp rep_tc tys',
75 mkTyConApp coe_tc tys')
77 tys' = rep_tys ++ restTys
78 coe_tc = expectJust "TcTyFun.tcUnfoldSynFamInst"
79 (tyConFamilyCoercion_maybe rep_tc)
83 (idxTys, restTys) = splitAt n tys
84 tcUnfoldSynFamInst _other = return Nothing
87 Normalise 'Type's and 'PredType's by unfolding type family applications where
88 possible (ie, we treat family instances as a TRS). Also zonk meta variables.
90 tcNormaliseFamInst ty = (co, ty')
94 tcNormaliseFamInst :: TcType -> TcM (CoercionI, TcType)
95 tcNormaliseFamInst = tcGenericNormaliseFamInst tcUnfoldSynFamInst
97 tcNormaliseFamInstPred :: TcPredType -> TcM (CoercionI, TcPredType)
98 tcNormaliseFamInstPred = tcGenericNormaliseFamInstPred tcUnfoldSynFamInst
101 An elementary rewrite is a properly oriented equality with associated coercion
102 that has one of the following two forms:
104 (1) co :: F t1..tn ~ t
105 (2) co :: a ~ t , where t /= F t1..tn and a is a skolem tyvar
107 NB: We do *not* use equalities of the form a ~ t where a is a meta tyvar as a
108 reqrite rule. Instead, such equalities are solved by unification. This is
109 essential; cf Note [skolemOccurs loop].
111 The following functions takes an equality instance and turns it into an
112 elementary rewrite if possible.
115 data Rewrite = Rewrite TcType -- lhs of rewrite rule
116 TcType -- rhs of rewrite rule
117 TcType -- coercion witnessing the rewrite rule
119 eqInstToRewrite :: Inst -> Maybe (Rewrite, Bool)
120 -- True iff rewrite swapped equality
122 = ASSERT( isEqInst inst )
123 go ty1 ty2 (eqInstType inst)
125 (ty1,ty2) = eqInstTys inst
127 -- look through synonyms
128 go ty1 ty2 co | Just ty1' <- tcView ty1 = go ty1' ty2 co
129 go ty1 ty2 co | Just ty2' <- tcView ty2 = go ty1 ty2' co
131 -- left-to-right rule with type family head
132 go ty1@(TyConApp con _) ty2 co
134 = Just (Rewrite ty1 ty2 co, False) -- not swapped
136 -- left-to-right rule with type variable head
137 go ty1@(TyVarTy tv) ty2 co
139 = Just (Rewrite ty1 ty2 co, False) -- not swapped
141 -- right-to-left rule with type family head, only after
142 -- having checked whether we can work left-to-right
143 go ty1 ty2@(TyConApp con _) co
145 = Just (Rewrite ty2 ty1 (mkSymCoercion co), True) -- swapped
147 -- right-to-left rule with type variable head, only after
148 -- having checked whether we can work left-to-right
149 go ty1 ty2@(TyVarTy tv) co
151 = Just (Rewrite ty2 ty1 (mkSymCoercion co), True) -- swapped
153 -- this equality is not a rewrite rule => ignore
157 Normalise a type relative to an elementary rewrite implied by an EqInst or an
158 explicitly given elementary rewrite.
162 -- Precondition: the EqInst passes the occurs check
163 tcEqInstNormaliseFamInst :: Inst -> TcType -> TcM (CoercionI, TcType)
164 tcEqInstNormaliseFamInst inst ty
165 = case eqInstToRewrite inst of
166 Just (rewrite, _) -> tcEqRuleNormaliseFamInst rewrite ty
167 Nothing -> return (IdCo, ty)
169 -- Rewrite by equality rewrite rule
170 tcEqRuleNormaliseFamInst :: Rewrite -- elementary rewrite
171 -> TcType -- type to rewrite
172 -> TcM (CoercionI, -- witnessing coercion
173 TcType) -- rewritten type
174 tcEqRuleNormaliseFamInst (Rewrite pat rhs co) ty
175 = tcGenericNormaliseFamInst matchEqRule ty
177 matchEqRule sty | pat `tcEqType` sty = return $ Just (rhs, co)
178 | otherwise = return $ Nothing
181 Generic normalisation of 'Type's and 'PredType's; ie, walk the type term and
182 apply the normalisation function gives as the first argument to every TyConApp
183 and every TyVarTy subterm.
185 tcGenericNormaliseFamInst fun ty = (co, ty')
188 This function is (by way of using smart constructors) careful to ensure that
189 the returned coercion is exactly IdCo (and not some semantically equivalent,
190 but syntactically different coercion) whenever (ty' `tcEqType` ty). This
191 makes it easy for the caller to determine whether the type changed. BUT
192 even if we return IdCo, ty' may be *syntactically* different from ty due to
193 unfolded closed type synonyms (by way of tcCoreView). In the interest of
194 good error messages, callers should discard ty' in favour of ty in this case.
197 tcGenericNormaliseFamInst :: (TcType -> TcM (Maybe (TcType, Coercion)))
198 -- what to do with type functions and tyvars
199 -> TcType -- old type
200 -> TcM (CoercionI, TcType) -- (coercion, new type)
201 tcGenericNormaliseFamInst fun ty
202 | Just ty' <- tcView ty = tcGenericNormaliseFamInst fun ty'
203 tcGenericNormaliseFamInst fun (TyConApp tyCon tys)
204 = do { (cois, ntys) <- mapAndUnzipM (tcGenericNormaliseFamInst fun) tys
205 ; let tycon_coi = mkTyConAppCoI tyCon ntys cois
206 ; maybe_ty_co <- fun (mkTyConApp tyCon ntys) -- use normalised args!
207 ; case maybe_ty_co of
208 -- a matching family instance exists
210 do { let first_coi = mkTransCoI tycon_coi (ACo co)
211 ; (rest_coi, nty) <- tcGenericNormaliseFamInst fun ty'
212 ; let fix_coi = mkTransCoI first_coi rest_coi
213 ; return (fix_coi, nty)
215 -- no matching family instance exists
216 -- we do not do anything
217 Nothing -> return (tycon_coi, mkTyConApp tyCon ntys)
219 tcGenericNormaliseFamInst fun (AppTy ty1 ty2)
220 = do { (coi1,nty1) <- tcGenericNormaliseFamInst fun ty1
221 ; (coi2,nty2) <- tcGenericNormaliseFamInst fun ty2
222 ; return (mkAppTyCoI nty1 coi1 nty2 coi2, mkAppTy nty1 nty2)
224 tcGenericNormaliseFamInst fun (FunTy ty1 ty2)
225 = do { (coi1,nty1) <- tcGenericNormaliseFamInst fun ty1
226 ; (coi2,nty2) <- tcGenericNormaliseFamInst fun ty2
227 ; return (mkFunTyCoI nty1 coi1 nty2 coi2, mkFunTy nty1 nty2)
229 tcGenericNormaliseFamInst fun (ForAllTy tyvar ty1)
230 = do { (coi,nty1) <- tcGenericNormaliseFamInst fun ty1
231 ; return (mkForAllTyCoI tyvar coi, mkForAllTy tyvar nty1)
233 tcGenericNormaliseFamInst fun (NoteTy note ty1)
234 = do { (coi,nty1) <- tcGenericNormaliseFamInst fun ty1
235 ; return (coi, NoteTy note nty1)
237 tcGenericNormaliseFamInst fun ty@(TyVarTy tv)
239 = do { traceTc (text "tcGenericNormaliseFamInst" <+> ppr ty)
240 ; res <- lookupTcTyVar tv
243 do { maybe_ty' <- fun ty
245 Nothing -> return (IdCo, ty)
247 do { (coi2, ty'') <- tcGenericNormaliseFamInst fun ty'
248 ; return (ACo co1 `mkTransCoI` coi2, ty'')
251 IndirectTv ty' -> tcGenericNormaliseFamInst fun ty'
255 tcGenericNormaliseFamInst fun (PredTy predty)
256 = do { (coi, pred') <- tcGenericNormaliseFamInstPred fun predty
257 ; return (coi, PredTy pred') }
259 ---------------------------------
260 tcGenericNormaliseFamInstPred :: (TcType -> TcM (Maybe (TcType,Coercion)))
262 -> TcM (CoercionI, TcPredType)
264 tcGenericNormaliseFamInstPred fun (ClassP cls tys)
265 = do { (cois, tys')<- mapAndUnzipM (tcGenericNormaliseFamInst fun) tys
266 ; return (mkClassPPredCoI cls tys' cois, ClassP cls tys')
268 tcGenericNormaliseFamInstPred fun (IParam ipn ty)
269 = do { (coi, ty') <- tcGenericNormaliseFamInst fun ty
270 ; return $ (mkIParamPredCoI ipn coi, IParam ipn ty')
272 tcGenericNormaliseFamInstPred fun (EqPred ty1 ty2)
273 = do { (coi1, ty1') <- tcGenericNormaliseFamInst fun ty1
274 ; (coi2, ty2') <- tcGenericNormaliseFamInst fun ty2
275 ; return (mkEqPredCoI ty1' coi1 ty2' coi2, EqPred ty1' ty2') }
279 %************************************************************************
281 \section{Normalisation of equality constraints}
283 %************************************************************************
285 Note [Inconsistencies in equality constraints]
286 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
287 We guarantee that we raise an error if we discover any inconsistencies (i.e.,
288 equalities that if presented to the unifer in TcUnify would result in an
289 error) during normalisation of wanted constraints. This is especially so that
290 we don't solve wanted constraints under an inconsistent given set. In
291 particular, we don't want to permit signatures, such as
293 bad :: (Int ~ Bool => Int) -> a -> a
296 normaliseGivenEqs :: [Inst] -> TcM ([Inst], TcM ())
297 normaliseGivenEqs givens
298 = do { traceTc (text "normaliseGivenEqs <-" <+> ppr givens)
299 ; (result, deSkolem) <-
300 rewriteToFixedPoint (Just ("(SkolemOccurs)", skolemOccurs))
301 [ ("(ZONK)", dontRerun $ zonkInsts)
302 , ("(TRIVIAL)", dontRerun $ trivialRule)
303 , ("(DECOMP)", decompRule)
305 , ("(SUBST)", substRule) -- incl. occurs check
307 ; traceTc (text "normaliseGivenEqs ->" <+> ppr result)
308 ; return (result, deSkolem)
313 normaliseWantedEqs :: [Inst] -> TcM [Inst]
314 normaliseWantedEqs insts
315 = do { traceTc (text "normaliseWantedEqs <-" <+> ppr insts)
316 ; result <- liftM fst $ rewriteToFixedPoint Nothing
317 [ ("(ZONK)", dontRerun $ zonkInsts)
318 , ("(TRIVIAL)", dontRerun $ trivialRule)
319 , ("(DECOMP)", decompRule)
321 , ("(UNIFY)", unifyMetaRule) -- incl. occurs check
322 , ("(SUBST)", substRule) -- incl. occurs check
324 ; traceTc (text "normaliseWantedEqs ->" <+> ppr result)
330 %************************************************************************
332 \section{Solving of wanted constraints with respect to a given set}
334 %************************************************************************
336 The set of given equalities must have been normalised already.
339 solveWantedEqs :: [Inst] -- givens
341 -> TcM [Inst] -- irreducible wanteds
342 solveWantedEqs givens wanteds
343 = do { traceTc $ text "solveWantedEqs <-" <+> ppr wanteds <+> text "with" <+>
345 ; result <- liftM fst $ rewriteToFixedPoint Nothing
346 [ ("(ZONK)", dontRerun $ zonkInsts)
347 , ("(TRIVIAL)", dontRerun $ trivialRule)
348 , ("(DECOMP)", decompRule)
350 , ("(GIVEN)", substGivens givens) -- incl. occurs check
351 , ("(UNIFY)", unifyMetaRule) -- incl. occurs check
353 ; traceTc (text "solveWantedEqs ->" <+> ppr result)
357 -- Use `substInst' with every given on all the wanteds.
358 substGivens :: [Inst] -> [Inst] -> TcM ([Inst], Bool)
359 substGivens [] wanteds = return (wanteds, False)
360 substGivens (g:gs) wanteds
361 = do { (wanteds1, changed1) <- substGivens gs wanteds
362 ; (wanteds2, changed2) <- substInst g wanteds1
363 ; return (wanteds2, changed1 || changed2)
368 %************************************************************************
370 \section{Normalisation of non-equality dictionaries}
372 %************************************************************************
375 normaliseGivenDicts, normaliseWantedDicts
376 :: [Inst] -- given equations
377 -> [Inst] -- dictionaries
378 -> TcM ([Inst],TcDictBinds)
380 normaliseGivenDicts eqs dicts = normalise_dicts eqs dicts False
381 normaliseWantedDicts eqs dicts = normalise_dicts eqs dicts True
384 :: [Inst] -- given equations
385 -> [Inst] -- dictionaries
386 -> Bool -- True <=> the dicts are wanted
387 -- Fals <=> they are given
388 -> TcM ([Inst],TcDictBinds)
389 normalise_dicts given_eqs dicts is_wanted
390 = do { traceTc $ let name | is_wanted = "normaliseWantedDicts <-"
391 | otherwise = "normaliseGivenDicts <-"
393 text name <+> ppr dicts <+>
394 text "with" <+> ppr given_eqs
395 ; (dicts0, binds0) <- normaliseInsts is_wanted dicts
396 ; (dicts1, binds1) <- substEqInDictInsts is_wanted given_eqs dicts0
397 ; let binds01 = binds0 `unionBags` binds1
398 ; if isEmptyBag binds1
399 then return (dicts1, binds01)
400 else do { (dicts2, binds2) <-
401 normalise_dicts given_eqs dicts1 is_wanted
402 ; return (dicts2, binds01 `unionBags` binds2) } }
406 %************************************************************************
408 \section{Normalisation rules and iterative rule application}
410 %************************************************************************
412 We have three kinds of normalising rewrite rules:
414 (1) Normalisation rules that rewrite a set of insts and return a flag indicating
415 whether any changes occurred during rewriting that necessitate re-running
416 the current rule set.
418 (2) Precondition rules that rewrite a set of insts and return a monadic action
419 that reverts the effect of preconditioning.
421 (3) Idempotent normalisation rules that never require re-running the rule set.
424 type RewriteRule = [Inst] -> TcM ([Inst], Bool) -- rewrite, maybe re-run
425 type PrecondRule = [Inst] -> TcM ([Inst], TcM ()) -- rewrite, revertable
426 type IdemRewriteRule = [Inst] -> TcM [Inst] -- rewrite, don't re-run
428 type NamedRule = (String, RewriteRule) -- rule with description
429 type NamedPreRule = (String, PrecondRule) -- precond with desc
432 Template lifting idempotent rules to full rules (which can be put into a rule
436 dontRerun :: IdemRewriteRule -> RewriteRule
437 dontRerun rule insts = liftM addFalse $ rule insts
439 addFalse x = (x, False)
442 The following function applies a set of rewrite rules until a fixed point is
443 reached; i.e., none of the `RewriteRule's require re-running the rule set.
444 Optionally, there may be a pre-conditing rule that is applied before any other
445 rules are applied and before the rule set is re-run.
447 The result is the set of rewritten (i.e., normalised) insts and, in case of a
448 pre-conditing rule, a monadic action that reverts the effects of
449 pre-conditioning - specifically, this is removing introduced skolems.
452 rewriteToFixedPoint :: Maybe NamedPreRule -- optional preconditioning rule
453 -> [NamedRule] -- rule set
454 -> [Inst] -- insts to rewrite
455 -> TcM ([Inst], TcM ())
456 rewriteToFixedPoint precondRule rules insts
457 = completeRewrite (return ()) precondRule insts
459 completeRewrite :: TcM () -> Maybe NamedPreRule -> [Inst]
460 -> TcM ([Inst], TcM ())
461 completeRewrite dePrecond (Just (precondName, precond)) insts
462 = do { traceTc $ text precondName <+> text " <- " <+> ppr insts
463 ; (insts', dePrecond') <- precond insts
464 ; traceTc $ text precondName <+> text " -> " <+> ppr insts'
465 ; tryRules (dePrecond >> dePrecond') rules insts'
467 completeRewrite dePrecond Nothing insts
468 = tryRules dePrecond rules insts
470 tryRules dePrecond _ [] = return ([] , dePrecond)
471 tryRules dePrecond [] insts = return (insts, dePrecond)
472 tryRules dePrecond ((name, rule):rules) insts
473 = do { traceTc $ text name <+> text " <- " <+> ppr insts
474 ; (insts', rerun) <- rule insts
475 ; traceTc $ text name <+> text " -> " <+> ppr insts'
476 ; if rerun then completeRewrite dePrecond precondRule insts'
477 else tryRules dePrecond rules insts'
482 %************************************************************************
484 \section{Different forms of Inst rewrite rules}
486 %************************************************************************
488 Splitting of non-terminating given constraints: skolemOccurs
489 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
490 This is a preconditioning rule exclusively applied to given constraints.
491 Moreover, its rewriting is only temporary, as it is undone by way of
492 side-effecting mutable type variables after simplification and constraint
493 entailment has been completed.
495 This version is an (attempt at, yet unproven, an) *unflattened* version of
496 the SubstL-Ev completion rule.
498 The above rule is essential to catch non-terminating rules that cannot be
499 oriented properly, like
503 a ~ [G a] , where a is a skolem tyvar
505 The left-to-right orientiation is not suitable because it does not
506 terminate. The right-to-left orientation is not suitable because it
507 does not have a type-function on the left. This is undesirable because
508 it would hide information. E.g. assume
512 then rewriting C [G (F a)] to C (F a) is bad because we cannot now
513 see that the C [x] instance applies.
515 The rule also caters for badly-oriented rules of the form:
519 for which other solutions are possible, but this one will do too.
523 co : ty1 ~ ty2{F ty1}
526 sym (F co) : F ty2{b} ~ b
527 where b is a fresh skolem variable
529 We also cater for the symmetric situation *if* the rule cannot be used as a
530 left-to-right rewrite rule.
532 We also return an action (b := ty1) which is used to eliminate b
533 after the dust of normalisation with the completed rewrite system
536 A subtle point of this transformation is that both coercions in the results
537 are strictly speaking incorrect. However, they are correct again after the
538 action {B := ty1} has removed the skolem again. This happens immediately
539 after constraint entailment has been checked; ie, code outside of the
540 simplification and entailment checking framework will never see these
541 temporarily incorrect coercions.
543 NB: We perform this transformation for multiple occurences of ty1 under one
544 or multiple family applications on the left-hand side at once (ie, the
545 rule doesn't need to be applied multiple times at a single inst). As a
546 result we can get two or more insts back.
548 Note [skolemOccurs loop]
549 ~~~~~~~~~~~~~~~~~~~~~~~~
550 You might think that under
553 type instance F [a] = [F a]
557 foo :: (F [a] ~ a) => a
559 will get us into a loop. However, this is *not* the case. Here is why:
570 F [b<tau>] ~ b<tau> , with b := F a
575 [F b<tau>] ~ b<tau> , with b := F a
577 At this point (SkolemOccurs) does *not* apply anymore, as
581 is not used as a rewrite rule. The variable b<tau> is not a skolem (cf
584 (The regression test indexed-types/should_compile/Simple20 checks that the
585 described property of the system does not change.)
588 skolemOccurs :: PrecondRule
590 = do { (instss, undoSkolems) <- mapAndUnzipM oneSkolemOccurs insts
591 ; return (concat instss, sequence_ undoSkolems)
595 = ASSERT( isEqInst inst )
596 case eqInstToRewrite inst of
597 Just (rewrite, swapped) -> breakRecursion rewrite swapped
598 Nothing -> return ([inst], return ())
600 -- inst is an elementary rewrite rule, check whether we need to break
602 breakRecursion (Rewrite pat body _) swapped
604 -- skolemOccurs does not apply, leave as is
606 = do { traceTc $ text "oneSkolemOccurs: no tys to lift out"
607 ; return ([inst], return ())
610 -- recursive occurence of pat in body under a type family application
612 = do { traceTc $ text "oneSkolemOccurs[TLO]:" <+> ppr tysToLiftOut
613 ; skTvs <- mapM (newMetaTyVar TauTv . typeKind) tysToLiftOut
614 ; let skTvs_tysTLO = zip skTvs tysToLiftOut
615 insertSkolems = return . replace skTvs_tysTLO
616 ; (_, body') <- tcGenericNormaliseFamInst insertSkolems body
617 ; inst' <- if swapped then mkEqInst (EqPred body' pat) co
618 else mkEqInst (EqPred pat body') co
619 -- ensure to reconstruct the inst in the
620 -- original orientation
621 ; traceTc $ text "oneSkolemOccurs[inst']:" <+> ppr inst'
622 ; (insts, undoSk) <- mapAndUnzipM (mkSkolemInst inst')
624 ; return (inst':insts, sequence_ undoSk)
627 co = eqInstCoercion inst
629 -- all subtypes that are (1) type family instances and (2) contain
630 -- the lhs type as part of the type arguments of the type family
632 tysToLiftOut = [mkTyConApp tc tys | (tc, tys) <- tyFamInsts body
633 , any (pat `tcPartOfType`) tys]
635 replace :: [(TcTyVar, Type)] -> Type -> Maybe (Type, Coercion)
636 replace [] _ = Nothing
637 replace ((skTv, tyTLO):rest) ty
638 | tyTLO `tcEqType` ty = Just (mkTyVarTy skTv, undefined)
639 | otherwise = replace rest ty
641 -- create the EqInst for the equality determining the skolem and a
642 -- TcM action undoing the skolem introduction
643 mkSkolemInst inst' (skTv, tyTLO)
644 = do { (co, tyLiftedOut) <- tcEqInstNormaliseFamInst inst' tyTLO
645 ; inst <- mkEqInst (EqPred tyLiftedOut (mkTyVarTy skTv))
646 (mkGivenCo $ mkSymCoercion (fromACo co))
647 -- co /= IdCo due to construction of inst'
648 ; return (inst, writeMetaTyVar skTv tyTLO)
653 Removal of trivial equalities: trivialRule
654 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
655 The following rules exploits the reflexivity of equality:
663 trivialRule :: IdemRewriteRule
665 = liftM catMaybes $ mapM trivial insts
668 | ASSERT( isEqInst inst )
670 = do { eitherEqInst inst
671 (\cotv -> writeMetaTyVar cotv ty1)
678 (ty1,ty2) = eqInstTys inst
682 Decomposition of data type constructors: decompRule
683 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
684 Whenever, the same *data* constructors occurs on both sides of an equality, we
685 can decompose as in standard unification.
690 g21 : c1 ~ d1, ..., g2n : cn ~ dn
693 Works also for the case where T is actually an application of a type family
694 constructor to a set of types, provided the applications on both sides of the
695 ~ are identical; see also Note [OpenSynTyCon app] in TcUnify.
697 We guarantee to raise an error for any inconsistent equalities;
698 cf Note [Inconsistencies in equality constraints].
701 decompRule :: RewriteRule
703 = do { (insts, changed) <- mapAndUnzipM decomp insts
704 ; return (concat insts, or changed)
708 = ASSERT( isEqInst inst )
711 (ty1,ty2) = eqInstTys inst
713 | Just ty1' <- tcView ty1 = go ty1' ty2
714 | Just ty2' <- tcView ty2 = go ty1 ty2'
716 go (TyConApp con1 tys1) (TyConApp con2 tys2)
717 | con1 == con2 && identicalHead
718 = mkArgInsts (mkTyConApp con1) tys1 tys2
720 | con1 /= con2 && not (isOpenSynTyCon con1 || isOpenSynTyCon con2)
721 -- not matching data constructors (of any flavour) are bad news
722 = eqInstMisMatch inst
725 (idxTys1, _) = splitAt n tys1
726 (idxTys2, _) = splitAt n tys2
727 identicalHead = not (isOpenSynTyCon con1) ||
728 idxTys1 `tcEqTypes` idxTys2
730 go (FunTy fun1 arg1) (FunTy fun2 arg2)
731 = mkArgInsts (\[funCo, argCo] -> mkFunTy funCo argCo) [fun1, arg1]
734 -- Applications need a bit of care!
735 -- They can match FunTy and TyConApp, so use splitAppTy_maybe
737 | Just (s2, t2) <- tcSplitAppTy_maybe ty2
738 = mkArgInsts (\[s, t] -> mkAppTy s t) [s1, t1] [s2, t2]
742 | Just (s1, t1) <- tcSplitAppTy_maybe ty1
743 = mkArgInsts (\[s, t] -> mkAppTy s t) [s1, t1] [s2, t2]
745 -- We already covered all the consistent cases of rigid types on both
746 -- sides; so, if we see two rigid types here, we discovered an
749 | isRigid ty1 && isRigid ty2
750 = eqInstMisMatch inst
752 -- We can neither assert consistency nor inconsistency => defer
753 go _ _ = return ([inst], False)
755 isRigid (TyConApp con _) = not (isOpenSynTyCon con)
756 isRigid (FunTy _ _) = True
757 isRigid (AppTy _ _) = True
760 -- Create insts for matching argument positions (ie, the bit after
761 -- '>-->' in the rule description above)
762 mkArgInsts con tys1 tys2
763 = do { cos <- eitherEqInst inst
764 -- old_co := Con1 cos
766 do { cotvs <- zipWithM newMetaCoVar tys1 tys2
767 ; let cos = map mkTyVarTy cotvs
768 ; writeMetaTyVar old_covar (con cos)
769 ; return $ map mkWantedCo cotvs
771 -- co_i := Con_i old_co
773 return $ map mkGivenCo $
774 mkRightCoercions (length tys1) old_co)
775 ; insts <- zipWithM mkEqInst (zipWith EqPred tys1 tys2) cos
776 ; traceTc (text "decomp identicalHead" <+> ppr insts)
777 ; return (insts, not $ null insts)
782 Rewriting with type instances: topRule
783 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
784 We use (toplevel) type instances to normalise both sides of equalities.
788 >--> co1 :: t ~ t' / co2 :: s ~ s'
790 g1 := co1 * g2 * sym co2
793 topRule :: RewriteRule
795 = do { (insts, changed) <- mapAndUnzipM top insts
796 ; return (insts, or changed)
800 = ASSERT( isEqInst inst )
801 do { (coi1, ty1') <- tcNormaliseFamInst ty1
802 ; (coi2, ty2') <- tcNormaliseFamInst ty2
803 ; case (coi1, coi2) of
804 (IdCo, IdCo) -> return (inst, False)
808 -- old_co = co1 * new_co * sym co2
810 do { new_cotv <- newMetaCoVar ty1' ty2'
811 ; let new_co = mkTyVarTy new_cotv
812 old_coi = coi1 `mkTransCoI`
813 ACo new_co `mkTransCoI`
815 ; writeMetaTyVar old_covar (fromACo old_coi)
816 ; return $ mkWantedCo new_cotv
818 -- new_co = sym co1 * old_co * co2
823 mkSymCoI coi1 `mkTransCoI`
824 ACo old_co `mkTransCoI` coi2)
825 ; new_inst <- mkEqInst (EqPred ty1' ty2') wg_co
826 ; return (new_inst, True)
830 (ty1,ty2) = eqInstTys inst
834 Rewriting with equalities: substRule
835 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
836 From a set of insts, use all insts that can be read as rewrite rules to
837 rewrite the types in all other insts.
841 forall g1 : s1{F c} ~ s2{F c}
844 g1 := s1{g} * g2 * sym s2{g} <=> g2 := sym s1{g} * g1 * s2{g}
846 Alternatively, the rewrite rule may have the form (g : a ~ t).
848 To avoid having to swap rules of the form (g : t ~ F c) and (g : t ~ a),
849 where t is neither a variable nor a type family application, we use them for
850 rewriting from right-to-left. However, it is crucial to only apply rules
851 from right-to-left if they cannot be used left-to-right.
853 The workhorse is substInst, which performs an occurs check before actually
854 using an equality for rewriting. If the type pattern occurs in the type we
855 substitute for the pattern, normalisation would diverge.
858 substRule :: RewriteRule
859 substRule insts = tryAllInsts insts []
861 -- for every inst check whether it can be used to rewrite the others
862 -- (we make an effort to keep the insts in order; it makes debugging
864 tryAllInsts [] triedInsts = return (reverse triedInsts, False)
865 tryAllInsts (inst:insts) triedInsts
866 = do { (insts', changed) <- substInst inst (reverse triedInsts ++ insts)
867 ; if changed then return (insertAt (length triedInsts) inst insts',
869 else tryAllInsts insts (inst:triedInsts)
872 insertAt n x xs = let (xs1, xs2) = splitAt n xs
875 -- Use the given inst as a rewrite rule to normalise the insts in the second
876 -- argument. Don't do anything if the inst cannot be used as a rewrite rule,
877 -- but do apply it right-to-left, if possible, and if it cannot be used
880 substInst :: Inst -> [Inst] -> TcM ([Inst], Bool)
882 = case eqInstToRewrite inst of
883 Just (rewrite, _) -> substEquality rewrite insts
884 Nothing -> return (insts, False)
886 substEquality :: Rewrite -- elementary rewrite
887 -> [Inst] -- insts to rewrite
888 -> TcM ([Inst], Bool)
889 substEquality eqRule@(Rewrite pat rhs _) insts
890 | pat `tcPartOfType` rhs -- occurs check!
891 = occurCheckErr pat rhs
893 = do { (insts', changed) <- mapAndUnzipM substOne insts
894 ; return (insts', or changed)
898 = ASSERT( isEqInst inst )
899 do { (coi1, ty1') <- tcEqRuleNormaliseFamInst eqRule ty1
900 ; (coi2, ty2') <- tcEqRuleNormaliseFamInst eqRule ty2
901 ; case (coi1, coi2) of
902 (IdCo, IdCo) -> return (inst, False)
906 -- old_co := co1 * new_co * sym co2
908 do { new_cotv <- newMetaCoVar ty1' ty2'
909 ; let new_co = mkTyVarTy new_cotv
910 old_coi = coi1 `mkTransCoI`
911 ACo new_co `mkTransCoI`
913 ; writeMetaTyVar old_covar (fromACo old_coi)
914 ; return $ mkWantedCo new_cotv
916 -- new_co := sym co1 * old_co * co2
921 mkSymCoI coi1 `mkTransCoI`
922 ACo old_co `mkTransCoI` coi2)
923 ; new_inst <- mkEqInst (EqPred ty1' ty2') gw_co
924 ; return (new_inst, True)
928 (ty1,ty2) = eqInstTys inst
932 Instantiate meta variables: unifyMetaRule
933 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
934 If an equality equates a meta type variable with a type, we simply instantiate
943 Meta variables can only appear in wanted constraints, and this rule should
944 only be applied to wanted constraints. We also know that t definitely is
945 distinct from alpha (as the trivialRule) has been run on the insts beforehand.
947 NB: We cannot assume that meta tyvars are empty. They may have been updated
948 by another inst in the currently processed wanted list. We need to be very
949 careful when updateing type variables (see TcUnify.uUnfilledVar), but at least
950 we know that we have no boxes. It's unclear that it would be an advantage to
951 common up the code in TcUnify and the code below. Firstly, we don't want
952 calls to TcUnify.defer_unification here, and secondly, TcUnify import the
953 current module, so we would have to move everything here (Yuk!) or to
954 TcMType. Besides, the code here is much simpler due to the lack of boxes.
957 unifyMetaRule :: RewriteRule
959 = do { (insts', changed) <- mapAndUnzipM unifyMeta insts
960 ; return (concat insts', or changed)
964 = ASSERT( isEqInst inst )
966 (fromWantedCo "unifyMetaRule" $ eqInstCoercion inst)
968 (ty1,ty2) = eqInstTys inst
970 | Just ty1' <- tcView ty1 = go ty1' ty2 cotv
971 | Just ty2' <- tcView ty2 = go ty1 ty2' cotv
974 , isMetaTyVar tv1 = do { lookupTV <- lookupTcTyVar tv1
975 ; uMeta False tv1 lookupTV ty2 cotv
978 , isMetaTyVar tv2 = do { lookupTV <- lookupTcTyVar tv2
979 ; uMeta True tv2 lookupTV ty1 cotv
981 | otherwise = return ([inst], False)
983 -- meta variable has been filled already
984 -- => ignore this inst (we'll come around again, after zonking)
985 uMeta _swapped _tv (IndirectTv _) _ty _cotv
986 = return ([inst], False)
988 -- type variable meets type variable
989 -- => check that tv2 hasn't been updated yet and choose which to update
990 uMeta swapped tv1 (DoneTv details1) (TyVarTy tv2) cotv
992 = return ([inst], False) -- The two types are already identical
995 = do { lookupTV2 <- lookupTcTyVar tv2
997 IndirectTv ty -> uMeta swapped tv1 (DoneTv details1) ty cotv
998 DoneTv details2 -> uMetaVar swapped tv1 details1 tv2 details2 cotv
1001 ------ Beyond this point we know that ty2 is not a type variable
1003 -- signature skolem meets non-variable type
1004 -- => cannot update!
1005 uMeta _swapped _tv (DoneTv (MetaTv (SigTv _) _)) _non_tv_ty _cotv
1006 = return ([inst], False)
1008 -- updatable meta variable meets non-variable type
1009 -- => occurs check, monotype check, and kinds match check, then update
1010 uMeta swapped tv (DoneTv (MetaTv _ ref)) non_tv_ty cotv
1011 = do { mb_ty' <- checkTauTvUpdate tv non_tv_ty -- occurs + monotype check
1013 Nothing -> return ([inst], False) -- tv occurs in faminst
1015 do { checkUpdateMeta swapped tv ref ty' -- update meta var
1016 ; writeMetaTyVar cotv ty' -- update co var
1021 uMeta _ _ _ _ _ = panic "uMeta"
1023 -- uMetaVar: unify two type variables
1024 -- meta variable meets skolem
1026 uMetaVar swapped tv1 (MetaTv _ ref) tv2 (SkolemTv _) cotv
1027 = do { checkUpdateMeta swapped tv1 ref (mkTyVarTy tv2)
1028 ; writeMetaTyVar cotv (mkTyVarTy tv2)
1032 -- meta variable meets meta variable
1033 -- => be clever about which of the two to update
1034 -- (from TcUnify.uUnfilledVars minus boxy stuff)
1035 uMetaVar swapped tv1 (MetaTv info1 ref1) tv2 (MetaTv info2 ref2) cotv
1036 = do { case (info1, info2) of
1037 -- Avoid SigTvs if poss
1038 (SigTv _, _ ) | k1_sub_k2 -> update_tv2
1039 (_, SigTv _) | k2_sub_k1 -> update_tv1
1041 (_, _) | k1_sub_k2 -> if k2_sub_k1 && nicer_to_update_tv1
1042 then update_tv1 -- Same kinds
1044 | k2_sub_k1 -> update_tv1
1045 | otherwise -> kind_err
1046 -- Update the variable with least kind info
1047 -- See notes on type inference in Kind.lhs
1048 -- The "nicer to" part only applies if the two kinds are the same,
1049 -- so we can choose which to do.
1051 ; writeMetaTyVar cotv (mkTyVarTy tv2)
1055 -- Kinds should be guaranteed ok at this point
1056 update_tv1 = updateMeta tv1 ref1 (mkTyVarTy tv2)
1057 update_tv2 = updateMeta tv2 ref2 (mkTyVarTy tv1)
1059 kind_err = addErrCtxtM (unifyKindCtxt swapped tv1 (mkTyVarTy tv2)) $
1060 unifyKindMisMatch k1 k2
1064 k1_sub_k2 = k1 `isSubKind` k2
1065 k2_sub_k1 = k2 `isSubKind` k1
1067 nicer_to_update_tv1 = isSystemName (Var.varName tv1)
1068 -- Try to update sys-y type variables in preference to ones
1069 -- gotten (say) by instantiating a polymorphic function with
1070 -- a user-written type sig
1072 uMetaVar _ _ _ _ _ _ = panic "uMetaVar"
1076 %************************************************************************
1078 \section{Normalisation of Insts}
1080 %************************************************************************
1082 Normalises a set of dictionaries relative to a set of given equalities (which
1083 are interpreted as rewrite rules). We only consider given equalities of the
1088 where F is a type family.
1091 substEqInDictInsts :: Bool -- whether the *dictionaries* are wanted/given
1092 -> [Inst] -- given equalities (used as rewrite rules)
1093 -> [Inst] -- dictinaries to be normalised
1094 -> TcM ([Inst], TcDictBinds)
1095 substEqInDictInsts isWanted eqInsts dictInsts
1096 = do { traceTc (text "substEqInDictInst <-" <+> ppr dictInsts)
1098 foldlM rewriteWithOneEquality (dictInsts, emptyBag) eqInsts
1099 ; traceTc (text "substEqInDictInst ->" <+> ppr dictInsts')
1103 -- (1) Given equality of form 'F ts ~ t' or 'a ~ t': use for rewriting
1104 rewriteWithOneEquality (dictInsts, dictBinds)
1105 eqInst@(EqInst {tci_left = pattern,
1106 tci_right = target})
1107 | isOpenSynTyConApp pattern || isTyVarTy pattern
1108 = do { (dictInsts', moreDictBinds) <-
1109 genericNormaliseInsts isWanted applyThisEq dictInsts
1110 ; return (dictInsts', dictBinds `unionBags` moreDictBinds)
1113 applyThisEq = tcGenericNormaliseFamInstPred (return . matchResult)
1115 -- rewrite in case of an exact match
1116 matchResult ty | tcEqType pattern ty = Just (target, eqInstType eqInst)
1117 | otherwise = Nothing
1119 -- (2) Given equality has the wrong form: ignore
1120 rewriteWithOneEquality (dictInsts, dictBinds) _not_a_rewrite_rule
1121 = return (dictInsts, dictBinds)
1125 Take a bunch of Insts (not EqInsts), and normalise them wrt the top-level
1126 type-function equations, where
1128 (norm_insts, binds) = normaliseInsts is_wanted insts
1131 = True, (binds + norm_insts) defines insts (wanteds)
1132 = False, (binds + insts) defines norm_insts (givens)
1134 Ie, in the case of normalising wanted dictionaries, we use the normalised
1135 dictionaries to define the originally wanted ones. However, in the case of
1136 given dictionaries, we use the originally given ones to define the normalised
1140 normaliseInsts :: Bool -- True <=> wanted insts
1141 -> [Inst] -- wanted or given insts
1142 -> TcM ([Inst], TcDictBinds) -- normalised insts and bindings
1143 normaliseInsts isWanted insts
1144 = genericNormaliseInsts isWanted tcNormaliseFamInstPred insts
1146 genericNormaliseInsts :: Bool -- True <=> wanted insts
1147 -> (TcPredType -> TcM (CoercionI, TcPredType))
1149 -> [Inst] -- wanted or given insts
1150 -> TcM ([Inst], TcDictBinds) -- normalised insts & binds
1151 genericNormaliseInsts isWanted fun insts
1152 = do { (insts', binds) <- mapAndUnzipM (normaliseOneInst isWanted fun) insts
1153 ; return (insts', unionManyBags binds)
1156 normaliseOneInst isWanted fun
1157 dict@(Dict {tci_pred = pred,
1159 = do { traceTc $ text "genericNormaliseInst <-" <+> ppr dict
1160 ; (coi, pred') <- fun pred
1164 do { traceTc $ text "genericNormaliseInst ->" <+> ppr dict
1165 ; return (dict, emptyBag)
1167 -- don't use pred' in this case; otherwise, we get
1168 -- more unfolded closed type synonyms in error messages
1170 do { -- an inst for the new pred
1171 ; dict' <- newDictBndr loc pred'
1172 -- relate the old inst to the new one
1173 -- target_dict = source_dict `cast` st_co
1174 ; let (target_dict, source_dict, st_co)
1175 | isWanted = (dict, dict', mkSymCoercion co)
1176 | otherwise = (dict', dict, co)
1178 -- co :: dict ~ dict'
1179 -- hence, if isWanted
1180 -- dict = dict' `cast` sym co
1182 -- dict' = dict `cast` co
1183 expr = HsVar $ instToId source_dict
1184 cast_expr = HsWrap (WpCo st_co) expr
1185 rhs = L (instLocSpan loc) cast_expr
1186 binds = instToDictBind target_dict rhs
1187 -- return the new inst
1188 ; traceTc $ let name | isWanted
1189 = "genericNormaliseInst (wanted) ->"
1191 = "genericNormaliseInst (given) ->"
1193 text name <+> ppr dict' <+>
1194 text "with" <+> ppr binds
1195 ; return (dict', binds)
1199 -- TOMDO: What do we have to do about ImplicInst, Method, and LitInst??
1200 normaliseOneInst _isWanted _fun inst
1201 = do { inst' <- zonkInst inst
1202 ; traceTc $ text "*** TcTyFuns.normaliseOneInst: Skipping" <+>
1204 ; return (inst', emptyBag)
1209 %************************************************************************
1213 %************************************************************************
1215 The infamous couldn't match expected type soandso against inferred type
1216 somethingdifferent message.
1219 eqInstMisMatch :: Inst -> TcM a
1221 = ASSERT( isEqInst inst )
1222 setErrCtxt ctxt $ failWithMisMatch ty_act ty_exp
1224 (ty_act, ty_exp) = eqInstTys inst
1225 InstLoc _ _ ctxt = instLoc inst
1227 -----------------------
1228 failWithMisMatch :: TcType -> TcType -> TcM a
1229 -- Generate the message when two types fail to match,
1230 -- going to some trouble to make it helpful.
1231 -- The argument order is: actual type, expected type
1232 failWithMisMatch ty_act ty_exp
1233 = do { env0 <- tcInitTidyEnv
1234 ; ty_exp <- zonkTcType ty_exp
1235 ; ty_act <- zonkTcType ty_act
1236 ; failWithTcM (misMatchMsg env0 (ty_act, ty_exp))
1239 misMatchMsg :: TidyEnv -> (TcType, TcType) -> (TidyEnv, SDoc)
1240 misMatchMsg env0 (ty_act, ty_exp)
1241 = let (env1, pp_exp, extra_exp) = ppr_ty env0 ty_exp
1242 (env2, pp_act, extra_act) = ppr_ty env1 ty_act
1243 msg = sep [sep [ptext SLIT("Couldn't match expected type") <+> pp_exp,
1245 ptext SLIT("against inferred type") <+> pp_act],
1246 nest 2 (extra_exp $$ extra_act)]
1251 ppr_ty :: TidyEnv -> TcType -> (TidyEnv, SDoc, SDoc)
1253 = let (env1, tidy_ty) = tidyOpenType env ty
1254 (env2, extra) = ppr_extra env1 tidy_ty
1256 (env2, quotes (ppr tidy_ty), extra)
1258 -- (ppr_extra env ty) shows extra info about 'ty'
1259 ppr_extra :: TidyEnv -> Type -> (TidyEnv, SDoc)
1260 ppr_extra env (TyVarTy tv)
1261 | isTcTyVar tv && (isSkolemTyVar tv || isSigTyVar tv) && not (isUnk tv)
1262 = (env1, pprSkolTvBinding tv1)
1264 (env1, tv1) = tidySkolemTyVar env tv
1266 ppr_extra env _ty = (env, empty) -- Normal case