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/CodingStyle#Warnings
12 partitionWantedEqInsts, partitionGivenEqInsts,
16 normaliseGivens, normaliseGivenDicts,
17 normaliseWanteds, normaliseWantedDicts,
21 addBind -- should not be here
25 #include "HsVersions.h"
36 import TypeRep ( Type(..) )
38 import Var ( mkCoVar, isTcTyVar )
40 import HscTypes ( ExternalPackageState(..) )
43 import SrcLoc ( Located(..) )
49 %************************************************************************
53 %************************************************************************
55 %************************************************************************
57 \section{Utility Code}
59 %************************************************************************
62 partitionWantedEqInsts
63 :: [Inst] -- wanted insts
64 -> ([Inst],[Inst]) -- (wanted equations,wanted dicts)
65 partitionWantedEqInsts = partitionEqInsts True
68 :: [Inst] -- given insts
69 -> ([Inst],[Inst]) -- (given equations,given dicts)
70 partitionGivenEqInsts = partitionEqInsts False
76 -> ([Inst],[Inst]) -- (equations,dicts)
77 partitionEqInsts wanted []
79 partitionEqInsts wanted (i:is)
84 where (es,ds) = partitionEqInsts wanted is
86 isEqDict :: Inst -> Bool
87 isEqDict (Dict {tci_pred = EqPred _ _}) = True
93 %************************************************************************
95 Normalisation of types
97 %************************************************************************
99 Unfold a single synonym family instance and yield the witnessing coercion.
100 Return 'Nothing' if the given type is either not synonym family instance
101 or is a synonym family instance that has no matching instance declaration.
102 (Applies only if the type family application is outermost.)
104 For example, if we have
106 :Co:R42T a :: T [a] ~ :R42T a
108 then 'T [Int]' unfolds to (:R42T Int, :Co:R42T Int).
111 tcUnfoldSynFamInst :: Type -> TcM (Maybe (Type, Coercion))
112 tcUnfoldSynFamInst (TyConApp tycon tys)
113 | not (isOpenSynTyCon tycon) -- unfold *only* _synonym_ family instances
116 = do { maybeFamInst <- tcLookupFamInst tycon tys
117 ; case maybeFamInst of
118 Nothing -> return Nothing
119 Just (rep_tc, rep_tys) -> return $ Just (mkTyConApp rep_tc rep_tys,
120 mkTyConApp coe_tc rep_tys)
122 coe_tc = expectJust "TcTyFun.tcUnfoldSynFamInst"
123 (tyConFamilyCoercion_maybe rep_tc)
125 tcUnfoldSynFamInst _other = return Nothing
128 Normalise 'Type's and 'PredType's by unfolding type family applications where
129 possible (ie, we treat family instances as a TRS). Also zonk meta variables.
131 tcNormalizeFamInst ty = (co, ty')
135 tcNormalizeFamInst :: Type -> TcM (CoercionI, Type)
136 tcNormalizeFamInst = tcGenericNormalizeFamInst tcUnfoldSynFamInst
138 tcNormalizeFamInstPred :: TcPredType -> TcM (CoercionI, TcPredType)
139 tcNormalizeFamInstPred = tcGenericNormalizeFamInstPred tcUnfoldSynFamInst
142 Generic normalisation of 'Type's and 'PredType's; ie, walk the type term and
143 apply the normalisation function gives as the first argument to every TyConApp
144 and every TyVarTy subterm.
146 tcGenericNormalizeFamInst fun ty = (co, ty')
149 This function is (by way of using smart constructors) careful to ensure that
150 the returned coercion is exactly IdCo (and not some semantically equivalent,
151 but syntactically different coercion) whenever (ty' `tcEqType` ty). This
152 makes it easy for the caller to determine whether the type changed. BUT
153 even if we return IdCo, ty' may be *syntactically* different from ty due to
154 unfolded closed type synonyms (by way of tcCoreView). In the interest of
155 good error messages, callers should discard ty' in favour of ty in this case.
158 tcGenericNormalizeFamInst :: (TcType -> TcM (Maybe (TcType,Coercion)))
159 -- what to do with type functions and tyvars
160 -> TcType -- old type
161 -> TcM (CoercionI, Type) -- (coercion, new type)
162 tcGenericNormalizeFamInst fun ty
163 | Just ty' <- tcView ty = tcGenericNormalizeFamInst fun ty'
164 tcGenericNormalizeFamInst fun ty@(TyConApp tyCon tys)
165 = do { (cois, ntys) <- mapAndUnzipM (tcGenericNormalizeFamInst fun) tys
166 ; let tycon_coi = mkTyConAppCoI tyCon ntys cois
167 ; maybe_ty_co <- fun (TyConApp tyCon ntys) -- use normalised args!
168 ; case maybe_ty_co of
169 -- a matching family instance exists
171 do { let first_coi = mkTransCoI tycon_coi (ACo co)
172 ; (rest_coi, nty) <- tcGenericNormalizeFamInst fun ty'
173 ; let fix_coi = mkTransCoI first_coi rest_coi
174 ; return (fix_coi, nty)
176 -- no matching family instance exists
177 -- we do not do anything
178 Nothing -> return (tycon_coi, TyConApp tyCon ntys)
180 tcGenericNormalizeFamInst fun ty@(AppTy ty1 ty2)
181 = do { (coi1,nty1) <- tcGenericNormalizeFamInst fun ty1
182 ; (coi2,nty2) <- tcGenericNormalizeFamInst fun ty2
183 ; return (mkAppTyCoI nty1 coi1 nty2 coi2, AppTy nty1 nty2)
185 tcGenericNormalizeFamInst fun ty@(FunTy ty1 ty2)
186 = do { (coi1,nty1) <- tcGenericNormalizeFamInst fun ty1
187 ; (coi2,nty2) <- tcGenericNormalizeFamInst fun ty2
188 ; return (mkFunTyCoI nty1 coi1 nty2 coi2, FunTy nty1 nty2)
190 tcGenericNormalizeFamInst fun ty@(ForAllTy tyvar ty1)
191 = do { (coi,nty1) <- tcGenericNormalizeFamInst fun ty1
192 ; return (mkForAllTyCoI tyvar coi,ForAllTy tyvar nty1)
194 tcGenericNormalizeFamInst fun ty@(NoteTy note ty1)
195 = do { (coi,nty1) <- tcGenericNormalizeFamInst fun ty1
196 ; return (mkNoteTyCoI note coi,NoteTy note nty1)
198 tcGenericNormalizeFamInst fun ty@(TyVarTy tv)
200 = do { traceTc (text "tcGenericNormalizeFamInst" <+> ppr ty)
201 ; res <- lookupTcTyVar tv
204 do { maybe_ty' <- fun ty
206 Nothing -> return (IdCo, ty)
208 do { (coi2, ty'') <- tcGenericNormalizeFamInst fun ty'
209 ; return (ACo co1 `mkTransCoI` coi2, ty'')
212 IndirectTv ty' -> tcGenericNormalizeFamInst fun ty'
216 tcGenericNormalizeFamInst fun (PredTy predty)
217 = do { (coi, pred') <- tcGenericNormalizeFamInstPred fun predty
218 ; return (coi, PredTy pred') }
220 ---------------------------------
221 tcGenericNormalizeFamInstPred :: (TcType -> TcM (Maybe (TcType,Coercion)))
223 -> TcM (CoercionI, TcPredType)
225 tcGenericNormalizeFamInstPred fun (ClassP cls tys)
226 = do { (cois, tys')<- mapAndUnzipM (tcGenericNormalizeFamInst fun) tys
227 ; return (mkClassPPredCoI cls tys' cois, ClassP cls tys')
229 tcGenericNormalizeFamInstPred fun (IParam ipn ty)
230 = do { (coi, ty') <- tcGenericNormalizeFamInst fun ty
231 ; return $ (mkIParamPredCoI ipn coi, IParam ipn ty')
233 tcGenericNormalizeFamInstPred fun (EqPred ty1 ty2)
234 = do { (coi1, ty1') <- tcGenericNormalizeFamInst fun ty1
235 ; (coi2, ty2') <- tcGenericNormalizeFamInst fun ty2
236 ; return (mkEqPredCoI ty1' coi1 ty2' coi2, EqPred ty1' ty2') }
240 %************************************************************************
242 \section{Normalisation of Given Dictionaries}
244 %************************************************************************
247 normaliseGivenDicts, normaliseWantedDicts
248 :: [Inst] -- given equations
249 -> [Inst] -- dictionaries
250 -> TcM ([Inst],TcDictBinds)
252 normaliseGivenDicts eqs dicts = normalise_dicts eqs dicts False
253 normaliseWantedDicts eqs dicts = normalise_dicts eqs dicts True
256 :: [Inst] -- given equations
257 -> [Inst] -- dictionaries
258 -> Bool -- True <=> the dicts are wanted
259 -- Fals <=> they are given
260 -> TcM ([Inst],TcDictBinds)
261 normalise_dicts given_eqs dicts is_wanted
262 = do { traceTc $ text "normaliseGivenDicts <-" <+> ppr dicts <+>
263 text "with" <+> ppr given_eqs
264 ; (dicts0, binds0) <- normaliseInsts is_wanted dicts
265 ; (dicts1, binds1) <- substEqInDictInsts given_eqs dicts0
266 ; let binds01 = binds0 `unionBags` binds1
267 ; if isEmptyBag binds1
268 then return (dicts1, binds01)
269 else do { (dicts2, binds2) <- normaliseGivenDicts given_eqs dicts1
270 ; return (dicts2, binds01 `unionBags` binds2) } }
274 %************************************************************************
276 \section{Normalisation of Wanteds}
278 %************************************************************************
281 normaliseWanteds :: [Inst] -> TcM [Inst]
282 normaliseWanteds insts
283 = do { traceTc (text "normaliseWanteds" <+> ppr insts)
284 ; result <- eq_rewrite
285 [ ("(Occurs)", simple_rewrite_check $ occursCheckInsts)
286 , ("(ZONK)", simple_rewrite $ zonkInsts)
287 , ("(TRIVIAL)", trivialInsts)
288 , ("(SWAP)", swapInsts)
289 , ("(DECOMP)", decompInsts)
290 , ("(TOP)", topInsts)
291 , ("(SUBST)", substInsts)
292 , ("(UNIFY)", unifyInsts)
294 ; traceTc (text "normaliseWanteds ->" <+> ppr result)
299 %************************************************************************
301 \section{Normalisation of Givens}
303 %************************************************************************
307 normaliseGivens :: [Inst] -> TcM ([Inst],TcM ())
308 normaliseGivens givens =
309 do { traceTc (text "normaliseGivens <-" <+> ppr givens)
310 ; (result,action) <- given_eq_rewrite
311 ("(SkolemOccurs)", skolemOccurs)
313 [("(Occurs)", simple_rewrite_check $ occursCheckInsts),
314 ("(ZONK)", simple_rewrite $ zonkInsts),
315 ("(TRIVIAL)", trivialInsts),
316 ("(SWAP)", swapInsts),
317 ("(DECOMP)", decompInsts),
319 ("(SUBST)", substInsts)]
321 ; traceTc (text "normaliseGivens ->" <+> ppr result)
322 ; return (result,action)
325 skolemOccurs :: [Inst] -> TcM ([Inst],TcM ())
326 skolemOccurs [] = return ([], return ())
327 skolemOccurs (inst@(EqInst {}):insts)
328 = do { (insts',actions) <- skolemOccurs insts
329 -- check whether the current inst co :: ty1 ~ ty2 suffers
330 -- from the occurs check issue: F ty1 \in ty2
331 ; let occurs = go False ty2
334 -- if it does generate two new coercions:
335 do { skolem_var <- newMetaTyVar TauTv (typeKind ty1)
336 ; let skolem_ty = TyVarTy skolem_var
338 ; inst1 <- mkEqInst (EqPred ty1 skolem_ty) (mkGivenCo ty1)
340 ; inst2 <- mkEqInst (EqPred ty2 skolem_ty) (mkGivenCo $ fromACo $ mkSymCoI $ ACo $ fromGivenCo co)
341 -- to replace the old one
342 -- the corresponding action is
344 ; let action = writeMetaTyVar skolem_var ty1
345 ; return (inst1:inst2:insts', action >> actions)
348 return (inst:insts', actions)
351 ty1 = eqInstLeftTy inst
352 ty2 = eqInstRightTy inst
353 co = eqInstCoercion inst
354 check :: Bool -> TcType -> Bool
356 = if flag && ty1 `tcEqType` ty
360 go flag (TyConApp con tys) = or $ map (check (isOpenSynTyCon con || flag)) tys
361 go flag (FunTy arg res) = or $ map (check flag) [arg,res]
362 go flag (AppTy fun arg) = or $ map (check flag) [fun,arg]
366 %************************************************************************
368 \section{Solving of Wanteds}
370 %************************************************************************
376 TcM [Inst] -- irreducible wanteds
377 solveWanteds givens wanteds =
378 do { traceTc (text "solveWanteds <-" <+> ppr wanteds <+> text "with" <+> ppr givens)
379 ; result <- eq_rewrite
380 [("(Occurs)", simple_rewrite_check $ occursCheckInsts),
381 ("(TRIVIAL)", trivialInsts),
382 ("(DECOMP)", decompInsts),
384 ("(GIVEN)", givenInsts givens),
385 ("(UNIFY)", unifyInsts)]
387 ; traceTc (text "solveWanteds ->" <+> ppr result)
392 givenInsts :: [Inst] -> [Inst] -> TcM ([Inst],Bool)
393 givenInsts [] wanteds
394 = return (wanteds,False)
395 givenInsts (g:gs) wanteds
396 = do { (wanteds1,changed1) <- givenInsts gs wanteds
397 ; (wanteds2,changed2) <- substInst g wanteds1
398 ; return (wanteds2,changed1 || changed2)
403 -- fixpoint computation
404 -- of a number of rewrites of equalities
406 [(String,[Inst] -> TcM ([Inst],Bool))] -> -- rewrite functions and descriptions
407 [Inst] -> -- initial equations
408 TcM [Inst] -- final equations (at fixed point)
409 eq_rewrite rewrites insts
412 go _ [] -- return quickly when there's nothing to be done
416 go ((desc,r):rs) insts
417 = do { (insts',changed) <- r insts
418 ; traceTc (text desc <+> ppr insts')
423 loop = eq_rewrite rewrites
425 -- fixpoint computation
426 -- of a number of rewrites of equalities
429 (String,[Inst] -> TcM ([Inst],TcM ())) ->
431 [(String,[Inst] -> TcM ([Inst],Bool))] -> -- rewrite functions and descriptions
432 [Inst] -> -- initial equations
433 TcM ([Inst],TcM ()) -- final equations (at fixed point)
434 given_eq_rewrite p@(desc,start) acc rewrites insts
435 = do { (insts',acc') <- start insts
436 ; go (acc >> acc') rewrites insts'
439 go acc _ [] -- return quickly when there's nothing to be done
443 go acc ((desc,r):rs) insts
444 = do { (insts',changed) <- r insts
445 ; traceTc (text desc <+> ppr insts')
448 else go acc rs insts'
450 loop acc = given_eq_rewrite p acc rewrites
453 ([Inst] -> TcM [Inst]) ->
454 ([Inst] -> TcM ([Inst],Bool))
455 simple_rewrite r insts
456 = do { insts' <- r insts
457 ; return (insts',False)
460 simple_rewrite_check ::
461 ([Inst] -> TcM ()) ->
462 ([Inst] -> TcM ([Inst],Bool))
463 simple_rewrite_check check insts
464 = check insts >> return (insts,False)
469 %************************************************************************
471 \section{Different forms of Inst rewritings}
473 %************************************************************************
475 Rewrite schemata applied by way of eq_rewrite and friends.
485 [Inst] -> -- equations
486 TcM ([Inst],Bool) -- remaining equations, any changes?
489 trivialInsts (i@(EqInst {}):is)
490 = do { (is',changed)<- trivialInsts is
491 ; if tcEqType ty1 ty2
492 then do { eitherEqInst i
493 (\covar -> writeMetaTyVar covar ty1)
497 else return (i:is',changed)
501 ty2 = eqInstRightTy i
503 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
504 swapInsts :: [Inst] -> TcM ([Inst],Bool)
505 -- All the inputs and outputs are equalities
506 swapInsts insts = mapAndUnzipM swapInst insts >>= \(insts',changeds) -> return (insts',or changeds)
515 swapInst i@(EqInst {})
519 ty2 = eqInstRightTy i
520 go ty1 ty2 | Just ty1' <- tcView ty1
522 go ty1 ty2 | Just ty2' <- tcView ty2
524 go (TyConApp tyCon _) _ | isOpenSynTyCon tyCon
527 go ty1 ty2@(TyConApp tyCon _)
528 | isOpenSynTyCon tyCon
529 = do { wg_co <- eitherEqInst i
530 -- old_co := sym new_co
532 do { new_cotv <- newMetaTyVar TauTv (mkCoKind ty2 ty1)
533 ; let new_co = TyVarTy new_cotv
534 ; writeMetaTyVar old_covar (mkCoercion symCoercionTyCon [new_co])
535 ; return $ mkWantedCo new_cotv
537 -- new_co := sym old_co
538 (\old_co -> return $ mkGivenCo $ mkCoercion symCoercionTyCon [old_co])
539 ; new_inst <- mkEqInst (EqPred ty2 ty1) wg_co
540 ; return (new_inst,True)
542 go _ _ = return (i,False)
544 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
545 decompInsts :: [Inst] -> TcM ([Inst],Bool)
546 decompInsts insts = do { (insts,bs) <- mapAndUnzipM decompInst insts
547 ; return (concat insts,or bs)
553 -- g21 : c1 ~ d1, ..., g2n : cn ~ dn
556 -- Works also for the case where T is actually an application of a
557 -- type family constructor to a set of types, provided the
558 -- applications on both sides of the ~ are identical;
559 -- see also Note [OpenSynTyCon app] in TcUnify
561 decompInst :: Inst -> TcM ([Inst],Bool)
562 decompInst i@(EqInst {})
566 ty2 = eqInstRightTy i
568 | Just ty1' <- tcView ty1 = go ty1' ty2
569 | Just ty2' <- tcView ty2 = go ty1 ty2'
571 go ty1@(TyConApp con1 tys1) ty2@(TyConApp con2 tys2)
572 | con1 == con2 && identicalHead
573 = do { cos <- eitherEqInst i
574 -- old_co := Con1 cos
576 do { cotvs <- zipWithM (\t1 t2 ->
580 ; let cos = map TyVarTy cotvs
581 ; writeMetaTyVar old_covar (TyConApp con1 cos)
582 ; return $ map mkWantedCo cotvs
584 -- co_i := Con_i old_co
587 mkRightCoercions (length tys1') old_co)
588 ; insts <- zipWithM mkEqInst (zipWith EqPred tys1' tys2') cos
589 ; return (insts, not $ null insts)
591 | con1 /= con2 && not (isOpenSynTyCon con1 || isOpenSynTyCon con2)
592 -- not matching data constructors (of any flavour) are bad news
593 = do { env0 <- tcInitTidyEnv
594 ; let (env1, tidy_ty1) = tidyOpenType env0 ty1
595 (env2, tidy_ty2) = tidyOpenType env1 ty2
596 extra = sep [ppr tidy_ty1, char '~', ppr tidy_ty2]
598 ptext SLIT("Unsolvable equality constraint:")
599 ; failWithTcM (env2, hang msg 2 extra)
603 (idxTys1, tys1') = splitAt n tys1
604 (idxTys2, tys2') = splitAt n tys2
605 identicalHead = not (isOpenSynTyCon con1) ||
606 idxTys1 `tcEqTypes` idxTys2
608 go _ _ = return ([i], False)
610 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
611 topInsts :: [Inst] -> TcM ([Inst],Bool)
613 = do { (insts,bs) <- mapAndUnzipM topInst insts
614 ; return (insts,or bs)
619 -- >--> co1 :: t ~ t' / co2 :: s ~ s'
621 -- g1 := co1 * g2 * sym co2
622 topInst :: Inst -> TcM (Inst,Bool)
623 topInst i@(EqInst {})
624 = do { (coi1,ty1') <- tcNormalizeFamInst ty1
625 ; (coi2,ty2') <- tcNormalizeFamInst ty2
626 ; case (coi1,coi2) of
630 do { wg_co <- eitherEqInst i
631 -- old_co = co1 * new_co * sym co2
633 do { new_cotv <- newMetaTyVar TauTv (mkCoKind ty1 ty2)
634 ; let new_co = TyVarTy new_cotv
635 ; let old_coi = coi1 `mkTransCoI` ACo new_co `mkTransCoI` (mkSymCoI coi2)
636 ; writeMetaTyVar old_covar (fromACo old_coi)
637 ; return $ mkWantedCo new_cotv
639 -- new_co = sym co1 * old_co * co2
640 (\old_co -> return $ mkGivenCo $ fromACo $ mkSymCoI coi1 `mkTransCoI` ACo old_co `mkTransCoI` coi2)
641 ; new_inst <- mkEqInst (EqPred ty1' ty2') wg_co
642 ; return (new_inst,True)
647 ty2 = eqInstRightTy i
649 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
650 substInsts :: [Inst] -> TcM ([Inst],Bool)
651 substInsts insts = substInstsWorker insts []
653 substInstsWorker [] acc
655 substInstsWorker (i:is) acc
656 | (TyConApp con _) <- tci_left i, isOpenSynTyCon con
657 = do { (is',change) <- substInst i (acc ++ is)
659 then return ((i:is'),True)
660 else substInstsWorker is (i:acc)
663 = substInstsWorker is (i:acc)
667 -- forall g1 : s1{F c} ~ s2{F c}
669 -- g2 : s1{t} ~ s2{t}
670 -- g1 := s1{g} * g2 * sym s2{g} <=> g2 := sym s1{g} * g1 * s2{g}
673 substInst inst@(EqInst {tci_left = pattern, tci_right = target}) (i@(EqInst {tci_left = ty1, tci_right = ty2}):is)
674 = do { (is',changed) <- substInst inst is
675 ; (coi1,ty1') <- tcGenericNormalizeFamInst fun ty1
676 ; (coi2,ty2') <- tcGenericNormalizeFamInst fun ty2
677 ; case (coi1,coi2) of
679 return (i:is',changed)
681 do { gw_co <- eitherEqInst i
682 -- old_co := co1 * new_co * sym co2
684 do { new_cotv <- newMetaTyVar TauTv (mkCoKind ty1' ty2')
685 ; let new_co = TyVarTy new_cotv
686 ; let old_coi = coi1 `mkTransCoI` ACo new_co `mkTransCoI` (mkSymCoI coi2)
687 ; writeMetaTyVar old_covar (fromACo old_coi)
688 ; return $ mkWantedCo new_cotv
690 -- new_co := sym co1 * old_co * co2
691 (\old_co -> return $ mkGivenCo $ fromACo $ (mkSymCoI coi1) `mkTransCoI` ACo old_co `mkTransCoI` coi2)
692 ; new_inst <- mkEqInst (EqPred ty1' ty2') gw_co
693 ; return (new_inst:is',True)
696 where fun ty = return $ if tcEqType pattern ty then Just (target,coercion) else Nothing
698 coercion = eitherEqInst inst TyVarTy id
699 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
701 :: [Inst] -- wanted equations
704 = do { (insts',changeds) <- mapAndUnzipM unifyInst insts
705 ; return (concat insts',or changeds)
714 -- TOMDO: you should only do this for certain `meta' type variables
715 unifyInst i@(EqInst {tci_left = ty1, tci_right = ty2})
716 | TyVarTy tv1 <- ty1, isMetaTyVar tv1 = go ty2 tv1
717 | TyVarTy tv2 <- ty2, isMetaTyVar tv2 = go ty1 tv2
718 | otherwise = return ([i],False)
720 = do { let cotv = fromWantedCo "unifyInst" $ eqInstCoercion i
721 ; writeMetaTyVar tv ty -- alpha := t
722 ; writeMetaTyVar cotv ty -- g := t
726 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
727 occursCheckInsts :: [Inst] -> TcM ()
728 occursCheckInsts insts = mappM_ occursCheckInst insts
736 occursCheckInst :: Inst -> TcM ()
737 occursCheckInst i@(EqInst {tci_left = ty1, tci_right = ty2})
740 check ty = if ty `tcEqType` ty1
744 go (TyConApp con tys) = if isOpenSynTyCon con then return () else mappM_ check tys
745 go (FunTy arg res) = mappM_ check [arg,res]
746 go (AppTy fun arg) = mappM_ check [fun,arg]
749 occursError = do { env0 <- tcInitTidyEnv
750 ; let (env1, tidy_ty1) = tidyOpenType env0 ty1
751 (env2, tidy_ty2) = tidyOpenType env1 ty2
752 extra = sep [ppr tidy_ty1, char '~', ppr tidy_ty2]
753 ; failWithTcM (env2, hang msg 2 extra)
755 where msg = ptext SLIT("Occurs check: cannot construct the infinite type")
758 Normalises a set of dictionaries relative to a set of given equalities (which
759 are interpreted as rewrite rules). We only consider given equalities of the
764 where F is a type family.
767 substEqInDictInsts :: [Inst] -- given equalities (used as rewrite rules)
768 -> [Inst] -- dictinaries to be normalised
769 -> TcM ([Inst], TcDictBinds)
770 substEqInDictInsts eq_insts insts
771 = do { traceTc (text "substEqInDictInst <-" <+> ppr insts)
772 ; result <- foldlM rewriteWithOneEquality (insts, emptyBag) eq_insts
773 ; traceTc (text "substEqInDictInst ->" <+> ppr result)
777 -- (1) Given equality of form 'F ts ~ t': use for rewriting
778 rewriteWithOneEquality (insts, dictBinds)
779 inst@(EqInst {tci_left = pattern,
781 | isOpenSynTyConApp pattern
782 = do { (insts', moreDictBinds) <- genericNormaliseInsts True {- wanted -}
784 ; return (insts', dictBinds `unionBags` moreDictBinds)
787 applyThisEq = tcGenericNormalizeFamInstPred (return . matchResult)
789 -- rewrite in case of an exact match
790 matchResult ty | tcEqType pattern ty = Just (target, eqInstType inst)
791 | otherwise = Nothing
793 -- (2) Given equality has the wrong form: ignore
794 rewriteWithOneEquality (insts, dictBinds) _not_a_rewrite_rule
795 = return (insts, dictBinds)
798 %************************************************************************
800 Normalisation of Insts
802 %************************************************************************
804 Take a bunch of Insts (not EqInsts), and normalise them wrt the top-level
805 type-function equations, where
807 (norm_insts, binds) = normaliseInsts is_wanted insts
810 = True, (binds + norm_insts) defines insts (wanteds)
811 = False, (binds + insts) defines norm_insts (givens)
814 normaliseInsts :: Bool -- True <=> wanted insts
815 -> [Inst] -- wanted or given insts
816 -> TcM ([Inst], TcDictBinds) -- normalized insts and bindings
817 normaliseInsts isWanted insts
818 = genericNormaliseInsts isWanted tcNormalizeFamInstPred insts
820 genericNormaliseInsts :: Bool -- True <=> wanted insts
821 -> (TcPredType -> TcM (CoercionI, TcPredType))
823 -> [Inst] -- wanted or given insts
824 -> TcM ([Inst], TcDictBinds) -- normalized insts & binds
825 genericNormaliseInsts isWanted fun insts
826 = do { (insts', binds) <- mapAndUnzipM (normaliseOneInst isWanted fun) insts
827 ; return (insts', unionManyBags binds)
830 normaliseOneInst isWanted fun
831 dict@(Dict {tci_name = name,
834 = do { traceTc (text "genericNormaliseInst 1")
835 ; (coi, pred') <- fun pred
836 ; traceTc (text "genericNormaliseInst 2")
839 IdCo -> return (dict, emptyBag)
840 -- don't use pred' in this case; otherwise, we get
841 -- more unfolded closed type synonyms in error messages
843 do { -- an inst for the new pred
844 ; dict' <- newDictBndr loc pred'
845 -- relate the old inst to the new one
846 -- target_dict = source_dict `cast` st_co
847 ; let (target_dict, source_dict, st_co)
848 | isWanted = (dict, dict', mkSymCoercion co)
849 | otherwise = (dict', dict, co)
851 -- co :: dict ~ dict'
852 -- hence dict = dict' `cast` sym co
854 -- co :: dict ~ dict'
855 -- hence dict' = dict `cast` co
856 expr = HsVar $ instToId source_dict
857 cast_expr = HsWrap (WpCo st_co) expr
858 rhs = L (instLocSpan loc) cast_expr
859 binds = mkBind target_dict rhs
860 -- return the new inst
861 ; return (dict', binds)
865 -- TOMDO: treat other insts appropriately
866 normaliseOneInst isWanted fun inst
867 = do { inst' <- zonkInst inst
868 ; return (inst', emptyBag)
871 addBind binds inst rhs = binds `unionBags` mkBind inst rhs
873 mkBind inst rhs = unitBag (L (instSpan inst)
874 (VarBind (instToId inst) rhs))