1 Normalisation of type terms relative to type instances as well as
2 normalisation and entailment checking of equality constraints.
8 normaliseGivenEqs, normaliseGivenDicts,
9 normaliseWantedEqs, normaliseWantedDicts,
12 misMatchMsg, failWithMisMatch
16 #include "HsVersions.h"
28 import TypeRep ( Type(..) )
36 import SrcLoc ( Located(..) )
46 %************************************************************************
48 Normalisation of types
50 %************************************************************************
52 Unfold a single synonym family instance and yield the witnessing coercion.
53 Return 'Nothing' if the given type is either not synonym family instance
54 or is a synonym family instance that has no matching instance declaration.
55 (Applies only if the type family application is outermost.)
57 For example, if we have
59 :Co:R42T a :: T [a] ~ :R42T a
61 then 'T [Int]' unfolds to (:R42T Int, :Co:R42T Int).
64 tcUnfoldSynFamInst :: Type -> TcM (Maybe (Type, Coercion))
65 tcUnfoldSynFamInst (TyConApp tycon tys)
66 | not (isOpenSynTyCon tycon) -- unfold *only* _synonym_ family instances
69 = do { -- we only use the indexing arguments for matching,
70 -- not the additional ones
71 ; maybeFamInst <- tcLookupFamInst tycon idxTys
72 ; case maybeFamInst of
73 Nothing -> return Nothing
74 Just (rep_tc, rep_tys) -> return $ Just (mkTyConApp rep_tc tys',
75 mkTyConApp coe_tc tys')
77 tys' = rep_tys ++ restTys
78 coe_tc = expectJust "TcTyFun.tcUnfoldSynFamInst"
79 (tyConFamilyCoercion_maybe rep_tc)
83 (idxTys, restTys) = splitAt n tys
84 tcUnfoldSynFamInst _other = return Nothing
87 Normalise 'Type's and 'PredType's by unfolding type family applications where
88 possible (ie, we treat family instances as a TRS). Also zonk meta variables.
90 tcNormaliseFamInst ty = (co, ty')
94 tcNormaliseFamInst :: TcType -> TcM (CoercionI, TcType)
95 tcNormaliseFamInst = tcGenericNormaliseFamInst tcUnfoldSynFamInst
97 tcNormaliseFamInstPred :: TcPredType -> TcM (CoercionI, TcPredType)
98 tcNormaliseFamInstPred = tcGenericNormaliseFamInstPred tcUnfoldSynFamInst
101 An elementary rewrite is a properly oriented equality with associated coercion
102 that has one of the following two forms:
104 (1) co :: F t1..tn ~ t
105 (2) co :: a ~ t , where t /= F t1..tn and a is a skolem tyvar
107 NB: We do *not* use equalities of the form a ~ t where a is a meta tyvar as a
108 reqrite rule. Instead, such equalities are solved by unification. This is
109 essential; cf Note [skolemOccurs loop].
111 The following functions takes an equality instance and turns it into an
112 elementary rewrite if possible.
115 data Rewrite = Rewrite TcType -- lhs of rewrite rule
116 TcType -- rhs of rewrite rule
117 TcType -- coercion witnessing the rewrite rule
119 eqInstToRewrite :: Inst -> Maybe (Rewrite, Bool)
120 -- True iff rewrite swapped equality
122 = ASSERT( isEqInst inst )
123 go ty1 ty2 (eqInstType inst)
125 (ty1,ty2) = eqInstTys inst
127 -- look through synonyms
128 go ty1 ty2 co | Just ty1' <- tcView ty1 = go ty1' ty2 co
129 go ty1 ty2 co | Just ty2' <- tcView ty2 = go ty1 ty2' co
131 -- left-to-right rule with type family head
132 go ty1@(TyConApp con _) ty2 co
134 = Just (Rewrite ty1 ty2 co, False) -- not swapped
136 -- left-to-right rule with type variable head
137 go ty1@(TyVarTy tv) ty2 co
139 = Just (Rewrite ty1 ty2 co, False) -- not swapped
141 -- right-to-left rule with type family head, only after
142 -- having checked whether we can work left-to-right
143 go ty1 ty2@(TyConApp con _) co
145 = Just (Rewrite ty2 ty1 (mkSymCoercion co), True) -- swapped
147 -- right-to-left rule with type variable head, only after
148 -- having checked whether we can work left-to-right
149 go ty1 ty2@(TyVarTy tv) co
151 = Just (Rewrite ty2 ty1 (mkSymCoercion co), True) -- swapped
153 -- this equality is not a rewrite rule => ignore
157 Normalise a type relative to an elementary rewrite implied by an EqInst or an
158 explicitly given elementary rewrite.
162 -- Precondition: the EqInst passes the occurs check
163 tcEqInstNormaliseFamInst :: Inst -> TcType -> TcM (CoercionI, TcType)
164 tcEqInstNormaliseFamInst inst ty
165 = case eqInstToRewrite inst of
166 Just (rewrite, _) -> tcEqRuleNormaliseFamInst rewrite ty
167 Nothing -> return (IdCo, ty)
169 -- Rewrite by equality rewrite rule
170 tcEqRuleNormaliseFamInst :: Rewrite -- elementary rewrite
171 -> TcType -- type to rewrite
172 -> TcM (CoercionI, -- witnessing coercion
173 TcType) -- rewritten type
174 tcEqRuleNormaliseFamInst (Rewrite pat rhs co) ty
175 = tcGenericNormaliseFamInst matchEqRule ty
177 matchEqRule sty | pat `tcEqType` sty = return $ Just (rhs, co)
178 | otherwise = return $ Nothing
181 Generic normalisation of 'Type's and 'PredType's; ie, walk the type term and
182 apply the normalisation function gives as the first argument to every TyConApp
183 and every TyVarTy subterm.
185 tcGenericNormaliseFamInst fun ty = (co, ty')
188 This function is (by way of using smart constructors) careful to ensure that
189 the returned coercion is exactly IdCo (and not some semantically equivalent,
190 but syntactically different coercion) whenever (ty' `tcEqType` ty). This
191 makes it easy for the caller to determine whether the type changed. BUT
192 even if we return IdCo, ty' may be *syntactically* different from ty due to
193 unfolded closed type synonyms (by way of tcCoreView). In the interest of
194 good error messages, callers should discard ty' in favour of ty in this case.
197 tcGenericNormaliseFamInst :: (TcType -> TcM (Maybe (TcType, Coercion)))
198 -- what to do with type functions and tyvars
199 -> TcType -- old type
200 -> TcM (CoercionI, TcType) -- (coercion, new type)
201 tcGenericNormaliseFamInst fun ty
202 | Just ty' <- tcView ty = tcGenericNormaliseFamInst fun ty'
203 tcGenericNormaliseFamInst fun (TyConApp tyCon tys)
204 = do { (cois, ntys) <- mapAndUnzipM (tcGenericNormaliseFamInst fun) tys
205 ; let tycon_coi = mkTyConAppCoI tyCon ntys cois
206 ; maybe_ty_co <- fun (mkTyConApp tyCon ntys) -- use normalised args!
207 ; case maybe_ty_co of
208 -- a matching family instance exists
210 do { let first_coi = mkTransCoI tycon_coi (ACo co)
211 ; (rest_coi, nty) <- tcGenericNormaliseFamInst fun ty'
212 ; let fix_coi = mkTransCoI first_coi rest_coi
213 ; return (fix_coi, nty)
215 -- no matching family instance exists
216 -- we do not do anything
217 Nothing -> return (tycon_coi, mkTyConApp tyCon ntys)
219 tcGenericNormaliseFamInst fun (AppTy ty1 ty2)
220 = do { (coi1,nty1) <- tcGenericNormaliseFamInst fun ty1
221 ; (coi2,nty2) <- tcGenericNormaliseFamInst fun ty2
222 ; return (mkAppTyCoI nty1 coi1 nty2 coi2, mkAppTy nty1 nty2)
224 tcGenericNormaliseFamInst fun (FunTy ty1 ty2)
225 = do { (coi1,nty1) <- tcGenericNormaliseFamInst fun ty1
226 ; (coi2,nty2) <- tcGenericNormaliseFamInst fun ty2
227 ; return (mkFunTyCoI nty1 coi1 nty2 coi2, mkFunTy nty1 nty2)
229 tcGenericNormaliseFamInst fun (ForAllTy tyvar ty1)
230 = do { (coi,nty1) <- tcGenericNormaliseFamInst fun ty1
231 ; return (mkForAllTyCoI tyvar coi, mkForAllTy tyvar nty1)
233 tcGenericNormaliseFamInst fun ty@(TyVarTy tv)
235 = do { traceTc (text "tcGenericNormaliseFamInst" <+> ppr ty)
236 ; res <- lookupTcTyVar tv
239 do { maybe_ty' <- fun ty
241 Nothing -> return (IdCo, ty)
243 do { (coi2, ty'') <- tcGenericNormaliseFamInst fun ty'
244 ; return (ACo co1 `mkTransCoI` coi2, ty'')
247 IndirectTv ty' -> tcGenericNormaliseFamInst fun ty'
251 tcGenericNormaliseFamInst fun (PredTy predty)
252 = do { (coi, pred') <- tcGenericNormaliseFamInstPred fun predty
253 ; return (coi, PredTy pred') }
255 ---------------------------------
256 tcGenericNormaliseFamInstPred :: (TcType -> TcM (Maybe (TcType,Coercion)))
258 -> TcM (CoercionI, TcPredType)
260 tcGenericNormaliseFamInstPred fun (ClassP cls tys)
261 = do { (cois, tys')<- mapAndUnzipM (tcGenericNormaliseFamInst fun) tys
262 ; return (mkClassPPredCoI cls tys' cois, ClassP cls tys')
264 tcGenericNormaliseFamInstPred fun (IParam ipn ty)
265 = do { (coi, ty') <- tcGenericNormaliseFamInst fun ty
266 ; return $ (mkIParamPredCoI ipn coi, IParam ipn ty')
268 tcGenericNormaliseFamInstPred fun (EqPred ty1 ty2)
269 = do { (coi1, ty1') <- tcGenericNormaliseFamInst fun ty1
270 ; (coi2, ty2') <- tcGenericNormaliseFamInst fun ty2
271 ; return (mkEqPredCoI ty1' coi1 ty2' coi2, EqPred ty1' ty2') }
275 %************************************************************************
277 \section{Normalisation of equality constraints}
279 %************************************************************************
281 Note [Inconsistencies in equality constraints]
282 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
283 We guarantee that we raise an error if we discover any inconsistencies (i.e.,
284 equalities that if presented to the unifer in TcUnify would result in an
285 error) during normalisation of wanted constraints. This is especially so that
286 we don't solve wanted constraints under an inconsistent given set. In
287 particular, we don't want to permit signatures, such as
289 bad :: (Int ~ Bool => Int) -> a -> a
292 normaliseGivenEqs :: [Inst] -> TcM ([Inst], TcM ())
293 normaliseGivenEqs givens
294 = do { traceTc (text "normaliseGivenEqs <-" <+> ppr givens)
295 ; (result, deSkolem) <-
296 rewriteToFixedPoint (Just ("(SkolemOccurs)", skolemOccurs))
297 [ ("(ZONK)", dontRerun $ zonkInsts)
298 , ("(TRIVIAL)", dontRerun $ trivialRule)
299 , ("(DECOMP)", decompRule)
301 , ("(SUBST)", substRule) -- incl. occurs check
303 ; traceTc (text "normaliseGivenEqs ->" <+> ppr result)
304 ; return (result, deSkolem)
309 normaliseWantedEqs :: [Inst] -- givens
311 -> TcM [Inst] -- irreducible wanteds
312 normaliseWantedEqs givens wanteds
313 = do { traceTc $ text "normaliseWantedEqs <-" <+> ppr wanteds
314 <+> text "with" <+> ppr givens
315 ; result <- liftM fst $ rewriteToFixedPoint Nothing
316 [ ("(ZONK)", dontRerun $ zonkInsts)
317 , ("(TRIVIAL)", dontRerun $ trivialRule)
318 , ("(DECOMP)", decompRule)
320 , ("(GIVEN)", substGivens givens) -- incl. occurs check
321 , ("(UNIFY)", unifyMetaRule) -- incl. occurs check
322 , ("(SUBST)", substRule) -- incl. occurs check
324 ; traceTc (text "normaliseWantedEqs ->" <+> ppr result)
328 -- Use `substInst' with every given on all the wanteds.
329 substGivens :: [Inst] -> [Inst] -> TcM ([Inst], Bool)
330 substGivens [] wanteds = return (wanteds, False)
331 substGivens (g:gs) wanteds
332 = do { (wanteds1, changed1) <- substGivens gs wanteds
333 ; (wanteds2, changed2) <- substInst g wanteds1
334 ; return (wanteds2, changed1 || changed2)
339 %************************************************************************
341 \section{Normalisation of non-equality dictionaries}
343 %************************************************************************
346 normaliseGivenDicts, normaliseWantedDicts
347 :: [Inst] -- given equations
348 -> [Inst] -- dictionaries
349 -> TcM ([Inst],TcDictBinds)
351 normaliseGivenDicts eqs dicts = normalise_dicts eqs dicts False
352 normaliseWantedDicts eqs dicts = normalise_dicts eqs dicts True
355 :: [Inst] -- given equations
356 -> [Inst] -- dictionaries
357 -> Bool -- True <=> the dicts are wanted
358 -- Fals <=> they are given
359 -> TcM ([Inst],TcDictBinds)
360 normalise_dicts given_eqs dicts is_wanted
361 = do { traceTc $ let name | is_wanted = "normaliseWantedDicts <-"
362 | otherwise = "normaliseGivenDicts <-"
364 text name <+> ppr dicts <+>
365 text "with" <+> ppr given_eqs
366 ; (dicts0, binds0) <- normaliseInsts is_wanted dicts
367 ; (dicts1, binds1) <- substEqInDictInsts is_wanted given_eqs dicts0
368 ; let binds01 = binds0 `unionBags` binds1
369 ; if isEmptyBag binds1
370 then return (dicts1, binds01)
371 else do { (dicts2, binds2) <-
372 normalise_dicts given_eqs dicts1 is_wanted
373 ; return (dicts2, binds01 `unionBags` binds2) } }
377 %************************************************************************
379 \section{Normalisation rules and iterative rule application}
381 %************************************************************************
383 We have three kinds of normalising rewrite rules:
385 (1) Normalisation rules that rewrite a set of insts and return a flag indicating
386 whether any changes occurred during rewriting that necessitate re-running
387 the current rule set.
389 (2) Precondition rules that rewrite a set of insts and return a monadic action
390 that reverts the effect of preconditioning.
392 (3) Idempotent normalisation rules that never require re-running the rule set.
395 type RewriteRule = [Inst] -> TcM ([Inst], Bool) -- rewrite, maybe re-run
396 type PrecondRule = [Inst] -> TcM ([Inst], TcM ()) -- rewrite, revertable
397 type IdemRewriteRule = [Inst] -> TcM [Inst] -- rewrite, don't re-run
399 type NamedRule = (String, RewriteRule) -- rule with description
400 type NamedPreRule = (String, PrecondRule) -- precond with desc
403 Template lifting idempotent rules to full rules (which can be put into a rule
407 dontRerun :: IdemRewriteRule -> RewriteRule
408 dontRerun rule insts = liftM addFalse $ rule insts
410 addFalse x = (x, False)
413 The following function applies a set of rewrite rules until a fixed point is
414 reached; i.e., none of the `RewriteRule's require re-running the rule set.
415 Optionally, there may be a pre-conditing rule that is applied before any other
416 rules are applied and before the rule set is re-run.
418 The result is the set of rewritten (i.e., normalised) insts and, in case of a
419 pre-conditing rule, a monadic action that reverts the effects of
420 pre-conditioning - specifically, this is removing introduced skolems.
423 rewriteToFixedPoint :: Maybe NamedPreRule -- optional preconditioning rule
424 -> [NamedRule] -- rule set
425 -> [Inst] -- insts to rewrite
426 -> TcM ([Inst], TcM ())
427 rewriteToFixedPoint precondRule rules insts
428 = completeRewrite (return ()) precondRule insts
430 completeRewrite :: TcM () -> Maybe NamedPreRule -> [Inst]
431 -> TcM ([Inst], TcM ())
432 completeRewrite dePrecond (Just (precondName, precond)) insts
433 = do { traceTc $ text precondName <+> text " <- " <+> ppr insts
434 ; (insts', dePrecond') <- precond insts
435 ; traceTc $ text precondName <+> text " -> " <+> ppr insts'
436 ; tryRules (dePrecond >> dePrecond') rules insts'
438 completeRewrite dePrecond Nothing insts
439 = tryRules dePrecond rules insts
441 tryRules dePrecond _ [] = return ([] , dePrecond)
442 tryRules dePrecond [] insts = return (insts, dePrecond)
443 tryRules dePrecond ((name, rule):rules) insts
444 = do { traceTc $ text name <+> text " <- " <+> ppr insts
445 ; (insts', rerun) <- rule insts
446 ; traceTc $ text name <+> text " -> " <+> ppr insts'
447 ; if rerun then completeRewrite dePrecond precondRule insts'
448 else tryRules dePrecond rules insts'
453 %************************************************************************
455 \section{Different forms of Inst rewrite rules}
457 %************************************************************************
459 Splitting of non-terminating given constraints: skolemOccurs
460 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
461 This is a preconditioning rule exclusively applied to given constraints.
462 Moreover, its rewriting is only temporary, as it is undone by way of
463 side-effecting mutable type variables after simplification and constraint
464 entailment has been completed.
466 This version is an (attempt at, yet unproven, an) *unflattened* version of
467 the SubstL-Ev completion rule.
469 The above rule is essential to catch non-terminating rules that cannot be
470 oriented properly, like
474 a ~ [G a] , where a is a skolem tyvar
476 The left-to-right orientiation is not suitable because it does not
477 terminate. The right-to-left orientation is not suitable because it
478 does not have a type-function on the left. This is undesirable because
479 it would hide information. E.g. assume
483 then rewriting C [G (F a)] to C (F a) is bad because we cannot now
484 see that the C [x] instance applies.
486 The rule also caters for badly-oriented rules of the form:
490 for which other solutions are possible, but this one will do too.
494 co : ty1 ~ ty2{F ty1}
497 sym (F co) : F ty2{b} ~ b
498 where b is a fresh skolem variable
500 We also cater for the symmetric situation *if* the rule cannot be used as a
501 left-to-right rewrite rule.
503 We also return an action (b := ty1) which is used to eliminate b
504 after the dust of normalisation with the completed rewrite system
507 A subtle point of this transformation is that both coercions in the results
508 are strictly speaking incorrect. However, they are correct again after the
509 action {B := ty1} has removed the skolem again. This happens immediately
510 after constraint entailment has been checked; ie, code outside of the
511 simplification and entailment checking framework will never see these
512 temporarily incorrect coercions.
514 NB: We perform this transformation for multiple occurences of ty1 under one
515 or multiple family applications on the left-hand side at once (ie, the
516 rule doesn't need to be applied multiple times at a single inst). As a
517 result we can get two or more insts back.
519 Note [skolemOccurs loop]
520 ~~~~~~~~~~~~~~~~~~~~~~~~
521 You might think that under
524 type instance F [a] = [F a]
528 foo :: (F [a] ~ a) => a
530 will get us into a loop. However, this is *not* the case. Here is why:
541 F [b<tau>] ~ b<tau> , with b := F a
546 [F b<tau>] ~ b<tau> , with b := F a
548 At this point (SkolemOccurs) does *not* apply anymore, as
552 is not used as a rewrite rule. The variable b<tau> is not a skolem (cf
555 (The regression test indexed-types/should_compile/Simple20 checks that the
556 described property of the system does not change.)
559 skolemOccurs :: PrecondRule
561 = do { (instss, undoSkolems) <- mapAndUnzipM oneSkolemOccurs insts
562 ; return (concat instss, sequence_ undoSkolems)
566 = ASSERT( isEqInst inst )
567 case eqInstToRewrite inst of
568 Just (rewrite, swapped) -> breakRecursion rewrite swapped
569 Nothing -> return ([inst], return ())
571 -- inst is an elementary rewrite rule, check whether we need to break
573 breakRecursion (Rewrite pat body _) swapped
575 -- skolemOccurs does not apply, leave as is
577 = do { traceTc $ text "oneSkolemOccurs: no tys to lift out"
578 ; return ([inst], return ())
581 -- recursive occurence of pat in body under a type family application
583 = do { traceTc $ text "oneSkolemOccurs[TLO]:" <+> ppr tysToLiftOut
584 ; skTvs <- mapM (newMetaTyVar TauTv . typeKind) tysToLiftOut
585 ; let skTvs_tysTLO = zip skTvs tysToLiftOut
586 insertSkolems = return . replace skTvs_tysTLO
587 ; (_, body') <- tcGenericNormaliseFamInst insertSkolems body
588 ; inst' <- if swapped then mkEqInst (EqPred body' pat) co
589 else mkEqInst (EqPred pat body') co
590 -- ensure to reconstruct the inst in the
591 -- original orientation
592 ; traceTc $ text "oneSkolemOccurs[inst']:" <+> ppr inst'
593 ; (insts, undoSk) <- mapAndUnzipM (mkSkolemInst inst')
595 ; return (inst':insts, sequence_ undoSk)
598 co = eqInstCoercion inst
600 -- all subtypes that are (1) type family instances and (2) contain
601 -- the lhs type as part of the type arguments of the type family
603 tysToLiftOut = [mkTyConApp tc tys | (tc, tys) <- tyFamInsts body
604 , any (pat `tcPartOfType`) tys]
606 replace :: [(TcTyVar, Type)] -> Type -> Maybe (Type, Coercion)
607 replace [] _ = Nothing
608 replace ((skTv, tyTLO):rest) ty
609 | tyTLO `tcEqType` ty = Just (mkTyVarTy skTv, undefined)
610 | otherwise = replace rest ty
612 -- create the EqInst for the equality determining the skolem and a
613 -- TcM action undoing the skolem introduction
614 mkSkolemInst inst' (skTv, tyTLO)
615 = do { (co, tyLiftedOut) <- tcEqInstNormaliseFamInst inst' tyTLO
616 ; inst <- mkEqInst (EqPred tyLiftedOut (mkTyVarTy skTv))
617 (mkGivenCo $ mkSymCoercion (fromACo co))
618 -- co /= IdCo due to construction of inst'
619 ; return (inst, writeMetaTyVar skTv tyTLO)
624 Removal of trivial equalities: trivialRule
625 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
626 The following rules exploits the reflexivity of equality:
634 trivialRule :: IdemRewriteRule
636 = liftM catMaybes $ mapM trivial insts
639 | ASSERT( isEqInst inst )
641 = do { eitherEqInst inst
642 (\cotv -> writeMetaTyVar cotv ty1)
649 (ty1,ty2) = eqInstTys inst
653 Decomposition of data type constructors: decompRule
654 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
655 Whenever, the same *data* constructors occurs on both sides of an equality, we
656 can decompose as in standard unification.
661 g21 : c1 ~ d1, ..., g2n : cn ~ dn
664 Works also for the case where T is actually an application of a type family
665 constructor to a set of types, provided the applications on both sides of the
666 ~ are identical; see also Note [OpenSynTyCon app] in TcUnify.
668 We guarantee to raise an error for any inconsistent equalities;
669 cf Note [Inconsistencies in equality constraints].
672 decompRule :: RewriteRule
674 = do { (insts, changed) <- mapAndUnzipM decomp insts
675 ; return (concat insts, or changed)
679 = ASSERT( isEqInst inst )
682 (ty1,ty2) = eqInstTys inst
684 | Just ty1' <- tcView ty1 = go ty1' ty2
685 | Just ty2' <- tcView ty2 = go ty1 ty2'
687 go (TyConApp con1 tys1) (TyConApp con2 tys2)
688 | con1 == con2 && identicalHead
689 = mkArgInsts (mkTyConApp con1) tys1 tys2
691 | con1 /= con2 && not (isOpenSynTyCon con1 || isOpenSynTyCon con2)
692 -- not matching data constructors (of any flavour) are bad news
693 = eqInstMisMatch inst
696 (idxTys1, _) = splitAt n tys1
697 (idxTys2, _) = splitAt n tys2
698 identicalHead = not (isOpenSynTyCon con1) ||
699 idxTys1 `tcEqTypes` idxTys2
701 go (FunTy fun1 arg1) (FunTy fun2 arg2)
702 = mkArgInsts (\[funCo, argCo] -> mkFunTy funCo argCo) [fun1, arg1]
705 -- Applications need a bit of care!
706 -- They can match FunTy and TyConApp, so use splitAppTy_maybe
708 | Just (s2, t2) <- tcSplitAppTy_maybe ty2
709 = mkArgInsts (\[s, t] -> mkAppTy s t) [s1, t1] [s2, t2]
713 | Just (s1, t1) <- tcSplitAppTy_maybe ty1
714 = mkArgInsts (\[s, t] -> mkAppTy s t) [s1, t1] [s2, t2]
716 -- We already covered all the consistent cases of rigid types on both
717 -- sides; so, if we see two rigid types here, we discovered an
720 | isRigid ty1 && isRigid ty2
721 = eqInstMisMatch inst
723 -- We can neither assert consistency nor inconsistency => defer
724 go _ _ = return ([inst], False)
726 isRigid (TyConApp con _) = not (isOpenSynTyCon con)
727 isRigid (FunTy _ _) = True
728 isRigid (AppTy _ _) = True
731 -- Create insts for matching argument positions (ie, the bit after
732 -- '>-->' in the rule description above)
733 mkArgInsts con tys1 tys2
734 = do { cos <- eitherEqInst inst
735 -- old_co := Con1 cos
737 do { cotvs <- zipWithM newMetaCoVar tys1 tys2
738 ; let cos = map mkTyVarTy cotvs
739 ; writeMetaTyVar old_covar (con cos)
740 ; return $ map mkWantedCo cotvs
742 -- co_i := Con_i old_co
744 return $ map mkGivenCo $
745 mkRightCoercions (length tys1) old_co)
746 ; insts <- zipWithM mkEqInst (zipWith EqPred tys1 tys2) cos
747 ; traceTc (text "decomp identicalHead" <+> ppr insts)
748 ; return (insts, not $ null insts)
753 Rewriting with type instances: topRule
754 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
755 We use (toplevel) type instances to normalise both sides of equalities.
759 >--> co1 :: t ~ t' / co2 :: s ~ s'
761 g1 := co1 * g2 * sym co2
764 topRule :: RewriteRule
766 = do { (insts, changed) <- mapAndUnzipM top insts
767 ; return (insts, or changed)
771 = ASSERT( isEqInst inst )
772 do { (coi1, ty1') <- tcNormaliseFamInst ty1
773 ; (coi2, ty2') <- tcNormaliseFamInst ty2
774 ; case (coi1, coi2) of
775 (IdCo, IdCo) -> return (inst, False)
779 -- old_co = co1 * new_co * sym co2
781 do { new_cotv <- newMetaCoVar ty1' ty2'
782 ; let new_co = mkTyVarTy new_cotv
783 old_coi = coi1 `mkTransCoI`
784 ACo new_co `mkTransCoI`
786 ; writeMetaTyVar old_covar (fromACo old_coi)
787 ; return $ mkWantedCo new_cotv
789 -- new_co = sym co1 * old_co * co2
794 mkSymCoI coi1 `mkTransCoI`
795 ACo old_co `mkTransCoI` coi2)
796 ; new_inst <- mkEqInst (EqPred ty1' ty2') wg_co
797 ; return (new_inst, True)
801 (ty1,ty2) = eqInstTys inst
805 Rewriting with equalities: substRule
806 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
807 From a set of insts, use all insts that can be read as rewrite rules to
808 rewrite the types in all other insts.
812 forall g1 : s1{F c} ~ s2{F c}
815 g1 := s1{g} * g2 * sym s2{g} <=> g2 := sym s1{g} * g1 * s2{g}
817 Alternatively, the rewrite rule may have the form (g : a ~ t).
819 To avoid having to swap rules of the form (g : t ~ F c) and (g : t ~ a),
820 where t is neither a variable nor a type family application, we use them for
821 rewriting from right-to-left. However, it is crucial to only apply rules
822 from right-to-left if they cannot be used left-to-right.
824 The workhorse is substInst, which performs an occurs check before actually
825 using an equality for rewriting. If the type pattern occurs in the type we
826 substitute for the pattern, normalisation would diverge.
829 substRule :: RewriteRule
830 substRule insts = tryAllInsts insts []
832 -- for every inst check whether it can be used to rewrite the others
833 -- (we make an effort to keep the insts in order; it makes debugging
835 tryAllInsts [] triedInsts = return (reverse triedInsts, False)
836 tryAllInsts (inst:insts) triedInsts
837 = do { (insts', changed) <- substInst inst (reverse triedInsts ++ insts)
838 ; if changed then return (insertAt (length triedInsts) inst insts',
840 else tryAllInsts insts (inst:triedInsts)
843 insertAt n x xs = let (xs1, xs2) = splitAt n xs
846 -- Use the given inst as a rewrite rule to normalise the insts in the second
847 -- argument. Don't do anything if the inst cannot be used as a rewrite rule,
848 -- but do apply it right-to-left, if possible, and if it cannot be used
851 substInst :: Inst -> [Inst] -> TcM ([Inst], Bool)
853 = case eqInstToRewrite inst of
854 Just (rewrite, _) -> substEquality rewrite insts
855 Nothing -> return (insts, False)
857 substEquality :: Rewrite -- elementary rewrite
858 -> [Inst] -- insts to rewrite
859 -> TcM ([Inst], Bool)
860 substEquality eqRule@(Rewrite pat rhs _) insts
861 | pat `tcPartOfType` rhs -- occurs check!
862 = occurCheckErr pat rhs
864 = do { (insts', changed) <- mapAndUnzipM substOne insts
865 ; return (insts', or changed)
869 = ASSERT( isEqInst inst )
870 do { (coi1, ty1') <- tcEqRuleNormaliseFamInst eqRule ty1
871 ; (coi2, ty2') <- tcEqRuleNormaliseFamInst eqRule ty2
872 ; case (coi1, coi2) of
873 (IdCo, IdCo) -> return (inst, False)
877 -- old_co := co1 * new_co * sym co2
879 do { new_cotv <- newMetaCoVar ty1' ty2'
880 ; let new_co = mkTyVarTy new_cotv
881 old_coi = coi1 `mkTransCoI`
882 ACo new_co `mkTransCoI`
884 ; writeMetaTyVar old_covar (fromACo old_coi)
885 ; return $ mkWantedCo new_cotv
887 -- new_co := sym co1 * old_co * co2
892 mkSymCoI coi1 `mkTransCoI`
893 ACo old_co `mkTransCoI` coi2)
894 ; new_inst <- mkEqInst (EqPred ty1' ty2') gw_co
895 ; return (new_inst, True)
899 (ty1,ty2) = eqInstTys inst
903 Instantiate meta variables: unifyMetaRule
904 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
905 If an equality equates a meta type variable with a type, we simply instantiate
914 Meta variables can only appear in wanted constraints, and this rule should
915 only be applied to wanted constraints. We also know that t definitely is
916 distinct from alpha (as the trivialRule) has been run on the insts beforehand.
918 NB: We cannot assume that meta tyvars are empty. They may have been updated
919 by another inst in the currently processed wanted list. We need to be very
920 careful when updateing type variables (see TcUnify.uUnfilledVar), but at least
921 we know that we have no boxes. It's unclear that it would be an advantage to
922 common up the code in TcUnify and the code below. Firstly, we don't want
923 calls to TcUnify.defer_unification here, and secondly, TcUnify import the
924 current module, so we would have to move everything here (Yuk!) or to
925 TcMType. Besides, the code here is much simpler due to the lack of boxes.
928 unifyMetaRule :: RewriteRule
930 = do { (insts', changed) <- mapAndUnzipM unifyMeta insts
931 ; return (concat insts', or changed)
935 = ASSERT( isEqInst inst )
937 (fromWantedCo "unifyMetaRule" $ eqInstCoercion inst)
939 (ty1,ty2) = eqInstTys inst
941 | Just ty1' <- tcView ty1 = go ty1' ty2 cotv
942 | Just ty2' <- tcView ty2 = go ty1 ty2' cotv
945 , isMetaTyVar tv1 = do { lookupTV <- lookupTcTyVar tv1
946 ; uMeta False tv1 lookupTV ty2 cotv
949 , isMetaTyVar tv2 = do { lookupTV <- lookupTcTyVar tv2
950 ; uMeta True tv2 lookupTV ty1 cotv
952 | otherwise = return ([inst], False)
954 -- meta variable has been filled already
955 -- => ignore this inst (we'll come around again, after zonking)
956 uMeta _swapped _tv (IndirectTv _) _ty _cotv
957 = return ([inst], False)
959 -- type variable meets type variable
960 -- => check that tv2 hasn't been updated yet and choose which to update
961 uMeta swapped tv1 (DoneTv details1) (TyVarTy tv2) cotv
963 = return ([inst], False) -- The two types are already identical
966 = do { lookupTV2 <- lookupTcTyVar tv2
968 IndirectTv ty -> uMeta swapped tv1 (DoneTv details1) ty cotv
969 DoneTv details2 -> uMetaVar swapped tv1 details1 tv2 details2 cotv
972 ------ Beyond this point we know that ty2 is not a type variable
974 -- signature skolem meets non-variable type
976 uMeta _swapped _tv (DoneTv (MetaTv (SigTv _) _)) _non_tv_ty _cotv
977 = return ([inst], False)
979 -- updatable meta variable meets non-variable type
980 -- => occurs check, monotype check, and kinds match check, then update
981 uMeta swapped tv (DoneTv (MetaTv _ ref)) non_tv_ty cotv
982 = do { mb_ty' <- checkTauTvUpdate tv non_tv_ty -- occurs + monotype check
984 Nothing -> return ([inst], False) -- tv occurs in faminst
986 do { checkUpdateMeta swapped tv ref ty' -- update meta var
987 ; writeMetaTyVar cotv ty' -- update co var
992 uMeta _ _ _ _ _ = panic "uMeta"
994 -- uMetaVar: unify two type variables
995 -- meta variable meets skolem
997 uMetaVar swapped tv1 (MetaTv _ ref) tv2 (SkolemTv _) cotv
998 = do { checkUpdateMeta swapped tv1 ref (mkTyVarTy tv2)
999 ; writeMetaTyVar cotv (mkTyVarTy tv2)
1003 -- meta variable meets meta variable
1004 -- => be clever about which of the two to update
1005 -- (from TcUnify.uUnfilledVars minus boxy stuff)
1006 uMetaVar swapped tv1 (MetaTv info1 ref1) tv2 (MetaTv info2 ref2) cotv
1007 = do { case (info1, info2) of
1008 -- Avoid SigTvs if poss
1009 (SigTv _, _ ) | k1_sub_k2 -> update_tv2
1010 (_, SigTv _) | k2_sub_k1 -> update_tv1
1012 (_, _) | k1_sub_k2 -> if k2_sub_k1 && nicer_to_update_tv1
1013 then update_tv1 -- Same kinds
1015 | k2_sub_k1 -> update_tv1
1016 | otherwise -> kind_err
1017 -- Update the variable with least kind info
1018 -- See notes on type inference in Kind.lhs
1019 -- The "nicer to" part only applies if the two kinds are the same,
1020 -- so we can choose which to do.
1022 ; writeMetaTyVar cotv (mkTyVarTy tv2)
1026 -- Kinds should be guaranteed ok at this point
1027 update_tv1 = updateMeta tv1 ref1 (mkTyVarTy tv2)
1028 update_tv2 = updateMeta tv2 ref2 (mkTyVarTy tv1)
1030 kind_err = addErrCtxtM (unifyKindCtxt swapped tv1 (mkTyVarTy tv2)) $
1031 unifyKindMisMatch k1 k2
1035 k1_sub_k2 = k1 `isSubKind` k2
1036 k2_sub_k1 = k2 `isSubKind` k1
1038 nicer_to_update_tv1 = isSystemName (Var.varName tv1)
1039 -- Try to update sys-y type variables in preference to ones
1040 -- gotten (say) by instantiating a polymorphic function with
1041 -- a user-written type sig
1043 uMetaVar _ _ _ _ _ _ = panic "uMetaVar"
1047 %************************************************************************
1049 \section{Normalisation of Insts}
1051 %************************************************************************
1053 Normalises a set of dictionaries relative to a set of given equalities (which
1054 are interpreted as rewrite rules). We only consider given equalities of the
1059 where F is a type family.
1062 substEqInDictInsts :: Bool -- whether the *dictionaries* are wanted/given
1063 -> [Inst] -- given equalities (used as rewrite rules)
1064 -> [Inst] -- dictinaries to be normalised
1065 -> TcM ([Inst], TcDictBinds)
1066 substEqInDictInsts isWanted eqInsts dictInsts
1067 = do { traceTc (text "substEqInDictInst <-" <+> ppr dictInsts)
1069 foldlM rewriteWithOneEquality (dictInsts, emptyBag) eqInsts
1070 ; traceTc (text "substEqInDictInst ->" <+> ppr dictInsts')
1074 -- (1) Given equality of form 'F ts ~ t' or 'a ~ t': use for rewriting
1075 rewriteWithOneEquality (dictInsts, dictBinds)
1076 eqInst@(EqInst {tci_left = pattern,
1077 tci_right = target})
1078 | isOpenSynTyConApp pattern || isTyVarTy pattern
1079 = do { (dictInsts', moreDictBinds) <-
1080 genericNormaliseInsts isWanted applyThisEq dictInsts
1081 ; return (dictInsts', dictBinds `unionBags` moreDictBinds)
1084 applyThisEq = tcGenericNormaliseFamInstPred (return . matchResult)
1086 -- rewrite in case of an exact match
1087 matchResult ty | tcEqType pattern ty = Just (target, eqInstType eqInst)
1088 | otherwise = Nothing
1090 -- (2) Given equality has the wrong form: ignore
1091 rewriteWithOneEquality (dictInsts, dictBinds) _not_a_rewrite_rule
1092 = return (dictInsts, dictBinds)
1096 Take a bunch of Insts (not EqInsts), and normalise them wrt the top-level
1097 type-function equations, where
1099 (norm_insts, binds) = normaliseInsts is_wanted insts
1102 = True, (binds + norm_insts) defines insts (wanteds)
1103 = False, (binds + insts) defines norm_insts (givens)
1105 Ie, in the case of normalising wanted dictionaries, we use the normalised
1106 dictionaries to define the originally wanted ones. However, in the case of
1107 given dictionaries, we use the originally given ones to define the normalised
1111 normaliseInsts :: Bool -- True <=> wanted insts
1112 -> [Inst] -- wanted or given insts
1113 -> TcM ([Inst], TcDictBinds) -- normalised insts and bindings
1114 normaliseInsts isWanted insts
1115 = genericNormaliseInsts isWanted tcNormaliseFamInstPred insts
1117 genericNormaliseInsts :: Bool -- True <=> wanted insts
1118 -> (TcPredType -> TcM (CoercionI, TcPredType))
1120 -> [Inst] -- wanted or given insts
1121 -> TcM ([Inst], TcDictBinds) -- normalised insts & binds
1122 genericNormaliseInsts isWanted fun insts
1123 = do { (insts', binds) <- mapAndUnzipM (normaliseOneInst isWanted fun) insts
1124 ; return (insts', unionManyBags binds)
1127 normaliseOneInst isWanted fun
1128 dict@(Dict {tci_pred = pred,
1130 = do { traceTc $ text "genericNormaliseInst <-" <+> ppr dict
1131 ; (coi, pred') <- fun pred
1135 do { traceTc $ text "genericNormaliseInst ->" <+> ppr dict
1136 ; return (dict, emptyBag)
1138 -- don't use pred' in this case; otherwise, we get
1139 -- more unfolded closed type synonyms in error messages
1141 do { -- an inst for the new pred
1142 ; dict' <- newDictBndr loc pred'
1143 -- relate the old inst to the new one
1144 -- target_dict = source_dict `cast` st_co
1145 ; let (target_dict, source_dict, st_co)
1146 | isWanted = (dict, dict', mkSymCoercion co)
1147 | otherwise = (dict', dict, co)
1149 -- co :: dict ~ dict'
1150 -- hence, if isWanted
1151 -- dict = dict' `cast` sym co
1153 -- dict' = dict `cast` co
1154 expr = HsVar $ instToId source_dict
1155 cast_expr = HsWrap (WpCast st_co) expr
1156 rhs = L (instLocSpan loc) cast_expr
1157 binds = instToDictBind target_dict rhs
1158 -- return the new inst
1159 ; traceTc $ let name | isWanted
1160 = "genericNormaliseInst (wanted) ->"
1162 = "genericNormaliseInst (given) ->"
1164 text name <+> ppr dict' <+>
1165 text "with" <+> ppr binds
1166 ; return (dict', binds)
1170 -- TOMDO: What do we have to do about ImplicInst, Method, and LitInst??
1171 normaliseOneInst _isWanted _fun inst
1172 = do { inst' <- zonkInst inst
1173 ; traceTc $ text "*** TcTyFuns.normaliseOneInst: Skipping" <+>
1175 ; return (inst', emptyBag)
1180 %************************************************************************
1184 %************************************************************************
1186 The infamous couldn't match expected type soandso against inferred type
1187 somethingdifferent message.
1190 eqInstMisMatch :: Inst -> TcM a
1192 = ASSERT( isEqInst inst )
1193 setErrCtxt ctxt $ failWithMisMatch ty_act ty_exp
1195 (ty_act, ty_exp) = eqInstTys inst
1196 InstLoc _ _ ctxt = instLoc inst
1198 -----------------------
1199 failWithMisMatch :: TcType -> TcType -> TcM a
1200 -- Generate the message when two types fail to match,
1201 -- going to some trouble to make it helpful.
1202 -- The argument order is: actual type, expected type
1203 failWithMisMatch ty_act ty_exp
1204 = do { env0 <- tcInitTidyEnv
1205 ; ty_exp <- zonkTcType ty_exp
1206 ; ty_act <- zonkTcType ty_act
1207 ; failWithTcM (misMatchMsg env0 (ty_act, ty_exp))
1210 misMatchMsg :: TidyEnv -> (TcType, TcType) -> (TidyEnv, SDoc)
1211 misMatchMsg env0 (ty_act, ty_exp)
1212 = let (env1, pp_exp, extra_exp) = ppr_ty env0 ty_exp
1213 (env2, pp_act, extra_act) = ppr_ty env1 ty_act
1214 msg = sep [sep [ptext (sLit "Couldn't match expected type") <+> pp_exp,
1216 ptext (sLit "against inferred type") <+> pp_act],
1217 nest 2 (extra_exp $$ extra_act)]
1222 ppr_ty :: TidyEnv -> TcType -> (TidyEnv, SDoc, SDoc)
1224 = let (env1, tidy_ty) = tidyOpenType env ty
1225 (env2, extra) = ppr_extra env1 tidy_ty
1227 (env2, quotes (ppr tidy_ty), extra)
1229 -- (ppr_extra env ty) shows extra info about 'ty'
1230 ppr_extra :: TidyEnv -> Type -> (TidyEnv, SDoc)
1231 ppr_extra env (TyVarTy tv)
1232 | isTcTyVar tv && (isSkolemTyVar tv || isSigTyVar tv) && not (isUnk tv)
1233 = (env1, pprSkolTvBinding tv1)
1235 (env1, tv1) = tidySkolemTyVar env tv
1237 ppr_extra env _ty = (env, empty) -- Normal case