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,
14 eqInstMisMatch, misMatchMsg,
18 #include "HsVersions.h"
30 import TypeRep ( Type(..) )
38 import SrcLoc ( Located(..) )
43 import Control.Monad (liftM)
47 %************************************************************************
49 Normalisation of types
51 %************************************************************************
53 Unfold a single synonym family instance and yield the witnessing coercion.
54 Return 'Nothing' if the given type is either not synonym family instance
55 or is a synonym family instance that has no matching instance declaration.
56 (Applies only if the type family application is outermost.)
58 For example, if we have
60 :Co:R42T a :: T [a] ~ :R42T a
62 then 'T [Int]' unfolds to (:R42T Int, :Co:R42T Int).
65 tcUnfoldSynFamInst :: Type -> TcM (Maybe (Type, Coercion))
66 tcUnfoldSynFamInst (TyConApp tycon tys)
67 | not (isOpenSynTyCon tycon) -- unfold *only* _synonym_ family instances
70 = do { -- we only use the indexing arguments for matching,
71 -- not the additional ones
72 ; maybeFamInst <- tcLookupFamInst tycon idxTys
73 ; case maybeFamInst of
74 Nothing -> return Nothing
75 Just (rep_tc, rep_tys) -> return $ Just (mkTyConApp rep_tc tys',
76 mkTyConApp coe_tc tys')
78 tys' = rep_tys ++ restTys
79 coe_tc = expectJust "TcTyFun.tcUnfoldSynFamInst"
80 (tyConFamilyCoercion_maybe rep_tc)
84 (idxTys, restTys) = splitAt n tys
85 tcUnfoldSynFamInst _other = return Nothing
88 Normalise 'Type's and 'PredType's by unfolding type family applications where
89 possible (ie, we treat family instances as a TRS). Also zonk meta variables.
91 tcNormaliseFamInst ty = (co, ty')
95 tcNormaliseFamInst :: TcType -> TcM (CoercionI, TcType)
96 tcNormaliseFamInst = tcGenericNormaliseFamInst tcUnfoldSynFamInst
98 tcNormaliseFamInstPred :: TcPredType -> TcM (CoercionI, TcPredType)
99 tcNormaliseFamInstPred = tcGenericNormaliseFamInstPred tcUnfoldSynFamInst
102 An elementary rewrite is a properly oriented equality with associated coercion
103 that has one of the following two forms:
105 (1) co :: F t1..tn ~ t
106 (2) co :: a ~ t , where t /= F t1..tn and a is a skolem tyvar
108 NB: We do *not* use equalities of the form a ~ t where a is a meta tyvar as a
109 reqrite rule. Instead, such equalities are solved by unification. This is
110 essential; cf Note [skolemOccurs loop].
112 The following functions takes an equality instance and turns it into an
113 elementary rewrite if possible.
116 data Rewrite = Rewrite TcType -- lhs of rewrite rule
117 TcType -- rhs of rewrite rule
118 TcType -- coercion witnessing the rewrite rule
120 eqInstToRewrite :: Inst -> Maybe (Rewrite, Bool)
121 -- True iff rewrite swapped equality
123 = ASSERT( isEqInst inst )
124 go (eqInstLeftTy inst) (eqInstRightTy inst) (eqInstType 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 (mkNoteTyCoI note 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] -> TcM [Inst]
313 normaliseWantedEqs insts
314 = do { traceTc (text "normaliseWantedEqs <-" <+> ppr insts)
315 ; result <- liftM fst $ rewriteToFixedPoint Nothing
316 [ ("(ZONK)", dontRerun $ zonkInsts)
317 , ("(TRIVIAL)", dontRerun $ trivialRule)
318 , ("(DECOMP)", decompRule)
320 , ("(UNIFY)", unifyMetaRule) -- incl. occurs check
321 , ("(SUBST)", substRule) -- incl. occurs check
323 ; traceTc (text "normaliseWantedEqs ->" <+> ppr result)
329 %************************************************************************
331 \section{Solving of wanted constraints with respect to a given set}
333 %************************************************************************
335 The set of given equalities must have been normalised already.
338 solveWantedEqs :: [Inst] -- givens
340 -> TcM [Inst] -- irreducible wanteds
341 solveWantedEqs givens wanteds
342 = do { traceTc $ text "solveWantedEqs <-" <+> ppr wanteds <+> text "with" <+>
344 ; result <- liftM fst $ rewriteToFixedPoint Nothing
345 [ ("(ZONK)", dontRerun $ zonkInsts)
346 , ("(TRIVIAL)", dontRerun $ trivialRule)
347 , ("(DECOMP)", decompRule)
349 , ("(GIVEN)", substGivens givens) -- incl. occurs check
350 , ("(UNIFY)", unifyMetaRule) -- incl. occurs check
352 ; traceTc (text "solveWantedEqs ->" <+> ppr result)
356 -- Use `substInst' with every given on all the wanteds.
357 substGivens :: [Inst] -> [Inst] -> TcM ([Inst], Bool)
358 substGivens [] wanteds = return (wanteds, False)
359 substGivens (g:gs) wanteds
360 = do { (wanteds1, changed1) <- substGivens gs wanteds
361 ; (wanteds2, changed2) <- substInst g wanteds1
362 ; return (wanteds2, changed1 || changed2)
367 %************************************************************************
369 \section{Normalisation of non-equality dictionaries}
371 %************************************************************************
374 normaliseGivenDicts, normaliseWantedDicts
375 :: [Inst] -- given equations
376 -> [Inst] -- dictionaries
377 -> TcM ([Inst],TcDictBinds)
379 normaliseGivenDicts eqs dicts = normalise_dicts eqs dicts False
380 normaliseWantedDicts eqs dicts = normalise_dicts eqs dicts True
383 :: [Inst] -- given equations
384 -> [Inst] -- dictionaries
385 -> Bool -- True <=> the dicts are wanted
386 -- Fals <=> they are given
387 -> TcM ([Inst],TcDictBinds)
388 normalise_dicts given_eqs dicts is_wanted
389 = do { traceTc $ text "normalise???Dicts <-" <+> ppr dicts <+>
390 text "with" <+> ppr given_eqs
391 ; (dicts0, binds0) <- normaliseInsts is_wanted dicts
392 ; (dicts1, binds1) <- substEqInDictInsts given_eqs dicts0
393 ; let binds01 = binds0 `unionBags` binds1
394 ; if isEmptyBag binds1
395 then return (dicts1, binds01)
396 else do { (dicts2, binds2) <- normaliseGivenDicts given_eqs dicts1
397 ; return (dicts2, binds01 `unionBags` binds2) } }
401 %************************************************************************
403 \section{Normalisation rules and iterative rule application}
405 %************************************************************************
407 We have three kinds of normalising rewrite rules:
409 (1) Normalisation rules that rewrite a set of insts and return a flag indicating
410 whether any changes occurred during rewriting that necessitate re-running
411 the current rule set.
413 (2) Precondition rules that rewrite a set of insts and return a monadic action
414 that reverts the effect of preconditioning.
416 (3) Idempotent normalisation rules that never require re-running the rule set.
419 type RewriteRule = [Inst] -> TcM ([Inst], Bool) -- rewrite, maybe re-run
420 type PrecondRule = [Inst] -> TcM ([Inst], TcM ()) -- rewrite, revertable
421 type IdemRewriteRule = [Inst] -> TcM [Inst] -- rewrite, don't re-run
423 type NamedRule = (String, RewriteRule) -- rule with description
424 type NamedPreRule = (String, PrecondRule) -- precond with desc
427 Template lifting idempotent rules to full rules (which can be put into a rule
431 dontRerun :: IdemRewriteRule -> RewriteRule
432 dontRerun rule insts = liftM addFalse $ rule insts
434 addFalse x = (x, False)
437 The following function applies a set of rewrite rules until a fixed point is
438 reached; i.e., none of the `RewriteRule's require re-running the rule set.
439 Optionally, there may be a pre-conditing rule that is applied before any other
440 rules are applied and before the rule set is re-run.
442 The result is the set of rewritten (i.e., normalised) insts and, in case of a
443 pre-conditing rule, a monadic action that reverts the effects of
444 pre-conditioning - specifically, this is removing introduced skolems.
447 rewriteToFixedPoint :: Maybe NamedPreRule -- optional preconditioning rule
448 -> [NamedRule] -- rule set
449 -> [Inst] -- insts to rewrite
450 -> TcM ([Inst], TcM ())
451 rewriteToFixedPoint precondRule rules insts
452 = completeRewrite (return ()) precondRule insts
454 completeRewrite :: TcM () -> Maybe NamedPreRule -> [Inst]
455 -> TcM ([Inst], TcM ())
456 completeRewrite dePrecond (Just (precondName, precond)) insts
457 = do { traceTc $ text precondName <+> text " <- " <+> ppr insts
458 ; (insts', dePrecond') <- precond insts
459 ; traceTc $ text precondName <+> text " -> " <+> ppr insts'
460 ; tryRules (dePrecond >> dePrecond') rules insts'
462 completeRewrite dePrecond Nothing insts
463 = tryRules dePrecond rules insts
465 tryRules dePrecond _ [] = return ([] , dePrecond)
466 tryRules dePrecond [] insts = return (insts, dePrecond)
467 tryRules dePrecond ((name, rule):rules) insts
468 = do { traceTc $ text name <+> text " <- " <+> ppr insts
469 ; (insts', rerun) <- rule insts
470 ; traceTc $ text name <+> text " -> " <+> ppr insts'
471 ; if rerun then completeRewrite dePrecond precondRule insts'
472 else tryRules dePrecond rules insts'
477 %************************************************************************
479 \section{Different forms of Inst rewrite rules}
481 %************************************************************************
483 Splitting of non-terminating given constraints: skolemOccurs
484 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
485 This is a preconditioning rule exclusively applied to given constraints.
486 Moreover, its rewriting is only temporary, as it is undone by way of
487 side-effecting mutable type variables after simplification and constraint
488 entailment has been completed.
490 This version is an (attempt at, yet unproven, an) *unflattened* version of
491 the SubstL-Ev completion rule.
493 The above rule is essential to catch non-terminating rules that cannot be
494 oriented properly, like
498 a ~ [G a] , where a is a skolem tyvar
500 The left-to-right orientiation is not suitable because it does not
501 terminate. The right-to-left orientation is not suitable because it
502 does not have a type-function on the left. This is undesirable because
503 it would hide information. E.g. assume
507 then rewriting C [G (F a)] to C (F a) is bad because we cannot now
508 see that the C [x] instance applies.
510 The rule also caters for badly-oriented rules of the form:
514 for which other solutions are possible, but this one will do too.
518 co : ty1 ~ ty2{F ty1}
521 sym (F co) : F ty2{b} ~ b
522 where b is a fresh skolem variable
524 We also cater for the symmetric situation *if* the rule cannot be used as a
525 left-to-right rewrite rule.
527 We also return an action (b := ty1) which is used to eliminate b
528 after the dust of normalisation with the completed rewrite system
531 A subtle point of this transformation is that both coercions in the results
532 are strictly speaking incorrect. However, they are correct again after the
533 action {B := ty1} has removed the skolem again. This happens immediately
534 after constraint entailment has been checked; ie, code outside of the
535 simplification and entailment checking framework will never see these
536 temporarily incorrect coercions.
538 NB: We perform this transformation for multiple occurences of ty1 under one
539 or multiple family applications on the left-hand side at once (ie, the
540 rule doesn't need to be applied multiple times at a single inst). As a
541 result we can get two or more insts back.
543 Note [skolemOccurs loop]
544 ~~~~~~~~~~~~~~~~~~~~~~~~
545 You might think that under
548 type instance F [a] = [F a]
552 foo :: (F [a] ~ a) => a
554 will get us into a loop. However, this is *not* the case. Here is why:
565 F [b<tau>] ~ b<tau> , with b := F a
570 [F b<tau>] ~ b<tau> , with b := F a
572 At this point (SkolemOccurs) does *not* apply anymore, as
576 is not used as a rewrite rule. The variable b<tau> is not a skolem (cf
579 (The regression test indexed-types/should_compile/Simple20 checks that the
580 described property of the system does not change.)
583 skolemOccurs :: PrecondRule
585 = do { (instss, undoSkolems) <- mapAndUnzipM oneSkolemOccurs insts
586 ; return (concat instss, sequence_ undoSkolems)
590 = ASSERT( isEqInst inst )
591 case eqInstToRewrite inst of
592 Just (rewrite, swapped) -> breakRecursion rewrite swapped
593 Nothing -> return ([inst], return ())
595 -- inst is an elementary rewrite rule, check whether we need to break
597 breakRecursion (Rewrite pat body _) swapped
599 -- skolemOccurs does not apply, leave as is
601 = do { traceTc $ text "oneSkolemOccurs: no tys to lift out"
602 ; return ([inst], return ())
605 -- recursive occurence of pat in body under a type family application
607 = do { traceTc $ text "oneSkolemOccurs[TLO]:" <+> ppr tysToLiftOut
608 ; skTvs <- mapM (newMetaTyVar TauTv . typeKind) tysToLiftOut
609 ; let skTvs_tysTLO = zip skTvs tysToLiftOut
610 insertSkolems = return . replace skTvs_tysTLO
611 ; (_, body') <- tcGenericNormaliseFamInst insertSkolems body
612 ; inst' <- if swapped then mkEqInst (EqPred body' pat) co
613 else mkEqInst (EqPred pat body') co
614 -- ensure to reconstruct the inst in the
615 -- original orientation
616 ; traceTc $ text "oneSkolemOccurs[inst']:" <+> ppr inst'
617 ; (insts, undoSk) <- mapAndUnzipM (mkSkolemInst inst')
619 ; return (inst':insts, sequence_ undoSk)
622 co = eqInstCoercion inst
624 -- all subtypes that are (1) type family instances and (2) contain
625 -- the lhs type as part of the type arguments of the type family
627 tysToLiftOut = [mkTyConApp tc tys | (tc, tys) <- tyFamInsts body
628 , any (pat `tcPartOfType`) tys]
630 replace :: [(TcTyVar, Type)] -> Type -> Maybe (Type, Coercion)
631 replace [] _ = Nothing
632 replace ((skTv, tyTLO):rest) ty
633 | tyTLO `tcEqType` ty = Just (mkTyVarTy skTv, undefined)
634 | otherwise = replace rest ty
636 -- create the EqInst for the equality determining the skolem and a
637 -- TcM action undoing the skolem introduction
638 mkSkolemInst inst' (skTv, tyTLO)
639 = do { (co, tyLiftedOut) <- tcEqInstNormaliseFamInst inst' tyTLO
640 ; inst <- mkEqInst (EqPred tyLiftedOut (mkTyVarTy skTv))
641 (mkGivenCo $ mkSymCoercion (fromACo co))
642 -- co /= IdCo due to construction of inst'
643 ; return (inst, writeMetaTyVar skTv tyTLO)
648 Removal of trivial equalities: trivialRule
649 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
650 The following rules exploits the reflexivity of equality:
658 trivialRule :: IdemRewriteRule
660 = liftM catMaybes $ mappM trivial insts
663 | ASSERT( isEqInst inst )
665 = do { eitherEqInst inst
666 (\cotv -> writeMetaTyVar cotv ty1)
673 ty1 = eqInstLeftTy inst
674 ty2 = eqInstRightTy inst
678 Decomposition of data type constructors: decompRule
679 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
680 Whenever, the same *data* constructors occurs on both sides of an equality, we
681 can decompose as in standard unification.
686 g21 : c1 ~ d1, ..., g2n : cn ~ dn
689 Works also for the case where T is actually an application of a type family
690 constructor to a set of types, provided the applications on both sides of the
691 ~ are identical; see also Note [OpenSynTyCon app] in TcUnify.
693 We guarantee to raise an error for any inconsistent equalities;
694 cf Note [Inconsistencies in equality constraints].
697 decompRule :: RewriteRule
699 = do { (insts, changed) <- mapAndUnzipM decomp insts
700 ; return (concat insts, or changed)
704 = ASSERT( isEqInst inst )
705 go (eqInstLeftTy inst) (eqInstRightTy inst)
708 | Just ty1' <- tcView ty1 = go ty1' ty2
709 | Just ty2' <- tcView ty2 = go ty1 ty2'
711 go (TyConApp con1 tys1) (TyConApp con2 tys2)
712 | con1 == con2 && identicalHead
713 = mkArgInsts (mkTyConApp con1) tys1 tys2
715 | con1 /= con2 && not (isOpenSynTyCon con1 || isOpenSynTyCon con2)
716 -- not matching data constructors (of any flavour) are bad news
717 = eqInstMisMatch inst
720 (idxTys1, _) = splitAt n tys1
721 (idxTys2, _) = splitAt n tys2
722 identicalHead = not (isOpenSynTyCon con1) ||
723 idxTys1 `tcEqTypes` idxTys2
725 go (FunTy fun1 arg1) (FunTy fun2 arg2)
726 = mkArgInsts (\[funCo, argCo] -> mkFunTy funCo argCo) [fun1, arg1]
729 -- Applications need a bit of care!
730 -- They can match FunTy and TyConApp, so use splitAppTy_maybe
732 | Just (s2, t2) <- tcSplitAppTy_maybe ty2
733 = mkArgInsts (\[s, t] -> mkAppTy s t) [s1, t1] [s2, t2]
737 | Just (s1, t1) <- tcSplitAppTy_maybe ty1
738 = mkArgInsts (\[s, t] -> mkAppTy s t) [s1, t1] [s2, t2]
740 -- We already covered all the consistent cases of rigid types on both
741 -- sides; so, if we see two rigid types here, we discovered an
744 | isRigid ty1 && isRigid ty2
745 = eqInstMisMatch inst
747 -- We can neither assert consistency nor inconsistency => defer
748 go _ _ = return ([inst], False)
750 isRigid (TyConApp con _) = not (isOpenSynTyCon con)
751 isRigid (FunTy _ _) = True
752 isRigid (AppTy _ _) = True
755 -- Create insts for matching argument positions (ie, the bit after
756 -- '>-->' in the rule description above)
757 mkArgInsts con tys1 tys2
758 = do { cos <- eitherEqInst inst
759 -- old_co := Con1 cos
761 do { cotvs <- zipWithM newMetaCoVar tys1 tys2
762 ; let cos = map mkTyVarTy cotvs
763 ; writeMetaTyVar old_covar (con cos)
764 ; return $ map mkWantedCo cotvs
766 -- co_i := Con_i old_co
768 return $ map mkGivenCo $
769 mkRightCoercions (length tys1) old_co)
770 ; insts <- zipWithM mkEqInst (zipWith EqPred tys1 tys2) cos
771 ; traceTc (text "decomp identicalHead" <+> ppr insts)
772 ; return (insts, not $ null insts)
777 Rewriting with type instances: topRule
778 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
779 We use (toplevel) type instances to normalise both sides of equalities.
783 >--> co1 :: t ~ t' / co2 :: s ~ s'
785 g1 := co1 * g2 * sym co2
788 topRule :: RewriteRule
790 = do { (insts, changed) <- mapAndUnzipM top insts
791 ; return (insts, or changed)
795 = ASSERT( isEqInst inst )
796 do { (coi1, ty1') <- tcNormaliseFamInst ty1
797 ; (coi2, ty2') <- tcNormaliseFamInst ty2
798 ; case (coi1, coi2) of
799 (IdCo, IdCo) -> return (inst, False)
803 -- old_co = co1 * new_co * sym co2
805 do { new_cotv <- newMetaCoVar ty1' ty2'
806 ; let new_co = mkTyVarTy new_cotv
807 old_coi = coi1 `mkTransCoI`
808 ACo new_co `mkTransCoI`
810 ; writeMetaTyVar old_covar (fromACo old_coi)
811 ; return $ mkWantedCo new_cotv
813 -- new_co = sym co1 * old_co * co2
818 mkSymCoI coi1 `mkTransCoI`
819 ACo old_co `mkTransCoI` coi2)
820 ; new_inst <- mkEqInst (EqPred ty1' ty2') wg_co
821 ; return (new_inst, True)
825 ty1 = eqInstLeftTy inst
826 ty2 = eqInstRightTy inst
830 Rewriting with equalities: substRule
831 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
832 From a set of insts, use all insts that can be read as rewrite rules to
833 rewrite the types in all other insts.
837 forall g1 : s1{F c} ~ s2{F c}
840 g1 := s1{g} * g2 * sym s2{g} <=> g2 := sym s1{g} * g1 * s2{g}
842 Alternatively, the rewrite rule may have the form (g : a ~ t).
844 To avoid having to swap rules of the form (g : t ~ F c) and (g : t ~ a),
845 where t is neither a variable nor a type family application, we use them for
846 rewriting from right-to-left. However, it is crucial to only apply rules
847 from right-to-left if they cannot be used left-to-right.
849 The workhorse is substInst, which performs an occurs check before actually
850 using an equality for rewriting. If the type pattern occurs in the type we
851 substitute for the pattern, normalisation would diverge.
854 substRule :: RewriteRule
855 substRule insts = tryAllInsts insts []
857 -- for every inst check whether it can be used to rewrite the others
858 -- (we make an effort to keep the insts in order; it makes debugging
860 tryAllInsts [] triedInsts = return (reverse triedInsts, False)
861 tryAllInsts (inst:insts) triedInsts
862 = do { (insts', changed) <- substInst inst (reverse triedInsts ++ insts)
863 ; if changed then return (insertAt (length triedInsts) inst insts',
865 else tryAllInsts insts (inst:triedInsts)
868 insertAt n x xs = let (xs1, xs2) = splitAt n xs
871 -- Use the given inst as a rewrite rule to normalise the insts in the second
872 -- argument. Don't do anything if the inst cannot be used as a rewrite rule,
873 -- but do apply it right-to-left, if possible, and if it cannot be used
876 substInst :: Inst -> [Inst] -> TcM ([Inst], Bool)
878 = case eqInstToRewrite inst of
879 Just (rewrite, _) -> substEquality rewrite insts
880 Nothing -> return (insts, False)
882 substEquality :: Rewrite -- elementary rewrite
883 -> [Inst] -- insts to rewrite
884 -> TcM ([Inst], Bool)
885 substEquality eqRule@(Rewrite pat rhs _) insts
886 | pat `tcPartOfType` rhs -- occurs check!
887 = occurCheckErr pat rhs
889 = do { (insts', changed) <- mapAndUnzipM substOne insts
890 ; return (insts', or changed)
894 = ASSERT( isEqInst inst )
895 do { (coi1, ty1') <- tcEqRuleNormaliseFamInst eqRule ty1
896 ; (coi2, ty2') <- tcEqRuleNormaliseFamInst eqRule ty2
897 ; case (coi1, coi2) of
898 (IdCo, IdCo) -> return (inst, False)
902 -- old_co := co1 * new_co * sym co2
904 do { new_cotv <- newMetaCoVar ty1' ty2'
905 ; let new_co = mkTyVarTy new_cotv
906 old_coi = coi1 `mkTransCoI`
907 ACo new_co `mkTransCoI`
909 ; writeMetaTyVar old_covar (fromACo old_coi)
910 ; return $ mkWantedCo new_cotv
912 -- new_co := sym co1 * old_co * co2
917 mkSymCoI coi1 `mkTransCoI`
918 ACo old_co `mkTransCoI` coi2)
919 ; new_inst <- mkEqInst (EqPred ty1' ty2') gw_co
920 ; return (new_inst, True)
924 ty1 = eqInstLeftTy inst
925 ty2 = eqInstRightTy inst
929 Instantiate meta variables: unifyMetaRule
930 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
931 If an equality equates a meta type variable with a type, we simply instantiate
940 Meta variables can only appear in wanted constraints, and this rule should
941 only be applied to wanted constraints. We also know that t definitely is
942 distinct from alpha (as the trivialRule) has been run on the insts beforehand.
944 NB: We cannot assume that meta tyvars are empty. They may have been updated
945 by another inst in the currently processed wanted list. We need to be very
946 careful when updateing type variables (see TcUnify.uUnfilledVar), but at least
947 we know that we have no boxes. It's unclear that it would be an advantage to
948 common up the code in TcUnify and the code below. Firstly, we don't want
949 calls to TcUnify.defer_unification here, and secondly, TcUnify import the
950 current module, so we would have to move everything here (Yuk!) or to
951 TcMType. Besides, the code here is much simpler due to the lack of boxes.
954 unifyMetaRule :: RewriteRule
956 = do { (insts', changed) <- mapAndUnzipM unifyMeta insts
957 ; return (concat insts', or changed)
961 = ASSERT( isEqInst inst )
962 go (eqInstLeftTy inst) (eqInstRightTy inst)
963 (fromWantedCo "unifyMetaRule" $ eqInstCoercion inst)
966 | Just ty1' <- tcView ty1 = go ty1' ty2 cotv
967 | Just ty2' <- tcView ty2 = go ty1 ty2' cotv
970 , isMetaTyVar tv1 = do { lookupTV <- lookupTcTyVar tv1
971 ; uMeta False tv1 lookupTV ty2 cotv
974 , isMetaTyVar tv2 = do { lookupTV <- lookupTcTyVar tv2
975 ; uMeta True tv2 lookupTV ty1 cotv
977 | otherwise = return ([inst], False)
979 -- meta variable has been filled already
980 -- => ignore this inst (we'll come around again, after zonking)
981 uMeta _swapped _tv (IndirectTv _) _ty _cotv
982 = return ([inst], False)
984 -- signature skolem meets non-variable type
986 uMeta _swapped _tv (DoneTv (MetaTv (SigTv _) _)) ty _cotv
988 = return ([inst], False)
990 -- type variable meets type variable
991 -- => check that tv2 hasn't been updated yet and choose which to update
992 uMeta swapped tv1 (DoneTv details1) (TyVarTy tv2) cotv
993 = do { lookupTV2 <- lookupTcTyVar tv2
995 IndirectTv ty -> uMeta swapped tv1 (DoneTv details1) ty cotv
997 uMetaVar swapped tv1 details1 tv2 details2 cotv
1000 -- updatable meta variable meets non-variable type
1001 -- => occurs check, monotype check, and kinds match check, then update
1002 uMeta swapped tv (DoneTv (MetaTv _ ref)) ty cotv
1003 = do { mb_ty' <- checkTauTvUpdate tv ty -- occurs + monotype check
1005 Nothing -> return ([inst], False) -- tv occurs in faminst
1007 do { checkUpdateMeta swapped tv ref ty' -- update meta var
1008 ; writeMetaTyVar cotv ty' -- update co var
1013 uMeta _ _ _ _ _ = panic "uMeta"
1015 -- meta variable meets skolem
1017 uMetaVar swapped tv1 (MetaTv _ ref) tv2 (SkolemTv _) cotv
1018 = do { checkUpdateMeta swapped tv1 ref (mkTyVarTy tv2)
1019 ; writeMetaTyVar cotv (mkTyVarTy tv2)
1023 -- meta variable meets meta variable
1024 -- => be clever about which of the two to update
1025 -- (from TcUnify.uUnfilledVars minus boxy stuff)
1026 uMetaVar swapped tv1 (MetaTv info1 ref1) tv2 (MetaTv info2 ref2) cotv
1027 = do { case (info1, info2) of
1028 -- Avoid SigTvs if poss
1029 (SigTv _, _ ) | k1_sub_k2 -> update_tv2
1030 (_, SigTv _) | k2_sub_k1 -> update_tv1
1032 (_, _) | k1_sub_k2 -> if k2_sub_k1 && nicer_to_update_tv1
1033 then update_tv1 -- Same kinds
1035 | k2_sub_k1 -> update_tv1
1036 | otherwise -> kind_err
1037 -- Update the variable with least kind info
1038 -- See notes on type inference in Kind.lhs
1039 -- The "nicer to" part only applies if the two kinds are the same,
1040 -- so we can choose which to do.
1042 ; writeMetaTyVar cotv (mkTyVarTy tv2)
1046 -- Kinds should be guaranteed ok at this point
1047 update_tv1 = updateMeta tv1 ref1 (mkTyVarTy tv2)
1048 update_tv2 = updateMeta tv2 ref2 (mkTyVarTy tv1)
1050 kind_err = addErrCtxtM (unifyKindCtxt swapped tv1 (mkTyVarTy tv2)) $
1051 unifyKindMisMatch k1 k2
1055 k1_sub_k2 = k1 `isSubKind` k2
1056 k2_sub_k1 = k2 `isSubKind` k1
1058 nicer_to_update_tv1 = isSystemName (Var.varName tv1)
1059 -- Try to update sys-y type variables in preference to ones
1060 -- gotten (say) by instantiating a polymorphic function with
1061 -- a user-written type sig
1063 uMetaVar _ _ _ _ _ _ = panic "uMetaVar"
1067 %************************************************************************
1069 \section{Normalisation of Insts}
1071 %************************************************************************
1073 Normalises a set of dictionaries relative to a set of given equalities (which
1074 are interpreted as rewrite rules). We only consider given equalities of the
1079 where F is a type family.
1082 substEqInDictInsts :: [Inst] -- given equalities (used as rewrite rules)
1083 -> [Inst] -- dictinaries to be normalised
1084 -> TcM ([Inst], TcDictBinds)
1085 substEqInDictInsts eqInsts dictInsts
1086 = do { traceTc (text "substEqInDictInst <-" <+> ppr dictInsts)
1088 foldlM rewriteWithOneEquality (dictInsts, emptyBag) eqInsts
1089 ; traceTc (text "substEqInDictInst ->" <+> ppr dictInsts')
1093 -- (1) Given equality of form 'F ts ~ t' or 'a ~ t': use for rewriting
1094 rewriteWithOneEquality (dictInsts, dictBinds)
1095 eqInst@(EqInst {tci_left = pattern,
1096 tci_right = target})
1097 | isOpenSynTyConApp pattern || isTyVarTy pattern
1098 = do { (dictInsts', moreDictBinds) <-
1099 genericNormaliseInsts True {- wanted -} applyThisEq dictInsts
1100 ; return (dictInsts', dictBinds `unionBags` moreDictBinds)
1103 applyThisEq = tcGenericNormaliseFamInstPred (return . matchResult)
1105 -- rewrite in case of an exact match
1106 matchResult ty | tcEqType pattern ty = Just (target, eqInstType eqInst)
1107 | otherwise = Nothing
1109 -- (2) Given equality has the wrong form: ignore
1110 rewriteWithOneEquality (dictInsts, dictBinds) _not_a_rewrite_rule
1111 = return (dictInsts, dictBinds)
1115 Take a bunch of Insts (not EqInsts), and normalise them wrt the top-level
1116 type-function equations, where
1118 (norm_insts, binds) = normaliseInsts is_wanted insts
1121 = True, (binds + norm_insts) defines insts (wanteds)
1122 = False, (binds + insts) defines norm_insts (givens)
1124 Ie, in the case of normalising wanted dictionaries, we use the normalised
1125 dictionaries to define the originally wanted ones. However, in the case of
1126 given dictionaries, we use the originally given ones to define the normalised
1130 normaliseInsts :: Bool -- True <=> wanted insts
1131 -> [Inst] -- wanted or given insts
1132 -> TcM ([Inst], TcDictBinds) -- normalised insts and bindings
1133 normaliseInsts isWanted insts
1134 = genericNormaliseInsts isWanted tcNormaliseFamInstPred insts
1136 genericNormaliseInsts :: Bool -- True <=> wanted insts
1137 -> (TcPredType -> TcM (CoercionI, TcPredType))
1139 -> [Inst] -- wanted or given insts
1140 -> TcM ([Inst], TcDictBinds) -- normalised insts & binds
1141 genericNormaliseInsts isWanted fun insts
1142 = do { (insts', binds) <- mapAndUnzipM (normaliseOneInst isWanted fun) insts
1143 ; return (insts', unionManyBags binds)
1146 normaliseOneInst isWanted fun
1147 dict@(Dict {tci_pred = pred,
1149 = do { traceTc $ text "genericNormaliseInst <-" <+> ppr dict
1150 ; (coi, pred') <- fun pred
1154 do { traceTc $ text "genericNormaliseInst ->" <+> ppr dict
1155 ; return (dict, emptyBag)
1157 -- don't use pred' in this case; otherwise, we get
1158 -- more unfolded closed type synonyms in error messages
1160 do { -- an inst for the new pred
1161 ; dict' <- newDictBndr loc pred'
1162 -- relate the old inst to the new one
1163 -- target_dict = source_dict `cast` st_co
1164 ; let (target_dict, source_dict, st_co)
1165 | isWanted = (dict, dict', mkSymCoercion co)
1166 | otherwise = (dict', dict, co)
1168 -- co :: dict ~ dict'
1169 -- hence, if isWanted
1170 -- dict = dict' `cast` sym co
1172 -- dict' = dict `cast` co
1173 expr = HsVar $ instToId source_dict
1174 cast_expr = HsWrap (WpCo st_co) expr
1175 rhs = L (instLocSpan loc) cast_expr
1176 binds = instToDictBind target_dict rhs
1177 -- return the new inst
1178 ; traceTc $ text "genericNormaliseInst ->" <+> ppr dict'
1179 ; return (dict', binds)
1183 -- TOMDO: What do we have to do about ImplicInst, Method, and LitInst??
1184 normaliseOneInst _isWanted _fun inst
1185 = do { inst' <- zonkInst inst
1186 ; return (inst', emptyBag)
1191 %************************************************************************
1195 %************************************************************************
1197 The infamous couldn't match expected type soandso against inferred type
1198 somethingdifferent message.
1201 eqInstMisMatch :: Inst -> TcM a
1203 = ASSERT( isEqInst inst )
1204 do { (env, msg) <- misMatchMsg ty_act ty_exp
1206 failWithTcM (env, msg)
1209 ty_act = eqInstLeftTy inst
1210 ty_exp = eqInstRightTy inst
1211 InstLoc _ _ ctxt = instLoc inst
1213 -----------------------
1214 misMatchMsg :: TcType -> TcType -> TcM (TidyEnv, SDoc)
1215 -- Generate the message when two types fail to match,
1216 -- going to some trouble to make it helpful.
1217 -- The argument order is: actual type, expected type
1218 misMatchMsg ty_act ty_exp
1219 = do { env0 <- tcInitTidyEnv
1220 ; ty_exp <- zonkTcType ty_exp
1221 ; ty_act <- zonkTcType ty_act
1222 ; (env1, pp_exp, extra_exp) <- ppr_ty env0 ty_exp
1223 ; (env2, pp_act, extra_act) <- ppr_ty env1 ty_act
1225 sep [sep [ptext SLIT("Couldn't match expected type") <+> pp_exp,
1227 ptext SLIT("against inferred type") <+> pp_act],
1228 nest 2 (extra_exp $$ extra_act)]) }
1230 ppr_ty :: TidyEnv -> TcType -> TcM (TidyEnv, SDoc, SDoc)
1232 = do { let (env1, tidy_ty) = tidyOpenType env ty
1233 ; (env2, extra) <- ppr_extra env1 tidy_ty
1234 ; return (env2, quotes (ppr tidy_ty), extra) }
1236 -- (ppr_extra env ty) shows extra info about 'ty'
1237 ppr_extra :: TidyEnv -> Type -> TcM (TidyEnv, SDoc)
1238 ppr_extra env (TyVarTy tv)
1239 | isTcTyVar tv && (isSkolemTyVar tv || isSigTyVar tv) && not (isUnk tv)
1240 = return (env1, pprSkolTvBinding tv1)
1242 (env1, tv1) = tidySkolemTyVar env tv
1244 ppr_extra env _ty = return (env, empty) -- Normal case