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(..) )
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 { maybeFamInst <- tcLookupFamInst tycon tys
71 ; case maybeFamInst of
72 Nothing -> return Nothing
73 Just (rep_tc, rep_tys) -> return $ Just (mkTyConApp rep_tc rep_tys,
74 mkTyConApp coe_tc rep_tys)
76 coe_tc = expectJust "TcTyFun.tcUnfoldSynFamInst"
77 (tyConFamilyCoercion_maybe rep_tc)
79 tcUnfoldSynFamInst _other = return Nothing
82 Normalise 'Type's and 'PredType's by unfolding type family applications where
83 possible (ie, we treat family instances as a TRS). Also zonk meta variables.
85 tcNormalizeFamInst ty = (co, ty')
89 tcNormalizeFamInst :: Type -> TcM (CoercionI, Type)
90 tcNormalizeFamInst = tcGenericNormalizeFamInst tcUnfoldSynFamInst
92 tcNormalizeFamInstPred :: TcPredType -> TcM (CoercionI, TcPredType)
93 tcNormalizeFamInstPred = tcGenericNormalizeFamInstPred tcUnfoldSynFamInst
96 Generic normalisation of 'Type's and 'PredType's; ie, walk the type term and
97 apply the normalisation function gives as the first argument to every TyConApp
98 and every TyVarTy subterm.
100 tcGenericNormalizeFamInst fun ty = (co, ty')
103 This function is (by way of using smart constructors) careful to ensure that
104 the returned coercion is exactly IdCo (and not some semantically equivalent,
105 but syntactically different coercion) whenever (ty' `tcEqType` ty). This
106 makes it easy for the caller to determine whether the type changed. BUT
107 even if we return IdCo, ty' may be *syntactically* different from ty due to
108 unfolded closed type synonyms (by way of tcCoreView). In the interest of
109 good error messages, callers should discard ty' in favour of ty in this case.
112 tcGenericNormalizeFamInst :: (TcType -> TcM (Maybe (TcType,Coercion)))
113 -- what to do with type functions and tyvars
114 -> TcType -- old type
115 -> TcM (CoercionI, Type) -- (coercion, new type)
116 tcGenericNormalizeFamInst fun ty
117 | Just ty' <- tcView ty = tcGenericNormalizeFamInst fun ty'
118 tcGenericNormalizeFamInst fun ty@(TyConApp tyCon tys)
119 = do { (cois, ntys) <- mapAndUnzipM (tcGenericNormalizeFamInst fun) tys
120 ; let tycon_coi = mkTyConAppCoI tyCon ntys cois
121 ; maybe_ty_co <- fun (TyConApp tyCon ntys) -- use normalised args!
122 ; case maybe_ty_co of
123 -- a matching family instance exists
125 do { let first_coi = mkTransCoI tycon_coi (ACo co)
126 ; (rest_coi, nty) <- tcGenericNormalizeFamInst fun ty'
127 ; let fix_coi = mkTransCoI first_coi rest_coi
128 ; return (fix_coi, nty)
130 -- no matching family instance exists
131 -- we do not do anything
132 Nothing -> return (tycon_coi, TyConApp tyCon ntys)
134 tcGenericNormalizeFamInst fun ty@(AppTy ty1 ty2)
135 = do { (coi1,nty1) <- tcGenericNormalizeFamInst fun ty1
136 ; (coi2,nty2) <- tcGenericNormalizeFamInst fun ty2
137 ; return (mkAppTyCoI nty1 coi1 nty2 coi2, AppTy nty1 nty2)
139 tcGenericNormalizeFamInst fun ty@(FunTy ty1 ty2)
140 = do { (coi1,nty1) <- tcGenericNormalizeFamInst fun ty1
141 ; (coi2,nty2) <- tcGenericNormalizeFamInst fun ty2
142 ; return (mkFunTyCoI nty1 coi1 nty2 coi2, FunTy nty1 nty2)
144 tcGenericNormalizeFamInst fun ty@(ForAllTy tyvar ty1)
145 = do { (coi,nty1) <- tcGenericNormalizeFamInst fun ty1
146 ; return (mkForAllTyCoI tyvar coi,ForAllTy tyvar nty1)
148 tcGenericNormalizeFamInst fun ty@(NoteTy note ty1)
149 = do { (coi,nty1) <- tcGenericNormalizeFamInst fun ty1
150 ; return (mkNoteTyCoI note coi,NoteTy note nty1)
152 tcGenericNormalizeFamInst fun ty@(TyVarTy tv)
154 = do { traceTc (text "tcGenericNormalizeFamInst" <+> ppr ty)
155 ; res <- lookupTcTyVar tv
158 do { maybe_ty' <- fun ty
160 Nothing -> return (IdCo, ty)
162 do { (coi2, ty'') <- tcGenericNormalizeFamInst fun ty'
163 ; return (ACo co1 `mkTransCoI` coi2, ty'')
166 IndirectTv ty' -> tcGenericNormalizeFamInst fun ty'
170 tcGenericNormalizeFamInst fun (PredTy predty)
171 = do { (coi, pred') <- tcGenericNormalizeFamInstPred fun predty
172 ; return (coi, PredTy pred') }
174 ---------------------------------
175 tcGenericNormalizeFamInstPred :: (TcType -> TcM (Maybe (TcType,Coercion)))
177 -> TcM (CoercionI, TcPredType)
179 tcGenericNormalizeFamInstPred fun (ClassP cls tys)
180 = do { (cois, tys')<- mapAndUnzipM (tcGenericNormalizeFamInst fun) tys
181 ; return (mkClassPPredCoI cls tys' cois, ClassP cls tys')
183 tcGenericNormalizeFamInstPred fun (IParam ipn ty)
184 = do { (coi, ty') <- tcGenericNormalizeFamInst fun ty
185 ; return $ (mkIParamPredCoI ipn coi, IParam ipn ty')
187 tcGenericNormalizeFamInstPred fun (EqPred ty1 ty2)
188 = do { (coi1, ty1') <- tcGenericNormalizeFamInst fun ty1
189 ; (coi2, ty2') <- tcGenericNormalizeFamInst fun ty2
190 ; return (mkEqPredCoI ty1' coi1 ty2' coi2, EqPred ty1' ty2') }
194 %************************************************************************
196 \section{Normalisation of Given Dictionaries}
198 %************************************************************************
201 normaliseGivenDicts, normaliseWantedDicts
202 :: [Inst] -- given equations
203 -> [Inst] -- dictionaries
204 -> TcM ([Inst],TcDictBinds)
206 normaliseGivenDicts eqs dicts = normalise_dicts eqs dicts False
207 normaliseWantedDicts eqs dicts = normalise_dicts eqs dicts True
210 :: [Inst] -- given equations
211 -> [Inst] -- dictionaries
212 -> Bool -- True <=> the dicts are wanted
213 -- Fals <=> they are given
214 -> TcM ([Inst],TcDictBinds)
215 normalise_dicts given_eqs dicts is_wanted
216 = do { traceTc $ text "normaliseGivenDicts <-" <+> ppr dicts <+>
217 text "with" <+> ppr given_eqs
218 ; (dicts0, binds0) <- normaliseInsts is_wanted dicts
219 ; (dicts1, binds1) <- substEqInDictInsts given_eqs dicts0
220 ; let binds01 = binds0 `unionBags` binds1
221 ; if isEmptyBag binds1
222 then return (dicts1, binds01)
223 else do { (dicts2, binds2) <- normaliseGivenDicts given_eqs dicts1
224 ; return (dicts2, binds01 `unionBags` binds2) } }
228 %************************************************************************
230 \section{Normalisation of Wanteds}
232 %************************************************************************
235 normaliseWanteds :: [Inst] -> TcM [Inst]
236 normaliseWanteds insts
237 = do { traceTc (text "normaliseWanteds" <+> ppr insts)
238 ; result <- eq_rewrite
239 [ ("(Occurs)", simple_rewrite_check $ occursCheckInsts)
240 , ("(ZONK)", simple_rewrite $ zonkInsts)
241 , ("(TRIVIAL)", trivialInsts)
242 , ("(SWAP)", swapInsts)
243 , ("(DECOMP)", decompInsts)
244 , ("(TOP)", topInsts)
245 , ("(SUBST)", substInsts)
246 , ("(UNIFY)", unifyInsts)
248 ; traceTc (text "normaliseWanteds ->" <+> ppr result)
253 %************************************************************************
255 \section{Normalisation of Givens}
257 %************************************************************************
261 normaliseGivens :: [Inst] -> TcM ([Inst],TcM ())
262 normaliseGivens givens =
263 do { traceTc (text "normaliseGivens <-" <+> ppr givens)
264 ; (result,action) <- given_eq_rewrite
265 ("(SkolemOccurs)", skolemOccurs)
267 [("(Occurs)", simple_rewrite_check $ occursCheckInsts),
268 ("(ZONK)", simple_rewrite $ zonkInsts),
269 ("(TRIVIAL)", trivialInsts),
270 ("(SWAP)", swapInsts),
271 ("(DECOMP)", decompInsts),
273 ("(SUBST)", substInsts)]
275 ; traceTc (text "normaliseGivens ->" <+> ppr result)
276 ; return (result,action)
279 skolemOccurs :: [Inst] -> TcM ([Inst],TcM ())
280 skolemOccurs [] = return ([], return ())
281 skolemOccurs (inst@(EqInst {}):insts)
282 = do { (insts',actions) <- skolemOccurs insts
283 -- check whether the current inst co :: ty1 ~ ty2 suffers
284 -- from the occurs check issue: F ty1 \in ty2
285 ; let occurs = go False ty2
288 -- if it does generate two new coercions:
289 do { skolem_var <- newMetaTyVar TauTv (typeKind ty1)
290 ; let skolem_ty = TyVarTy skolem_var
292 ; inst1 <- mkEqInst (EqPred ty1 skolem_ty) (mkGivenCo ty1)
294 ; inst2 <- mkEqInst (EqPred ty2 skolem_ty) (mkGivenCo $ fromACo $ mkSymCoI $ ACo $ fromGivenCo co)
295 -- to replace the old one
296 -- the corresponding action is
298 ; let action = writeMetaTyVar skolem_var ty1
299 ; return (inst1:inst2:insts', action >> actions)
302 return (inst:insts', actions)
305 ty1 = eqInstLeftTy inst
306 ty2 = eqInstRightTy inst
307 co = eqInstCoercion inst
308 check :: Bool -> TcType -> Bool
310 = if flag && ty1 `tcEqType` ty
314 go flag (TyConApp con tys) = or $ map (check (isOpenSynTyCon con || flag)) tys
315 go flag (FunTy arg res) = or $ map (check flag) [arg,res]
316 go flag (AppTy fun arg) = or $ map (check flag) [fun,arg]
320 %************************************************************************
322 \section{Solving of Wanteds}
324 %************************************************************************
330 TcM [Inst] -- irreducible wanteds
331 solveWanteds givens wanteds =
332 do { traceTc (text "solveWanteds <-" <+> ppr wanteds <+> text "with" <+> ppr givens)
333 ; result <- eq_rewrite
334 [("(Occurs)", simple_rewrite_check $ occursCheckInsts),
335 ("(TRIVIAL)", trivialInsts),
336 ("(DECOMP)", decompInsts),
338 ("(GIVEN)", givenInsts givens),
339 ("(UNIFY)", unifyInsts)]
341 ; traceTc (text "solveWanteds ->" <+> ppr result)
346 givenInsts :: [Inst] -> [Inst] -> TcM ([Inst],Bool)
347 givenInsts [] wanteds
348 = return (wanteds,False)
349 givenInsts (g:gs) wanteds
350 = do { (wanteds1,changed1) <- givenInsts gs wanteds
351 ; (wanteds2,changed2) <- substInst g wanteds1
352 ; return (wanteds2,changed1 || changed2)
357 -- fixpoint computation
358 -- of a number of rewrites of equalities
360 [(String,[Inst] -> TcM ([Inst],Bool))] -> -- rewrite functions and descriptions
361 [Inst] -> -- initial equations
362 TcM [Inst] -- final equations (at fixed point)
363 eq_rewrite rewrites insts
366 go _ [] -- return quickly when there's nothing to be done
370 go ((desc,r):rs) insts
371 = do { (insts',changed) <- r insts
372 ; traceTc (text desc <+> ppr insts')
377 loop = eq_rewrite rewrites
379 -- fixpoint computation
380 -- of a number of rewrites of equalities
383 (String,[Inst] -> TcM ([Inst],TcM ())) ->
385 [(String,[Inst] -> TcM ([Inst],Bool))] -> -- rewrite functions and descriptions
386 [Inst] -> -- initial equations
387 TcM ([Inst],TcM ()) -- final equations (at fixed point)
388 given_eq_rewrite p@(desc,start) acc rewrites insts
389 = do { (insts',acc') <- start insts
390 ; go (acc >> acc') rewrites insts'
393 go acc _ [] -- return quickly when there's nothing to be done
397 go acc ((desc,r):rs) insts
398 = do { (insts',changed) <- r insts
399 ; traceTc (text desc <+> ppr insts')
402 else go acc rs insts'
404 loop acc = given_eq_rewrite p acc rewrites
407 ([Inst] -> TcM [Inst]) ->
408 ([Inst] -> TcM ([Inst],Bool))
409 simple_rewrite r insts
410 = do { insts' <- r insts
411 ; return (insts',False)
414 simple_rewrite_check ::
415 ([Inst] -> TcM ()) ->
416 ([Inst] -> TcM ([Inst],Bool))
417 simple_rewrite_check check insts
418 = check insts >> return (insts,False)
423 %************************************************************************
425 \section{Different forms of Inst rewritings}
427 %************************************************************************
429 Rewrite schemata applied by way of eq_rewrite and friends.
439 [Inst] -> -- equations
440 TcM ([Inst],Bool) -- remaining equations, any changes?
443 trivialInsts (i@(EqInst {}):is)
444 = do { (is',changed)<- trivialInsts is
445 ; if tcEqType ty1 ty2
446 then do { eitherEqInst i
447 (\covar -> writeMetaTyVar covar ty1)
451 else return (i:is',changed)
455 ty2 = eqInstRightTy i
457 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
458 swapInsts :: [Inst] -> TcM ([Inst],Bool)
459 -- All the inputs and outputs are equalities
461 = do { (insts', changeds) <- mapAndUnzipM swapInst insts
462 ; return (insts', or changeds)
471 swapInst i@(EqInst {})
475 ty2 = eqInstRightTy i
476 go ty1 ty2 | Just ty1' <- tcView ty1
478 go ty1 ty2 | Just ty2' <- tcView ty2
480 go (TyConApp tyCon _) _ | isOpenSynTyCon tyCon
483 go ty1 ty2@(TyConApp tyCon _)
484 | isOpenSynTyCon tyCon
485 = actual_swap ty1 ty2
486 go ty1@(TyConApp _ _) ty2@(TyVarTy _)
487 = actual_swap ty1 ty2
488 go _ _ = return (i,False)
490 actual_swap ty1 ty2 = do { wg_co <- eitherEqInst i
491 -- old_co := sym new_co
493 do { new_cotv <- newMetaTyVar TauTv (mkCoKind ty2 ty1)
494 ; let new_co = TyVarTy new_cotv
495 ; writeMetaTyVar old_covar (mkCoercion symCoercionTyCon [new_co])
496 ; return $ mkWantedCo new_cotv
498 -- new_co := sym old_co
499 (\old_co -> return $ mkGivenCo $ mkCoercion symCoercionTyCon [old_co])
500 ; new_inst <- mkEqInst (EqPred ty2 ty1) wg_co
501 ; return (new_inst,True)
504 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
505 decompInsts :: [Inst] -> TcM ([Inst],Bool)
506 decompInsts insts = do { (insts,bs) <- mapAndUnzipM decompInst insts
507 ; return (concat insts,or bs)
513 -- g21 : c1 ~ d1, ..., g2n : cn ~ dn
516 -- Works also for the case where T is actually an application of a
517 -- type family constructor to a set of types, provided the
518 -- applications on both sides of the ~ are identical;
519 -- see also Note [OpenSynTyCon app] in TcUnify
521 decompInst :: Inst -> TcM ([Inst],Bool)
522 decompInst i@(EqInst {})
526 ty2 = eqInstRightTy i
528 | Just ty1' <- tcView ty1 = go ty1' ty2
529 | Just ty2' <- tcView ty2 = go ty1 ty2'
531 go ty1@(TyConApp con1 tys1) ty2@(TyConApp con2 tys2)
532 | con1 == con2 && identicalHead
533 = do { cos <- eitherEqInst i
534 -- old_co := Con1 cos
536 do { cotvs <- zipWithM (\t1 t2 ->
540 ; let cos = map TyVarTy cotvs
541 ; writeMetaTyVar old_covar (TyConApp con1 cos)
542 ; return $ map mkWantedCo cotvs
544 -- co_i := Con_i old_co
547 mkRightCoercions (length tys1) old_co)
548 ; insts <- zipWithM mkEqInst (zipWith EqPred tys1 tys2) cos
549 ; traceTc (text "decomp identicalHead" <+> ppr insts)
550 ; return (insts, not $ null insts)
552 | con1 /= con2 && not (isOpenSynTyCon con1 || isOpenSynTyCon con2)
553 -- not matching data constructors (of any flavour) are bad news
554 = do { env0 <- tcInitTidyEnv
555 ; let (env1, tidy_ty1) = tidyOpenType env0 ty1
556 (env2, tidy_ty2) = tidyOpenType env1 ty2
557 extra = sep [ppr tidy_ty1, char '~', ppr tidy_ty2]
559 ptext SLIT("Unsolvable equality constraint:")
560 ; failWithTcM (env2, hang msg 2 extra)
564 (idxTys1, tys1') = splitAt n tys1
565 (idxTys2, tys2') = splitAt n tys2
566 identicalHead = not (isOpenSynTyCon con1) ||
567 idxTys1 `tcEqTypes` idxTys2
569 go _ _ = return ([i], False)
571 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
572 topInsts :: [Inst] -> TcM ([Inst],Bool)
574 = do { (insts,bs) <- mapAndUnzipM topInst insts
575 ; return (insts,or bs)
580 -- >--> co1 :: t ~ t' / co2 :: s ~ s'
582 -- g1 := co1 * g2 * sym co2
583 topInst :: Inst -> TcM (Inst,Bool)
584 topInst i@(EqInst {})
585 = do { (coi1,ty1') <- tcNormalizeFamInst ty1
586 ; (coi2,ty2') <- tcNormalizeFamInst ty2
587 ; case (coi1,coi2) of
591 do { wg_co <- eitherEqInst i
592 -- old_co = co1 * new_co * sym co2
594 do { new_cotv <- newMetaTyVar TauTv (mkCoKind ty1 ty2)
595 ; let new_co = TyVarTy new_cotv
596 ; let old_coi = coi1 `mkTransCoI` ACo new_co `mkTransCoI` (mkSymCoI coi2)
597 ; writeMetaTyVar old_covar (fromACo old_coi)
598 ; return $ mkWantedCo new_cotv
600 -- new_co = sym co1 * old_co * co2
601 (\old_co -> return $ mkGivenCo $ fromACo $ mkSymCoI coi1 `mkTransCoI` ACo old_co `mkTransCoI` coi2)
602 ; new_inst <- mkEqInst (EqPred ty1' ty2') wg_co
603 ; return (new_inst,True)
608 ty2 = eqInstRightTy i
610 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
611 substInsts :: [Inst] -> TcM ([Inst],Bool)
612 substInsts insts = substInstsWorker insts []
614 substInstsWorker [] acc
616 substInstsWorker (i:is) acc
617 | (TyConApp con _) <- tci_left i, isOpenSynTyCon con
618 = do { (is',change) <- substInst i (acc ++ is)
620 then return ((i:is'),True)
621 else substInstsWorker is (i:acc)
624 = substInstsWorker is (i:acc)
628 -- forall g1 : s1{F c} ~ s2{F c}
630 -- g2 : s1{t} ~ s2{t}
631 -- g1 := s1{g} * g2 * sym s2{g} <=> g2 := sym s1{g} * g1 * s2{g}
634 substInst inst@(EqInst {tci_left = pattern, tci_right = target}) (i@(EqInst {tci_left = ty1, tci_right = ty2}):is)
635 = do { (is',changed) <- substInst inst is
636 ; (coi1,ty1') <- tcGenericNormalizeFamInst fun ty1
637 ; (coi2,ty2') <- tcGenericNormalizeFamInst fun ty2
638 ; case (coi1,coi2) of
640 return (i:is',changed)
642 do { gw_co <- eitherEqInst i
643 -- old_co := co1 * new_co * sym co2
645 do { new_cotv <- newMetaTyVar TauTv (mkCoKind ty1' ty2')
646 ; let new_co = TyVarTy new_cotv
647 ; let old_coi = coi1 `mkTransCoI` ACo new_co `mkTransCoI` (mkSymCoI coi2)
648 ; writeMetaTyVar old_covar (fromACo old_coi)
649 ; return $ mkWantedCo new_cotv
651 -- new_co := sym co1 * old_co * co2
652 (\old_co -> return $ mkGivenCo $ fromACo $ (mkSymCoI coi1) `mkTransCoI` ACo old_co `mkTransCoI` coi2)
653 ; new_inst <- mkEqInst (EqPred ty1' ty2') gw_co
654 ; return (new_inst:is',True)
657 where fun ty = return $ if tcEqType pattern ty then Just (target,coercion) else Nothing
659 coercion = eitherEqInst inst TyVarTy id
660 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
662 :: [Inst] -- wanted equations
665 = do { (insts',changeds) <- mapAndUnzipM unifyInst insts
666 ; return (concat insts',or changeds)
675 -- TOMDO: you should only do this for certain `meta' type variables
676 unifyInst i@(EqInst {tci_left = ty1, tci_right = ty2})
677 | TyVarTy tv1 <- ty1, isMetaTyVar tv1 = go ty2 tv1
678 | TyVarTy tv2 <- ty2, isMetaTyVar tv2 = go ty1 tv2
679 | otherwise = return ([i],False)
681 = do { let cotv = fromWantedCo "unifyInst" $ eqInstCoercion i
682 ; writeMetaTyVar tv ty -- alpha := t
683 ; writeMetaTyVar cotv ty -- g := t
687 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
688 occursCheckInsts :: [Inst] -> TcM ()
689 occursCheckInsts insts = mappM_ occursCheckInst insts
697 occursCheckInst :: Inst -> TcM ()
698 occursCheckInst i@(EqInst {tci_left = ty1, tci_right = ty2})
701 check ty = if ty `tcEqType` ty1
705 go (TyConApp con tys) = if isOpenSynTyCon con then return () else mappM_ check tys
706 go (FunTy arg res) = mappM_ check [arg,res]
707 go (AppTy fun arg) = mappM_ check [fun,arg]
710 occursError = do { env0 <- tcInitTidyEnv
711 ; let (env1, tidy_ty1) = tidyOpenType env0 ty1
712 (env2, tidy_ty2) = tidyOpenType env1 ty2
713 extra = sep [ppr tidy_ty1, char '~', ppr tidy_ty2]
714 ; failWithTcM (env2, hang msg 2 extra)
716 where msg = ptext SLIT("Occurs check: cannot construct the infinite type")
719 Normalises a set of dictionaries relative to a set of given equalities (which
720 are interpreted as rewrite rules). We only consider given equalities of the
725 where F is a type family.
728 substEqInDictInsts :: [Inst] -- given equalities (used as rewrite rules)
729 -> [Inst] -- dictinaries to be normalised
730 -> TcM ([Inst], TcDictBinds)
731 substEqInDictInsts eq_insts insts
732 = do { traceTc (text "substEqInDictInst <-" <+> ppr insts)
733 ; result <- foldlM rewriteWithOneEquality (insts, emptyBag) eq_insts
734 ; traceTc (text "substEqInDictInst ->" <+> ppr result)
738 -- (1) Given equality of form 'F ts ~ t': use for rewriting
739 rewriteWithOneEquality (insts, dictBinds)
740 inst@(EqInst {tci_left = pattern,
742 | isOpenSynTyConApp pattern
743 = do { (insts', moreDictBinds) <- genericNormaliseInsts True {- wanted -}
745 ; return (insts', dictBinds `unionBags` moreDictBinds)
748 applyThisEq = tcGenericNormalizeFamInstPred (return . matchResult)
750 -- rewrite in case of an exact match
751 matchResult ty | tcEqType pattern ty = Just (target, eqInstType inst)
752 | otherwise = Nothing
754 -- (2) Given equality has the wrong form: ignore
755 rewriteWithOneEquality (insts, dictBinds) _not_a_rewrite_rule
756 = return (insts, dictBinds)
759 %************************************************************************
761 Normalisation of Insts
763 %************************************************************************
765 Take a bunch of Insts (not EqInsts), and normalise them wrt the top-level
766 type-function equations, where
768 (norm_insts, binds) = normaliseInsts is_wanted insts
771 = True, (binds + norm_insts) defines insts (wanteds)
772 = False, (binds + insts) defines norm_insts (givens)
775 normaliseInsts :: Bool -- True <=> wanted insts
776 -> [Inst] -- wanted or given insts
777 -> TcM ([Inst], TcDictBinds) -- normalized insts and bindings
778 normaliseInsts isWanted insts
779 = genericNormaliseInsts isWanted tcNormalizeFamInstPred insts
781 genericNormaliseInsts :: Bool -- True <=> wanted insts
782 -> (TcPredType -> TcM (CoercionI, TcPredType))
784 -> [Inst] -- wanted or given insts
785 -> TcM ([Inst], TcDictBinds) -- normalized insts & binds
786 genericNormaliseInsts isWanted fun insts
787 = do { (insts', binds) <- mapAndUnzipM (normaliseOneInst isWanted fun) insts
788 ; return (insts', unionManyBags binds)
791 normaliseOneInst isWanted fun
792 dict@(Dict {tci_name = name,
795 = do { traceTc (text "genericNormaliseInst 1")
796 ; (coi, pred') <- fun pred
797 ; traceTc (text "genericNormaliseInst 2")
800 IdCo -> return (dict, emptyBag)
801 -- don't use pred' in this case; otherwise, we get
802 -- more unfolded closed type synonyms in error messages
804 do { -- an inst for the new pred
805 ; dict' <- newDictBndr loc pred'
806 -- relate the old inst to the new one
807 -- target_dict = source_dict `cast` st_co
808 ; let (target_dict, source_dict, st_co)
809 | isWanted = (dict, dict', mkSymCoercion co)
810 | otherwise = (dict', dict, co)
812 -- co :: dict ~ dict'
813 -- hence dict = dict' `cast` sym co
815 -- co :: dict ~ dict'
816 -- hence dict' = dict `cast` co
817 expr = HsVar $ instToId source_dict
818 cast_expr = HsWrap (WpCo st_co) expr
819 rhs = L (instLocSpan loc) cast_expr
820 binds = mkBind target_dict rhs
821 -- return the new inst
822 ; return (dict', binds)
826 -- TOMDO: treat other insts appropriately
827 normaliseOneInst isWanted fun inst
828 = do { inst' <- zonkInst inst
829 ; return (inst', emptyBag)
832 addBind binds inst rhs = binds `unionBags` mkBind inst rhs
834 mkBind inst rhs = unitBag (L (instSpan inst)
835 (VarBind (instToId inst) rhs))