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 misMatchMsg, failWithMisMatch
18 #include "HsVersions.h"
30 import TypeRep ( Type(..) )
38 import SrcLoc ( Located(..) )
47 %************************************************************************
49 Normalisation of types
51 %************************************************************************
53 Unfold a single synonym family instance and yield the witnessing coercion.
54 Return 'Nothing' if the given type is either not synonym family instance
55 or is a synonym family instance that has no matching instance declaration.
56 (Applies only if the type family application is outermost.)
58 For example, if we have
60 :Co:R42T a :: T [a] ~ :R42T a
62 then 'T [Int]' unfolds to (:R42T Int, :Co:R42T Int).
65 tcUnfoldSynFamInst :: Type -> TcM (Maybe (Type, Coercion))
66 tcUnfoldSynFamInst (TyConApp tycon tys)
67 | not (isOpenSynTyCon tycon) -- unfold *only* _synonym_ family instances
70 = do { -- we only use the indexing arguments for matching,
71 -- not the additional ones
72 ; maybeFamInst <- tcLookupFamInst tycon idxTys
73 ; case maybeFamInst of
74 Nothing -> return Nothing
75 Just (rep_tc, rep_tys) -> return $ Just (mkTyConApp rep_tc tys',
76 mkTyConApp coe_tc tys')
78 tys' = rep_tys ++ restTys
79 coe_tc = expectJust "TcTyFun.tcUnfoldSynFamInst"
80 (tyConFamilyCoercion_maybe rep_tc)
84 (idxTys, restTys) = splitAt n tys
85 tcUnfoldSynFamInst _other = return Nothing
88 Normalise 'Type's and 'PredType's by unfolding type family applications where
89 possible (ie, we treat family instances as a TRS). Also zonk meta variables.
91 tcNormaliseFamInst ty = (co, ty')
95 tcNormaliseFamInst :: TcType -> TcM (CoercionI, TcType)
96 tcNormaliseFamInst = tcGenericNormaliseFamInst tcUnfoldSynFamInst
98 tcNormaliseFamInstPred :: TcPredType -> TcM (CoercionI, TcPredType)
99 tcNormaliseFamInstPred = tcGenericNormaliseFamInstPred tcUnfoldSynFamInst
102 An elementary rewrite is a properly oriented equality with associated coercion
103 that has one of the following two forms:
105 (1) co :: F t1..tn ~ t
106 (2) co :: a ~ t , where t /= F t1..tn and a is a skolem tyvar
108 NB: We do *not* use equalities of the form a ~ t where a is a meta tyvar as a
109 reqrite rule. Instead, such equalities are solved by unification. This is
110 essential; cf Note [skolemOccurs loop].
112 The following functions takes an equality instance and turns it into an
113 elementary rewrite if possible.
116 data Rewrite = Rewrite TcType -- lhs of rewrite rule
117 TcType -- rhs of rewrite rule
118 TcType -- coercion witnessing the rewrite rule
120 eqInstToRewrite :: Inst -> Maybe (Rewrite, Bool)
121 -- True iff rewrite swapped equality
123 = ASSERT( isEqInst inst )
124 go ty1 ty2 (eqInstType inst)
126 (ty1,ty2) = eqInstTys inst
128 -- look through synonyms
129 go ty1 ty2 co | Just ty1' <- tcView ty1 = go ty1' ty2 co
130 go ty1 ty2 co | Just ty2' <- tcView ty2 = go ty1 ty2' co
132 -- left-to-right rule with type family head
133 go ty1@(TyConApp con _) ty2 co
135 = Just (Rewrite ty1 ty2 co, False) -- not swapped
137 -- left-to-right rule with type variable head
138 go ty1@(TyVarTy tv) ty2 co
140 = Just (Rewrite ty1 ty2 co, False) -- not swapped
142 -- right-to-left rule with type family head, only after
143 -- having checked whether we can work left-to-right
144 go ty1 ty2@(TyConApp con _) co
146 = Just (Rewrite ty2 ty1 (mkSymCoercion co), True) -- swapped
148 -- right-to-left rule with type variable head, only after
149 -- having checked whether we can work left-to-right
150 go ty1 ty2@(TyVarTy tv) co
152 = Just (Rewrite ty2 ty1 (mkSymCoercion co), True) -- swapped
154 -- this equality is not a rewrite rule => ignore
158 Normalise a type relative to an elementary rewrite implied by an EqInst or an
159 explicitly given elementary rewrite.
163 -- Precondition: the EqInst passes the occurs check
164 tcEqInstNormaliseFamInst :: Inst -> TcType -> TcM (CoercionI, TcType)
165 tcEqInstNormaliseFamInst inst ty
166 = case eqInstToRewrite inst of
167 Just (rewrite, _) -> tcEqRuleNormaliseFamInst rewrite ty
168 Nothing -> return (IdCo, ty)
170 -- Rewrite by equality rewrite rule
171 tcEqRuleNormaliseFamInst :: Rewrite -- elementary rewrite
172 -> TcType -- type to rewrite
173 -> TcM (CoercionI, -- witnessing coercion
174 TcType) -- rewritten type
175 tcEqRuleNormaliseFamInst (Rewrite pat rhs co) ty
176 = tcGenericNormaliseFamInst matchEqRule ty
178 matchEqRule sty | pat `tcEqType` sty = return $ Just (rhs, co)
179 | otherwise = return $ Nothing
182 Generic normalisation of 'Type's and 'PredType's; ie, walk the type term and
183 apply the normalisation function gives as the first argument to every TyConApp
184 and every TyVarTy subterm.
186 tcGenericNormaliseFamInst fun ty = (co, ty')
189 This function is (by way of using smart constructors) careful to ensure that
190 the returned coercion is exactly IdCo (and not some semantically equivalent,
191 but syntactically different coercion) whenever (ty' `tcEqType` ty). This
192 makes it easy for the caller to determine whether the type changed. BUT
193 even if we return IdCo, ty' may be *syntactically* different from ty due to
194 unfolded closed type synonyms (by way of tcCoreView). In the interest of
195 good error messages, callers should discard ty' in favour of ty in this case.
198 tcGenericNormaliseFamInst :: (TcType -> TcM (Maybe (TcType, Coercion)))
199 -- what to do with type functions and tyvars
200 -> TcType -- old type
201 -> TcM (CoercionI, TcType) -- (coercion, new type)
202 tcGenericNormaliseFamInst fun ty
203 | Just ty' <- tcView ty = tcGenericNormaliseFamInst fun ty'
204 tcGenericNormaliseFamInst fun (TyConApp tyCon tys)
205 = do { (cois, ntys) <- mapAndUnzipM (tcGenericNormaliseFamInst fun) tys
206 ; let tycon_coi = mkTyConAppCoI tyCon ntys cois
207 ; maybe_ty_co <- fun (mkTyConApp tyCon ntys) -- use normalised args!
208 ; case maybe_ty_co of
209 -- a matching family instance exists
211 do { let first_coi = mkTransCoI tycon_coi (ACo co)
212 ; (rest_coi, nty) <- tcGenericNormaliseFamInst fun ty'
213 ; let fix_coi = mkTransCoI first_coi rest_coi
214 ; return (fix_coi, nty)
216 -- no matching family instance exists
217 -- we do not do anything
218 Nothing -> return (tycon_coi, mkTyConApp tyCon ntys)
220 tcGenericNormaliseFamInst fun (AppTy ty1 ty2)
221 = do { (coi1,nty1) <- tcGenericNormaliseFamInst fun ty1
222 ; (coi2,nty2) <- tcGenericNormaliseFamInst fun ty2
223 ; return (mkAppTyCoI nty1 coi1 nty2 coi2, mkAppTy nty1 nty2)
225 tcGenericNormaliseFamInst fun (FunTy ty1 ty2)
226 = do { (coi1,nty1) <- tcGenericNormaliseFamInst fun ty1
227 ; (coi2,nty2) <- tcGenericNormaliseFamInst fun ty2
228 ; return (mkFunTyCoI nty1 coi1 nty2 coi2, mkFunTy nty1 nty2)
230 tcGenericNormaliseFamInst fun (ForAllTy tyvar ty1)
231 = do { (coi,nty1) <- tcGenericNormaliseFamInst fun ty1
232 ; return (mkForAllTyCoI tyvar coi, mkForAllTy tyvar nty1)
234 tcGenericNormaliseFamInst fun (NoteTy note ty1)
235 = do { (coi,nty1) <- tcGenericNormaliseFamInst fun ty1
236 ; return (coi, NoteTy note nty1)
238 tcGenericNormaliseFamInst fun ty@(TyVarTy tv)
240 = do { traceTc (text "tcGenericNormaliseFamInst" <+> ppr ty)
241 ; res <- lookupTcTyVar tv
244 do { maybe_ty' <- fun ty
246 Nothing -> return (IdCo, ty)
248 do { (coi2, ty'') <- tcGenericNormaliseFamInst fun ty'
249 ; return (ACo co1 `mkTransCoI` coi2, ty'')
252 IndirectTv ty' -> tcGenericNormaliseFamInst fun ty'
256 tcGenericNormaliseFamInst fun (PredTy predty)
257 = do { (coi, pred') <- tcGenericNormaliseFamInstPred fun predty
258 ; return (coi, PredTy pred') }
260 ---------------------------------
261 tcGenericNormaliseFamInstPred :: (TcType -> TcM (Maybe (TcType,Coercion)))
263 -> TcM (CoercionI, TcPredType)
265 tcGenericNormaliseFamInstPred fun (ClassP cls tys)
266 = do { (cois, tys')<- mapAndUnzipM (tcGenericNormaliseFamInst fun) tys
267 ; return (mkClassPPredCoI cls tys' cois, ClassP cls tys')
269 tcGenericNormaliseFamInstPred fun (IParam ipn ty)
270 = do { (coi, ty') <- tcGenericNormaliseFamInst fun ty
271 ; return $ (mkIParamPredCoI ipn coi, IParam ipn ty')
273 tcGenericNormaliseFamInstPred fun (EqPred ty1 ty2)
274 = do { (coi1, ty1') <- tcGenericNormaliseFamInst fun ty1
275 ; (coi2, ty2') <- tcGenericNormaliseFamInst fun ty2
276 ; return (mkEqPredCoI ty1' coi1 ty2' coi2, EqPred ty1' ty2') }
280 %************************************************************************
282 \section{Normalisation of equality constraints}
284 %************************************************************************
286 Note [Inconsistencies in equality constraints]
287 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
288 We guarantee that we raise an error if we discover any inconsistencies (i.e.,
289 equalities that if presented to the unifer in TcUnify would result in an
290 error) during normalisation of wanted constraints. This is especially so that
291 we don't solve wanted constraints under an inconsistent given set. In
292 particular, we don't want to permit signatures, such as
294 bad :: (Int ~ Bool => Int) -> a -> a
297 normaliseGivenEqs :: [Inst] -> TcM ([Inst], TcM ())
298 normaliseGivenEqs givens
299 = do { traceTc (text "normaliseGivenEqs <-" <+> ppr givens)
300 ; (result, deSkolem) <-
301 rewriteToFixedPoint (Just ("(SkolemOccurs)", skolemOccurs))
302 [ ("(ZONK)", dontRerun $ zonkInsts)
303 , ("(TRIVIAL)", dontRerun $ trivialRule)
304 , ("(DECOMP)", decompRule)
306 , ("(SUBST)", substRule) -- incl. occurs check
308 ; traceTc (text "normaliseGivenEqs ->" <+> ppr result)
309 ; return (result, deSkolem)
314 normaliseWantedEqs :: [Inst] -> TcM [Inst]
315 normaliseWantedEqs insts
316 = do { traceTc (text "normaliseWantedEqs <-" <+> ppr insts)
317 ; result <- liftM fst $ rewriteToFixedPoint Nothing
318 [ ("(ZONK)", dontRerun $ zonkInsts)
319 , ("(TRIVIAL)", dontRerun $ trivialRule)
320 , ("(DECOMP)", decompRule)
322 , ("(UNIFY)", unifyMetaRule) -- incl. occurs check
323 , ("(SUBST)", substRule) -- incl. occurs check
325 ; traceTc (text "normaliseWantedEqs ->" <+> ppr result)
331 %************************************************************************
333 \section{Solving of wanted constraints with respect to a given set}
335 %************************************************************************
337 The set of given equalities must have been normalised already.
340 solveWantedEqs :: [Inst] -- givens
342 -> TcM [Inst] -- irreducible wanteds
343 solveWantedEqs givens wanteds
344 = do { traceTc $ text "solveWantedEqs <-" <+> ppr wanteds <+> text "with" <+>
346 ; result <- liftM fst $ rewriteToFixedPoint Nothing
347 [ ("(ZONK)", dontRerun $ zonkInsts)
348 , ("(TRIVIAL)", dontRerun $ trivialRule)
349 , ("(DECOMP)", decompRule)
351 , ("(GIVEN)", substGivens givens) -- incl. occurs check
352 , ("(UNIFY)", unifyMetaRule) -- incl. occurs check
354 ; traceTc (text "solveWantedEqs ->" <+> ppr result)
358 -- Use `substInst' with every given on all the wanteds.
359 substGivens :: [Inst] -> [Inst] -> TcM ([Inst], Bool)
360 substGivens [] wanteds = return (wanteds, False)
361 substGivens (g:gs) wanteds
362 = do { (wanteds1, changed1) <- substGivens gs wanteds
363 ; (wanteds2, changed2) <- substInst g wanteds1
364 ; return (wanteds2, changed1 || changed2)
369 %************************************************************************
371 \section{Normalisation of non-equality dictionaries}
373 %************************************************************************
376 normaliseGivenDicts, normaliseWantedDicts
377 :: [Inst] -- given equations
378 -> [Inst] -- dictionaries
379 -> TcM ([Inst],TcDictBinds)
381 normaliseGivenDicts eqs dicts = normalise_dicts eqs dicts False
382 normaliseWantedDicts eqs dicts = normalise_dicts eqs dicts True
385 :: [Inst] -- given equations
386 -> [Inst] -- dictionaries
387 -> Bool -- True <=> the dicts are wanted
388 -- Fals <=> they are given
389 -> TcM ([Inst],TcDictBinds)
390 normalise_dicts given_eqs dicts is_wanted
391 = do { traceTc $ let name | is_wanted = "normaliseWantedDicts <-"
392 | otherwise = "normaliseGivenDicts <-"
394 text name <+> ppr dicts <+>
395 text "with" <+> ppr given_eqs
396 ; (dicts0, binds0) <- normaliseInsts is_wanted dicts
397 ; (dicts1, binds1) <- substEqInDictInsts is_wanted given_eqs dicts0
398 ; let binds01 = binds0 `unionBags` binds1
399 ; if isEmptyBag binds1
400 then return (dicts1, binds01)
401 else do { (dicts2, binds2) <-
402 normalise_dicts given_eqs dicts1 is_wanted
403 ; return (dicts2, binds01 `unionBags` binds2) } }
407 %************************************************************************
409 \section{Normalisation rules and iterative rule application}
411 %************************************************************************
413 We have three kinds of normalising rewrite rules:
415 (1) Normalisation rules that rewrite a set of insts and return a flag indicating
416 whether any changes occurred during rewriting that necessitate re-running
417 the current rule set.
419 (2) Precondition rules that rewrite a set of insts and return a monadic action
420 that reverts the effect of preconditioning.
422 (3) Idempotent normalisation rules that never require re-running the rule set.
425 type RewriteRule = [Inst] -> TcM ([Inst], Bool) -- rewrite, maybe re-run
426 type PrecondRule = [Inst] -> TcM ([Inst], TcM ()) -- rewrite, revertable
427 type IdemRewriteRule = [Inst] -> TcM [Inst] -- rewrite, don't re-run
429 type NamedRule = (String, RewriteRule) -- rule with description
430 type NamedPreRule = (String, PrecondRule) -- precond with desc
433 Template lifting idempotent rules to full rules (which can be put into a rule
437 dontRerun :: IdemRewriteRule -> RewriteRule
438 dontRerun rule insts = liftM addFalse $ rule insts
440 addFalse x = (x, False)
443 The following function applies a set of rewrite rules until a fixed point is
444 reached; i.e., none of the `RewriteRule's require re-running the rule set.
445 Optionally, there may be a pre-conditing rule that is applied before any other
446 rules are applied and before the rule set is re-run.
448 The result is the set of rewritten (i.e., normalised) insts and, in case of a
449 pre-conditing rule, a monadic action that reverts the effects of
450 pre-conditioning - specifically, this is removing introduced skolems.
453 rewriteToFixedPoint :: Maybe NamedPreRule -- optional preconditioning rule
454 -> [NamedRule] -- rule set
455 -> [Inst] -- insts to rewrite
456 -> TcM ([Inst], TcM ())
457 rewriteToFixedPoint precondRule rules insts
458 = completeRewrite (return ()) precondRule insts
460 completeRewrite :: TcM () -> Maybe NamedPreRule -> [Inst]
461 -> TcM ([Inst], TcM ())
462 completeRewrite dePrecond (Just (precondName, precond)) insts
463 = do { traceTc $ text precondName <+> text " <- " <+> ppr insts
464 ; (insts', dePrecond') <- precond insts
465 ; traceTc $ text precondName <+> text " -> " <+> ppr insts'
466 ; tryRules (dePrecond >> dePrecond') rules insts'
468 completeRewrite dePrecond Nothing insts
469 = tryRules dePrecond rules insts
471 tryRules dePrecond _ [] = return ([] , dePrecond)
472 tryRules dePrecond [] insts = return (insts, dePrecond)
473 tryRules dePrecond ((name, rule):rules) insts
474 = do { traceTc $ text name <+> text " <- " <+> ppr insts
475 ; (insts', rerun) <- rule insts
476 ; traceTc $ text name <+> text " -> " <+> ppr insts'
477 ; if rerun then completeRewrite dePrecond precondRule insts'
478 else tryRules dePrecond rules insts'
483 %************************************************************************
485 \section{Different forms of Inst rewrite rules}
487 %************************************************************************
489 Splitting of non-terminating given constraints: skolemOccurs
490 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
491 This is a preconditioning rule exclusively applied to given constraints.
492 Moreover, its rewriting is only temporary, as it is undone by way of
493 side-effecting mutable type variables after simplification and constraint
494 entailment has been completed.
496 This version is an (attempt at, yet unproven, an) *unflattened* version of
497 the SubstL-Ev completion rule.
499 The above rule is essential to catch non-terminating rules that cannot be
500 oriented properly, like
504 a ~ [G a] , where a is a skolem tyvar
506 The left-to-right orientiation is not suitable because it does not
507 terminate. The right-to-left orientation is not suitable because it
508 does not have a type-function on the left. This is undesirable because
509 it would hide information. E.g. assume
513 then rewriting C [G (F a)] to C (F a) is bad because we cannot now
514 see that the C [x] instance applies.
516 The rule also caters for badly-oriented rules of the form:
520 for which other solutions are possible, but this one will do too.
524 co : ty1 ~ ty2{F ty1}
527 sym (F co) : F ty2{b} ~ b
528 where b is a fresh skolem variable
530 We also cater for the symmetric situation *if* the rule cannot be used as a
531 left-to-right rewrite rule.
533 We also return an action (b := ty1) which is used to eliminate b
534 after the dust of normalisation with the completed rewrite system
537 A subtle point of this transformation is that both coercions in the results
538 are strictly speaking incorrect. However, they are correct again after the
539 action {B := ty1} has removed the skolem again. This happens immediately
540 after constraint entailment has been checked; ie, code outside of the
541 simplification and entailment checking framework will never see these
542 temporarily incorrect coercions.
544 NB: We perform this transformation for multiple occurences of ty1 under one
545 or multiple family applications on the left-hand side at once (ie, the
546 rule doesn't need to be applied multiple times at a single inst). As a
547 result we can get two or more insts back.
549 Note [skolemOccurs loop]
550 ~~~~~~~~~~~~~~~~~~~~~~~~
551 You might think that under
554 type instance F [a] = [F a]
558 foo :: (F [a] ~ a) => a
560 will get us into a loop. However, this is *not* the case. Here is why:
571 F [b<tau>] ~ b<tau> , with b := F a
576 [F b<tau>] ~ b<tau> , with b := F a
578 At this point (SkolemOccurs) does *not* apply anymore, as
582 is not used as a rewrite rule. The variable b<tau> is not a skolem (cf
585 (The regression test indexed-types/should_compile/Simple20 checks that the
586 described property of the system does not change.)
589 skolemOccurs :: PrecondRule
591 = do { (instss, undoSkolems) <- mapAndUnzipM oneSkolemOccurs insts
592 ; return (concat instss, sequence_ undoSkolems)
596 = ASSERT( isEqInst inst )
597 case eqInstToRewrite inst of
598 Just (rewrite, swapped) -> breakRecursion rewrite swapped
599 Nothing -> return ([inst], return ())
601 -- inst is an elementary rewrite rule, check whether we need to break
603 breakRecursion (Rewrite pat body _) swapped
605 -- skolemOccurs does not apply, leave as is
607 = do { traceTc $ text "oneSkolemOccurs: no tys to lift out"
608 ; return ([inst], return ())
611 -- recursive occurence of pat in body under a type family application
613 = do { traceTc $ text "oneSkolemOccurs[TLO]:" <+> ppr tysToLiftOut
614 ; skTvs <- mapM (newMetaTyVar TauTv . typeKind) tysToLiftOut
615 ; let skTvs_tysTLO = zip skTvs tysToLiftOut
616 insertSkolems = return . replace skTvs_tysTLO
617 ; (_, body') <- tcGenericNormaliseFamInst insertSkolems body
618 ; inst' <- if swapped then mkEqInst (EqPred body' pat) co
619 else mkEqInst (EqPred pat body') co
620 -- ensure to reconstruct the inst in the
621 -- original orientation
622 ; traceTc $ text "oneSkolemOccurs[inst']:" <+> ppr inst'
623 ; (insts, undoSk) <- mapAndUnzipM (mkSkolemInst inst')
625 ; return (inst':insts, sequence_ undoSk)
628 co = eqInstCoercion inst
630 -- all subtypes that are (1) type family instances and (2) contain
631 -- the lhs type as part of the type arguments of the type family
633 tysToLiftOut = [mkTyConApp tc tys | (tc, tys) <- tyFamInsts body
634 , any (pat `tcPartOfType`) tys]
636 replace :: [(TcTyVar, Type)] -> Type -> Maybe (Type, Coercion)
637 replace [] _ = Nothing
638 replace ((skTv, tyTLO):rest) ty
639 | tyTLO `tcEqType` ty = Just (mkTyVarTy skTv, undefined)
640 | otherwise = replace rest ty
642 -- create the EqInst for the equality determining the skolem and a
643 -- TcM action undoing the skolem introduction
644 mkSkolemInst inst' (skTv, tyTLO)
645 = do { (co, tyLiftedOut) <- tcEqInstNormaliseFamInst inst' tyTLO
646 ; inst <- mkEqInst (EqPred tyLiftedOut (mkTyVarTy skTv))
647 (mkGivenCo $ mkSymCoercion (fromACo co))
648 -- co /= IdCo due to construction of inst'
649 ; return (inst, writeMetaTyVar skTv tyTLO)
654 Removal of trivial equalities: trivialRule
655 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
656 The following rules exploits the reflexivity of equality:
664 trivialRule :: IdemRewriteRule
666 = liftM catMaybes $ mapM trivial insts
669 | ASSERT( isEqInst inst )
671 = do { eitherEqInst inst
672 (\cotv -> writeMetaTyVar cotv ty1)
679 (ty1,ty2) = eqInstTys inst
683 Decomposition of data type constructors: decompRule
684 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
685 Whenever, the same *data* constructors occurs on both sides of an equality, we
686 can decompose as in standard unification.
691 g21 : c1 ~ d1, ..., g2n : cn ~ dn
694 Works also for the case where T is actually an application of a type family
695 constructor to a set of types, provided the applications on both sides of the
696 ~ are identical; see also Note [OpenSynTyCon app] in TcUnify.
698 We guarantee to raise an error for any inconsistent equalities;
699 cf Note [Inconsistencies in equality constraints].
702 decompRule :: RewriteRule
704 = do { (insts, changed) <- mapAndUnzipM decomp insts
705 ; return (concat insts, or changed)
709 = ASSERT( isEqInst inst )
712 (ty1,ty2) = eqInstTys inst
714 | Just ty1' <- tcView ty1 = go ty1' ty2
715 | Just ty2' <- tcView ty2 = go ty1 ty2'
717 go (TyConApp con1 tys1) (TyConApp con2 tys2)
718 | con1 == con2 && identicalHead
719 = mkArgInsts (mkTyConApp con1) tys1 tys2
721 | con1 /= con2 && not (isOpenSynTyCon con1 || isOpenSynTyCon con2)
722 -- not matching data constructors (of any flavour) are bad news
723 = eqInstMisMatch inst
726 (idxTys1, _) = splitAt n tys1
727 (idxTys2, _) = splitAt n tys2
728 identicalHead = not (isOpenSynTyCon con1) ||
729 idxTys1 `tcEqTypes` idxTys2
731 go (FunTy fun1 arg1) (FunTy fun2 arg2)
732 = mkArgInsts (\[funCo, argCo] -> mkFunTy funCo argCo) [fun1, arg1]
735 -- Applications need a bit of care!
736 -- They can match FunTy and TyConApp, so use splitAppTy_maybe
738 | Just (s2, t2) <- tcSplitAppTy_maybe ty2
739 = mkArgInsts (\[s, t] -> mkAppTy s t) [s1, t1] [s2, t2]
743 | Just (s1, t1) <- tcSplitAppTy_maybe ty1
744 = mkArgInsts (\[s, t] -> mkAppTy s t) [s1, t1] [s2, t2]
746 -- We already covered all the consistent cases of rigid types on both
747 -- sides; so, if we see two rigid types here, we discovered an
750 | isRigid ty1 && isRigid ty2
751 = eqInstMisMatch inst
753 -- We can neither assert consistency nor inconsistency => defer
754 go _ _ = return ([inst], False)
756 isRigid (TyConApp con _) = not (isOpenSynTyCon con)
757 isRigid (FunTy _ _) = True
758 isRigid (AppTy _ _) = True
761 -- Create insts for matching argument positions (ie, the bit after
762 -- '>-->' in the rule description above)
763 mkArgInsts con tys1 tys2
764 = do { cos <- eitherEqInst inst
765 -- old_co := Con1 cos
767 do { cotvs <- zipWithM newMetaCoVar tys1 tys2
768 ; let cos = map mkTyVarTy cotvs
769 ; writeMetaTyVar old_covar (con cos)
770 ; return $ map mkWantedCo cotvs
772 -- co_i := Con_i old_co
774 return $ map mkGivenCo $
775 mkRightCoercions (length tys1) old_co)
776 ; insts <- zipWithM mkEqInst (zipWith EqPred tys1 tys2) cos
777 ; traceTc (text "decomp identicalHead" <+> ppr insts)
778 ; return (insts, not $ null insts)
783 Rewriting with type instances: topRule
784 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
785 We use (toplevel) type instances to normalise both sides of equalities.
789 >--> co1 :: t ~ t' / co2 :: s ~ s'
791 g1 := co1 * g2 * sym co2
794 topRule :: RewriteRule
796 = do { (insts, changed) <- mapAndUnzipM top insts
797 ; return (insts, or changed)
801 = ASSERT( isEqInst inst )
802 do { (coi1, ty1') <- tcNormaliseFamInst ty1
803 ; (coi2, ty2') <- tcNormaliseFamInst ty2
804 ; case (coi1, coi2) of
805 (IdCo, IdCo) -> return (inst, False)
809 -- old_co = co1 * new_co * sym co2
811 do { new_cotv <- newMetaCoVar ty1' ty2'
812 ; let new_co = mkTyVarTy new_cotv
813 old_coi = coi1 `mkTransCoI`
814 ACo new_co `mkTransCoI`
816 ; writeMetaTyVar old_covar (fromACo old_coi)
817 ; return $ mkWantedCo new_cotv
819 -- new_co = sym co1 * old_co * co2
824 mkSymCoI coi1 `mkTransCoI`
825 ACo old_co `mkTransCoI` coi2)
826 ; new_inst <- mkEqInst (EqPred ty1' ty2') wg_co
827 ; return (new_inst, True)
831 (ty1,ty2) = eqInstTys inst
835 Rewriting with equalities: substRule
836 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
837 From a set of insts, use all insts that can be read as rewrite rules to
838 rewrite the types in all other insts.
842 forall g1 : s1{F c} ~ s2{F c}
845 g1 := s1{g} * g2 * sym s2{g} <=> g2 := sym s1{g} * g1 * s2{g}
847 Alternatively, the rewrite rule may have the form (g : a ~ t).
849 To avoid having to swap rules of the form (g : t ~ F c) and (g : t ~ a),
850 where t is neither a variable nor a type family application, we use them for
851 rewriting from right-to-left. However, it is crucial to only apply rules
852 from right-to-left if they cannot be used left-to-right.
854 The workhorse is substInst, which performs an occurs check before actually
855 using an equality for rewriting. If the type pattern occurs in the type we
856 substitute for the pattern, normalisation would diverge.
859 substRule :: RewriteRule
860 substRule insts = tryAllInsts insts []
862 -- for every inst check whether it can be used to rewrite the others
863 -- (we make an effort to keep the insts in order; it makes debugging
865 tryAllInsts [] triedInsts = return (reverse triedInsts, False)
866 tryAllInsts (inst:insts) triedInsts
867 = do { (insts', changed) <- substInst inst (reverse triedInsts ++ insts)
868 ; if changed then return (insertAt (length triedInsts) inst insts',
870 else tryAllInsts insts (inst:triedInsts)
873 insertAt n x xs = let (xs1, xs2) = splitAt n xs
876 -- Use the given inst as a rewrite rule to normalise the insts in the second
877 -- argument. Don't do anything if the inst cannot be used as a rewrite rule,
878 -- but do apply it right-to-left, if possible, and if it cannot be used
881 substInst :: Inst -> [Inst] -> TcM ([Inst], Bool)
883 = case eqInstToRewrite inst of
884 Just (rewrite, _) -> substEquality rewrite insts
885 Nothing -> return (insts, False)
887 substEquality :: Rewrite -- elementary rewrite
888 -> [Inst] -- insts to rewrite
889 -> TcM ([Inst], Bool)
890 substEquality eqRule@(Rewrite pat rhs _) insts
891 | pat `tcPartOfType` rhs -- occurs check!
892 = occurCheckErr pat rhs
894 = do { (insts', changed) <- mapAndUnzipM substOne insts
895 ; return (insts', or changed)
899 = ASSERT( isEqInst inst )
900 do { (coi1, ty1') <- tcEqRuleNormaliseFamInst eqRule ty1
901 ; (coi2, ty2') <- tcEqRuleNormaliseFamInst eqRule ty2
902 ; case (coi1, coi2) of
903 (IdCo, IdCo) -> return (inst, False)
907 -- old_co := co1 * new_co * sym co2
909 do { new_cotv <- newMetaCoVar ty1' ty2'
910 ; let new_co = mkTyVarTy new_cotv
911 old_coi = coi1 `mkTransCoI`
912 ACo new_co `mkTransCoI`
914 ; writeMetaTyVar old_covar (fromACo old_coi)
915 ; return $ mkWantedCo new_cotv
917 -- new_co := sym co1 * old_co * co2
922 mkSymCoI coi1 `mkTransCoI`
923 ACo old_co `mkTransCoI` coi2)
924 ; new_inst <- mkEqInst (EqPred ty1' ty2') gw_co
925 ; return (new_inst, True)
929 (ty1,ty2) = eqInstTys inst
933 Instantiate meta variables: unifyMetaRule
934 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
935 If an equality equates a meta type variable with a type, we simply instantiate
944 Meta variables can only appear in wanted constraints, and this rule should
945 only be applied to wanted constraints. We also know that t definitely is
946 distinct from alpha (as the trivialRule) has been run on the insts beforehand.
948 NB: We cannot assume that meta tyvars are empty. They may have been updated
949 by another inst in the currently processed wanted list. We need to be very
950 careful when updateing type variables (see TcUnify.uUnfilledVar), but at least
951 we know that we have no boxes. It's unclear that it would be an advantage to
952 common up the code in TcUnify and the code below. Firstly, we don't want
953 calls to TcUnify.defer_unification here, and secondly, TcUnify import the
954 current module, so we would have to move everything here (Yuk!) or to
955 TcMType. Besides, the code here is much simpler due to the lack of boxes.
958 unifyMetaRule :: RewriteRule
960 = do { (insts', changed) <- mapAndUnzipM unifyMeta insts
961 ; return (concat insts', or changed)
965 = ASSERT( isEqInst inst )
967 (fromWantedCo "unifyMetaRule" $ eqInstCoercion inst)
969 (ty1,ty2) = eqInstTys inst
971 | Just ty1' <- tcView ty1 = go ty1' ty2 cotv
972 | Just ty2' <- tcView ty2 = go ty1 ty2' cotv
975 , isMetaTyVar tv1 = do { lookupTV <- lookupTcTyVar tv1
976 ; uMeta False tv1 lookupTV ty2 cotv
979 , isMetaTyVar tv2 = do { lookupTV <- lookupTcTyVar tv2
980 ; uMeta True tv2 lookupTV ty1 cotv
982 | otherwise = return ([inst], False)
984 -- meta variable has been filled already
985 -- => ignore this inst (we'll come around again, after zonking)
986 uMeta _swapped _tv (IndirectTv _) _ty _cotv
987 = return ([inst], False)
989 -- signature skolem meets non-variable type
991 uMeta _swapped _tv (DoneTv (MetaTv (SigTv _) _)) ty _cotv
993 = return ([inst], False)
995 -- type variable meets type variable
996 -- => check that tv2 hasn't been updated yet and choose which to update
997 uMeta swapped tv1 (DoneTv details1) (TyVarTy tv2) cotv
998 = do { lookupTV2 <- lookupTcTyVar tv2
1000 IndirectTv ty -> uMeta swapped tv1 (DoneTv details1) ty cotv
1002 uMetaVar swapped tv1 details1 tv2 details2 cotv
1005 -- updatable meta variable meets non-variable type
1006 -- => occurs check, monotype check, and kinds match check, then update
1007 uMeta swapped tv (DoneTv (MetaTv _ ref)) ty cotv
1008 = do { mb_ty' <- checkTauTvUpdate tv ty -- occurs + monotype check
1010 Nothing -> return ([inst], False) -- tv occurs in faminst
1012 do { checkUpdateMeta swapped tv ref ty' -- update meta var
1013 ; writeMetaTyVar cotv ty' -- update co var
1018 uMeta _ _ _ _ _ = panic "uMeta"
1020 -- meta variable meets skolem
1022 uMetaVar swapped tv1 (MetaTv _ ref) tv2 (SkolemTv _) cotv
1023 = do { checkUpdateMeta swapped tv1 ref (mkTyVarTy tv2)
1024 ; writeMetaTyVar cotv (mkTyVarTy tv2)
1028 -- meta variable meets meta variable
1029 -- => be clever about which of the two to update
1030 -- (from TcUnify.uUnfilledVars minus boxy stuff)
1031 uMetaVar swapped tv1 (MetaTv info1 ref1) tv2 (MetaTv info2 ref2) cotv
1032 = do { case (info1, info2) of
1033 -- Avoid SigTvs if poss
1034 (SigTv _, _ ) | k1_sub_k2 -> update_tv2
1035 (_, SigTv _) | k2_sub_k1 -> update_tv1
1037 (_, _) | k1_sub_k2 -> if k2_sub_k1 && nicer_to_update_tv1
1038 then update_tv1 -- Same kinds
1040 | k2_sub_k1 -> update_tv1
1041 | otherwise -> kind_err
1042 -- Update the variable with least kind info
1043 -- See notes on type inference in Kind.lhs
1044 -- The "nicer to" part only applies if the two kinds are the same,
1045 -- so we can choose which to do.
1047 ; writeMetaTyVar cotv (mkTyVarTy tv2)
1051 -- Kinds should be guaranteed ok at this point
1052 update_tv1 = updateMeta tv1 ref1 (mkTyVarTy tv2)
1053 update_tv2 = updateMeta tv2 ref2 (mkTyVarTy tv1)
1055 kind_err = addErrCtxtM (unifyKindCtxt swapped tv1 (mkTyVarTy tv2)) $
1056 unifyKindMisMatch k1 k2
1060 k1_sub_k2 = k1 `isSubKind` k2
1061 k2_sub_k1 = k2 `isSubKind` k1
1063 nicer_to_update_tv1 = isSystemName (Var.varName tv1)
1064 -- Try to update sys-y type variables in preference to ones
1065 -- gotten (say) by instantiating a polymorphic function with
1066 -- a user-written type sig
1068 uMetaVar _ _ _ _ _ _ = panic "uMetaVar"
1072 %************************************************************************
1074 \section{Normalisation of Insts}
1076 %************************************************************************
1078 Normalises a set of dictionaries relative to a set of given equalities (which
1079 are interpreted as rewrite rules). We only consider given equalities of the
1084 where F is a type family.
1087 substEqInDictInsts :: Bool -- whether the *dictionaries* are wanted/given
1088 -> [Inst] -- given equalities (used as rewrite rules)
1089 -> [Inst] -- dictinaries to be normalised
1090 -> TcM ([Inst], TcDictBinds)
1091 substEqInDictInsts isWanted eqInsts dictInsts
1092 = do { traceTc (text "substEqInDictInst <-" <+> ppr dictInsts)
1094 foldlM rewriteWithOneEquality (dictInsts, emptyBag) eqInsts
1095 ; traceTc (text "substEqInDictInst ->" <+> ppr dictInsts')
1099 -- (1) Given equality of form 'F ts ~ t' or 'a ~ t': use for rewriting
1100 rewriteWithOneEquality (dictInsts, dictBinds)
1101 eqInst@(EqInst {tci_left = pattern,
1102 tci_right = target})
1103 | isOpenSynTyConApp pattern || isTyVarTy pattern
1104 = do { (dictInsts', moreDictBinds) <-
1105 genericNormaliseInsts isWanted applyThisEq dictInsts
1106 ; return (dictInsts', dictBinds `unionBags` moreDictBinds)
1109 applyThisEq = tcGenericNormaliseFamInstPred (return . matchResult)
1111 -- rewrite in case of an exact match
1112 matchResult ty | tcEqType pattern ty = Just (target, eqInstType eqInst)
1113 | otherwise = Nothing
1115 -- (2) Given equality has the wrong form: ignore
1116 rewriteWithOneEquality (dictInsts, dictBinds) _not_a_rewrite_rule
1117 = return (dictInsts, dictBinds)
1121 Take a bunch of Insts (not EqInsts), and normalise them wrt the top-level
1122 type-function equations, where
1124 (norm_insts, binds) = normaliseInsts is_wanted insts
1127 = True, (binds + norm_insts) defines insts (wanteds)
1128 = False, (binds + insts) defines norm_insts (givens)
1130 Ie, in the case of normalising wanted dictionaries, we use the normalised
1131 dictionaries to define the originally wanted ones. However, in the case of
1132 given dictionaries, we use the originally given ones to define the normalised
1136 normaliseInsts :: Bool -- True <=> wanted insts
1137 -> [Inst] -- wanted or given insts
1138 -> TcM ([Inst], TcDictBinds) -- normalised insts and bindings
1139 normaliseInsts isWanted insts
1140 = genericNormaliseInsts isWanted tcNormaliseFamInstPred insts
1142 genericNormaliseInsts :: Bool -- True <=> wanted insts
1143 -> (TcPredType -> TcM (CoercionI, TcPredType))
1145 -> [Inst] -- wanted or given insts
1146 -> TcM ([Inst], TcDictBinds) -- normalised insts & binds
1147 genericNormaliseInsts isWanted fun insts
1148 = do { (insts', binds) <- mapAndUnzipM (normaliseOneInst isWanted fun) insts
1149 ; return (insts', unionManyBags binds)
1152 normaliseOneInst isWanted fun
1153 dict@(Dict {tci_pred = pred,
1155 = do { traceTc $ text "genericNormaliseInst <-" <+> ppr dict
1156 ; (coi, pred') <- fun pred
1160 do { traceTc $ text "genericNormaliseInst ->" <+> ppr dict
1161 ; return (dict, emptyBag)
1163 -- don't use pred' in this case; otherwise, we get
1164 -- more unfolded closed type synonyms in error messages
1166 do { -- an inst for the new pred
1167 ; dict' <- newDictBndr loc pred'
1168 -- relate the old inst to the new one
1169 -- target_dict = source_dict `cast` st_co
1170 ; let (target_dict, source_dict, st_co)
1171 | isWanted = (dict, dict', mkSymCoercion co)
1172 | otherwise = (dict', dict, co)
1174 -- co :: dict ~ dict'
1175 -- hence, if isWanted
1176 -- dict = dict' `cast` sym co
1178 -- dict' = dict `cast` co
1179 expr = HsVar $ instToId source_dict
1180 cast_expr = HsWrap (WpCo st_co) expr
1181 rhs = L (instLocSpan loc) cast_expr
1182 binds = instToDictBind target_dict rhs
1183 -- return the new inst
1184 ; traceTc $ let name | isWanted
1185 = "genericNormaliseInst (wanted) ->"
1187 = "genericNormaliseInst (given) ->"
1189 text name <+> ppr dict' <+>
1190 text "with" <+> ppr binds
1191 ; return (dict', binds)
1195 -- TOMDO: What do we have to do about ImplicInst, Method, and LitInst??
1196 normaliseOneInst _isWanted _fun inst
1197 = do { inst' <- zonkInst inst
1198 ; traceTc $ text "*** TcTyFuns.normaliseOneInst: Skipping" <+>
1200 ; return (inst', emptyBag)
1205 %************************************************************************
1209 %************************************************************************
1211 The infamous couldn't match expected type soandso against inferred type
1212 somethingdifferent message.
1215 eqInstMisMatch :: Inst -> TcM a
1217 = ASSERT( isEqInst inst )
1218 setErrCtxt ctxt $ failWithMisMatch ty_act ty_exp
1220 (ty_act, ty_exp) = eqInstTys inst
1221 InstLoc _ _ ctxt = instLoc inst
1223 -----------------------
1224 failWithMisMatch :: TcType -> TcType -> TcM a
1225 -- Generate the message when two types fail to match,
1226 -- going to some trouble to make it helpful.
1227 -- The argument order is: actual type, expected type
1228 failWithMisMatch ty_act ty_exp
1229 = do { env0 <- tcInitTidyEnv
1230 ; ty_exp <- zonkTcType ty_exp
1231 ; ty_act <- zonkTcType ty_act
1232 ; failWithTcM (misMatchMsg env0 (ty_act, ty_exp))
1235 misMatchMsg :: TidyEnv -> (TcType, TcType) -> (TidyEnv, SDoc)
1236 misMatchMsg env0 (ty_act, ty_exp)
1237 = let (env1, pp_exp, extra_exp) = ppr_ty env0 ty_exp
1238 (env2, pp_act, extra_act) = ppr_ty env1 ty_act
1239 msg = sep [sep [ptext SLIT("Couldn't match expected type") <+> pp_exp,
1241 ptext SLIT("against inferred type") <+> pp_act],
1242 nest 2 (extra_exp $$ extra_act)]
1247 ppr_ty :: TidyEnv -> TcType -> (TidyEnv, SDoc, SDoc)
1249 = let (env1, tidy_ty) = tidyOpenType env ty
1250 (env2, extra) = ppr_extra env1 tidy_ty
1252 (env2, quotes (ppr tidy_ty), extra)
1254 -- (ppr_extra env ty) shows extra info about 'ty'
1255 ppr_extra :: TidyEnv -> Type -> (TidyEnv, SDoc)
1256 ppr_extra env (TyVarTy tv)
1257 | isTcTyVar tv && (isSkolemTyVar tv || isSigTyVar tv) && not (isUnk tv)
1258 = (env1, pprSkolTvBinding tv1)
1260 (env1, tv1) = tidySkolemTyVar env tv
1262 ppr_extra env _ty = (env, empty) -- Normal case