6 partitionWantedEqInsts, partitionGivenEqInsts,
10 normaliseGivens, normaliseGivenDicts,
11 normaliseWanteds, normaliseWantedDicts,
15 addBind -- should not be here
19 #include "HsVersions.h"
30 import TypeRep ( Type(..) )
32 import Var ( mkCoVar, isTcTyVar )
34 import HscTypes ( ExternalPackageState(..) )
37 import SrcLoc ( Located(..) )
43 %************************************************************************
47 %************************************************************************
49 %************************************************************************
51 \section{Utility Code}
53 %************************************************************************
56 partitionWantedEqInsts
57 :: [Inst] -- wanted insts
58 -> ([Inst],[Inst]) -- (wanted equations,wanted dicts)
59 partitionWantedEqInsts = partitionEqInsts True
62 :: [Inst] -- given insts
63 -> ([Inst],[Inst]) -- (given equations,given dicts)
64 partitionGivenEqInsts = partitionEqInsts False
70 -> ([Inst],[Inst]) -- (equations,dicts)
71 partitionEqInsts wanted []
73 partitionEqInsts wanted (i:is)
78 where (es,ds) = partitionEqInsts wanted is
80 isEqDict :: Inst -> Bool
81 isEqDict (Dict {tci_pred = EqPred _ _}) = True
87 %************************************************************************
89 Normalisation of types
91 %************************************************************************
93 Unfold a single synonym family instance and yield the witnessing coercion.
94 Return 'Nothing' if the given type is either not synonym family instance
95 or is a synonym family instance that has no matching instance declaration.
96 (Applies only if the type family application is outermost.)
98 For example, if we have
100 :Co:R42T a :: T [a] ~ :R42T a
102 then 'T [Int]' unfolds to (:R42T Int, :Co:R42T Int).
105 tcUnfoldSynFamInst :: Type -> TcM (Maybe (Type, Coercion))
106 tcUnfoldSynFamInst (TyConApp tycon tys)
107 | not (isOpenSynTyCon tycon) -- unfold *only* _synonym_ family instances
110 = do { maybeFamInst <- tcLookupFamInst tycon tys
111 ; case maybeFamInst of
112 Nothing -> return Nothing
113 Just (rep_tc, rep_tys) -> return $ Just (mkTyConApp rep_tc rep_tys,
114 mkTyConApp coe_tc rep_tys)
116 coe_tc = expectJust "TcTyFun.tcUnfoldSynFamInst"
117 (tyConFamilyCoercion_maybe rep_tc)
119 tcUnfoldSynFamInst _other = return Nothing
122 Normalise 'Type's and 'PredType's by unfolding type family applications where
123 possible (ie, we treat family instances as a TRS). Also zonk meta variables.
125 tcNormalizeFamInst ty = (co, ty')
129 tcNormalizeFamInst :: Type -> TcM (CoercionI, Type)
130 tcNormalizeFamInst = tcGenericNormalizeFamInst tcUnfoldSynFamInst
132 tcNormalizeFamInstPred :: TcPredType -> TcM (CoercionI, TcPredType)
133 tcNormalizeFamInstPred = tcGenericNormalizeFamInstPred tcUnfoldSynFamInst
136 Generic normalisation of 'Type's and 'PredType's; ie, walk the type term and
137 apply the normalisation function gives as the first argument to every TyConApp
138 and every TyVarTy subterm.
140 tcGenericNormalizeFamInst fun ty = (co, ty')
143 This function is (by way of using smart constructors) careful to ensure that
144 the returned coercion is exactly IdCo (and not some semantically equivalent,
145 but syntactically different coercion) whenever (ty' `tcEqType` ty). This
146 makes it easy for the caller to determine whether the type changed. BUT
147 even if we return IdCo, ty' may be *syntactically* different from ty due to
148 unfolded closed type synonyms (by way of tcCoreView). In the interest of
149 good error messages, callers should discard ty' in favour of ty in this case.
152 tcGenericNormalizeFamInst :: (TcType -> TcM (Maybe (TcType,Coercion)))
153 -- what to do with type functions and tyvars
154 -> TcType -- old type
155 -> TcM (CoercionI, Type) -- (coercion, new type)
156 tcGenericNormalizeFamInst fun ty
157 | Just ty' <- tcView ty = tcGenericNormalizeFamInst fun ty'
158 tcGenericNormalizeFamInst fun ty@(TyConApp tyCon tys)
159 = do { (cois, ntys) <- mapAndUnzipM (tcGenericNormalizeFamInst fun) tys
160 ; let tycon_coi = mkTyConAppCoI tyCon ntys cois
161 ; maybe_ty_co <- fun (TyConApp tyCon ntys) -- use normalised args!
162 ; case maybe_ty_co of
163 -- a matching family instance exists
165 do { let first_coi = mkTransCoI tycon_coi (ACo co)
166 ; (rest_coi, nty) <- tcGenericNormalizeFamInst fun ty'
167 ; let fix_coi = mkTransCoI first_coi rest_coi
168 ; return (fix_coi, nty)
170 -- no matching family instance exists
171 -- we do not do anything
172 Nothing -> return (tycon_coi, TyConApp tyCon ntys)
174 tcGenericNormalizeFamInst fun ty@(AppTy ty1 ty2)
175 = do { (coi1,nty1) <- tcGenericNormalizeFamInst fun ty1
176 ; (coi2,nty2) <- tcGenericNormalizeFamInst fun ty2
177 ; return (mkAppTyCoI nty1 coi1 nty2 coi2, AppTy nty1 nty2)
179 tcGenericNormalizeFamInst fun ty@(FunTy ty1 ty2)
180 = do { (coi1,nty1) <- tcGenericNormalizeFamInst fun ty1
181 ; (coi2,nty2) <- tcGenericNormalizeFamInst fun ty2
182 ; return (mkFunTyCoI nty1 coi1 nty2 coi2, FunTy nty1 nty2)
184 tcGenericNormalizeFamInst fun ty@(ForAllTy tyvar ty1)
185 = do { (coi,nty1) <- tcGenericNormalizeFamInst fun ty1
186 ; return (mkForAllTyCoI tyvar coi,ForAllTy tyvar nty1)
188 tcGenericNormalizeFamInst fun ty@(NoteTy note ty1)
189 = do { (coi,nty1) <- tcGenericNormalizeFamInst fun ty1
190 ; return (mkNoteTyCoI note coi,NoteTy note nty1)
192 tcGenericNormalizeFamInst fun ty@(TyVarTy tv)
194 = do { traceTc (text "tcGenericNormalizeFamInst" <+> ppr ty)
195 ; res <- lookupTcTyVar tv
198 do { maybe_ty' <- fun ty
200 Nothing -> return (IdCo, ty)
202 do { (coi2, ty'') <- tcGenericNormalizeFamInst fun ty'
203 ; return (ACo co1 `mkTransCoI` coi2, ty'')
206 IndirectTv ty' -> tcGenericNormalizeFamInst fun ty'
210 tcGenericNormalizeFamInst fun (PredTy predty)
211 = do { (coi, pred') <- tcGenericNormalizeFamInstPred fun predty
212 ; return (coi, PredTy pred') }
214 ---------------------------------
215 tcGenericNormalizeFamInstPred :: (TcType -> TcM (Maybe (TcType,Coercion)))
217 -> TcM (CoercionI, TcPredType)
219 tcGenericNormalizeFamInstPred fun (ClassP cls tys)
220 = do { (cois, tys')<- mapAndUnzipM (tcGenericNormalizeFamInst fun) tys
221 ; return (mkClassPPredCoI cls tys' cois, ClassP cls tys')
223 tcGenericNormalizeFamInstPred fun (IParam ipn ty)
224 = do { (coi, ty') <- tcGenericNormalizeFamInst fun ty
225 ; return $ (mkIParamPredCoI ipn coi, IParam ipn ty')
227 tcGenericNormalizeFamInstPred fun (EqPred ty1 ty2)
228 = do { (coi1, ty1') <- tcGenericNormalizeFamInst fun ty1
229 ; (coi2, ty2') <- tcGenericNormalizeFamInst fun ty2
230 ; return (mkEqPredCoI ty1' coi1 ty2' coi2, EqPred ty1' ty2') }
234 %************************************************************************
236 \section{Normalisation of Given Dictionaries}
238 %************************************************************************
241 normaliseGivenDicts, normaliseWantedDicts
242 :: [Inst] -- given equations
243 -> [Inst] -- dictionaries
244 -> TcM ([Inst],TcDictBinds)
246 normaliseGivenDicts eqs dicts = normalise_dicts eqs dicts False
247 normaliseWantedDicts eqs dicts = normalise_dicts eqs dicts True
250 :: [Inst] -- given equations
251 -> [Inst] -- dictionaries
252 -> Bool -- True <=> the dicts are wanted
253 -- Fals <=> they are given
254 -> TcM ([Inst],TcDictBinds)
255 normalise_dicts given_eqs dicts is_wanted
256 = do { traceTc $ text "normaliseGivenDicts <-" <+> ppr dicts <+>
257 text "with" <+> ppr given_eqs
258 ; (dicts0, binds0) <- normaliseInsts is_wanted dicts
259 ; (dicts1, binds1) <- substEqInDictInsts given_eqs dicts0
260 ; let binds01 = binds0 `unionBags` binds1
261 ; if isEmptyBag binds1
262 then return (dicts1, binds01)
263 else do { (dicts2, binds2) <- normaliseGivenDicts given_eqs dicts1
264 ; return (dicts2, binds01 `unionBags` binds2) } }
268 %************************************************************************
270 \section{Normalisation of Wanteds}
272 %************************************************************************
275 normaliseWanteds :: [Inst] -> TcM [Inst]
276 normaliseWanteds insts
277 = do { traceTc (text "normaliseWanteds" <+> ppr insts)
278 ; result <- eq_rewrite
279 [ ("(Occurs)", simple_rewrite_check $ occursCheckInsts)
280 , ("(ZONK)", simple_rewrite $ zonkInsts)
281 , ("(TRIVIAL)", trivialInsts)
282 , ("(SWAP)", swapInsts)
283 , ("(DECOMP)", decompInsts)
284 , ("(TOP)", topInsts)
285 , ("(SUBST)", substInsts)
286 , ("(UNIFY)", unifyInsts)
288 ; traceTc (text "normaliseWanteds ->" <+> ppr result)
293 %************************************************************************
295 \section{Normalisation of Givens}
297 %************************************************************************
301 normaliseGivens :: [Inst] -> TcM ([Inst],TcM ())
302 normaliseGivens givens =
303 do { traceTc (text "normaliseGivens <-" <+> ppr givens)
304 ; (result,action) <- given_eq_rewrite
305 ("(SkolemOccurs)", skolemOccurs)
307 [("(Occurs)", simple_rewrite_check $ occursCheckInsts),
308 ("(ZONK)", simple_rewrite $ zonkInsts),
309 ("(TRIVIAL)", trivialInsts),
310 ("(SWAP)", swapInsts),
311 ("(DECOMP)", decompInsts),
313 ("(SUBST)", substInsts)]
315 ; traceTc (text "normaliseGivens ->" <+> ppr result)
316 ; return (result,action)
319 skolemOccurs :: [Inst] -> TcM ([Inst],TcM ())
320 skolemOccurs [] = return ([], return ())
321 skolemOccurs (inst@(EqInst {}):insts)
322 = do { (insts',actions) <- skolemOccurs insts
323 -- check whether the current inst co :: ty1 ~ ty2 suffers
324 -- from the occurs check issue: F ty1 \in ty2
325 ; let occurs = go False ty2
328 -- if it does generate two new coercions:
329 do { skolem_var <- newMetaTyVar TauTv (typeKind ty1)
330 ; let skolem_ty = TyVarTy skolem_var
332 ; inst1 <- mkEqInst (EqPred ty1 skolem_ty) (mkGivenCo ty1)
334 ; inst2 <- mkEqInst (EqPred ty2 skolem_ty) (mkGivenCo $ fromACo $ mkSymCoI $ ACo $ fromGivenCo co)
335 -- to replace the old one
336 -- the corresponding action is
338 ; let action = writeMetaTyVar skolem_var ty1
339 ; return (inst1:inst2:insts', action >> actions)
342 return (inst:insts', actions)
345 ty1 = eqInstLeftTy inst
346 ty2 = eqInstRightTy inst
347 co = eqInstCoercion inst
348 check :: Bool -> TcType -> Bool
350 = if flag && ty1 `tcEqType` ty
354 go flag (TyConApp con tys) = or $ map (check (isOpenSynTyCon con || flag)) tys
355 go flag (FunTy arg res) = or $ map (check flag) [arg,res]
356 go flag (AppTy fun arg) = or $ map (check flag) [fun,arg]
360 %************************************************************************
362 \section{Solving of Wanteds}
364 %************************************************************************
370 TcM [Inst] -- irreducible wanteds
371 solveWanteds givens wanteds =
372 do { traceTc (text "solveWanteds <-" <+> ppr wanteds <+> text "with" <+> ppr givens)
373 ; result <- eq_rewrite
374 [("(Occurs)", simple_rewrite_check $ occursCheckInsts),
375 ("(TRIVIAL)", trivialInsts),
376 ("(DECOMP)", decompInsts),
378 ("(GIVEN)", givenInsts givens),
379 ("(UNIFY)", unifyInsts)]
381 ; traceTc (text "solveWanteds ->" <+> ppr result)
386 givenInsts :: [Inst] -> [Inst] -> TcM ([Inst],Bool)
387 givenInsts [] wanteds
388 = return (wanteds,False)
389 givenInsts (g:gs) wanteds
390 = do { (wanteds1,changed1) <- givenInsts gs wanteds
391 ; (wanteds2,changed2) <- substInst g wanteds1
392 ; return (wanteds2,changed1 || changed2)
397 -- fixpoint computation
398 -- of a number of rewrites of equalities
400 [(String,[Inst] -> TcM ([Inst],Bool))] -> -- rewrite functions and descriptions
401 [Inst] -> -- initial equations
402 TcM [Inst] -- final equations (at fixed point)
403 eq_rewrite rewrites insts
406 go _ [] -- return quickly when there's nothing to be done
410 go ((desc,r):rs) insts
411 = do { (insts',changed) <- r insts
412 ; traceTc (text desc <+> ppr insts')
417 loop = eq_rewrite rewrites
419 -- fixpoint computation
420 -- of a number of rewrites of equalities
423 (String,[Inst] -> TcM ([Inst],TcM ())) ->
425 [(String,[Inst] -> TcM ([Inst],Bool))] -> -- rewrite functions and descriptions
426 [Inst] -> -- initial equations
427 TcM ([Inst],TcM ()) -- final equations (at fixed point)
428 given_eq_rewrite p@(desc,start) acc rewrites insts
429 = do { (insts',acc') <- start insts
430 ; go (acc >> acc') rewrites insts'
433 go acc _ [] -- return quickly when there's nothing to be done
437 go acc ((desc,r):rs) insts
438 = do { (insts',changed) <- r insts
439 ; traceTc (text desc <+> ppr insts')
442 else go acc rs insts'
444 loop acc = given_eq_rewrite p acc rewrites
447 ([Inst] -> TcM [Inst]) ->
448 ([Inst] -> TcM ([Inst],Bool))
449 simple_rewrite r insts
450 = do { insts' <- r insts
451 ; return (insts',False)
454 simple_rewrite_check ::
455 ([Inst] -> TcM ()) ->
456 ([Inst] -> TcM ([Inst],Bool))
457 simple_rewrite_check check insts
458 = check insts >> return (insts,False)
463 %************************************************************************
465 \section{Different forms of Inst rewritings}
467 %************************************************************************
469 Rewrite schemata applied by way of eq_rewrite and friends.
479 [Inst] -> -- equations
480 TcM ([Inst],Bool) -- remaining equations, any changes?
483 trivialInsts (i@(EqInst {}):is)
484 = do { (is',changed)<- trivialInsts is
485 ; if tcEqType ty1 ty2
486 then do { eitherEqInst i
487 (\covar -> writeMetaTyVar covar ty1)
491 else return (i:is',changed)
495 ty2 = eqInstRightTy i
497 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
498 swapInsts :: [Inst] -> TcM ([Inst],Bool)
499 -- All the inputs and outputs are equalities
500 swapInsts insts = mapAndUnzipM swapInst insts >>= \(insts',changeds) -> return (insts',or changeds)
509 swapInst i@(EqInst {})
513 ty2 = eqInstRightTy i
514 go ty1 ty2 | Just ty1' <- tcView ty1
516 go ty1 ty2 | Just ty2' <- tcView ty2
518 go (TyConApp tyCon _) _ | isOpenSynTyCon tyCon
521 go ty1 ty2@(TyConApp tyCon _)
522 | isOpenSynTyCon tyCon
523 = do { wg_co <- eitherEqInst i
524 -- old_co := sym new_co
526 do { new_cotv <- newMetaTyVar TauTv (mkCoKind ty2 ty1)
527 ; let new_co = TyVarTy new_cotv
528 ; writeMetaTyVar old_covar (mkCoercion symCoercionTyCon [new_co])
529 ; return $ mkWantedCo new_cotv
531 -- new_co := sym old_co
532 (\old_co -> return $ mkGivenCo $ mkCoercion symCoercionTyCon [old_co])
533 ; new_inst <- mkEqInst (EqPred ty2 ty1) wg_co
534 ; return (new_inst,True)
536 go _ _ = return (i,False)
538 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
539 decompInsts :: [Inst] -> TcM ([Inst],Bool)
540 decompInsts insts = do { (insts,bs) <- mapAndUnzipM decompInst insts
541 ; return (concat insts,or bs)
547 -- g21 : c1 ~ d1, ..., g2n : cn ~ dn
550 -- Works also for the case where T is actually an application of a
551 -- type family constructor to a set of types, provided the
552 -- applications on both sides of the ~ are identical;
553 -- see also Note [OpenSynTyCon app] in TcUnify
555 decompInst :: Inst -> TcM ([Inst],Bool)
556 decompInst i@(EqInst {})
560 ty2 = eqInstRightTy i
562 | Just ty1' <- tcView ty1 = go ty1' ty2
563 | Just ty2' <- tcView ty2 = go ty1 ty2'
565 go ty1@(TyConApp con1 tys1) ty2@(TyConApp con2 tys2)
566 | con1 == con2 && identicalHead
567 = do { cos <- eitherEqInst i
568 -- old_co := Con1 cos
570 do { cotvs <- zipWithM (\t1 t2 ->
574 ; let cos = map TyVarTy cotvs
575 ; writeMetaTyVar old_covar (TyConApp con1 cos)
576 ; return $ map mkWantedCo cotvs
578 -- co_i := Con_i old_co
581 mkRightCoercions (length tys1') old_co)
582 ; insts <- zipWithM mkEqInst (zipWith EqPred tys1' tys2') cos
583 ; return (insts, not $ null insts)
585 | con1 /= con2 && not (isOpenSynTyCon con1 || isOpenSynTyCon con2)
586 -- not matching data constructors (of any flavour) are bad news
587 = do { env0 <- tcInitTidyEnv
588 ; let (env1, tidy_ty1) = tidyOpenType env0 ty1
589 (env2, tidy_ty2) = tidyOpenType env1 ty2
590 extra = sep [ppr tidy_ty1, char '~', ppr tidy_ty2]
591 msg = ptext SLIT("Couldn't match expected type against inferred type")
592 ; failWithTcM (env2, hang msg 2 extra)
596 (idxTys1, tys1') = splitAt n tys1
597 (idxTys2, tys2') = splitAt n tys2
598 identicalHead = not (isOpenSynTyCon con1) ||
599 idxTys1 `tcEqTypes` idxTys2
601 go _ _ = return ([i], False)
603 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
604 topInsts :: [Inst] -> TcM ([Inst],Bool)
606 = do { (insts,bs) <- mapAndUnzipM topInst insts
607 ; return (insts,or bs)
612 -- >--> co1 :: t ~ t' / co2 :: s ~ s'
614 -- g1 := co1 * g2 * sym co2
615 topInst :: Inst -> TcM (Inst,Bool)
616 topInst i@(EqInst {})
617 = do { (coi1,ty1') <- tcNormalizeFamInst ty1
618 ; (coi2,ty2') <- tcNormalizeFamInst ty2
619 ; case (coi1,coi2) of
623 do { wg_co <- eitherEqInst i
624 -- old_co = co1 * new_co * sym co2
626 do { new_cotv <- newMetaTyVar TauTv (mkCoKind ty1 ty2)
627 ; let new_co = TyVarTy new_cotv
628 ; let old_coi = coi1 `mkTransCoI` ACo new_co `mkTransCoI` (mkSymCoI coi2)
629 ; writeMetaTyVar old_covar (fromACo old_coi)
630 ; return $ mkWantedCo new_cotv
632 -- new_co = sym co1 * old_co * co2
633 (\old_co -> return $ mkGivenCo $ fromACo $ mkSymCoI coi1 `mkTransCoI` ACo old_co `mkTransCoI` coi2)
634 ; new_inst <- mkEqInst (EqPred ty1' ty2') wg_co
635 ; return (new_inst,True)
640 ty2 = eqInstRightTy i
642 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
643 substInsts :: [Inst] -> TcM ([Inst],Bool)
644 substInsts insts = substInstsWorker insts []
646 substInstsWorker [] acc
648 substInstsWorker (i:is) acc
649 | (TyConApp con _) <- tci_left i, isOpenSynTyCon con
650 = do { (is',change) <- substInst i (acc ++ is)
652 then return ((i:is'),True)
653 else substInstsWorker is (i:acc)
656 = substInstsWorker is (i:acc)
660 -- forall g1 : s1{F c} ~ s2{F c}
662 -- g2 : s1{t} ~ s2{t}
663 -- g1 := s1{g} * g2 * sym s2{g} <=> g2 := sym s1{g} * g1 * s2{g}
666 substInst inst@(EqInst {tci_left = pattern, tci_right = target}) (i@(EqInst {tci_left = ty1, tci_right = ty2}):is)
667 = do { (is',changed) <- substInst inst is
668 ; (coi1,ty1') <- tcGenericNormalizeFamInst fun ty1
669 ; (coi2,ty2') <- tcGenericNormalizeFamInst fun ty2
670 ; case (coi1,coi2) of
672 return (i:is',changed)
674 do { gw_co <- eitherEqInst i
675 -- old_co := co1 * new_co * sym co2
677 do { new_cotv <- newMetaTyVar TauTv (mkCoKind ty1' ty2')
678 ; let new_co = TyVarTy new_cotv
679 ; let old_coi = coi1 `mkTransCoI` ACo new_co `mkTransCoI` (mkSymCoI coi2)
680 ; writeMetaTyVar old_covar (fromACo old_coi)
681 ; return $ mkWantedCo new_cotv
683 -- new_co := sym co1 * old_co * co2
684 (\old_co -> return $ mkGivenCo $ fromACo $ (mkSymCoI coi1) `mkTransCoI` ACo old_co `mkTransCoI` coi2)
685 ; new_inst <- mkEqInst (EqPred ty1' ty2') gw_co
686 ; return (new_inst:is',True)
689 where fun ty = return $ if tcEqType pattern ty then Just (target,coercion) else Nothing
691 coercion = eitherEqInst inst TyVarTy id
692 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
694 :: [Inst] -- wanted equations
697 = do { (insts',changeds) <- mapAndUnzipM unifyInst insts
698 ; return (concat insts',or changeds)
707 -- TOMDO: you should only do this for certain `meta' type variables
708 unifyInst i@(EqInst {tci_left = ty1, tci_right = ty2})
709 | TyVarTy tv1 <- ty1, isMetaTyVar tv1 = go ty2 tv1
710 | TyVarTy tv2 <- ty2, isMetaTyVar tv2 = go ty1 tv2
711 | otherwise = return ([i],False)
713 = do { let cotv = fromWantedCo "unifyInst" $ eqInstCoercion i
714 ; writeMetaTyVar tv ty -- alpha := t
715 ; writeMetaTyVar cotv ty -- g := t
719 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
720 occursCheckInsts :: [Inst] -> TcM ()
721 occursCheckInsts insts = mappM_ occursCheckInst insts
729 occursCheckInst :: Inst -> TcM ()
730 occursCheckInst i@(EqInst {tci_left = ty1, tci_right = ty2})
733 check ty = if ty `tcEqType` ty1
737 go (TyConApp con tys) = if isOpenSynTyCon con then return () else mappM_ check tys
738 go (FunTy arg res) = mappM_ check [arg,res]
739 go (AppTy fun arg) = mappM_ check [fun,arg]
742 occursError = do { env0 <- tcInitTidyEnv
743 ; let (env1, tidy_ty1) = tidyOpenType env0 ty1
744 (env2, tidy_ty2) = tidyOpenType env1 ty2
745 extra = sep [ppr tidy_ty1, char '~', ppr tidy_ty2]
746 ; failWithTcM (env2, hang msg 2 extra)
748 where msg = ptext SLIT("Occurs check: cannot construct the infinite type")
751 Normalises a set of dictionaries relative to a set of given equalities (which
752 are interpreted as rewrite rules). We only consider given equalities of the
757 where F is a type family.
760 substEqInDictInsts :: [Inst] -- given equalities (used as rewrite rules)
761 -> [Inst] -- dictinaries to be normalised
762 -> TcM ([Inst], TcDictBinds)
763 substEqInDictInsts eq_insts insts
764 = do { traceTc (text "substEqInDictInst <-" <+> ppr insts)
765 ; result <- foldlM rewriteWithOneEquality (insts, emptyBag) eq_insts
766 ; traceTc (text "substEqInDictInst ->" <+> ppr result)
770 -- (1) Given equality of form 'F ts ~ t': use for rewriting
771 rewriteWithOneEquality (insts, dictBinds)
772 inst@(EqInst {tci_left = pattern,
774 | isOpenSynTyConApp pattern
775 = do { (insts', moreDictBinds) <- genericNormaliseInsts True {- wanted -}
777 ; return (insts', dictBinds `unionBags` moreDictBinds)
780 applyThisEq = tcGenericNormalizeFamInstPred (return . matchResult)
782 -- rewrite in case of an exact match
783 matchResult ty | tcEqType pattern ty = Just (target, eqInstType inst)
784 | otherwise = Nothing
786 -- (2) Given equality has the wrong form: ignore
787 rewriteWithOneEquality (insts, dictBinds) _not_a_rewrite_rule
788 = return (insts, dictBinds)
791 %************************************************************************
793 Normalisation of Insts
795 %************************************************************************
797 Take a bunch of Insts (not EqInsts), and normalise them wrt the top-level
798 type-function equations, where
800 (norm_insts, binds) = normaliseInsts is_wanted insts
803 = True, (binds + norm_insts) defines insts (wanteds)
804 = False, (binds + insts) defines norm_insts (givens)
807 normaliseInsts :: Bool -- True <=> wanted insts
808 -> [Inst] -- wanted or given insts
809 -> TcM ([Inst], TcDictBinds) -- normalized insts and bindings
810 normaliseInsts isWanted insts
811 = genericNormaliseInsts isWanted tcNormalizeFamInstPred insts
813 genericNormaliseInsts :: Bool -- True <=> wanted insts
814 -> (TcPredType -> TcM (CoercionI, TcPredType))
816 -> [Inst] -- wanted or given insts
817 -> TcM ([Inst], TcDictBinds) -- normalized insts & binds
818 genericNormaliseInsts isWanted fun insts
819 = do { (insts', binds) <- mapAndUnzipM (normaliseOneInst isWanted fun) insts
820 ; return (insts', unionManyBags binds)
823 normaliseOneInst isWanted fun
824 dict@(Dict {tci_name = name,
827 = do { traceTc (text "genericNormaliseInst 1")
828 ; (coi, pred') <- fun pred
829 ; traceTc (text "genericNormaliseInst 2")
832 IdCo -> return (dict, emptyBag)
833 -- don't use pred' in this case; otherwise, we get
834 -- more unfolded closed type synonyms in error messages
836 do { -- an inst for the new pred
837 ; dict' <- newDictBndr loc pred'
838 -- relate the old inst to the new one
839 -- target_dict = source_dict `cast` st_co
840 ; let (target_dict, source_dict, st_co)
841 | isWanted = (dict, dict', mkSymCoercion co)
842 | otherwise = (dict', dict, co)
844 -- co :: dict ~ dict'
845 -- hence dict = dict' `cast` sym co
847 -- co :: dict ~ dict'
848 -- hence dict' = dict `cast` co
849 expr = HsVar $ instToId source_dict
850 cast_expr = HsWrap (WpCo st_co) expr
851 rhs = L (instLocSpan loc) cast_expr
852 binds = mkBind target_dict rhs
853 -- return the new inst
854 ; return (dict', binds)
858 -- TOMDO: treat other insts appropriately
859 normaliseOneInst isWanted fun inst
860 = do { inst' <- zonkInst inst
861 ; return (inst', emptyBag)
864 addBind binds inst rhs = binds `unionBags` mkBind inst rhs
866 mkBind inst rhs = unitBag (L (instSpan inst)
867 (VarBind (instToId inst) rhs))