6 normaliseGivens, normaliseGivenDicts,
7 normaliseWanteds, normaliseWantedDicts,
11 addBind -- should not be here
15 #include "HsVersions.h"
25 import TypeRep ( Type(..) )
27 import Var ( isTcTyVar )
31 import SrcLoc ( Located(..) )
35 import Control.Monad (liftM)
39 %************************************************************************
41 Normalisation of types
43 %************************************************************************
45 Unfold a single synonym family instance and yield the witnessing coercion.
46 Return 'Nothing' if the given type is either not synonym family instance
47 or is a synonym family instance that has no matching instance declaration.
48 (Applies only if the type family application is outermost.)
50 For example, if we have
52 :Co:R42T a :: T [a] ~ :R42T a
54 then 'T [Int]' unfolds to (:R42T Int, :Co:R42T Int).
57 tcUnfoldSynFamInst :: Type -> TcM (Maybe (Type, Coercion))
58 tcUnfoldSynFamInst (TyConApp tycon tys)
59 | not (isOpenSynTyCon tycon) -- unfold *only* _synonym_ family instances
62 = do { -- we only use the indexing arguments for matching,
63 -- not the additional ones
64 ; maybeFamInst <- tcLookupFamInst tycon idxTys
65 ; case maybeFamInst of
66 Nothing -> return Nothing
67 Just (rep_tc, rep_tys) -> return $ Just (mkTyConApp rep_tc tys',
68 mkTyConApp coe_tc tys')
70 tys' = rep_tys ++ restTys
71 coe_tc = expectJust "TcTyFun.tcUnfoldSynFamInst"
72 (tyConFamilyCoercion_maybe rep_tc)
76 (idxTys, restTys) = splitAt n tys
77 tcUnfoldSynFamInst _other = return Nothing
80 Normalise 'Type's and 'PredType's by unfolding type family applications where
81 possible (ie, we treat family instances as a TRS). Also zonk meta variables.
83 tcNormalizeFamInst ty = (co, ty')
87 tcNormalizeFamInst :: TcType -> TcM (CoercionI, TcType)
88 tcNormalizeFamInst = tcGenericNormalizeFamInst tcUnfoldSynFamInst
90 tcNormalizeFamInstPred :: TcPredType -> TcM (CoercionI, TcPredType)
91 tcNormalizeFamInstPred = tcGenericNormalizeFamInstPred tcUnfoldSynFamInst
94 Normalise a type relative to the rewrite rule implied by one EqInst.
97 tcEqInstNormalizeFamInst :: Inst -> TcType -> TcM (CoercionI, Type)
98 tcEqInstNormalizeFamInst inst = ASSERT( isEqInst inst )
99 tcGenericNormalizeFamInst matchInst
101 pat = eqInstLeftTy inst
102 rhs = eqInstRightTy inst
103 co = eitherEqInst inst TyVarTy id
105 matchInst ty | pat `tcEqType` ty = return $ Just (rhs, co)
106 | otherwise = return $ Nothing
109 Generic normalisation of 'Type's and 'PredType's; ie, walk the type term and
110 apply the normalisation function gives as the first argument to every TyConApp
111 and every TyVarTy subterm.
113 tcGenericNormalizeFamInst fun ty = (co, ty')
116 This function is (by way of using smart constructors) careful to ensure that
117 the returned coercion is exactly IdCo (and not some semantically equivalent,
118 but syntactically different coercion) whenever (ty' `tcEqType` ty). This
119 makes it easy for the caller to determine whether the type changed. BUT
120 even if we return IdCo, ty' may be *syntactically* different from ty due to
121 unfolded closed type synonyms (by way of tcCoreView). In the interest of
122 good error messages, callers should discard ty' in favour of ty in this case.
125 tcGenericNormalizeFamInst :: (TcType -> TcM (Maybe (TcType, Coercion)))
126 -- what to do with type functions and tyvars
127 -> TcType -- old type
128 -> TcM (CoercionI, TcType) -- (coercion, new type)
129 tcGenericNormalizeFamInst fun ty
130 | Just ty' <- tcView ty = tcGenericNormalizeFamInst fun ty'
131 tcGenericNormalizeFamInst fun (TyConApp tyCon tys)
132 = do { (cois, ntys) <- mapAndUnzipM (tcGenericNormalizeFamInst fun) tys
133 ; let tycon_coi = mkTyConAppCoI tyCon ntys cois
134 ; maybe_ty_co <- fun (TyConApp tyCon ntys) -- use normalised args!
135 ; case maybe_ty_co of
136 -- a matching family instance exists
138 do { let first_coi = mkTransCoI tycon_coi (ACo co)
139 ; (rest_coi, nty) <- tcGenericNormalizeFamInst fun ty'
140 ; let fix_coi = mkTransCoI first_coi rest_coi
141 ; return (fix_coi, nty)
143 -- no matching family instance exists
144 -- we do not do anything
145 Nothing -> return (tycon_coi, TyConApp tyCon ntys)
147 tcGenericNormalizeFamInst fun (AppTy ty1 ty2)
148 = do { (coi1,nty1) <- tcGenericNormalizeFamInst fun ty1
149 ; (coi2,nty2) <- tcGenericNormalizeFamInst fun ty2
150 ; return (mkAppTyCoI nty1 coi1 nty2 coi2, AppTy nty1 nty2)
152 tcGenericNormalizeFamInst fun (FunTy ty1 ty2)
153 = do { (coi1,nty1) <- tcGenericNormalizeFamInst fun ty1
154 ; (coi2,nty2) <- tcGenericNormalizeFamInst fun ty2
155 ; return (mkFunTyCoI nty1 coi1 nty2 coi2, FunTy nty1 nty2)
157 tcGenericNormalizeFamInst fun (ForAllTy tyvar ty1)
158 = do { (coi,nty1) <- tcGenericNormalizeFamInst fun ty1
159 ; return (mkForAllTyCoI tyvar coi,ForAllTy tyvar nty1)
161 tcGenericNormalizeFamInst fun (NoteTy note ty1)
162 = do { (coi,nty1) <- tcGenericNormalizeFamInst fun ty1
163 ; return (mkNoteTyCoI note coi,NoteTy note nty1)
165 tcGenericNormalizeFamInst fun ty@(TyVarTy tv)
167 = do { traceTc (text "tcGenericNormalizeFamInst" <+> ppr ty)
168 ; res <- lookupTcTyVar tv
171 do { maybe_ty' <- fun ty
173 Nothing -> return (IdCo, ty)
175 do { (coi2, ty'') <- tcGenericNormalizeFamInst fun ty'
176 ; return (ACo co1 `mkTransCoI` coi2, ty'')
179 IndirectTv ty' -> tcGenericNormalizeFamInst fun ty'
183 tcGenericNormalizeFamInst fun (PredTy predty)
184 = do { (coi, pred') <- tcGenericNormalizeFamInstPred fun predty
185 ; return (coi, PredTy pred') }
187 ---------------------------------
188 tcGenericNormalizeFamInstPred :: (TcType -> TcM (Maybe (TcType,Coercion)))
190 -> TcM (CoercionI, TcPredType)
192 tcGenericNormalizeFamInstPred fun (ClassP cls tys)
193 = do { (cois, tys')<- mapAndUnzipM (tcGenericNormalizeFamInst fun) tys
194 ; return (mkClassPPredCoI cls tys' cois, ClassP cls tys')
196 tcGenericNormalizeFamInstPred fun (IParam ipn ty)
197 = do { (coi, ty') <- tcGenericNormalizeFamInst fun ty
198 ; return $ (mkIParamPredCoI ipn coi, IParam ipn ty')
200 tcGenericNormalizeFamInstPred fun (EqPred ty1 ty2)
201 = do { (coi1, ty1') <- tcGenericNormalizeFamInst fun ty1
202 ; (coi2, ty2') <- tcGenericNormalizeFamInst fun ty2
203 ; return (mkEqPredCoI ty1' coi1 ty2' coi2, EqPred ty1' ty2') }
207 %************************************************************************
209 \section{Normalisation of Given Dictionaries}
211 %************************************************************************
214 normaliseGivenDicts, normaliseWantedDicts
215 :: [Inst] -- given equations
216 -> [Inst] -- dictionaries
217 -> TcM ([Inst],TcDictBinds)
219 normaliseGivenDicts eqs dicts = normalise_dicts eqs dicts False
220 normaliseWantedDicts eqs dicts = normalise_dicts eqs dicts True
223 :: [Inst] -- given equations
224 -> [Inst] -- dictionaries
225 -> Bool -- True <=> the dicts are wanted
226 -- Fals <=> they are given
227 -> TcM ([Inst],TcDictBinds)
228 normalise_dicts given_eqs dicts is_wanted
229 = do { traceTc $ text "normaliseGivenDicts <-" <+> ppr dicts <+>
230 text "with" <+> ppr given_eqs
231 ; (dicts0, binds0) <- normaliseInsts is_wanted dicts
232 ; (dicts1, binds1) <- substEqInDictInsts given_eqs dicts0
233 ; let binds01 = binds0 `unionBags` binds1
234 ; if isEmptyBag binds1
235 then return (dicts1, binds01)
236 else do { (dicts2, binds2) <- normaliseGivenDicts given_eqs dicts1
237 ; return (dicts2, binds01 `unionBags` binds2) } }
241 %************************************************************************
243 \section{Normalisation of wanteds constraints}
245 %************************************************************************
248 normaliseWanteds :: [Inst] -> TcM [Inst]
249 normaliseWanteds insts
250 = do { traceTc (text "normaliseWanteds <-" <+> ppr insts)
251 ; result <- liftM fst $ rewriteToFixedPoint Nothing
252 [ ("(Occurs)", noChange $ occursCheckInsts)
253 , ("(ZONK)", dontRerun $ zonkInsts)
254 , ("(TRIVIAL)", trivialInsts)
255 -- no `swapInsts'; it messes up error messages and should
256 -- not be necessary -=chak
257 , ("(DECOMP)", decompInsts)
258 , ("(TOP)", topInsts)
259 , ("(SUBST)", substInsts)
260 , ("(UNIFY)", unifyInsts)
262 ; traceTc (text "normaliseWanteds ->" <+> ppr result)
268 %************************************************************************
270 \section{Normalisation of givens constraints}
272 %************************************************************************
275 normaliseGivens :: [Inst] -> TcM ([Inst], TcM ())
276 normaliseGivens givens
277 = do { traceTc (text "normaliseGivens <-" <+> ppr givens)
278 ; (result, deSkolem) <-
279 rewriteToFixedPoint (Just ("(SkolemOccurs)", skolemOccurs))
280 [ ("(Occurs)", noChange $ occursCheckInsts)
281 , ("(ZONK)", dontRerun $ zonkInsts)
282 , ("(TRIVIAL)", trivialInsts)
283 , ("(SWAP)", swapInsts)
284 , ("(DECOMP)", decompInsts)
285 , ("(TOP)", topInsts)
286 , ("(SUBST)", substInsts)
288 ; traceTc (text "normaliseGivens ->" <+> ppr result)
289 ; return (result, deSkolem)
294 This is an (attempt at, yet unproven, an) *unflattened* version of
295 the SubstL-Ev completion rule.
297 The above rule is essential to catch non-terminating
298 rules that cannot be oriented properly, like
304 The left-to-right orientiation is not suitable because it does not
306 The right-to-left orientation is not suitable because it
307 does not have a type-function on the left. This is undesirable because
308 it would hide information. E.g. assume
310 then rewriting C [G (F a)] to C (F a) is bad because we cannot now
311 see that the C [x] instance applies.
313 The rule also caters for badly-oriented rules of the form:
315 for which other solutions are possible, but this one will do too.
318 co : ty1 ~ ty2{F ty1}
321 sym (F co) : F ty2{b} ~ b
322 where b is a fresh skolem variable
324 We also return an action (b := ty1) which is used to eliminate b
325 after the dust of normalisation with the completed rewrite system
328 A subtle point of this transformation is that both coercions in the results
329 are strictly speaking incorrect. However, they are correct again after the
330 action {B := ty1} has removed the skolem again. This happens immediately
331 after constraint entailment has been checked; ie, code outside of the
332 simplification and entailment checking framework will never see these
333 temporarily incorrect coercions.
335 NB: We perform this transformation for multiple occurences of ty1 under one
336 or multiple family applications on the left-hand side at once (ie, the
337 rule doesn't need to be applied multiple times at a single inst). As a
338 result we can get two or more insts back.
341 skolemOccurs :: PrecondRule
343 = do { (instss, undoSkolems) <- mapAndUnzipM oneSkolemOccurs insts
344 ; return (concat instss, sequence_ undoSkolems)
349 = return ([inst], return ())
351 = do { skTvs <- mapM (newMetaTyVar TauTv . typeKind) tysToLiftOut
352 ; let skTvs_tysTLO = zip skTvs tysToLiftOut
353 insertSkolems = return . replace skTvs_tysTLO
354 ; (_, ty2') <- tcGenericNormalizeFamInst insertSkolems ty2
355 ; inst' <- mkEqInst (EqPred ty1 ty2') co
356 ; (insts, undoSk) <- mapAndUnzipM (mkSkolemInst inst') skTvs_tysTLO
357 ; return (inst':insts, sequence_ undoSk)
360 ty1 = eqInstLeftTy inst
361 ty2 = eqInstRightTy inst
362 co = eqInstCoercion inst
364 -- all subtypes that are (1) type family instances and (2) contain the
365 -- lhs type as part of the type arguments of the type family constructor
366 tysToLiftOut = ASSERT( isEqInst inst )
367 [mkTyConApp tc tys | (tc, tys) <- tyFamInsts ty2
368 , any (ty1 `tcPartOfType`) tys]
370 replace :: [(TcTyVar, Type)] -> Type -> Maybe (Type, Coercion)
371 replace [] _ = Nothing
372 replace ((skTv, tyTLO):rest) ty
373 | tyTLO `tcEqType` ty = Just (mkTyVarTy skTv, undefined)
374 | otherwise = replace rest ty
376 -- create the EqInst for the equality determining the skolem and a
377 -- TcM action undoing the skolem introduction
378 mkSkolemInst inst' (skTv, tyTLO)
379 = do { (co, tyLiftedOut) <- tcEqInstNormalizeFamInst inst' tyTLO
380 ; inst <- mkEqInst (EqPred tyLiftedOut (mkTyVarTy skTv))
381 (mkGivenCo $ mkSymCoercion (fromACo co))
382 ; return (inst, writeMetaTyVar skTv tyTLO)
387 %************************************************************************
389 \section{Solving of wanted constraints with respect to a given set}
391 %************************************************************************
394 solveWanteds :: [Inst] -- givens
396 -> TcM [Inst] -- irreducible wanteds
397 solveWanteds givens wanteds
398 = do { traceTc $ text "solveWanteds <-" <+> ppr wanteds <+> text "with" <+>
400 ; result <- liftM fst $ rewriteToFixedPoint Nothing
401 [ ("(Occurs)", noChange $ occursCheckInsts)
402 , ("(TRIVIAL)", trivialInsts)
403 , ("(DECOMP)", decompInsts)
404 , ("(TOP)", topInsts)
405 , ("(GIVEN)", givenInsts givens)
406 , ("(UNIFY)", unifyInsts)
408 ; traceTc (text "solveWanteds ->" <+> ppr result)
412 -- Use `substInst' with every given on all the wanteds.
413 givenInsts :: [Inst] -> [Inst] -> TcM ([Inst],Bool)
414 givenInsts [] wanteds = return (wanteds,False)
415 givenInsts (g:gs) wanteds
416 = do { (wanteds1, changed1) <- givenInsts gs wanteds
417 ; (wanteds2, changed2) <- substInst g wanteds1
418 ; return (wanteds2, changed1 || changed2)
423 %************************************************************************
425 \section{Normalisation rules and iterative rule application}
427 %************************************************************************
429 We have four kinds of normalising rewrite rules:
431 (1) Normalisation rules that rewrite a set of insts and return a flag indicating
432 whether any changes occurred during rewriting that necessitate re-running
433 the current rule set.
435 (2) Precondition rules that rewrite a set of insts and return a monadic action
436 that reverts the effect of preconditioning.
438 (3) Idempotent normalisation rules that never require re-running the rule set.
440 (4) Checking rule that does not alter the set of insts.
443 type RewriteRule = [Inst] -> TcM ([Inst], Bool) -- rewrite, maybe re-run
444 type PrecondRule = [Inst] -> TcM ([Inst], TcM ()) -- rewrite, revertable
445 type IdemRewriteRule = [Inst] -> TcM [Inst] -- rewrite, don't re-run
446 type CheckRule = [Inst] -> TcM () -- check
448 type NamedRule = (String, RewriteRule) -- rule with description
449 type NamedPreRule = (String, PrecondRule) -- precond with desc
452 Templates lifting idempotent and checking rules to full rules (which can be put
456 dontRerun :: IdemRewriteRule -> RewriteRule
457 dontRerun rule insts = liftM addFalse $ rule insts
459 addFalse x = (x, False)
461 noChange :: CheckRule -> RewriteRule
462 noChange rule insts = rule insts >> return (insts, False)
465 The following function applies a set of rewrite rules until a fixed point is
466 reached; i.e., none of the `RewriteRule's require re-running the rule set.
467 Optionally, there may be a pre-conditing rule that is applied before any other
468 rules are applied and before the rule set is re-run.
470 The result is the set of rewritten (i.e., normalised) insts and, in case of a
471 pre-conditing rule, a monadic action that reverts the effects of
472 pre-conditioning - specifically, this is removing introduced skolems.
475 rewriteToFixedPoint :: Maybe NamedPreRule -- optional preconditioning rule
476 -> [NamedRule] -- rule set
477 -> [Inst] -- insts to rewrite
478 -> TcM ([Inst], TcM ())
479 rewriteToFixedPoint precondRule rules insts
480 = completeRewrite (return ()) precondRule insts
482 completeRewrite :: TcM () -> Maybe NamedPreRule -> [Inst]
483 -> TcM ([Inst], TcM ())
484 completeRewrite dePrecond (Just (precondName, precond)) insts
485 = do { (insts', dePrecond') <- precond insts
486 ; traceTc $ text precondName <+> ppr insts'
487 ; tryRules (dePrecond >> dePrecond') rules insts'
489 completeRewrite dePrecond Nothing insts
490 = tryRules dePrecond rules insts
492 tryRules dePrecond _ [] = return ([] , dePrecond)
493 tryRules dePrecond [] insts = return (insts, dePrecond)
494 tryRules dePrecond ((name, rule):rules) insts
495 = do { (insts', rerun) <- rule insts
496 ; traceTc $ text name <+> ppr insts'
497 ; if rerun then completeRewrite dePrecond precondRule insts'
498 else tryRules dePrecond rules insts'
503 %************************************************************************
505 \section{Different forms of Inst rewritings}
507 %************************************************************************
509 Rewrite schemata applied by way of eq_rewrite and friends.
518 trivialInsts :: RewriteRule
521 trivialInsts (i@(EqInst {}):is)
522 = do { (is',changed)<- trivialInsts is
523 ; if tcEqType ty1 ty2
524 then do { eitherEqInst i
525 (\covar -> writeMetaTyVar covar ty1)
529 else return (i:is',changed)
533 ty2 = eqInstRightTy i
534 trivialInsts _ = panic "TcTyFuns.trivialInsts: not EqInst"
536 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
537 swapInsts :: RewriteRule
538 -- All the inputs and outputs are equalities
540 = do { (insts', changeds) <- mapAndUnzipM swapInst insts
541 ; return (insts', or changeds)
549 -- where c isn't a function call
556 -- where c isn't a function call or other variable
557 swapInst :: Inst -> TcM (Inst, Bool)
558 swapInst i@(EqInst {})
562 ty2 = eqInstRightTy i
563 go ty1 ty2 | Just ty1' <- tcView ty1
565 go ty1 ty2 | Just ty2' <- tcView ty2
567 go (TyConApp tyCon _) _ | isOpenSynTyCon tyCon
570 go ty1 ty2@(TyConApp tyCon _)
571 | isOpenSynTyCon tyCon
572 = actual_swap ty1 ty2
573 go ty1@(TyConApp _ _) ty2@(TyVarTy _)
574 = actual_swap ty1 ty2
575 go _ _ = return (i,False)
577 actual_swap ty1 ty2 = do { wg_co <- eitherEqInst i
578 -- old_co := sym new_co
580 do { new_cotv <- newMetaTyVar TauTv (mkCoKind ty2 ty1)
581 ; let new_co = TyVarTy new_cotv
582 ; writeMetaTyVar old_covar (mkCoercion symCoercionTyCon [new_co])
583 ; return $ mkWantedCo new_cotv
585 -- new_co := sym old_co
586 (\old_co -> return $ mkGivenCo $ mkCoercion symCoercionTyCon [old_co])
587 ; new_inst <- mkEqInst (EqPred ty2 ty1) wg_co
588 ; return (new_inst,True)
590 swapInst _ = panic "TcTyFuns.swapInst: not EqInst"
592 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
593 decompInsts :: RewriteRule
594 decompInsts insts = do { (insts,bs) <- mapAndUnzipM decompInst insts
595 ; return (concat insts,or bs)
601 -- g21 : c1 ~ d1, ..., g2n : cn ~ dn
604 -- Works also for the case where T is actually an application of a
605 -- type family constructor to a set of types, provided the
606 -- applications on both sides of the ~ are identical;
607 -- see also Note [OpenSynTyCon app] in TcUnify
609 decompInst :: Inst -> TcM ([Inst],Bool)
610 decompInst i@(EqInst {})
614 ty2 = eqInstRightTy i
616 | Just ty1' <- tcView ty1 = go ty1' ty2
617 | Just ty2' <- tcView ty2 = go ty1 ty2'
619 go ty1@(TyConApp con1 tys1) ty2@(TyConApp con2 tys2)
620 | con1 == con2 && identicalHead
621 = do { cos <- eitherEqInst i
622 -- old_co := Con1 cos
624 do { cotvs <- zipWithM (\t1 t2 ->
628 ; let cos = map TyVarTy cotvs
629 ; writeMetaTyVar old_covar (TyConApp con1 cos)
630 ; return $ map mkWantedCo cotvs
632 -- co_i := Con_i old_co
635 mkRightCoercions (length tys1) old_co)
636 ; insts <- zipWithM mkEqInst (zipWith EqPred tys1 tys2) cos
637 ; traceTc (text "decomp identicalHead" <+> ppr insts)
638 ; return (insts, not $ null insts)
640 | con1 /= con2 && not (isOpenSynTyCon con1 || isOpenSynTyCon con2)
641 -- not matching data constructors (of any flavour) are bad news
642 = do { env0 <- tcInitTidyEnv
643 ; let (env1, tidy_ty1) = tidyOpenType env0 ty1
644 (env2, tidy_ty2) = tidyOpenType env1 ty2
645 extra = sep [ppr tidy_ty1, char '~', ppr tidy_ty2]
647 ptext SLIT("Unsolvable equality constraint:")
648 ; failWithTcM (env2, hang msg 2 extra)
652 (idxTys1, _) = splitAt n tys1
653 (idxTys2, _) = splitAt n tys2
654 identicalHead = not (isOpenSynTyCon con1) ||
655 idxTys1 `tcEqTypes` idxTys2
657 go _ _ = return ([i], False)
658 decompInst _ = panic "TcTyFuns.decompInst: not EqInst"
660 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
661 topInsts :: RewriteRule
663 = do { (insts,bs) <- mapAndUnzipM topInst insts
664 ; return (insts,or bs)
669 -- >--> co1 :: t ~ t' / co2 :: s ~ s'
671 -- g1 := co1 * g2 * sym co2
672 topInst :: Inst -> TcM (Inst,Bool)
673 topInst i@(EqInst {})
674 = do { (coi1,ty1') <- tcNormalizeFamInst ty1
675 ; (coi2,ty2') <- tcNormalizeFamInst ty2
676 ; case (coi1,coi2) of
680 do { wg_co <- eitherEqInst i
681 -- old_co = co1 * new_co * sym co2
683 do { new_cotv <- newMetaTyVar TauTv (mkCoKind ty1 ty2)
684 ; let new_co = TyVarTy new_cotv
685 ; let old_coi = coi1 `mkTransCoI` ACo new_co `mkTransCoI` (mkSymCoI coi2)
686 ; writeMetaTyVar old_covar (fromACo old_coi)
687 ; return $ mkWantedCo new_cotv
689 -- new_co = sym co1 * old_co * co2
690 (\old_co -> return $ mkGivenCo $ fromACo $ mkSymCoI coi1 `mkTransCoI` ACo old_co `mkTransCoI` coi2)
691 ; new_inst <- mkEqInst (EqPred ty1' ty2') wg_co
692 ; return (new_inst,True)
697 ty2 = eqInstRightTy i
698 topInst _ = panic "TcTyFuns.topInsts: not EqInst"
700 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
701 substInsts :: RewriteRule
702 substInsts insts = substInstsWorker insts []
704 substInstsWorker :: [Inst] -> [Inst] -> TcM ([Inst],Bool)
705 substInstsWorker [] acc
707 substInstsWorker (i:is) acc
708 | (TyConApp con _) <- tci_left i, isOpenSynTyCon con
709 = do { (is',change) <- substInst i (acc ++ is)
711 then return ((i:is'),True)
712 else substInstsWorker is (i:acc)
714 | (TyVarTy _) <- tci_left i
715 = do { (is',change) <- substInst i (acc ++ is)
717 then return ((i:is'),True)
718 else substInstsWorker is (i:acc)
721 = substInstsWorker is (i:acc)
725 -- forall g1 : s1{F c} ~ s2{F c}
727 -- g2 : s1{t} ~ s2{t}
728 -- g1 := s1{g} * g2 * sym s2{g} <=> g2 := sym s1{g} * g1 * s2{g}
729 substInst :: Inst -> [Inst] -> TcM ([Inst], Bool)
730 substInst _inst [] = return ([],False)
731 substInst inst (i@(EqInst {tci_left = ty1, tci_right = ty2}):is)
732 = do { (is',changed) <- substInst inst is
733 ; (coi1,ty1') <- normalise ty1
734 ; (coi2,ty2') <- normalise ty2
735 ; case (coi1,coi2) of
737 return (i:is',changed)
739 do { gw_co <- eitherEqInst i
740 -- old_co := co1 * new_co * sym co2
742 do { new_cotv <- newMetaTyVar TauTv (mkCoKind ty1' ty2')
743 ; let new_co = TyVarTy new_cotv
744 ; let old_coi = coi1 `mkTransCoI` ACo new_co `mkTransCoI` (mkSymCoI coi2)
745 ; writeMetaTyVar old_covar (fromACo old_coi)
746 ; return $ mkWantedCo new_cotv
748 -- new_co := sym co1 * old_co * co2
749 (\old_co -> return $ mkGivenCo $ fromACo $ (mkSymCoI coi1) `mkTransCoI` ACo old_co `mkTransCoI` coi2)
750 ; new_inst <- mkEqInst (EqPred ty1' ty2') gw_co
751 ; return (new_inst:is',True)
755 normalise = tcEqInstNormalizeFamInst inst
756 substInst _ _ = panic "TcTyFuns.substInst: not EqInst"
758 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
759 unifyInsts :: RewriteRule
761 = do { (insts',changeds) <- mapAndUnzipM unifyInst insts
762 ; return (concat insts',or changeds)
771 -- TOMDO: you should only do this for certain `meta' type variables
772 unifyInst :: Inst -> TcM ([Inst], Bool)
773 unifyInst i@(EqInst {tci_left = ty1, tci_right = ty2})
774 | TyVarTy tv1 <- ty1, isMetaTyVar tv1 = go ty2 tv1
775 | TyVarTy tv2 <- ty2, isMetaTyVar tv2 = go ty1 tv2
776 | otherwise = return ([i],False)
778 = do { let cotv = fromWantedCo "unifyInst" $ eqInstCoercion i
779 ; writeMetaTyVar tv ty -- alpha := t
780 ; writeMetaTyVar cotv ty -- g := t
783 unifyInst _ = panic "TcTyFuns.unifyInst: not EqInst"
785 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
786 occursCheckInsts :: CheckRule
787 occursCheckInsts insts = mappM_ occursCheckInst insts
795 occursCheckInst :: Inst -> TcM ()
796 occursCheckInst (EqInst {tci_left = ty1, tci_right = ty2})
799 check ty = if ty `tcEqType` ty1
803 go (TyConApp con tys) = if isOpenSynTyCon con then return () else mappM_ check tys
804 go (FunTy arg res) = mappM_ check [arg,res]
805 go (AppTy fun arg) = mappM_ check [fun,arg]
808 occursError = do { env0 <- tcInitTidyEnv
809 ; let (env1, tidy_ty1) = tidyOpenType env0 ty1
810 (env2, tidy_ty2) = tidyOpenType env1 ty2
811 extra = sep [ppr tidy_ty1, char '~', ppr tidy_ty2]
812 ; failWithTcM (env2, hang msg 2 extra)
814 where msg = ptext SLIT("Occurs check: cannot construct the infinite type")
815 occursCheckInst _ = panic "TcTyFuns.occursCheckInst: not eqInst"
818 Normalises a set of dictionaries relative to a set of given equalities (which
819 are interpreted as rewrite rules). We only consider given equalities of the
824 where F is a type family.
827 substEqInDictInsts :: [Inst] -- given equalities (used as rewrite rules)
828 -> [Inst] -- dictinaries to be normalised
829 -> TcM ([Inst], TcDictBinds)
830 substEqInDictInsts eq_insts insts
831 = do { traceTc (text "substEqInDictInst <-" <+> ppr insts)
832 ; result <- foldlM rewriteWithOneEquality (insts, emptyBag) eq_insts
833 ; traceTc (text "substEqInDictInst ->" <+> ppr result)
837 -- (1) Given equality of form 'F ts ~ t': use for rewriting
838 rewriteWithOneEquality (insts, dictBinds)
839 inst@(EqInst {tci_left = pattern,
841 | isOpenSynTyConApp pattern
842 = do { (insts', moreDictBinds) <- genericNormaliseInsts True {- wanted -}
844 ; return (insts', dictBinds `unionBags` moreDictBinds)
847 applyThisEq = tcGenericNormalizeFamInstPred (return . matchResult)
849 -- rewrite in case of an exact match
850 matchResult ty | tcEqType pattern ty = Just (target, eqInstType inst)
851 | otherwise = Nothing
853 -- (2) Given equality has the wrong form: ignore
854 rewriteWithOneEquality (insts, dictBinds) _not_a_rewrite_rule
855 = return (insts, dictBinds)
858 %************************************************************************
860 Normalisation of Insts
862 %************************************************************************
864 Take a bunch of Insts (not EqInsts), and normalise them wrt the top-level
865 type-function equations, where
867 (norm_insts, binds) = normaliseInsts is_wanted insts
870 = True, (binds + norm_insts) defines insts (wanteds)
871 = False, (binds + insts) defines norm_insts (givens)
874 normaliseInsts :: Bool -- True <=> wanted insts
875 -> [Inst] -- wanted or given insts
876 -> TcM ([Inst], TcDictBinds) -- normalized insts and bindings
877 normaliseInsts isWanted insts
878 = genericNormaliseInsts isWanted tcNormalizeFamInstPred insts
880 genericNormaliseInsts :: Bool -- True <=> wanted insts
881 -> (TcPredType -> TcM (CoercionI, TcPredType))
883 -> [Inst] -- wanted or given insts
884 -> TcM ([Inst], TcDictBinds) -- normalized insts & binds
885 genericNormaliseInsts isWanted fun insts
886 = do { (insts', binds) <- mapAndUnzipM (normaliseOneInst isWanted fun) insts
887 ; return (insts', unionManyBags binds)
890 normaliseOneInst isWanted fun
891 dict@(Dict {tci_pred = pred,
893 = do { traceTc (text "genericNormaliseInst 1")
894 ; (coi, pred') <- fun pred
895 ; traceTc (text "genericNormaliseInst 2")
898 IdCo -> return (dict, emptyBag)
899 -- don't use pred' in this case; otherwise, we get
900 -- more unfolded closed type synonyms in error messages
902 do { -- an inst for the new pred
903 ; dict' <- newDictBndr loc pred'
904 -- relate the old inst to the new one
905 -- target_dict = source_dict `cast` st_co
906 ; let (target_dict, source_dict, st_co)
907 | isWanted = (dict, dict', mkSymCoercion co)
908 | otherwise = (dict', dict, co)
910 -- co :: dict ~ dict'
911 -- hence dict = dict' `cast` sym co
913 -- co :: dict ~ dict'
914 -- hence dict' = dict `cast` co
915 expr = HsVar $ instToId source_dict
916 cast_expr = HsWrap (WpCo st_co) expr
917 rhs = L (instLocSpan loc) cast_expr
918 binds = mkBind target_dict rhs
919 -- return the new inst
920 ; return (dict', binds)
924 -- TOMDO: treat other insts appropriately
925 normaliseOneInst _isWanted _fun inst
926 = do { inst' <- zonkInst inst
927 ; return (inst', emptyBag)
930 addBind :: Bag (LHsBind TcId) -> Inst -> LHsExpr TcId -> Bag (LHsBind TcId)
931 addBind binds inst rhs = binds `unionBags` mkBind inst rhs
933 mkBind :: Inst -> LHsExpr TcId -> Bag (LHsBind TcId)
934 mkBind inst rhs = unitBag (L (instSpan inst)
935 (VarBind (instToId inst) rhs))