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 Normalise a type relative to the rewrite rule implied by one EqInst or an
103 already unpacked EqInst (ie, an equality rewrite rule).
107 tcEqInstNormaliseFamInst :: Inst -> TcType -> TcM (CoercionI, Type)
108 tcEqInstNormaliseFamInst inst =
109 ASSERT( isEqInst inst )
110 tcEqRuleNormaliseFamInst (pat, rhs, co)
112 pat = eqInstLeftTy inst
113 rhs = eqInstRightTy inst
116 -- Rewrite by equality rewrite rule
117 tcEqRuleNormaliseFamInst :: (TcType, -- rewrite rule lhs
118 TcType, -- rewrite rule rhs
119 TcType) -- coercion witnessing the rewrite rule
120 -> TcType -- type to rewrite
121 -> TcM (CoercionI, Type)
122 tcEqRuleNormaliseFamInst (pat, rhs, co) ty
123 = tcGenericNormaliseFamInst matchEqRule ty
125 matchEqRule sty | pat `tcEqType` sty = return $ Just (rhs, co)
126 | otherwise = return $ Nothing
129 Generic normalisation of 'Type's and 'PredType's; ie, walk the type term and
130 apply the normalisation function gives as the first argument to every TyConApp
131 and every TyVarTy subterm.
133 tcGenericNormaliseFamInst fun ty = (co, ty')
136 This function is (by way of using smart constructors) careful to ensure that
137 the returned coercion is exactly IdCo (and not some semantically equivalent,
138 but syntactically different coercion) whenever (ty' `tcEqType` ty). This
139 makes it easy for the caller to determine whether the type changed. BUT
140 even if we return IdCo, ty' may be *syntactically* different from ty due to
141 unfolded closed type synonyms (by way of tcCoreView). In the interest of
142 good error messages, callers should discard ty' in favour of ty in this case.
145 tcGenericNormaliseFamInst :: (TcType -> TcM (Maybe (TcType, Coercion)))
146 -- what to do with type functions and tyvars
147 -> TcType -- old type
148 -> TcM (CoercionI, TcType) -- (coercion, new type)
149 tcGenericNormaliseFamInst fun ty
150 | Just ty' <- tcView ty = tcGenericNormaliseFamInst fun ty'
151 tcGenericNormaliseFamInst fun (TyConApp tyCon tys)
152 = do { (cois, ntys) <- mapAndUnzipM (tcGenericNormaliseFamInst fun) tys
153 ; let tycon_coi = mkTyConAppCoI tyCon ntys cois
154 ; maybe_ty_co <- fun (mkTyConApp tyCon ntys) -- use normalised args!
155 ; case maybe_ty_co of
156 -- a matching family instance exists
158 do { let first_coi = mkTransCoI tycon_coi (ACo co)
159 ; (rest_coi, nty) <- tcGenericNormaliseFamInst fun ty'
160 ; let fix_coi = mkTransCoI first_coi rest_coi
161 ; return (fix_coi, nty)
163 -- no matching family instance exists
164 -- we do not do anything
165 Nothing -> return (tycon_coi, mkTyConApp tyCon ntys)
167 tcGenericNormaliseFamInst fun (AppTy ty1 ty2)
168 = do { (coi1,nty1) <- tcGenericNormaliseFamInst fun ty1
169 ; (coi2,nty2) <- tcGenericNormaliseFamInst fun ty2
170 ; return (mkAppTyCoI nty1 coi1 nty2 coi2, mkAppTy nty1 nty2)
172 tcGenericNormaliseFamInst fun (FunTy ty1 ty2)
173 = do { (coi1,nty1) <- tcGenericNormaliseFamInst fun ty1
174 ; (coi2,nty2) <- tcGenericNormaliseFamInst fun ty2
175 ; return (mkFunTyCoI nty1 coi1 nty2 coi2, mkFunTy nty1 nty2)
177 tcGenericNormaliseFamInst fun (ForAllTy tyvar ty1)
178 = do { (coi,nty1) <- tcGenericNormaliseFamInst fun ty1
179 ; return (mkForAllTyCoI tyvar coi, mkForAllTy tyvar nty1)
181 tcGenericNormaliseFamInst fun (NoteTy note ty1)
182 = do { (coi,nty1) <- tcGenericNormaliseFamInst fun ty1
183 ; return (mkNoteTyCoI note coi, NoteTy note nty1)
185 tcGenericNormaliseFamInst fun ty@(TyVarTy tv)
187 = do { traceTc (text "tcGenericNormaliseFamInst" <+> ppr ty)
188 ; res <- lookupTcTyVar tv
191 do { maybe_ty' <- fun ty
193 Nothing -> return (IdCo, ty)
195 do { (coi2, ty'') <- tcGenericNormaliseFamInst fun ty'
196 ; return (ACo co1 `mkTransCoI` coi2, ty'')
199 IndirectTv ty' -> tcGenericNormaliseFamInst fun ty'
203 tcGenericNormaliseFamInst fun (PredTy predty)
204 = do { (coi, pred') <- tcGenericNormaliseFamInstPred fun predty
205 ; return (coi, PredTy pred') }
207 ---------------------------------
208 tcGenericNormaliseFamInstPred :: (TcType -> TcM (Maybe (TcType,Coercion)))
210 -> TcM (CoercionI, TcPredType)
212 tcGenericNormaliseFamInstPred fun (ClassP cls tys)
213 = do { (cois, tys')<- mapAndUnzipM (tcGenericNormaliseFamInst fun) tys
214 ; return (mkClassPPredCoI cls tys' cois, ClassP cls tys')
216 tcGenericNormaliseFamInstPred fun (IParam ipn ty)
217 = do { (coi, ty') <- tcGenericNormaliseFamInst fun ty
218 ; return $ (mkIParamPredCoI ipn coi, IParam ipn ty')
220 tcGenericNormaliseFamInstPred fun (EqPred ty1 ty2)
221 = do { (coi1, ty1') <- tcGenericNormaliseFamInst fun ty1
222 ; (coi2, ty2') <- tcGenericNormaliseFamInst fun ty2
223 ; return (mkEqPredCoI ty1' coi1 ty2' coi2, EqPred ty1' ty2') }
227 %************************************************************************
229 \section{Normalisation of equality constraints}
231 %************************************************************************
233 Note [Inconsistencies in equality constraints]
234 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
235 We guarantee that we raise an error if we discover any inconsistencies (i.e.,
236 equalities that if presented to the unifer in TcUnify would result in an
237 error) during normalisation of wanted constraints. This is especially so that
238 we don't solve wanted constraints under an inconsistent given set. In
239 particular, we don't want to permit signatures, such as
241 bad :: (Int ~ Bool => Int) -> a -> a
244 normaliseGivenEqs :: [Inst] -> TcM ([Inst], TcM ())
245 normaliseGivenEqs givens
246 = do { traceTc (text "normaliseGivenEqs <-" <+> ppr givens)
247 ; (result, deSkolem) <-
248 rewriteToFixedPoint (Just ("(SkolemOccurs)", skolemOccurs))
249 [ ("(ZONK)", dontRerun $ zonkInsts)
250 , ("(TRIVIAL)", dontRerun $ trivialRule)
251 , ("(DECOMP)", decompRule)
253 , ("(SUBST)", substRule) -- incl. occurs check
255 ; traceTc (text "normaliseGivenEqs ->" <+> ppr result)
256 ; return (result, deSkolem)
261 normaliseWantedEqs :: [Inst] -> TcM [Inst]
262 normaliseWantedEqs insts
263 = do { traceTc (text "normaliseWantedEqs <-" <+> ppr insts)
264 ; result <- liftM fst $ rewriteToFixedPoint Nothing
265 [ ("(ZONK)", dontRerun $ zonkInsts)
266 , ("(TRIVIAL)", dontRerun $ trivialRule)
267 , ("(DECOMP)", decompRule)
269 , ("(UNIFY)", unifyMetaRule) -- incl. occurs check
270 , ("(SUBST)", substRule) -- incl. occurs check
272 ; traceTc (text "normaliseWantedEqs ->" <+> ppr result)
278 %************************************************************************
280 \section{Solving of wanted constraints with respect to a given set}
282 %************************************************************************
284 The set of given equalities must have been normalised already.
287 solveWantedEqs :: [Inst] -- givens
289 -> TcM [Inst] -- irreducible wanteds
290 solveWantedEqs givens wanteds
291 = do { traceTc $ text "solveWantedEqs <-" <+> ppr wanteds <+> text "with" <+>
293 ; result <- liftM fst $ rewriteToFixedPoint Nothing
294 [ ("(ZONK)", dontRerun $ zonkInsts)
295 , ("(TRIVIAL)", dontRerun $ trivialRule)
296 , ("(DECOMP)", decompRule)
298 , ("(GIVEN)", substGivens givens) -- incl. occurs check
299 , ("(UNIFY)", unifyMetaRule) -- incl. occurs check
301 ; traceTc (text "solveWantedEqs ->" <+> ppr result)
305 -- Use `substInst' with every given on all the wanteds.
306 substGivens :: [Inst] -> [Inst] -> TcM ([Inst], Bool)
307 substGivens [] wanteds = return (wanteds, False)
308 substGivens (g:gs) wanteds
309 = do { (wanteds1, changed1) <- substGivens gs wanteds
310 ; (wanteds2, changed2) <- substInst g wanteds1
311 ; return (wanteds2, changed1 || changed2)
316 %************************************************************************
318 \section{Normalisation of non-equality dictionaries}
320 %************************************************************************
323 normaliseGivenDicts, normaliseWantedDicts
324 :: [Inst] -- given equations
325 -> [Inst] -- dictionaries
326 -> TcM ([Inst],TcDictBinds)
328 normaliseGivenDicts eqs dicts = normalise_dicts eqs dicts False
329 normaliseWantedDicts eqs dicts = normalise_dicts eqs dicts True
332 :: [Inst] -- given equations
333 -> [Inst] -- dictionaries
334 -> Bool -- True <=> the dicts are wanted
335 -- Fals <=> they are given
336 -> TcM ([Inst],TcDictBinds)
337 normalise_dicts given_eqs dicts is_wanted
338 = do { traceTc $ text "normalise???Dicts <-" <+> ppr dicts <+>
339 text "with" <+> ppr given_eqs
340 ; (dicts0, binds0) <- normaliseInsts is_wanted dicts
341 ; (dicts1, binds1) <- substEqInDictInsts given_eqs dicts0
342 ; let binds01 = binds0 `unionBags` binds1
343 ; if isEmptyBag binds1
344 then return (dicts1, binds01)
345 else do { (dicts2, binds2) <- normaliseGivenDicts given_eqs dicts1
346 ; return (dicts2, binds01 `unionBags` binds2) } }
350 %************************************************************************
352 \section{Normalisation rules and iterative rule application}
354 %************************************************************************
356 We have three kinds of normalising rewrite rules:
358 (1) Normalisation rules that rewrite a set of insts and return a flag indicating
359 whether any changes occurred during rewriting that necessitate re-running
360 the current rule set.
362 (2) Precondition rules that rewrite a set of insts and return a monadic action
363 that reverts the effect of preconditioning.
365 (3) Idempotent normalisation rules that never require re-running the rule set.
368 type RewriteRule = [Inst] -> TcM ([Inst], Bool) -- rewrite, maybe re-run
369 type PrecondRule = [Inst] -> TcM ([Inst], TcM ()) -- rewrite, revertable
370 type IdemRewriteRule = [Inst] -> TcM [Inst] -- rewrite, don't re-run
372 type NamedRule = (String, RewriteRule) -- rule with description
373 type NamedPreRule = (String, PrecondRule) -- precond with desc
376 Template lifting idempotent rules to full rules (which can be put into a rule
380 dontRerun :: IdemRewriteRule -> RewriteRule
381 dontRerun rule insts = liftM addFalse $ rule insts
383 addFalse x = (x, False)
386 The following function applies a set of rewrite rules until a fixed point is
387 reached; i.e., none of the `RewriteRule's require re-running the rule set.
388 Optionally, there may be a pre-conditing rule that is applied before any other
389 rules are applied and before the rule set is re-run.
391 The result is the set of rewritten (i.e., normalised) insts and, in case of a
392 pre-conditing rule, a monadic action that reverts the effects of
393 pre-conditioning - specifically, this is removing introduced skolems.
396 rewriteToFixedPoint :: Maybe NamedPreRule -- optional preconditioning rule
397 -> [NamedRule] -- rule set
398 -> [Inst] -- insts to rewrite
399 -> TcM ([Inst], TcM ())
400 rewriteToFixedPoint precondRule rules insts
401 = completeRewrite (return ()) precondRule insts
403 completeRewrite :: TcM () -> Maybe NamedPreRule -> [Inst]
404 -> TcM ([Inst], TcM ())
405 completeRewrite dePrecond (Just (precondName, precond)) insts
406 = do { traceTc $ text precondName <+> text " <- " <+> ppr insts
407 ; (insts', dePrecond') <- precond insts
408 ; traceTc $ text precondName <+> text " -> " <+> ppr insts'
409 ; tryRules (dePrecond >> dePrecond') rules insts'
411 completeRewrite dePrecond Nothing insts
412 = tryRules dePrecond rules insts
414 tryRules dePrecond _ [] = return ([] , dePrecond)
415 tryRules dePrecond [] insts = return (insts, dePrecond)
416 tryRules dePrecond ((name, rule):rules) insts
417 = do { traceTc $ text name <+> text " <- " <+> ppr insts
418 ; (insts', rerun) <- rule insts
419 ; traceTc $ text name <+> text " -> " <+> ppr insts'
420 ; if rerun then completeRewrite dePrecond precondRule insts'
421 else tryRules dePrecond rules insts'
426 %************************************************************************
428 \section{Different forms of Inst rewrite rules}
430 %************************************************************************
432 Splitting of non-terminating given constraints: skolemOccurs
433 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
434 This is a preconditioning rule exclusively applied to given constraints.
435 Moreover, its rewriting is only temporary, as it is undone by way of
436 side-effecting mutable type variables after simplification and constraint
437 entailment has been completed.
439 This version is an (attempt at, yet unproven, an) *unflattened* version of
440 the SubstL-Ev completion rule.
442 The above rule is essential to catch non-terminating rules that cannot be
443 oriented properly, like
449 The left-to-right orientiation is not suitable because it does not
450 terminate. The right-to-left orientation is not suitable because it
451 does not have a type-function on the left. This is undesirable because
452 it would hide information. E.g. assume
456 then rewriting C [G (F a)] to C (F a) is bad because we cannot now
457 see that the C [x] instance applies.
459 The rule also caters for badly-oriented rules of the form:
463 for which other solutions are possible, but this one will do too.
467 co : ty1 ~ ty2{F ty1}
470 sym (F co) : F ty2{b} ~ b
471 where b is a fresh skolem variable
473 We also cater for the symmetric situation *if* the rule cannot be used as a
474 left-to-right rewrite rule.
476 We also return an action (b := ty1) which is used to eliminate b
477 after the dust of normalisation with the completed rewrite system
480 A subtle point of this transformation is that both coercions in the results
481 are strictly speaking incorrect. However, they are correct again after the
482 action {B := ty1} has removed the skolem again. This happens immediately
483 after constraint entailment has been checked; ie, code outside of the
484 simplification and entailment checking framework will never see these
485 temporarily incorrect coercions.
487 NB: We perform this transformation for multiple occurences of ty1 under one
488 or multiple family applications on the left-hand side at once (ie, the
489 rule doesn't need to be applied multiple times at a single inst). As a
490 result we can get two or more insts back.
493 skolemOccurs :: PrecondRule
495 = do { (instss, undoSkolems) <- mapAndUnzipM oneSkolemOccurs insts
496 ; return (concat instss, sequence_ undoSkolems)
500 = ASSERT( isEqInst inst )
501 isRewriteRule (eqInstLeftTy inst) (eqInstRightTy inst)
504 -- look through synonyms
505 isRewriteRule ty1 ty2 | Just ty1' <- tcView ty1 = isRewriteRule ty1' ty2
506 isRewriteRule ty1 ty2 | Just ty2' <- tcView ty2 = isRewriteRule ty1 ty2'
508 -- left-to-right rule with type family head
509 isRewriteRule ty1@(TyConApp con _) ty2
511 = breakRecursion ty1 ty2 False -- not swapped
513 -- left-to-right rule with type variable head
514 isRewriteRule ty1@(TyVarTy _) ty2
515 = breakRecursion ty1 ty2 False -- not swapped
517 -- right-to-left rule with type family head
518 isRewriteRule ty1 ty2@(TyConApp con _)
520 = breakRecursion ty2 ty1 True -- swapped
522 -- right-to-left rule with type variable head
523 isRewriteRule ty1 ty2@(TyVarTy _)
524 = breakRecursion ty2 ty1 True -- swapped
526 -- this equality is not a rewrite rule => ignore
527 isRewriteRule _ _ = return ([inst], return ())
530 breakRecursion pat body swapped
532 = return ([inst], return ())
534 = do { skTvs <- mapM (newMetaTyVar TauTv . typeKind) tysToLiftOut
535 ; let skTvs_tysTLO = zip skTvs tysToLiftOut
536 insertSkolems = return . replace skTvs_tysTLO
537 ; (_, body') <- tcGenericNormaliseFamInst insertSkolems body
538 ; inst' <- if swapped then mkEqInst (EqPred body' pat) co
539 else mkEqInst (EqPred pat body') co
540 -- ensure to reconstruct the inst in the
541 -- original orientation
542 ; (insts, undoSk) <- mapAndUnzipM (mkSkolemInst inst')
544 ; return (inst':insts, sequence_ undoSk)
547 co = eqInstCoercion inst
549 -- all subtypes that are (1) type family instances and (2) contain
550 -- the lhs type as part of the type arguments of the type family
552 tysToLiftOut = [mkTyConApp tc tys | (tc, tys) <- tyFamInsts body
553 , any (pat `tcPartOfType`) tys]
555 replace :: [(TcTyVar, Type)] -> Type -> Maybe (Type, Coercion)
556 replace [] _ = Nothing
557 replace ((skTv, tyTLO):rest) ty
558 | tyTLO `tcEqType` ty = Just (mkTyVarTy skTv, undefined)
559 | otherwise = replace rest ty
561 -- create the EqInst for the equality determining the skolem and a
562 -- TcM action undoing the skolem introduction
563 mkSkolemInst inst' (skTv, tyTLO)
564 = do { (co, tyLiftedOut) <- tcEqInstNormaliseFamInst inst' tyTLO
565 ; inst <- mkEqInst (EqPred tyLiftedOut (mkTyVarTy skTv))
566 (mkGivenCo $ mkSymCoercion (fromACo co))
567 ; return (inst, writeMetaTyVar skTv tyTLO)
572 Removal of trivial equalities: trivialRule
573 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
574 The following rules exploits the reflexivity of equality:
582 trivialRule :: IdemRewriteRule
584 = liftM catMaybes $ mappM trivial insts
587 | ASSERT( isEqInst inst )
589 = do { eitherEqInst inst
590 (\cotv -> writeMetaTyVar cotv ty1)
597 ty1 = eqInstLeftTy inst
598 ty2 = eqInstRightTy inst
602 Decomposition of data type constructors: decompRule
603 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
604 Whenever, the same *data* constructors occurs on both sides of an equality, we
605 can decompose as in standard unification.
610 g21 : c1 ~ d1, ..., g2n : cn ~ dn
613 Works also for the case where T is actually an application of a type family
614 constructor to a set of types, provided the applications on both sides of the
615 ~ are identical; see also Note [OpenSynTyCon app] in TcUnify.
617 We guarantee to raise an error for any inconsistent equalities;
618 cf Note [Inconsistencies in equality constraints].
621 decompRule :: RewriteRule
623 = do { (insts, changed) <- mapAndUnzipM decomp insts
624 ; return (concat insts, or changed)
628 = ASSERT( isEqInst inst )
629 go (eqInstLeftTy inst) (eqInstRightTy inst)
632 | Just ty1' <- tcView ty1 = go ty1' ty2
633 | Just ty2' <- tcView ty2 = go ty1 ty2'
635 go (TyConApp con1 tys1) (TyConApp con2 tys2)
636 | con1 == con2 && identicalHead
637 = mkArgInsts (mkTyConApp con1) tys1 tys2
639 | con1 /= con2 && not (isOpenSynTyCon con1 || isOpenSynTyCon con2)
640 -- not matching data constructors (of any flavour) are bad news
641 = eqInstMisMatch inst
644 (idxTys1, _) = splitAt n tys1
645 (idxTys2, _) = splitAt n tys2
646 identicalHead = not (isOpenSynTyCon con1) ||
647 idxTys1 `tcEqTypes` idxTys2
649 go (FunTy fun1 arg1) (FunTy fun2 arg2)
650 = mkArgInsts (\[funCo, argCo] -> mkFunTy funCo argCo) [fun1, arg1]
653 -- Applications need a bit of care!
654 -- They can match FunTy and TyConApp, so use splitAppTy_maybe
656 | Just (s2, t2) <- tcSplitAppTy_maybe ty2
657 = mkArgInsts (\[s, t] -> mkAppTy s t) [s1, t1] [s2, t2]
661 | Just (s1, t1) <- tcSplitAppTy_maybe ty1
662 = mkArgInsts (\[s, t] -> mkAppTy s t) [s1, t1] [s2, t2]
664 -- We already covered all the consistent cases of rigid types on both
665 -- sides; so, if we see two rigid types here, we discovered an
668 | isRigid ty1 && isRigid ty2
669 = eqInstMisMatch inst
671 -- We can neither assert consistency nor inconsistency => defer
672 go _ _ = return ([inst], False)
674 isRigid (TyConApp con _) = not (isOpenSynTyCon con)
675 isRigid (FunTy _ _) = True
676 isRigid (AppTy _ _) = True
679 -- Create insts for matching argument positions (ie, the bit after
680 -- '>-->' in the rule description above)
681 mkArgInsts con tys1 tys2
682 = do { cos <- eitherEqInst inst
683 -- old_co := Con1 cos
685 do { cotvs <- zipWithM newMetaCoVar tys1 tys2
686 ; let cos = map mkTyVarTy cotvs
687 ; writeMetaTyVar old_covar (con cos)
688 ; return $ map mkWantedCo cotvs
690 -- co_i := Con_i old_co
692 return $ map mkGivenCo $
693 mkRightCoercions (length tys1) old_co)
694 ; insts <- zipWithM mkEqInst (zipWith EqPred tys1 tys2) cos
695 ; traceTc (text "decomp identicalHead" <+> ppr insts)
696 ; return (insts, not $ null insts)
701 Rewriting with type instances: topRule
702 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
703 We use (toplevel) type instances to normalise both sides of equalities.
707 >--> co1 :: t ~ t' / co2 :: s ~ s'
709 g1 := co1 * g2 * sym co2
712 topRule :: RewriteRule
714 = do { (insts, changed) <- mapAndUnzipM top insts
715 ; return (insts, or changed)
719 = ASSERT( isEqInst inst )
720 do { (coi1, ty1') <- tcNormaliseFamInst ty1
721 ; (coi2, ty2') <- tcNormaliseFamInst ty2
722 ; case (coi1, coi2) of
723 (IdCo, IdCo) -> return (inst, False)
727 -- old_co = co1 * new_co * sym co2
729 do { new_cotv <- newMetaCoVar ty1' ty2'
730 ; let new_co = mkTyVarTy new_cotv
731 old_coi = coi1 `mkTransCoI`
732 ACo new_co `mkTransCoI`
734 ; writeMetaTyVar old_covar (fromACo old_coi)
735 ; return $ mkWantedCo new_cotv
737 -- new_co = sym co1 * old_co * co2
742 mkSymCoI coi1 `mkTransCoI`
743 ACo old_co `mkTransCoI` coi2)
744 ; new_inst <- mkEqInst (EqPred ty1' ty2') wg_co
745 ; return (new_inst, True)
749 ty1 = eqInstLeftTy inst
750 ty2 = eqInstRightTy inst
754 Rewriting with equalities: substRule
755 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
756 From a set of insts, use all insts that can be read as rewrite rules to
757 rewrite the types in all other insts.
761 forall g1 : s1{F c} ~ s2{F c}
764 g1 := s1{g} * g2 * sym s2{g} <=> g2 := sym s1{g} * g1 * s2{g}
766 Alternatively, the rewrite rule may have the form (g : a ~ t).
768 To avoid having to swap rules of the form (g : t ~ F c) and (g : t ~ a),
769 where t is neither a variable nor a type family application, we use them for
770 rewriting from right-to-left. However, it is crucial to only apply rules
771 from right-to-left if they cannot be used left-to-right.
773 The workhorse is substInst, which performs an occurs check before actually
774 using an equality for rewriting. If the type pattern occurs in the type we
775 substitute for the pattern, normalisation would diverge.
778 substRule :: RewriteRule
779 substRule insts = tryAllInsts insts []
781 -- for every inst check whether it can be used to rewrite the others
782 -- (we make an effort to keep the insts in order; it makes debugging
784 tryAllInsts [] triedInsts = return (reverse triedInsts, False)
785 tryAllInsts (inst:insts) triedInsts
786 = do { (insts', changed) <- substInst inst (reverse triedInsts ++ insts)
787 ; if changed then return (insertAt (length triedInsts) inst insts',
789 else tryAllInsts insts (inst:triedInsts)
792 insertAt n x xs = let (xs1, xs2) = splitAt n xs
795 -- Use the given inst as a rewrite rule to normalise the insts in the second
796 -- argument. Don't do anything if the inst cannot be used as a rewrite rule,
797 -- but do apply it right-to-left, if possible, and if it cannot be used
800 substInst :: Inst -> [Inst] -> TcM ([Inst], Bool)
802 = ASSERT( isEqInst inst )
803 go (eqInstLeftTy inst) (eqInstRightTy inst) (eqInstType inst)
805 -- look through synonyms
806 go ty1 ty2 co | Just ty1' <- tcView ty1 = go ty1' ty2 co
807 go ty1 ty2 co | Just ty2' <- tcView ty2 = go ty1 ty2' co
809 -- rewrite type family applications
810 go ty1@(TyConApp con _) ty2 co
812 = substEquality (ty1, ty2, co) insts
815 go ty1@(TyVarTy tv) ty2 co
817 = substEquality (ty1, ty2, co) insts
819 -- rewrite type family applications from right-to-left, only after
820 -- having checked whether we can work left-to-right
821 go ty1 ty2@(TyConApp con _) co
823 = substEquality (ty2, ty1, mkSymCoercion co) insts
825 -- rewrite skolems from right-to-left, only after having checked
826 -- whether we can work left-to-right
827 go ty1 ty2@(TyVarTy tv) co
829 = substEquality (ty2, ty1, mkSymCoercion co) insts
831 go _ _ _ = return (insts, False)
833 substEquality :: (TcType, -- rewrite rule lhs
834 TcType, -- rewrite rule rhs
835 TcType) -- coercion witnessing the rewrite rule
836 -> [Inst] -- insts to rewrite
837 -> TcM ([Inst], Bool)
838 substEquality eqRule@(pat, rhs, _) insts
839 | pat `tcPartOfType` rhs -- occurs check!
840 = occurCheckErr pat rhs
842 = do { (insts', changed) <- mapAndUnzipM substOne insts
843 ; return (insts', or changed)
847 = ASSERT( isEqInst inst )
848 do { (coi1, ty1') <- tcEqRuleNormaliseFamInst eqRule ty1
849 ; (coi2, ty2') <- tcEqRuleNormaliseFamInst eqRule ty2
850 ; case (coi1, coi2) of
851 (IdCo, IdCo) -> return (inst, False)
855 -- old_co := co1 * new_co * sym co2
857 do { new_cotv <- newMetaCoVar ty1' ty2'
858 ; let new_co = mkTyVarTy new_cotv
859 old_coi = coi1 `mkTransCoI`
860 ACo new_co `mkTransCoI`
862 ; writeMetaTyVar old_covar (fromACo old_coi)
863 ; return $ mkWantedCo new_cotv
865 -- new_co := sym co1 * old_co * co2
870 mkSymCoI coi1 `mkTransCoI`
871 ACo old_co `mkTransCoI` coi2)
872 ; new_inst <- mkEqInst (EqPred ty1' ty2') gw_co
873 ; return (new_inst, True)
877 ty1 = eqInstLeftTy inst
878 ty2 = eqInstRightTy inst
882 Instantiate meta variables: unifyMetaRule
883 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
884 If an equality equates a meta type variable with a type, we simply instantiate
893 Meta variables can only appear in wanted constraints, and this rule should
894 only be applied to wanted constraints. We also know that t definitely is
895 distinct from alpha (as the trivialRule) has been run on the insts beforehand.
897 NB: We cannot assume that meta tyvars are empty. They may have been updated
898 by another inst in the currently processed wanted list. We need to be very
899 careful when updateing type variables (see TcUnify.uUnfilledVar), but at least
900 we know that we have no boxes. It's unclear that it would be an advantage to
901 common up the code in TcUnify and the code below. Firstly, we don't want
902 calls to TcUnify.defer_unification here, and secondly, TcUnify import the
903 current module, so we would have to move everything here (Yuk!) or to
904 TcMType. Besides, the code here is much simpler due to the lack of boxes.
907 unifyMetaRule :: RewriteRule
909 = do { (insts', changed) <- mapAndUnzipM unifyMeta insts
910 ; return (concat insts', or changed)
914 = ASSERT( isEqInst inst )
915 go (eqInstLeftTy inst) (eqInstRightTy inst)
916 (fromWantedCo "unifyMetaRule" $ eqInstCoercion inst)
919 | Just ty1' <- tcView ty1 = go ty1' ty2 cotv
920 | Just ty2' <- tcView ty2 = go ty1 ty2' cotv
923 , isMetaTyVar tv1 = do { lookupTV <- lookupTcTyVar tv1
924 ; uMeta False tv1 lookupTV ty2 cotv
927 , isMetaTyVar tv2 = do { lookupTV <- lookupTcTyVar tv2
928 ; uMeta True tv2 lookupTV ty1 cotv
930 | otherwise = return ([inst], False)
932 -- meta variable has been filled already
933 -- => ignore this inst (we'll come around again, after zonking)
934 uMeta _swapped _tv (IndirectTv _) _ty _cotv
935 = return ([inst], False)
937 -- signature skolem meets non-variable type
939 uMeta _swapped _tv (DoneTv (MetaTv (SigTv _) _)) ty _cotv
941 = return ([inst], False)
943 -- type variable meets type variable
944 -- => check that tv2 hasn't been updated yet and choose which to update
945 uMeta swapped tv1 (DoneTv details1) (TyVarTy tv2) cotv
946 = do { lookupTV2 <- lookupTcTyVar tv2
948 IndirectTv ty -> uMeta swapped tv1 (DoneTv details1) ty cotv
950 uMetaVar swapped tv1 details1 tv2 details2 cotv
953 -- updatable meta variable meets non-variable type
954 -- => occurs check, monotype check, and kinds match check, then update
955 uMeta swapped tv (DoneTv (MetaTv _ ref)) ty cotv
956 = do { mb_ty' <- checkTauTvUpdate tv ty -- occurs + monotype check
958 Nothing -> return ([inst], False) -- tv occurs in faminst
960 do { checkUpdateMeta swapped tv ref ty' -- update meta var
961 ; writeMetaTyVar cotv ty' -- update co var
966 uMeta _ _ _ _ _ = panic "uMeta"
968 -- meta variable meets skolem
970 uMetaVar swapped tv1 (MetaTv _ ref) tv2 (SkolemTv _) cotv
971 = do { checkUpdateMeta swapped tv1 ref (mkTyVarTy tv2)
972 ; writeMetaTyVar cotv (mkTyVarTy tv2)
976 -- meta variable meets meta variable
977 -- => be clever about which of the two to update
978 -- (from TcUnify.uUnfilledVars minus boxy stuff)
979 uMetaVar swapped tv1 (MetaTv info1 ref1) tv2 (MetaTv info2 ref2) cotv
980 = do { case (info1, info2) of
981 -- Avoid SigTvs if poss
982 (SigTv _, _ ) | k1_sub_k2 -> update_tv2
983 (_, SigTv _) | k2_sub_k1 -> update_tv1
985 (_, _) | k1_sub_k2 -> if k2_sub_k1 && nicer_to_update_tv1
986 then update_tv1 -- Same kinds
988 | k2_sub_k1 -> update_tv1
989 | otherwise -> kind_err
990 -- Update the variable with least kind info
991 -- See notes on type inference in Kind.lhs
992 -- The "nicer to" part only applies if the two kinds are the same,
993 -- so we can choose which to do.
995 ; writeMetaTyVar cotv (mkTyVarTy tv2)
999 -- Kinds should be guaranteed ok at this point
1000 update_tv1 = updateMeta tv1 ref1 (mkTyVarTy tv2)
1001 update_tv2 = updateMeta tv2 ref2 (mkTyVarTy tv1)
1003 kind_err = addErrCtxtM (unifyKindCtxt swapped tv1 (mkTyVarTy tv2)) $
1004 unifyKindMisMatch k1 k2
1008 k1_sub_k2 = k1 `isSubKind` k2
1009 k2_sub_k1 = k2 `isSubKind` k1
1011 nicer_to_update_tv1 = isSystemName (Var.varName tv1)
1012 -- Try to update sys-y type variables in preference to ones
1013 -- gotten (say) by instantiating a polymorphic function with
1014 -- a user-written type sig
1016 uMetaVar _ _ _ _ _ _ = panic "uMetaVar"
1020 %************************************************************************
1022 \section{Normalisation of Insts}
1024 %************************************************************************
1026 Normalises a set of dictionaries relative to a set of given equalities (which
1027 are interpreted as rewrite rules). We only consider given equalities of the
1032 where F is a type family.
1035 substEqInDictInsts :: [Inst] -- given equalities (used as rewrite rules)
1036 -> [Inst] -- dictinaries to be normalised
1037 -> TcM ([Inst], TcDictBinds)
1038 substEqInDictInsts eqInsts dictInsts
1039 = do { traceTc (text "substEqInDictInst <-" <+> ppr dictInsts)
1041 foldlM rewriteWithOneEquality (dictInsts, emptyBag) eqInsts
1042 ; traceTc (text "substEqInDictInst ->" <+> ppr dictInsts')
1046 -- (1) Given equality of form 'F ts ~ t' or 'a ~ t': use for rewriting
1047 rewriteWithOneEquality (dictInsts, dictBinds)
1048 eqInst@(EqInst {tci_left = pattern,
1049 tci_right = target})
1050 | isOpenSynTyConApp pattern || isTyVarTy pattern
1051 = do { (dictInsts', moreDictBinds) <-
1052 genericNormaliseInsts True {- wanted -} applyThisEq dictInsts
1053 ; return (dictInsts', dictBinds `unionBags` moreDictBinds)
1056 applyThisEq = tcGenericNormaliseFamInstPred (return . matchResult)
1058 -- rewrite in case of an exact match
1059 matchResult ty | tcEqType pattern ty = Just (target, eqInstType eqInst)
1060 | otherwise = Nothing
1062 -- (2) Given equality has the wrong form: ignore
1063 rewriteWithOneEquality (dictInsts, dictBinds) _not_a_rewrite_rule
1064 = return (dictInsts, dictBinds)
1068 Take a bunch of Insts (not EqInsts), and normalise them wrt the top-level
1069 type-function equations, where
1071 (norm_insts, binds) = normaliseInsts is_wanted insts
1074 = True, (binds + norm_insts) defines insts (wanteds)
1075 = False, (binds + insts) defines norm_insts (givens)
1077 Ie, in the case of normalising wanted dictionaries, we use the normalised
1078 dictionaries to define the originally wanted ones. However, in the case of
1079 given dictionaries, we use the originally given ones to define the normalised
1083 normaliseInsts :: Bool -- True <=> wanted insts
1084 -> [Inst] -- wanted or given insts
1085 -> TcM ([Inst], TcDictBinds) -- normalised insts and bindings
1086 normaliseInsts isWanted insts
1087 = genericNormaliseInsts isWanted tcNormaliseFamInstPred insts
1089 genericNormaliseInsts :: Bool -- True <=> wanted insts
1090 -> (TcPredType -> TcM (CoercionI, TcPredType))
1092 -> [Inst] -- wanted or given insts
1093 -> TcM ([Inst], TcDictBinds) -- normalised insts & binds
1094 genericNormaliseInsts isWanted fun insts
1095 = do { (insts', binds) <- mapAndUnzipM (normaliseOneInst isWanted fun) insts
1096 ; return (insts', unionManyBags binds)
1099 normaliseOneInst isWanted fun
1100 dict@(Dict {tci_pred = pred,
1102 = do { traceTc $ text "genericNormaliseInst <-" <+> ppr dict
1103 ; (coi, pred') <- fun pred
1107 do { traceTc $ text "genericNormaliseInst ->" <+> ppr dict
1108 ; return (dict, emptyBag)
1110 -- don't use pred' in this case; otherwise, we get
1111 -- more unfolded closed type synonyms in error messages
1113 do { -- an inst for the new pred
1114 ; dict' <- newDictBndr loc pred'
1115 -- relate the old inst to the new one
1116 -- target_dict = source_dict `cast` st_co
1117 ; let (target_dict, source_dict, st_co)
1118 | isWanted = (dict, dict', mkSymCoercion co)
1119 | otherwise = (dict', dict, co)
1121 -- co :: dict ~ dict'
1122 -- hence, if isWanted
1123 -- dict = dict' `cast` sym co
1125 -- dict' = dict `cast` co
1126 expr = HsVar $ instToId source_dict
1127 cast_expr = HsWrap (WpCo st_co) expr
1128 rhs = L (instLocSpan loc) cast_expr
1129 binds = instToDictBind target_dict rhs
1130 -- return the new inst
1131 ; traceTc $ text "genericNormaliseInst ->" <+> ppr dict'
1132 ; return (dict', binds)
1136 -- TOMDO: What do we have to do about ImplicInst, Method, and LitInst??
1137 normaliseOneInst _isWanted _fun inst
1138 = do { inst' <- zonkInst inst
1139 ; return (inst', emptyBag)
1144 %************************************************************************
1148 %************************************************************************
1150 The infamous couldn't match expected type soandso against inferred type
1151 somethingdifferent message.
1154 eqInstMisMatch :: Inst -> TcM a
1156 = ASSERT( isEqInst inst )
1157 do { (env, msg) <- misMatchMsg ty_act ty_exp
1159 failWithTcM (env, msg)
1162 ty_act = eqInstLeftTy inst
1163 ty_exp = eqInstRightTy inst
1164 InstLoc _ _ ctxt = instLoc inst
1166 -----------------------
1167 misMatchMsg :: TcType -> TcType -> TcM (TidyEnv, SDoc)
1168 -- Generate the message when two types fail to match,
1169 -- going to some trouble to make it helpful.
1170 -- The argument order is: actual type, expected type
1171 misMatchMsg ty_act ty_exp
1172 = do { env0 <- tcInitTidyEnv
1173 ; ty_exp <- zonkTcType ty_exp
1174 ; ty_act <- zonkTcType ty_act
1175 ; (env1, pp_exp, extra_exp) <- ppr_ty env0 ty_exp
1176 ; (env2, pp_act, extra_act) <- ppr_ty env1 ty_act
1178 sep [sep [ptext SLIT("Couldn't match expected type") <+> pp_exp,
1180 ptext SLIT("against inferred type") <+> pp_act],
1181 nest 2 (extra_exp $$ extra_act)]) }
1183 ppr_ty :: TidyEnv -> TcType -> TcM (TidyEnv, SDoc, SDoc)
1185 = do { let (env1, tidy_ty) = tidyOpenType env ty
1186 ; (env2, extra) <- ppr_extra env1 tidy_ty
1187 ; return (env2, quotes (ppr tidy_ty), extra) }
1189 -- (ppr_extra env ty) shows extra info about 'ty'
1190 ppr_extra :: TidyEnv -> Type -> TcM (TidyEnv, SDoc)
1191 ppr_extra env (TyVarTy tv)
1192 | isSkolemTyVar tv || isSigTyVar tv
1193 = return (env1, pprSkolTvBinding tv1)
1195 (env1, tv1) = tidySkolemTyVar env tv
1197 ppr_extra env _ty = return (env, empty) -- Normal case