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
108 The following functions takes an equality instance and turns it into an
109 elementary rewrite if possible.
112 data Rewrite = Rewrite TcType -- lhs of rewrite rule
113 TcType -- rhs of rewrite rule
114 TcType -- coercion witnessing the rewrite rule
116 eqInstToRewrite :: Inst -> Maybe Rewrite
118 = ASSERT( isEqInst inst )
119 go (eqInstLeftTy inst) (eqInstRightTy inst) (eqInstType inst)
121 -- look through synonyms
122 go ty1 ty2 co | Just ty1' <- tcView ty1 = go ty1' ty2 co
123 go ty1 ty2 co | Just ty2' <- tcView ty2 = go ty1 ty2' co
125 -- rewrite type family applications
126 go ty1@(TyConApp con _) ty2 co
128 = Just $ Rewrite ty1 ty2 co
131 go ty1@(TyVarTy tv) ty2 co
133 = Just $ Rewrite ty1 ty2 co
135 -- rewrite type family applications from right-to-left, only after
136 -- having checked whether we can work left-to-right
137 go ty1 ty2@(TyConApp con _) co
139 = Just $ Rewrite ty2 ty1 (mkSymCoercion co)
141 -- rewrite skolems from right-to-left, only after having checked
142 -- whether we can work left-to-right
143 go ty1 ty2@(TyVarTy tv) co
145 = Just $ Rewrite ty2 ty1 (mkSymCoercion co)
150 Normalise a type relative to an elementary rewrite implied by an EqInst or an
151 explicitly given elementary rewrite.
155 -- Precondition: the EqInst passes the occurs check
156 tcEqInstNormaliseFamInst :: Inst -> TcType -> TcM (CoercionI, TcType)
157 tcEqInstNormaliseFamInst inst ty
158 = case eqInstToRewrite inst of
159 Just rewrite -> tcEqRuleNormaliseFamInst rewrite ty
160 Nothing -> return (IdCo, ty)
162 -- Rewrite by equality rewrite rule
163 tcEqRuleNormaliseFamInst :: Rewrite -- elementary rewrite
164 -> TcType -- type to rewrite
165 -> TcM (CoercionI, -- witnessing coercion
166 TcType) -- rewritten type
167 tcEqRuleNormaliseFamInst (Rewrite pat rhs co) ty
168 = tcGenericNormaliseFamInst matchEqRule ty
170 matchEqRule sty | pat `tcEqType` sty = return $ Just (rhs, co)
171 | otherwise = return $ Nothing
174 Generic normalisation of 'Type's and 'PredType's; ie, walk the type term and
175 apply the normalisation function gives as the first argument to every TyConApp
176 and every TyVarTy subterm.
178 tcGenericNormaliseFamInst fun ty = (co, ty')
181 This function is (by way of using smart constructors) careful to ensure that
182 the returned coercion is exactly IdCo (and not some semantically equivalent,
183 but syntactically different coercion) whenever (ty' `tcEqType` ty). This
184 makes it easy for the caller to determine whether the type changed. BUT
185 even if we return IdCo, ty' may be *syntactically* different from ty due to
186 unfolded closed type synonyms (by way of tcCoreView). In the interest of
187 good error messages, callers should discard ty' in favour of ty in this case.
190 tcGenericNormaliseFamInst :: (TcType -> TcM (Maybe (TcType, Coercion)))
191 -- what to do with type functions and tyvars
192 -> TcType -- old type
193 -> TcM (CoercionI, TcType) -- (coercion, new type)
194 tcGenericNormaliseFamInst fun ty
195 | Just ty' <- tcView ty = tcGenericNormaliseFamInst fun ty'
196 tcGenericNormaliseFamInst fun (TyConApp tyCon tys)
197 = do { (cois, ntys) <- mapAndUnzipM (tcGenericNormaliseFamInst fun) tys
198 ; let tycon_coi = mkTyConAppCoI tyCon ntys cois
199 ; maybe_ty_co <- fun (mkTyConApp tyCon ntys) -- use normalised args!
200 ; case maybe_ty_co of
201 -- a matching family instance exists
203 do { let first_coi = mkTransCoI tycon_coi (ACo co)
204 ; (rest_coi, nty) <- tcGenericNormaliseFamInst fun ty'
205 ; let fix_coi = mkTransCoI first_coi rest_coi
206 ; return (fix_coi, nty)
208 -- no matching family instance exists
209 -- we do not do anything
210 Nothing -> return (tycon_coi, mkTyConApp tyCon ntys)
212 tcGenericNormaliseFamInst fun (AppTy ty1 ty2)
213 = do { (coi1,nty1) <- tcGenericNormaliseFamInst fun ty1
214 ; (coi2,nty2) <- tcGenericNormaliseFamInst fun ty2
215 ; return (mkAppTyCoI nty1 coi1 nty2 coi2, mkAppTy nty1 nty2)
217 tcGenericNormaliseFamInst fun (FunTy ty1 ty2)
218 = do { (coi1,nty1) <- tcGenericNormaliseFamInst fun ty1
219 ; (coi2,nty2) <- tcGenericNormaliseFamInst fun ty2
220 ; return (mkFunTyCoI nty1 coi1 nty2 coi2, mkFunTy nty1 nty2)
222 tcGenericNormaliseFamInst fun (ForAllTy tyvar ty1)
223 = do { (coi,nty1) <- tcGenericNormaliseFamInst fun ty1
224 ; return (mkForAllTyCoI tyvar coi, mkForAllTy tyvar nty1)
226 tcGenericNormaliseFamInst fun (NoteTy note ty1)
227 = do { (coi,nty1) <- tcGenericNormaliseFamInst fun ty1
228 ; return (mkNoteTyCoI note coi, NoteTy note nty1)
230 tcGenericNormaliseFamInst fun ty@(TyVarTy tv)
232 = do { traceTc (text "tcGenericNormaliseFamInst" <+> ppr ty)
233 ; res <- lookupTcTyVar tv
236 do { maybe_ty' <- fun ty
238 Nothing -> return (IdCo, ty)
240 do { (coi2, ty'') <- tcGenericNormaliseFamInst fun ty'
241 ; return (ACo co1 `mkTransCoI` coi2, ty'')
244 IndirectTv ty' -> tcGenericNormaliseFamInst fun ty'
248 tcGenericNormaliseFamInst fun (PredTy predty)
249 = do { (coi, pred') <- tcGenericNormaliseFamInstPred fun predty
250 ; return (coi, PredTy pred') }
252 ---------------------------------
253 tcGenericNormaliseFamInstPred :: (TcType -> TcM (Maybe (TcType,Coercion)))
255 -> TcM (CoercionI, TcPredType)
257 tcGenericNormaliseFamInstPred fun (ClassP cls tys)
258 = do { (cois, tys')<- mapAndUnzipM (tcGenericNormaliseFamInst fun) tys
259 ; return (mkClassPPredCoI cls tys' cois, ClassP cls tys')
261 tcGenericNormaliseFamInstPred fun (IParam ipn ty)
262 = do { (coi, ty') <- tcGenericNormaliseFamInst fun ty
263 ; return $ (mkIParamPredCoI ipn coi, IParam ipn ty')
265 tcGenericNormaliseFamInstPred fun (EqPred ty1 ty2)
266 = do { (coi1, ty1') <- tcGenericNormaliseFamInst fun ty1
267 ; (coi2, ty2') <- tcGenericNormaliseFamInst fun ty2
268 ; return (mkEqPredCoI ty1' coi1 ty2' coi2, EqPred ty1' ty2') }
272 %************************************************************************
274 \section{Normalisation of equality constraints}
276 %************************************************************************
278 Note [Inconsistencies in equality constraints]
279 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
280 We guarantee that we raise an error if we discover any inconsistencies (i.e.,
281 equalities that if presented to the unifer in TcUnify would result in an
282 error) during normalisation of wanted constraints. This is especially so that
283 we don't solve wanted constraints under an inconsistent given set. In
284 particular, we don't want to permit signatures, such as
286 bad :: (Int ~ Bool => Int) -> a -> a
289 normaliseGivenEqs :: [Inst] -> TcM ([Inst], TcM ())
290 normaliseGivenEqs givens
291 = do { traceTc (text "normaliseGivenEqs <-" <+> ppr givens)
292 ; (result, deSkolem) <-
293 rewriteToFixedPoint (Just ("(SkolemOccurs)", skolemOccurs))
294 [ ("(ZONK)", dontRerun $ zonkInsts)
295 , ("(TRIVIAL)", dontRerun $ trivialRule)
296 , ("(DECOMP)", decompRule)
298 , ("(SUBST)", substRule) -- incl. occurs check
300 ; traceTc (text "normaliseGivenEqs ->" <+> ppr result)
301 ; return (result, deSkolem)
306 normaliseWantedEqs :: [Inst] -> TcM [Inst]
307 normaliseWantedEqs insts
308 = do { traceTc (text "normaliseWantedEqs <-" <+> ppr insts)
309 ; result <- liftM fst $ rewriteToFixedPoint Nothing
310 [ ("(ZONK)", dontRerun $ zonkInsts)
311 , ("(TRIVIAL)", dontRerun $ trivialRule)
312 , ("(DECOMP)", decompRule)
314 , ("(UNIFY)", unifyMetaRule) -- incl. occurs check
315 , ("(SUBST)", substRule) -- incl. occurs check
317 ; traceTc (text "normaliseWantedEqs ->" <+> ppr result)
323 %************************************************************************
325 \section{Solving of wanted constraints with respect to a given set}
327 %************************************************************************
329 The set of given equalities must have been normalised already.
332 solveWantedEqs :: [Inst] -- givens
334 -> TcM [Inst] -- irreducible wanteds
335 solveWantedEqs givens wanteds
336 = do { traceTc $ text "solveWantedEqs <-" <+> ppr wanteds <+> text "with" <+>
338 ; result <- liftM fst $ rewriteToFixedPoint Nothing
339 [ ("(ZONK)", dontRerun $ zonkInsts)
340 , ("(TRIVIAL)", dontRerun $ trivialRule)
341 , ("(DECOMP)", decompRule)
343 , ("(GIVEN)", substGivens givens) -- incl. occurs check
344 , ("(UNIFY)", unifyMetaRule) -- incl. occurs check
346 ; traceTc (text "solveWantedEqs ->" <+> ppr result)
350 -- Use `substInst' with every given on all the wanteds.
351 substGivens :: [Inst] -> [Inst] -> TcM ([Inst], Bool)
352 substGivens [] wanteds = return (wanteds, False)
353 substGivens (g:gs) wanteds
354 = do { (wanteds1, changed1) <- substGivens gs wanteds
355 ; (wanteds2, changed2) <- substInst g wanteds1
356 ; return (wanteds2, changed1 || changed2)
361 %************************************************************************
363 \section{Normalisation of non-equality dictionaries}
365 %************************************************************************
368 normaliseGivenDicts, normaliseWantedDicts
369 :: [Inst] -- given equations
370 -> [Inst] -- dictionaries
371 -> TcM ([Inst],TcDictBinds)
373 normaliseGivenDicts eqs dicts = normalise_dicts eqs dicts False
374 normaliseWantedDicts eqs dicts = normalise_dicts eqs dicts True
377 :: [Inst] -- given equations
378 -> [Inst] -- dictionaries
379 -> Bool -- True <=> the dicts are wanted
380 -- Fals <=> they are given
381 -> TcM ([Inst],TcDictBinds)
382 normalise_dicts given_eqs dicts is_wanted
383 = do { traceTc $ text "normalise???Dicts <-" <+> ppr dicts <+>
384 text "with" <+> ppr given_eqs
385 ; (dicts0, binds0) <- normaliseInsts is_wanted dicts
386 ; (dicts1, binds1) <- substEqInDictInsts given_eqs dicts0
387 ; let binds01 = binds0 `unionBags` binds1
388 ; if isEmptyBag binds1
389 then return (dicts1, binds01)
390 else do { (dicts2, binds2) <- normaliseGivenDicts given_eqs dicts1
391 ; return (dicts2, binds01 `unionBags` binds2) } }
395 %************************************************************************
397 \section{Normalisation rules and iterative rule application}
399 %************************************************************************
401 We have three kinds of normalising rewrite rules:
403 (1) Normalisation rules that rewrite a set of insts and return a flag indicating
404 whether any changes occurred during rewriting that necessitate re-running
405 the current rule set.
407 (2) Precondition rules that rewrite a set of insts and return a monadic action
408 that reverts the effect of preconditioning.
410 (3) Idempotent normalisation rules that never require re-running the rule set.
413 type RewriteRule = [Inst] -> TcM ([Inst], Bool) -- rewrite, maybe re-run
414 type PrecondRule = [Inst] -> TcM ([Inst], TcM ()) -- rewrite, revertable
415 type IdemRewriteRule = [Inst] -> TcM [Inst] -- rewrite, don't re-run
417 type NamedRule = (String, RewriteRule) -- rule with description
418 type NamedPreRule = (String, PrecondRule) -- precond with desc
421 Template lifting idempotent rules to full rules (which can be put into a rule
425 dontRerun :: IdemRewriteRule -> RewriteRule
426 dontRerun rule insts = liftM addFalse $ rule insts
428 addFalse x = (x, False)
431 The following function applies a set of rewrite rules until a fixed point is
432 reached; i.e., none of the `RewriteRule's require re-running the rule set.
433 Optionally, there may be a pre-conditing rule that is applied before any other
434 rules are applied and before the rule set is re-run.
436 The result is the set of rewritten (i.e., normalised) insts and, in case of a
437 pre-conditing rule, a monadic action that reverts the effects of
438 pre-conditioning - specifically, this is removing introduced skolems.
441 rewriteToFixedPoint :: Maybe NamedPreRule -- optional preconditioning rule
442 -> [NamedRule] -- rule set
443 -> [Inst] -- insts to rewrite
444 -> TcM ([Inst], TcM ())
445 rewriteToFixedPoint precondRule rules insts
446 = completeRewrite (return ()) precondRule insts
448 completeRewrite :: TcM () -> Maybe NamedPreRule -> [Inst]
449 -> TcM ([Inst], TcM ())
450 completeRewrite dePrecond (Just (precondName, precond)) insts
451 = do { traceTc $ text precondName <+> text " <- " <+> ppr insts
452 ; (insts', dePrecond') <- precond insts
453 ; traceTc $ text precondName <+> text " -> " <+> ppr insts'
454 ; tryRules (dePrecond >> dePrecond') rules insts'
456 completeRewrite dePrecond Nothing insts
457 = tryRules dePrecond rules insts
459 tryRules dePrecond _ [] = return ([] , dePrecond)
460 tryRules dePrecond [] insts = return (insts, dePrecond)
461 tryRules dePrecond ((name, rule):rules) insts
462 = do { traceTc $ text name <+> text " <- " <+> ppr insts
463 ; (insts', rerun) <- rule insts
464 ; traceTc $ text name <+> text " -> " <+> ppr insts'
465 ; if rerun then completeRewrite dePrecond precondRule insts'
466 else tryRules dePrecond rules insts'
471 %************************************************************************
473 \section{Different forms of Inst rewrite rules}
475 %************************************************************************
477 Splitting of non-terminating given constraints: skolemOccurs
478 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
479 This is a preconditioning rule exclusively applied to given constraints.
480 Moreover, its rewriting is only temporary, as it is undone by way of
481 side-effecting mutable type variables after simplification and constraint
482 entailment has been completed.
484 This version is an (attempt at, yet unproven, an) *unflattened* version of
485 the SubstL-Ev completion rule.
487 The above rule is essential to catch non-terminating rules that cannot be
488 oriented properly, like
494 The left-to-right orientiation is not suitable because it does not
495 terminate. The right-to-left orientation is not suitable because it
496 does not have a type-function on the left. This is undesirable because
497 it would hide information. E.g. assume
501 then rewriting C [G (F a)] to C (F a) is bad because we cannot now
502 see that the C [x] instance applies.
504 The rule also caters for badly-oriented rules of the form:
508 for which other solutions are possible, but this one will do too.
512 co : ty1 ~ ty2{F ty1}
515 sym (F co) : F ty2{b} ~ b
516 where b is a fresh skolem variable
518 We also cater for the symmetric situation *if* the rule cannot be used as a
519 left-to-right rewrite rule.
521 We also return an action (b := ty1) which is used to eliminate b
522 after the dust of normalisation with the completed rewrite system
525 A subtle point of this transformation is that both coercions in the results
526 are strictly speaking incorrect. However, they are correct again after the
527 action {B := ty1} has removed the skolem again. This happens immediately
528 after constraint entailment has been checked; ie, code outside of the
529 simplification and entailment checking framework will never see these
530 temporarily incorrect coercions.
532 NB: We perform this transformation for multiple occurences of ty1 under one
533 or multiple family applications on the left-hand side at once (ie, the
534 rule doesn't need to be applied multiple times at a single inst). As a
535 result we can get two or more insts back.
538 skolemOccurs :: PrecondRule
540 = do { (instss, undoSkolems) <- mapAndUnzipM oneSkolemOccurs insts
541 ; return (concat instss, sequence_ undoSkolems)
545 = ASSERT( isEqInst inst )
546 isRewriteRule (eqInstLeftTy inst) (eqInstRightTy inst)
549 -- look through synonyms
550 isRewriteRule ty1 ty2 | Just ty1' <- tcView ty1 = isRewriteRule ty1' ty2
551 isRewriteRule ty1 ty2 | Just ty2' <- tcView ty2 = isRewriteRule ty1 ty2'
553 -- left-to-right rule with type family head
554 isRewriteRule ty1@(TyConApp con _) ty2
556 = breakRecursion ty1 ty2 False -- not swapped
558 -- left-to-right rule with type variable head
559 isRewriteRule ty1@(TyVarTy _) ty2
560 = breakRecursion ty1 ty2 False -- not swapped
562 -- right-to-left rule with type family head
563 isRewriteRule ty1 ty2@(TyConApp con _)
565 = breakRecursion ty2 ty1 True -- swapped
567 -- right-to-left rule with type variable head
568 isRewriteRule ty1 ty2@(TyVarTy _)
569 = breakRecursion ty2 ty1 True -- swapped
571 -- this equality is not a rewrite rule => ignore
572 isRewriteRule _ _ = return ([inst], return ())
575 breakRecursion pat body swapped
577 = return ([inst], return ())
579 = do { traceTc $ text "oneSkolemOccurs[TLO]:" <+> ppr tysToLiftOut
580 ; skTvs <- mapM (newMetaTyVar TauTv . typeKind) tysToLiftOut
581 ; let skTvs_tysTLO = zip skTvs tysToLiftOut
582 insertSkolems = return . replace skTvs_tysTLO
583 ; (_, body') <- tcGenericNormaliseFamInst insertSkolems body
584 ; inst' <- if swapped then mkEqInst (EqPred body' pat) co
585 else mkEqInst (EqPred pat body') co
586 -- ensure to reconstruct the inst in the
587 -- original orientation
588 ; traceTc $ text "oneSkolemOccurs[inst']:" <+> ppr inst'
589 ; (insts, undoSk) <- mapAndUnzipM (mkSkolemInst inst')
591 ; return (inst':insts, sequence_ undoSk)
594 co = eqInstCoercion inst
596 -- all subtypes that are (1) type family instances and (2) contain
597 -- the lhs type as part of the type arguments of the type family
599 tysToLiftOut = [mkTyConApp tc tys | (tc, tys) <- tyFamInsts body
600 , any (pat `tcPartOfType`) tys]
602 replace :: [(TcTyVar, Type)] -> Type -> Maybe (Type, Coercion)
603 replace [] _ = Nothing
604 replace ((skTv, tyTLO):rest) ty
605 | tyTLO `tcEqType` ty = Just (mkTyVarTy skTv, undefined)
606 | otherwise = replace rest ty
608 -- create the EqInst for the equality determining the skolem and a
609 -- TcM action undoing the skolem introduction
610 mkSkolemInst inst' (skTv, tyTLO)
611 = do { (co, tyLiftedOut) <- tcEqInstNormaliseFamInst inst' tyTLO
612 ; inst <- mkEqInst (EqPred tyLiftedOut (mkTyVarTy skTv))
613 (mkGivenCo $ mkSymCoercion (fromACo co))
614 -- co /= IdCo due to construction of inst'
615 ; return (inst, writeMetaTyVar skTv tyTLO)
620 Removal of trivial equalities: trivialRule
621 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
622 The following rules exploits the reflexivity of equality:
630 trivialRule :: IdemRewriteRule
632 = liftM catMaybes $ mappM trivial insts
635 | ASSERT( isEqInst inst )
637 = do { eitherEqInst inst
638 (\cotv -> writeMetaTyVar cotv ty1)
645 ty1 = eqInstLeftTy inst
646 ty2 = eqInstRightTy inst
650 Decomposition of data type constructors: decompRule
651 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
652 Whenever, the same *data* constructors occurs on both sides of an equality, we
653 can decompose as in standard unification.
658 g21 : c1 ~ d1, ..., g2n : cn ~ dn
661 Works also for the case where T is actually an application of a type family
662 constructor to a set of types, provided the applications on both sides of the
663 ~ are identical; see also Note [OpenSynTyCon app] in TcUnify.
665 We guarantee to raise an error for any inconsistent equalities;
666 cf Note [Inconsistencies in equality constraints].
669 decompRule :: RewriteRule
671 = do { (insts, changed) <- mapAndUnzipM decomp insts
672 ; return (concat insts, or changed)
676 = ASSERT( isEqInst inst )
677 go (eqInstLeftTy inst) (eqInstRightTy inst)
680 | Just ty1' <- tcView ty1 = go ty1' ty2
681 | Just ty2' <- tcView ty2 = go ty1 ty2'
683 go (TyConApp con1 tys1) (TyConApp con2 tys2)
684 | con1 == con2 && identicalHead
685 = mkArgInsts (mkTyConApp con1) tys1 tys2
687 | con1 /= con2 && not (isOpenSynTyCon con1 || isOpenSynTyCon con2)
688 -- not matching data constructors (of any flavour) are bad news
689 = eqInstMisMatch inst
692 (idxTys1, _) = splitAt n tys1
693 (idxTys2, _) = splitAt n tys2
694 identicalHead = not (isOpenSynTyCon con1) ||
695 idxTys1 `tcEqTypes` idxTys2
697 go (FunTy fun1 arg1) (FunTy fun2 arg2)
698 = mkArgInsts (\[funCo, argCo] -> mkFunTy funCo argCo) [fun1, arg1]
701 -- Applications need a bit of care!
702 -- They can match FunTy and TyConApp, so use splitAppTy_maybe
704 | Just (s2, t2) <- tcSplitAppTy_maybe ty2
705 = mkArgInsts (\[s, t] -> mkAppTy s t) [s1, t1] [s2, t2]
709 | Just (s1, t1) <- tcSplitAppTy_maybe ty1
710 = mkArgInsts (\[s, t] -> mkAppTy s t) [s1, t1] [s2, t2]
712 -- We already covered all the consistent cases of rigid types on both
713 -- sides; so, if we see two rigid types here, we discovered an
716 | isRigid ty1 && isRigid ty2
717 = eqInstMisMatch inst
719 -- We can neither assert consistency nor inconsistency => defer
720 go _ _ = return ([inst], False)
722 isRigid (TyConApp con _) = not (isOpenSynTyCon con)
723 isRigid (FunTy _ _) = True
724 isRigid (AppTy _ _) = True
727 -- Create insts for matching argument positions (ie, the bit after
728 -- '>-->' in the rule description above)
729 mkArgInsts con tys1 tys2
730 = do { cos <- eitherEqInst inst
731 -- old_co := Con1 cos
733 do { cotvs <- zipWithM newMetaCoVar tys1 tys2
734 ; let cos = map mkTyVarTy cotvs
735 ; writeMetaTyVar old_covar (con cos)
736 ; return $ map mkWantedCo cotvs
738 -- co_i := Con_i old_co
740 return $ map mkGivenCo $
741 mkRightCoercions (length tys1) old_co)
742 ; insts <- zipWithM mkEqInst (zipWith EqPred tys1 tys2) cos
743 ; traceTc (text "decomp identicalHead" <+> ppr insts)
744 ; return (insts, not $ null insts)
749 Rewriting with type instances: topRule
750 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
751 We use (toplevel) type instances to normalise both sides of equalities.
755 >--> co1 :: t ~ t' / co2 :: s ~ s'
757 g1 := co1 * g2 * sym co2
760 topRule :: RewriteRule
762 = do { (insts, changed) <- mapAndUnzipM top insts
763 ; return (insts, or changed)
767 = ASSERT( isEqInst inst )
768 do { (coi1, ty1') <- tcNormaliseFamInst ty1
769 ; (coi2, ty2') <- tcNormaliseFamInst ty2
770 ; case (coi1, coi2) of
771 (IdCo, IdCo) -> return (inst, False)
775 -- old_co = co1 * new_co * sym co2
777 do { new_cotv <- newMetaCoVar ty1' ty2'
778 ; let new_co = mkTyVarTy new_cotv
779 old_coi = coi1 `mkTransCoI`
780 ACo new_co `mkTransCoI`
782 ; writeMetaTyVar old_covar (fromACo old_coi)
783 ; return $ mkWantedCo new_cotv
785 -- new_co = sym co1 * old_co * co2
790 mkSymCoI coi1 `mkTransCoI`
791 ACo old_co `mkTransCoI` coi2)
792 ; new_inst <- mkEqInst (EqPred ty1' ty2') wg_co
793 ; return (new_inst, True)
797 ty1 = eqInstLeftTy inst
798 ty2 = eqInstRightTy inst
802 Rewriting with equalities: substRule
803 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
804 From a set of insts, use all insts that can be read as rewrite rules to
805 rewrite the types in all other insts.
809 forall g1 : s1{F c} ~ s2{F c}
812 g1 := s1{g} * g2 * sym s2{g} <=> g2 := sym s1{g} * g1 * s2{g}
814 Alternatively, the rewrite rule may have the form (g : a ~ t).
816 To avoid having to swap rules of the form (g : t ~ F c) and (g : t ~ a),
817 where t is neither a variable nor a type family application, we use them for
818 rewriting from right-to-left. However, it is crucial to only apply rules
819 from right-to-left if they cannot be used left-to-right.
821 The workhorse is substInst, which performs an occurs check before actually
822 using an equality for rewriting. If the type pattern occurs in the type we
823 substitute for the pattern, normalisation would diverge.
826 substRule :: RewriteRule
827 substRule insts = tryAllInsts insts []
829 -- for every inst check whether it can be used to rewrite the others
830 -- (we make an effort to keep the insts in order; it makes debugging
832 tryAllInsts [] triedInsts = return (reverse triedInsts, False)
833 tryAllInsts (inst:insts) triedInsts
834 = do { (insts', changed) <- substInst inst (reverse triedInsts ++ insts)
835 ; if changed then return (insertAt (length triedInsts) inst insts',
837 else tryAllInsts insts (inst:triedInsts)
840 insertAt n x xs = let (xs1, xs2) = splitAt n xs
843 -- Use the given inst as a rewrite rule to normalise the insts in the second
844 -- argument. Don't do anything if the inst cannot be used as a rewrite rule,
845 -- but do apply it right-to-left, if possible, and if it cannot be used
848 substInst :: Inst -> [Inst] -> TcM ([Inst], Bool)
850 = case eqInstToRewrite inst of
851 Just rewrite -> substEquality rewrite insts
852 Nothing -> return (insts, False)
854 substEquality :: Rewrite -- elementary rewrite
855 -> [Inst] -- insts to rewrite
856 -> TcM ([Inst], Bool)
857 substEquality eqRule@(Rewrite pat rhs _) insts
858 | pat `tcPartOfType` rhs -- occurs check!
859 = occurCheckErr pat rhs
861 = do { (insts', changed) <- mapAndUnzipM substOne insts
862 ; return (insts', or changed)
866 = ASSERT( isEqInst inst )
867 do { (coi1, ty1') <- tcEqRuleNormaliseFamInst eqRule ty1
868 ; (coi2, ty2') <- tcEqRuleNormaliseFamInst eqRule ty2
869 ; case (coi1, coi2) of
870 (IdCo, IdCo) -> return (inst, False)
874 -- old_co := co1 * new_co * sym co2
876 do { new_cotv <- newMetaCoVar ty1' ty2'
877 ; let new_co = mkTyVarTy new_cotv
878 old_coi = coi1 `mkTransCoI`
879 ACo new_co `mkTransCoI`
881 ; writeMetaTyVar old_covar (fromACo old_coi)
882 ; return $ mkWantedCo new_cotv
884 -- new_co := sym co1 * old_co * co2
889 mkSymCoI coi1 `mkTransCoI`
890 ACo old_co `mkTransCoI` coi2)
891 ; new_inst <- mkEqInst (EqPred ty1' ty2') gw_co
892 ; return (new_inst, True)
896 ty1 = eqInstLeftTy inst
897 ty2 = eqInstRightTy inst
901 Instantiate meta variables: unifyMetaRule
902 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
903 If an equality equates a meta type variable with a type, we simply instantiate
912 Meta variables can only appear in wanted constraints, and this rule should
913 only be applied to wanted constraints. We also know that t definitely is
914 distinct from alpha (as the trivialRule) has been run on the insts beforehand.
916 NB: We cannot assume that meta tyvars are empty. They may have been updated
917 by another inst in the currently processed wanted list. We need to be very
918 careful when updateing type variables (see TcUnify.uUnfilledVar), but at least
919 we know that we have no boxes. It's unclear that it would be an advantage to
920 common up the code in TcUnify and the code below. Firstly, we don't want
921 calls to TcUnify.defer_unification here, and secondly, TcUnify import the
922 current module, so we would have to move everything here (Yuk!) or to
923 TcMType. Besides, the code here is much simpler due to the lack of boxes.
926 unifyMetaRule :: RewriteRule
928 = do { (insts', changed) <- mapAndUnzipM unifyMeta insts
929 ; return (concat insts', or changed)
933 = ASSERT( isEqInst inst )
934 go (eqInstLeftTy inst) (eqInstRightTy inst)
935 (fromWantedCo "unifyMetaRule" $ eqInstCoercion inst)
938 | Just ty1' <- tcView ty1 = go ty1' ty2 cotv
939 | Just ty2' <- tcView ty2 = go ty1 ty2' cotv
942 , isMetaTyVar tv1 = do { lookupTV <- lookupTcTyVar tv1
943 ; uMeta False tv1 lookupTV ty2 cotv
946 , isMetaTyVar tv2 = do { lookupTV <- lookupTcTyVar tv2
947 ; uMeta True tv2 lookupTV ty1 cotv
949 | otherwise = return ([inst], False)
951 -- meta variable has been filled already
952 -- => ignore this inst (we'll come around again, after zonking)
953 uMeta _swapped _tv (IndirectTv _) _ty _cotv
954 = return ([inst], False)
956 -- signature skolem meets non-variable type
958 uMeta _swapped _tv (DoneTv (MetaTv (SigTv _) _)) ty _cotv
960 = return ([inst], False)
962 -- type variable meets type variable
963 -- => check that tv2 hasn't been updated yet and choose which to update
964 uMeta swapped tv1 (DoneTv details1) (TyVarTy tv2) cotv
965 = do { lookupTV2 <- lookupTcTyVar tv2
967 IndirectTv ty -> uMeta swapped tv1 (DoneTv details1) ty cotv
969 uMetaVar swapped tv1 details1 tv2 details2 cotv
972 -- updatable meta variable meets non-variable type
973 -- => occurs check, monotype check, and kinds match check, then update
974 uMeta swapped tv (DoneTv (MetaTv _ ref)) ty cotv
975 = do { mb_ty' <- checkTauTvUpdate tv ty -- occurs + monotype check
977 Nothing -> return ([inst], False) -- tv occurs in faminst
979 do { checkUpdateMeta swapped tv ref ty' -- update meta var
980 ; writeMetaTyVar cotv ty' -- update co var
985 uMeta _ _ _ _ _ = panic "uMeta"
987 -- meta variable meets skolem
989 uMetaVar swapped tv1 (MetaTv _ ref) tv2 (SkolemTv _) cotv
990 = do { checkUpdateMeta swapped tv1 ref (mkTyVarTy tv2)
991 ; writeMetaTyVar cotv (mkTyVarTy tv2)
995 -- meta variable meets meta variable
996 -- => be clever about which of the two to update
997 -- (from TcUnify.uUnfilledVars minus boxy stuff)
998 uMetaVar swapped tv1 (MetaTv info1 ref1) tv2 (MetaTv info2 ref2) cotv
999 = do { case (info1, info2) of
1000 -- Avoid SigTvs if poss
1001 (SigTv _, _ ) | k1_sub_k2 -> update_tv2
1002 (_, SigTv _) | k2_sub_k1 -> update_tv1
1004 (_, _) | k1_sub_k2 -> if k2_sub_k1 && nicer_to_update_tv1
1005 then update_tv1 -- Same kinds
1007 | k2_sub_k1 -> update_tv1
1008 | otherwise -> kind_err
1009 -- Update the variable with least kind info
1010 -- See notes on type inference in Kind.lhs
1011 -- The "nicer to" part only applies if the two kinds are the same,
1012 -- so we can choose which to do.
1014 ; writeMetaTyVar cotv (mkTyVarTy tv2)
1018 -- Kinds should be guaranteed ok at this point
1019 update_tv1 = updateMeta tv1 ref1 (mkTyVarTy tv2)
1020 update_tv2 = updateMeta tv2 ref2 (mkTyVarTy tv1)
1022 kind_err = addErrCtxtM (unifyKindCtxt swapped tv1 (mkTyVarTy tv2)) $
1023 unifyKindMisMatch k1 k2
1027 k1_sub_k2 = k1 `isSubKind` k2
1028 k2_sub_k1 = k2 `isSubKind` k1
1030 nicer_to_update_tv1 = isSystemName (Var.varName tv1)
1031 -- Try to update sys-y type variables in preference to ones
1032 -- gotten (say) by instantiating a polymorphic function with
1033 -- a user-written type sig
1035 uMetaVar _ _ _ _ _ _ = panic "uMetaVar"
1039 %************************************************************************
1041 \section{Normalisation of Insts}
1043 %************************************************************************
1045 Normalises a set of dictionaries relative to a set of given equalities (which
1046 are interpreted as rewrite rules). We only consider given equalities of the
1051 where F is a type family.
1054 substEqInDictInsts :: [Inst] -- given equalities (used as rewrite rules)
1055 -> [Inst] -- dictinaries to be normalised
1056 -> TcM ([Inst], TcDictBinds)
1057 substEqInDictInsts eqInsts dictInsts
1058 = do { traceTc (text "substEqInDictInst <-" <+> ppr dictInsts)
1060 foldlM rewriteWithOneEquality (dictInsts, emptyBag) eqInsts
1061 ; traceTc (text "substEqInDictInst ->" <+> ppr dictInsts')
1065 -- (1) Given equality of form 'F ts ~ t' or 'a ~ t': use for rewriting
1066 rewriteWithOneEquality (dictInsts, dictBinds)
1067 eqInst@(EqInst {tci_left = pattern,
1068 tci_right = target})
1069 | isOpenSynTyConApp pattern || isTyVarTy pattern
1070 = do { (dictInsts', moreDictBinds) <-
1071 genericNormaliseInsts True {- wanted -} applyThisEq dictInsts
1072 ; return (dictInsts', dictBinds `unionBags` moreDictBinds)
1075 applyThisEq = tcGenericNormaliseFamInstPred (return . matchResult)
1077 -- rewrite in case of an exact match
1078 matchResult ty | tcEqType pattern ty = Just (target, eqInstType eqInst)
1079 | otherwise = Nothing
1081 -- (2) Given equality has the wrong form: ignore
1082 rewriteWithOneEquality (dictInsts, dictBinds) _not_a_rewrite_rule
1083 = return (dictInsts, dictBinds)
1087 Take a bunch of Insts (not EqInsts), and normalise them wrt the top-level
1088 type-function equations, where
1090 (norm_insts, binds) = normaliseInsts is_wanted insts
1093 = True, (binds + norm_insts) defines insts (wanteds)
1094 = False, (binds + insts) defines norm_insts (givens)
1096 Ie, in the case of normalising wanted dictionaries, we use the normalised
1097 dictionaries to define the originally wanted ones. However, in the case of
1098 given dictionaries, we use the originally given ones to define the normalised
1102 normaliseInsts :: Bool -- True <=> wanted insts
1103 -> [Inst] -- wanted or given insts
1104 -> TcM ([Inst], TcDictBinds) -- normalised insts and bindings
1105 normaliseInsts isWanted insts
1106 = genericNormaliseInsts isWanted tcNormaliseFamInstPred insts
1108 genericNormaliseInsts :: Bool -- True <=> wanted insts
1109 -> (TcPredType -> TcM (CoercionI, TcPredType))
1111 -> [Inst] -- wanted or given insts
1112 -> TcM ([Inst], TcDictBinds) -- normalised insts & binds
1113 genericNormaliseInsts isWanted fun insts
1114 = do { (insts', binds) <- mapAndUnzipM (normaliseOneInst isWanted fun) insts
1115 ; return (insts', unionManyBags binds)
1118 normaliseOneInst isWanted fun
1119 dict@(Dict {tci_pred = pred,
1121 = do { traceTc $ text "genericNormaliseInst <-" <+> ppr dict
1122 ; (coi, pred') <- fun pred
1126 do { traceTc $ text "genericNormaliseInst ->" <+> ppr dict
1127 ; return (dict, emptyBag)
1129 -- don't use pred' in this case; otherwise, we get
1130 -- more unfolded closed type synonyms in error messages
1132 do { -- an inst for the new pred
1133 ; dict' <- newDictBndr loc pred'
1134 -- relate the old inst to the new one
1135 -- target_dict = source_dict `cast` st_co
1136 ; let (target_dict, source_dict, st_co)
1137 | isWanted = (dict, dict', mkSymCoercion co)
1138 | otherwise = (dict', dict, co)
1140 -- co :: dict ~ dict'
1141 -- hence, if isWanted
1142 -- dict = dict' `cast` sym co
1144 -- dict' = dict `cast` co
1145 expr = HsVar $ instToId source_dict
1146 cast_expr = HsWrap (WpCo st_co) expr
1147 rhs = L (instLocSpan loc) cast_expr
1148 binds = instToDictBind target_dict rhs
1149 -- return the new inst
1150 ; traceTc $ text "genericNormaliseInst ->" <+> ppr dict'
1151 ; return (dict', binds)
1155 -- TOMDO: What do we have to do about ImplicInst, Method, and LitInst??
1156 normaliseOneInst _isWanted _fun inst
1157 = do { inst' <- zonkInst inst
1158 ; return (inst', emptyBag)
1163 %************************************************************************
1167 %************************************************************************
1169 The infamous couldn't match expected type soandso against inferred type
1170 somethingdifferent message.
1173 eqInstMisMatch :: Inst -> TcM a
1175 = ASSERT( isEqInst inst )
1176 do { (env, msg) <- misMatchMsg ty_act ty_exp
1178 failWithTcM (env, msg)
1181 ty_act = eqInstLeftTy inst
1182 ty_exp = eqInstRightTy inst
1183 InstLoc _ _ ctxt = instLoc inst
1185 -----------------------
1186 misMatchMsg :: TcType -> TcType -> TcM (TidyEnv, SDoc)
1187 -- Generate the message when two types fail to match,
1188 -- going to some trouble to make it helpful.
1189 -- The argument order is: actual type, expected type
1190 misMatchMsg ty_act ty_exp
1191 = do { env0 <- tcInitTidyEnv
1192 ; ty_exp <- zonkTcType ty_exp
1193 ; ty_act <- zonkTcType ty_act
1194 ; (env1, pp_exp, extra_exp) <- ppr_ty env0 ty_exp
1195 ; (env2, pp_act, extra_act) <- ppr_ty env1 ty_act
1197 sep [sep [ptext SLIT("Couldn't match expected type") <+> pp_exp,
1199 ptext SLIT("against inferred type") <+> pp_act],
1200 nest 2 (extra_exp $$ extra_act)]) }
1202 ppr_ty :: TidyEnv -> TcType -> TcM (TidyEnv, SDoc, SDoc)
1204 = do { let (env1, tidy_ty) = tidyOpenType env ty
1205 ; (env2, extra) <- ppr_extra env1 tidy_ty
1206 ; return (env2, quotes (ppr tidy_ty), extra) }
1208 -- (ppr_extra env ty) shows extra info about 'ty'
1209 ppr_extra :: TidyEnv -> Type -> TcM (TidyEnv, SDoc)
1210 ppr_extra env (TyVarTy tv)
1211 | isSkolemTyVar tv || isSigTyVar tv
1212 = return (env1, pprSkolTvBinding tv1)
1214 (env1, tv1) = tidySkolemTyVar env tv
1216 ppr_extra env _ty = return (env, empty) -- Normal case