4 -- The above warning supression flag is a temporary kludge.
5 -- While working on this module you are encouraged to remove it and fix
6 -- any warnings in the module. See
7 -- http://hackage.haskell.org/trac/ghc/wiki/Commentary/CodingStyle#Warnings
13 normaliseGivens, normaliseGivenDicts,
14 normaliseWanteds, normaliseWantedDicts,
18 addBind -- should not be here
22 #include "HsVersions.h"
33 import TypeRep ( Type(..) )
35 import Var ( mkCoVar, isTcTyVar )
37 import HscTypes ( ExternalPackageState(..) )
40 import SrcLoc ( Located(..) )
44 import Control.Monad (liftM)
48 %************************************************************************
50 Normalisation of types
52 %************************************************************************
54 Unfold a single synonym family instance and yield the witnessing coercion.
55 Return 'Nothing' if the given type is either not synonym family instance
56 or is a synonym family instance that has no matching instance declaration.
57 (Applies only if the type family application is outermost.)
59 For example, if we have
61 :Co:R42T a :: T [a] ~ :R42T a
63 then 'T [Int]' unfolds to (:R42T Int, :Co:R42T Int).
66 tcUnfoldSynFamInst :: Type -> TcM (Maybe (Type, Coercion))
67 tcUnfoldSynFamInst (TyConApp tycon tys)
68 | not (isOpenSynTyCon tycon) -- unfold *only* _synonym_ family instances
71 = do { maybeFamInst <- tcLookupFamInst tycon tys
72 ; case maybeFamInst of
73 Nothing -> return Nothing
74 Just (rep_tc, rep_tys) -> return $ Just (mkTyConApp rep_tc rep_tys,
75 mkTyConApp coe_tc rep_tys)
77 coe_tc = expectJust "TcTyFun.tcUnfoldSynFamInst"
78 (tyConFamilyCoercion_maybe rep_tc)
80 tcUnfoldSynFamInst _other = return Nothing
83 Normalise 'Type's and 'PredType's by unfolding type family applications where
84 possible (ie, we treat family instances as a TRS). Also zonk meta variables.
86 tcNormalizeFamInst ty = (co, ty')
90 tcNormalizeFamInst :: Type -> TcM (CoercionI, Type)
91 tcNormalizeFamInst = tcGenericNormalizeFamInst tcUnfoldSynFamInst
93 tcNormalizeFamInstPred :: TcPredType -> TcM (CoercionI, TcPredType)
94 tcNormalizeFamInstPred = tcGenericNormalizeFamInstPred tcUnfoldSynFamInst
97 Generic normalisation of 'Type's and 'PredType's; ie, walk the type term and
98 apply the normalisation function gives as the first argument to every TyConApp
99 and every TyVarTy subterm.
101 tcGenericNormalizeFamInst fun ty = (co, ty')
104 This function is (by way of using smart constructors) careful to ensure that
105 the returned coercion is exactly IdCo (and not some semantically equivalent,
106 but syntactically different coercion) whenever (ty' `tcEqType` ty). This
107 makes it easy for the caller to determine whether the type changed. BUT
108 even if we return IdCo, ty' may be *syntactically* different from ty due to
109 unfolded closed type synonyms (by way of tcCoreView). In the interest of
110 good error messages, callers should discard ty' in favour of ty in this case.
113 tcGenericNormalizeFamInst :: (TcType -> TcM (Maybe (TcType,Coercion)))
114 -- what to do with type functions and tyvars
115 -> TcType -- old type
116 -> TcM (CoercionI, Type) -- (coercion, new type)
117 tcGenericNormalizeFamInst fun ty
118 | Just ty' <- tcView ty = tcGenericNormalizeFamInst fun ty'
119 tcGenericNormalizeFamInst fun ty@(TyConApp tyCon tys)
120 = do { (cois, ntys) <- mapAndUnzipM (tcGenericNormalizeFamInst fun) tys
121 ; let tycon_coi = mkTyConAppCoI tyCon ntys cois
122 ; maybe_ty_co <- fun (TyConApp tyCon ntys) -- use normalised args!
123 ; case maybe_ty_co of
124 -- a matching family instance exists
126 do { let first_coi = mkTransCoI tycon_coi (ACo co)
127 ; (rest_coi, nty) <- tcGenericNormalizeFamInst fun ty'
128 ; let fix_coi = mkTransCoI first_coi rest_coi
129 ; return (fix_coi, nty)
131 -- no matching family instance exists
132 -- we do not do anything
133 Nothing -> return (tycon_coi, TyConApp tyCon ntys)
135 tcGenericNormalizeFamInst fun ty@(AppTy ty1 ty2)
136 = do { (coi1,nty1) <- tcGenericNormalizeFamInst fun ty1
137 ; (coi2,nty2) <- tcGenericNormalizeFamInst fun ty2
138 ; return (mkAppTyCoI nty1 coi1 nty2 coi2, AppTy nty1 nty2)
140 tcGenericNormalizeFamInst fun ty@(FunTy ty1 ty2)
141 = do { (coi1,nty1) <- tcGenericNormalizeFamInst fun ty1
142 ; (coi2,nty2) <- tcGenericNormalizeFamInst fun ty2
143 ; return (mkFunTyCoI nty1 coi1 nty2 coi2, FunTy nty1 nty2)
145 tcGenericNormalizeFamInst fun ty@(ForAllTy tyvar ty1)
146 = do { (coi,nty1) <- tcGenericNormalizeFamInst fun ty1
147 ; return (mkForAllTyCoI tyvar coi,ForAllTy tyvar nty1)
149 tcGenericNormalizeFamInst fun ty@(NoteTy note ty1)
150 = do { (coi,nty1) <- tcGenericNormalizeFamInst fun ty1
151 ; return (mkNoteTyCoI note coi,NoteTy note nty1)
153 tcGenericNormalizeFamInst fun ty@(TyVarTy tv)
155 = do { traceTc (text "tcGenericNormalizeFamInst" <+> ppr ty)
156 ; res <- lookupTcTyVar tv
159 do { maybe_ty' <- fun ty
161 Nothing -> return (IdCo, ty)
163 do { (coi2, ty'') <- tcGenericNormalizeFamInst fun ty'
164 ; return (ACo co1 `mkTransCoI` coi2, ty'')
167 IndirectTv ty' -> tcGenericNormalizeFamInst fun ty'
171 tcGenericNormalizeFamInst fun (PredTy predty)
172 = do { (coi, pred') <- tcGenericNormalizeFamInstPred fun predty
173 ; return (coi, PredTy pred') }
175 ---------------------------------
176 tcGenericNormalizeFamInstPred :: (TcType -> TcM (Maybe (TcType,Coercion)))
178 -> TcM (CoercionI, TcPredType)
180 tcGenericNormalizeFamInstPred fun (ClassP cls tys)
181 = do { (cois, tys')<- mapAndUnzipM (tcGenericNormalizeFamInst fun) tys
182 ; return (mkClassPPredCoI cls tys' cois, ClassP cls tys')
184 tcGenericNormalizeFamInstPred fun (IParam ipn ty)
185 = do { (coi, ty') <- tcGenericNormalizeFamInst fun ty
186 ; return $ (mkIParamPredCoI ipn coi, IParam ipn ty')
188 tcGenericNormalizeFamInstPred fun (EqPred ty1 ty2)
189 = do { (coi1, ty1') <- tcGenericNormalizeFamInst fun ty1
190 ; (coi2, ty2') <- tcGenericNormalizeFamInst fun ty2
191 ; return (mkEqPredCoI ty1' coi1 ty2' coi2, EqPred ty1' ty2') }
195 %************************************************************************
197 \section{Normalisation of Given Dictionaries}
199 %************************************************************************
202 normaliseGivenDicts, normaliseWantedDicts
203 :: [Inst] -- given equations
204 -> [Inst] -- dictionaries
205 -> TcM ([Inst],TcDictBinds)
207 normaliseGivenDicts eqs dicts = normalise_dicts eqs dicts False
208 normaliseWantedDicts eqs dicts = normalise_dicts eqs dicts True
211 :: [Inst] -- given equations
212 -> [Inst] -- dictionaries
213 -> Bool -- True <=> the dicts are wanted
214 -- Fals <=> they are given
215 -> TcM ([Inst],TcDictBinds)
216 normalise_dicts given_eqs dicts is_wanted
217 = do { traceTc $ text "normaliseGivenDicts <-" <+> ppr dicts <+>
218 text "with" <+> ppr given_eqs
219 ; (dicts0, binds0) <- normaliseInsts is_wanted dicts
220 ; (dicts1, binds1) <- substEqInDictInsts given_eqs dicts0
221 ; let binds01 = binds0 `unionBags` binds1
222 ; if isEmptyBag binds1
223 then return (dicts1, binds01)
224 else do { (dicts2, binds2) <- normaliseGivenDicts given_eqs dicts1
225 ; return (dicts2, binds01 `unionBags` binds2) } }
229 %************************************************************************
231 \section{Normalisation of wanteds constraints}
233 %************************************************************************
236 normaliseWanteds :: [Inst] -> TcM [Inst]
237 normaliseWanteds insts
238 = do { traceTc (text "normaliseWanteds <-" <+> ppr insts)
239 ; result <- liftM fst $ rewriteToFixedPoint Nothing
240 [ ("(Occurs)", noChange $ occursCheckInsts)
241 , ("(ZONK)", dontRerun $ zonkInsts)
242 , ("(TRIVIAL)", trivialInsts)
243 -- no `swapInsts'; it messes up error messages and should
244 -- not be necessary -=chak
245 , ("(DECOMP)", decompInsts)
246 , ("(TOP)", topInsts)
247 , ("(SUBST)", substInsts)
248 , ("(UNIFY)", unifyInsts)
250 ; traceTc (text "normaliseWanteds ->" <+> ppr result)
256 %************************************************************************
258 \section{Normalisation of givens constraints}
260 %************************************************************************
263 normaliseGivens :: [Inst] -> TcM ([Inst], TcM ())
264 normaliseGivens givens
265 = do { traceTc (text "normaliseGivens <-" <+> ppr givens)
266 ; (result, deSkolem) <-
267 rewriteToFixedPoint (Just ("(SkolemOccurs)", skolemOccurs))
268 [ ("(Occurs)", noChange $ occursCheckInsts)
269 , ("(ZONK)", dontRerun $ zonkInsts)
270 , ("(TRIVIAL)", trivialInsts)
271 , ("(SWAP)", swapInsts)
272 , ("(DECOMP)", decompInsts)
273 , ("(TOP)", topInsts)
274 , ("(SUBST)", substInsts)
276 ; traceTc (text "normaliseGivens ->" <+> ppr result)
277 ; return (result, deSkolem)
280 -- An explanation of what this does would be helpful! -=chak
281 skolemOccurs :: PrecondRule
282 skolemOccurs [] = return ([], return ())
283 skolemOccurs (inst@(EqInst {}):insts)
284 = do { (insts',actions) <- skolemOccurs insts
285 -- check whether the current inst co :: ty1 ~ ty2 suffers
286 -- from the occurs check issue: F ty1 \in ty2
287 ; let occurs = go False ty2
290 -- if it does generate two new coercions:
291 do { skolem_var <- newMetaTyVar TauTv (typeKind ty1)
292 ; let skolem_ty = TyVarTy skolem_var
294 ; inst1 <- mkEqInst (EqPred ty1 skolem_ty) (mkGivenCo ty1)
296 ; inst2 <- mkEqInst (EqPred ty2 skolem_ty) (mkGivenCo $ fromACo $ mkSymCoI $ ACo $ fromGivenCo co)
297 -- to replace the old one
298 -- the corresponding action is
300 ; let action = writeMetaTyVar skolem_var ty1
301 ; return (inst1:inst2:insts', action >> actions)
304 return (inst:insts', actions)
307 ty1 = eqInstLeftTy inst
308 ty2 = eqInstRightTy inst
309 co = eqInstCoercion inst
310 check :: Bool -> TcType -> Bool
312 = if flag && ty1 `tcEqType` ty
316 go flag (TyConApp con tys) = or $ map (check (isOpenSynTyCon con || flag)) tys
317 go flag (FunTy arg res) = or $ map (check flag) [arg,res]
318 go flag (AppTy fun arg) = or $ map (check flag) [fun,arg]
323 %************************************************************************
325 \section{Solving of wanted constraints with respect to a given set}
327 %************************************************************************
330 solveWanteds :: [Inst] -- givens
332 -> TcM [Inst] -- irreducible wanteds
333 solveWanteds givens wanteds
334 = do { traceTc $ text "solveWanteds <-" <+> ppr wanteds <+> text "with" <+>
336 ; result <- liftM fst $ rewriteToFixedPoint Nothing
337 [ ("(Occurs)", noChange $ occursCheckInsts)
338 , ("(TRIVIAL)", trivialInsts)
339 , ("(DECOMP)", decompInsts)
340 , ("(TOP)", topInsts)
341 , ("(GIVEN)", givenInsts givens)
342 , ("(UNIFY)", unifyInsts)
344 ; traceTc (text "solveWanteds ->" <+> ppr result)
348 -- Use `substInst' with every given on all the wanteds.
349 givenInsts :: [Inst] -> [Inst] -> TcM ([Inst],Bool)
350 givenInsts [] wanteds = return (wanteds,False)
351 givenInsts (g:gs) wanteds
352 = do { (wanteds1, changed1) <- givenInsts gs wanteds
353 ; (wanteds2, changed2) <- substInst g wanteds1
354 ; return (wanteds2, changed1 || changed2)
359 %************************************************************************
361 \section{Normalisation rules and iterative rule application}
363 %************************************************************************
365 We have four kinds of normalising rewrite rules:
367 (1) Normalisation rules that rewrite a set of insts and return a flag indicating
368 whether any changes occurred during rewriting that necessitate re-running
369 the current rule set.
371 (2) Precondition rules that rewrite a set of insts and return a monadic action
372 that reverts the effect of preconditioning.
374 (3) Idempotent normalisation rules that never require re-running the rule set.
376 (4) Checking rule that does not alter the set of insts.
379 type RewriteRule = [Inst] -> TcM ([Inst], Bool) -- rewrite, maybe re-run
380 type PrecondRule = [Inst] -> TcM ([Inst], TcM ()) -- rewrite, revertable
381 type IdemRewriteRule = [Inst] -> TcM [Inst] -- rewrite, don't re-run
382 type CheckRule = [Inst] -> TcM () -- check
384 type NamedRule = (String, RewriteRule) -- rule with description
385 type NamedPreRule = (String, PrecondRule) -- precond with desc
388 Templates lifting idempotent and checking rules to full rules (which can be put
392 dontRerun :: IdemRewriteRule -> RewriteRule
393 dontRerun rule insts = liftM addFalse $ rule insts
395 addFalse x = (x, False)
397 noChange :: CheckRule -> RewriteRule
398 noChange rule insts = rule insts >> return (insts, False)
401 The following function applies a set of rewrite rules until a fixed point is
402 reached; i.e., none of the `RewriteRule's require re-running the rule set.
403 Optionally, there may be a pre-conditing rule that is applied before any other
404 rules are applied and before the rule set is re-run.
406 The result is the set of rewritten (i.e., normalised) insts and, in case of a
407 pre-conditing rule, a monadic action that reverts the effects of
408 pre-conditioning - specifically, this is removing introduced skolems.
411 rewriteToFixedPoint :: Maybe NamedPreRule -- optional preconditioning rule
412 -> [NamedRule] -- rule set
413 -> [Inst] -- insts to rewrite
414 -> TcM ([Inst], TcM ())
415 rewriteToFixedPoint precondRule rules insts
416 = completeRewrite (return ()) precondRule insts
418 completeRewrite :: TcM () -> Maybe NamedPreRule -> [Inst]
419 -> TcM ([Inst], TcM ())
420 completeRewrite dePrecond (Just (precondName, precond)) insts
421 = do { (insts', dePrecond') <- precond insts
422 ; traceTc $ text precondName <+> ppr insts'
423 ; tryRules dePrecond rules insts'
425 completeRewrite dePrecond Nothing insts
426 = tryRules dePrecond rules insts
428 tryRules dePrecond _ [] = return ([] , dePrecond)
429 tryRules dePrecond [] insts = return (insts, dePrecond)
430 tryRules dePrecond ((name, rule):rules) insts
431 = do { (insts', rerun) <- rule insts
432 ; traceTc $ text name <+> ppr insts'
433 ; if rerun then completeRewrite dePrecond precondRule insts'
434 else tryRules dePrecond rules insts'
439 %************************************************************************
441 \section{Different forms of Inst rewritings}
443 %************************************************************************
445 Rewrite schemata applied by way of eq_rewrite and friends.
455 [Inst] -> -- equations
456 TcM ([Inst],Bool) -- remaining equations, any changes?
459 trivialInsts (i@(EqInst {}):is)
460 = do { (is',changed)<- trivialInsts is
461 ; if tcEqType ty1 ty2
462 then do { eitherEqInst i
463 (\covar -> writeMetaTyVar covar ty1)
467 else return (i:is',changed)
471 ty2 = eqInstRightTy i
473 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
474 swapInsts :: [Inst] -> TcM ([Inst],Bool)
475 -- All the inputs and outputs are equalities
477 = do { (insts', changeds) <- mapAndUnzipM swapInst insts
478 ; return (insts', or changeds)
487 -- This is not all, is it? Td ~ c is also rewritten to c ~ Td!
488 swapInst i@(EqInst {})
492 ty2 = eqInstRightTy i
493 go ty1 ty2 | Just ty1' <- tcView ty1
495 go ty1 ty2 | Just ty2' <- tcView ty2
497 go (TyConApp tyCon _) _ | isOpenSynTyCon tyCon
500 go ty1 ty2@(TyConApp tyCon _)
501 | isOpenSynTyCon tyCon
502 = actual_swap ty1 ty2
503 go ty1@(TyConApp _ _) ty2@(TyVarTy _)
504 = actual_swap ty1 ty2
505 go _ _ = return (i,False)
507 actual_swap ty1 ty2 = do { wg_co <- eitherEqInst i
508 -- old_co := sym new_co
510 do { new_cotv <- newMetaTyVar TauTv (mkCoKind ty2 ty1)
511 ; let new_co = TyVarTy new_cotv
512 ; writeMetaTyVar old_covar (mkCoercion symCoercionTyCon [new_co])
513 ; return $ mkWantedCo new_cotv
515 -- new_co := sym old_co
516 (\old_co -> return $ mkGivenCo $ mkCoercion symCoercionTyCon [old_co])
517 ; new_inst <- mkEqInst (EqPred ty2 ty1) wg_co
518 ; return (new_inst,True)
521 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
522 decompInsts :: [Inst] -> TcM ([Inst],Bool)
523 decompInsts insts = do { (insts,bs) <- mapAndUnzipM decompInst insts
524 ; return (concat insts,or bs)
530 -- g21 : c1 ~ d1, ..., g2n : cn ~ dn
533 -- Works also for the case where T is actually an application of a
534 -- type family constructor to a set of types, provided the
535 -- applications on both sides of the ~ are identical;
536 -- see also Note [OpenSynTyCon app] in TcUnify
538 decompInst :: Inst -> TcM ([Inst],Bool)
539 decompInst i@(EqInst {})
543 ty2 = eqInstRightTy i
545 | Just ty1' <- tcView ty1 = go ty1' ty2
546 | Just ty2' <- tcView ty2 = go ty1 ty2'
548 go ty1@(TyConApp con1 tys1) ty2@(TyConApp con2 tys2)
549 | con1 == con2 && identicalHead
550 = do { cos <- eitherEqInst i
551 -- old_co := Con1 cos
553 do { cotvs <- zipWithM (\t1 t2 ->
557 ; let cos = map TyVarTy cotvs
558 ; writeMetaTyVar old_covar (TyConApp con1 cos)
559 ; return $ map mkWantedCo cotvs
561 -- co_i := Con_i old_co
564 mkRightCoercions (length tys1) old_co)
565 ; insts <- zipWithM mkEqInst (zipWith EqPred tys1 tys2) cos
566 ; traceTc (text "decomp identicalHead" <+> ppr insts)
567 ; return (insts, not $ null insts)
569 | con1 /= con2 && not (isOpenSynTyCon con1 || isOpenSynTyCon con2)
570 -- not matching data constructors (of any flavour) are bad news
571 = do { env0 <- tcInitTidyEnv
572 ; let (env1, tidy_ty1) = tidyOpenType env0 ty1
573 (env2, tidy_ty2) = tidyOpenType env1 ty2
574 extra = sep [ppr tidy_ty1, char '~', ppr tidy_ty2]
576 ptext SLIT("Unsolvable equality constraint:")
577 ; failWithTcM (env2, hang msg 2 extra)
581 (idxTys1, tys1') = splitAt n tys1
582 (idxTys2, tys2') = splitAt n tys2
583 identicalHead = not (isOpenSynTyCon con1) ||
584 idxTys1 `tcEqTypes` idxTys2
586 go _ _ = return ([i], False)
588 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
589 topInsts :: [Inst] -> TcM ([Inst],Bool)
591 = do { (insts,bs) <- mapAndUnzipM topInst insts
592 ; return (insts,or bs)
597 -- >--> co1 :: t ~ t' / co2 :: s ~ s'
599 -- g1 := co1 * g2 * sym co2
600 topInst :: Inst -> TcM (Inst,Bool)
601 topInst i@(EqInst {})
602 = do { (coi1,ty1') <- tcNormalizeFamInst ty1
603 ; (coi2,ty2') <- tcNormalizeFamInst ty2
604 ; case (coi1,coi2) of
608 do { wg_co <- eitherEqInst i
609 -- old_co = co1 * new_co * sym co2
611 do { new_cotv <- newMetaTyVar TauTv (mkCoKind ty1 ty2)
612 ; let new_co = TyVarTy new_cotv
613 ; let old_coi = coi1 `mkTransCoI` ACo new_co `mkTransCoI` (mkSymCoI coi2)
614 ; writeMetaTyVar old_covar (fromACo old_coi)
615 ; return $ mkWantedCo new_cotv
617 -- new_co = sym co1 * old_co * co2
618 (\old_co -> return $ mkGivenCo $ fromACo $ mkSymCoI coi1 `mkTransCoI` ACo old_co `mkTransCoI` coi2)
619 ; new_inst <- mkEqInst (EqPred ty1' ty2') wg_co
620 ; return (new_inst,True)
625 ty2 = eqInstRightTy i
627 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
628 substInsts :: [Inst] -> TcM ([Inst],Bool)
629 substInsts insts = substInstsWorker insts []
631 substInstsWorker [] acc
633 substInstsWorker (i:is) acc
634 | (TyConApp con _) <- tci_left i, isOpenSynTyCon con
635 = do { (is',change) <- substInst i (acc ++ is)
637 then return ((i:is'),True)
638 else substInstsWorker is (i:acc)
641 = substInstsWorker is (i:acc)
645 -- forall g1 : s1{F c} ~ s2{F c}
647 -- g2 : s1{t} ~ s2{t}
648 -- g1 := s1{g} * g2 * sym s2{g} <=> g2 := sym s1{g} * g1 * s2{g}
651 substInst inst@(EqInst {tci_left = pattern, tci_right = target}) (i@(EqInst {tci_left = ty1, tci_right = ty2}):is)
652 = do { (is',changed) <- substInst inst is
653 ; (coi1,ty1') <- tcGenericNormalizeFamInst fun ty1
654 ; (coi2,ty2') <- tcGenericNormalizeFamInst fun ty2
655 ; case (coi1,coi2) of
657 return (i:is',changed)
659 do { gw_co <- eitherEqInst i
660 -- old_co := co1 * new_co * sym co2
662 do { new_cotv <- newMetaTyVar TauTv (mkCoKind ty1' ty2')
663 ; let new_co = TyVarTy new_cotv
664 ; let old_coi = coi1 `mkTransCoI` ACo new_co `mkTransCoI` (mkSymCoI coi2)
665 ; writeMetaTyVar old_covar (fromACo old_coi)
666 ; return $ mkWantedCo new_cotv
668 -- new_co := sym co1 * old_co * co2
669 (\old_co -> return $ mkGivenCo $ fromACo $ (mkSymCoI coi1) `mkTransCoI` ACo old_co `mkTransCoI` coi2)
670 ; new_inst <- mkEqInst (EqPred ty1' ty2') gw_co
671 ; return (new_inst:is',True)
674 where fun ty = return $ if tcEqType pattern ty then Just (target,coercion) else Nothing
676 coercion = eitherEqInst inst TyVarTy id
677 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
679 :: [Inst] -- wanted equations
682 = do { (insts',changeds) <- mapAndUnzipM unifyInst insts
683 ; return (concat insts',or changeds)
692 -- TOMDO: you should only do this for certain `meta' type variables
693 unifyInst i@(EqInst {tci_left = ty1, tci_right = ty2})
694 | TyVarTy tv1 <- ty1, isMetaTyVar tv1 = go ty2 tv1
695 | TyVarTy tv2 <- ty2, isMetaTyVar tv2 = go ty1 tv2
696 | otherwise = return ([i],False)
698 = do { let cotv = fromWantedCo "unifyInst" $ eqInstCoercion i
699 ; writeMetaTyVar tv ty -- alpha := t
700 ; writeMetaTyVar cotv ty -- g := t
704 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
705 occursCheckInsts :: [Inst] -> TcM ()
706 occursCheckInsts insts = mappM_ occursCheckInst insts
714 occursCheckInst :: Inst -> TcM ()
715 occursCheckInst i@(EqInst {tci_left = ty1, tci_right = ty2})
718 check ty = if ty `tcEqType` ty1
722 go (TyConApp con tys) = if isOpenSynTyCon con then return () else mappM_ check tys
723 go (FunTy arg res) = mappM_ check [arg,res]
724 go (AppTy fun arg) = mappM_ check [fun,arg]
727 occursError = do { env0 <- tcInitTidyEnv
728 ; let (env1, tidy_ty1) = tidyOpenType env0 ty1
729 (env2, tidy_ty2) = tidyOpenType env1 ty2
730 extra = sep [ppr tidy_ty1, char '~', ppr tidy_ty2]
731 ; failWithTcM (env2, hang msg 2 extra)
733 where msg = ptext SLIT("Occurs check: cannot construct the infinite type")
736 Normalises a set of dictionaries relative to a set of given equalities (which
737 are interpreted as rewrite rules). We only consider given equalities of the
742 where F is a type family.
745 substEqInDictInsts :: [Inst] -- given equalities (used as rewrite rules)
746 -> [Inst] -- dictinaries to be normalised
747 -> TcM ([Inst], TcDictBinds)
748 substEqInDictInsts eq_insts insts
749 = do { traceTc (text "substEqInDictInst <-" <+> ppr insts)
750 ; result <- foldlM rewriteWithOneEquality (insts, emptyBag) eq_insts
751 ; traceTc (text "substEqInDictInst ->" <+> ppr result)
755 -- (1) Given equality of form 'F ts ~ t': use for rewriting
756 rewriteWithOneEquality (insts, dictBinds)
757 inst@(EqInst {tci_left = pattern,
759 | isOpenSynTyConApp pattern
760 = do { (insts', moreDictBinds) <- genericNormaliseInsts True {- wanted -}
762 ; return (insts', dictBinds `unionBags` moreDictBinds)
765 applyThisEq = tcGenericNormalizeFamInstPred (return . matchResult)
767 -- rewrite in case of an exact match
768 matchResult ty | tcEqType pattern ty = Just (target, eqInstType inst)
769 | otherwise = Nothing
771 -- (2) Given equality has the wrong form: ignore
772 rewriteWithOneEquality (insts, dictBinds) _not_a_rewrite_rule
773 = return (insts, dictBinds)
776 %************************************************************************
778 Normalisation of Insts
780 %************************************************************************
782 Take a bunch of Insts (not EqInsts), and normalise them wrt the top-level
783 type-function equations, where
785 (norm_insts, binds) = normaliseInsts is_wanted insts
788 = True, (binds + norm_insts) defines insts (wanteds)
789 = False, (binds + insts) defines norm_insts (givens)
792 normaliseInsts :: Bool -- True <=> wanted insts
793 -> [Inst] -- wanted or given insts
794 -> TcM ([Inst], TcDictBinds) -- normalized insts and bindings
795 normaliseInsts isWanted insts
796 = genericNormaliseInsts isWanted tcNormalizeFamInstPred insts
798 genericNormaliseInsts :: Bool -- True <=> wanted insts
799 -> (TcPredType -> TcM (CoercionI, TcPredType))
801 -> [Inst] -- wanted or given insts
802 -> TcM ([Inst], TcDictBinds) -- normalized insts & binds
803 genericNormaliseInsts isWanted fun insts
804 = do { (insts', binds) <- mapAndUnzipM (normaliseOneInst isWanted fun) insts
805 ; return (insts', unionManyBags binds)
808 normaliseOneInst isWanted fun
809 dict@(Dict {tci_name = name,
812 = do { traceTc (text "genericNormaliseInst 1")
813 ; (coi, pred') <- fun pred
814 ; traceTc (text "genericNormaliseInst 2")
817 IdCo -> return (dict, emptyBag)
818 -- don't use pred' in this case; otherwise, we get
819 -- more unfolded closed type synonyms in error messages
821 do { -- an inst for the new pred
822 ; dict' <- newDictBndr loc pred'
823 -- relate the old inst to the new one
824 -- target_dict = source_dict `cast` st_co
825 ; let (target_dict, source_dict, st_co)
826 | isWanted = (dict, dict', mkSymCoercion co)
827 | otherwise = (dict', dict, co)
829 -- co :: dict ~ dict'
830 -- hence dict = dict' `cast` sym co
832 -- co :: dict ~ dict'
833 -- hence dict' = dict `cast` co
834 expr = HsVar $ instToId source_dict
835 cast_expr = HsWrap (WpCo st_co) expr
836 rhs = L (instLocSpan loc) cast_expr
837 binds = mkBind target_dict rhs
838 -- return the new inst
839 ; return (dict', binds)
843 -- TOMDO: treat other insts appropriately
844 normaliseOneInst isWanted fun inst
845 = do { inst' <- zonkInst inst
846 ; return (inst', emptyBag)
849 addBind binds inst rhs = binds `unionBags` mkBind inst rhs
851 mkBind inst rhs = unitBag (L (instSpan inst)
852 (VarBind (instToId inst) rhs))