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
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 = actual_swap ty1 ty2
530 go ty1@(TyConApp _ _) ty2@(TyVarTy _)
531 = actual_swap ty1 ty2
532 go _ _ = return (i,False)
534 actual_swap ty1 ty2 = do { wg_co <- eitherEqInst i
535 -- old_co := sym new_co
537 do { new_cotv <- newMetaTyVar TauTv (mkCoKind ty2 ty1)
538 ; let new_co = TyVarTy new_cotv
539 ; writeMetaTyVar old_covar (mkCoercion symCoercionTyCon [new_co])
540 ; return $ mkWantedCo new_cotv
542 -- new_co := sym old_co
543 (\old_co -> return $ mkGivenCo $ mkCoercion symCoercionTyCon [old_co])
544 ; new_inst <- mkEqInst (EqPred ty2 ty1) wg_co
545 ; return (new_inst,True)
548 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
549 decompInsts :: [Inst] -> TcM ([Inst],Bool)
550 decompInsts insts = do { (insts,bs) <- mapAndUnzipM decompInst insts
551 ; return (concat insts,or bs)
557 -- g21 : c1 ~ d1, ..., g2n : cn ~ dn
560 -- Works also for the case where T is actually an application of a
561 -- type family constructor to a set of types, provided the
562 -- applications on both sides of the ~ are identical;
563 -- see also Note [OpenSynTyCon app] in TcUnify
565 decompInst :: Inst -> TcM ([Inst],Bool)
566 decompInst i@(EqInst {})
570 ty2 = eqInstRightTy i
572 | Just ty1' <- tcView ty1 = go ty1' ty2
573 | Just ty2' <- tcView ty2 = go ty1 ty2'
575 go ty1@(TyConApp con1 tys1) ty2@(TyConApp con2 tys2)
576 | con1 == con2 && identicalHead
577 = do { cos <- eitherEqInst i
578 -- old_co := Con1 cos
580 do { cotvs <- zipWithM (\t1 t2 ->
584 ; let cos = map TyVarTy cotvs
585 ; writeMetaTyVar old_covar (TyConApp con1 cos)
586 ; return $ map mkWantedCo cotvs
588 -- co_i := Con_i old_co
591 mkRightCoercions (length tys1) old_co)
592 ; insts <- zipWithM mkEqInst (zipWith EqPred tys1 tys2) cos
593 ; traceTc (text "decomp identicalHead" <+> ppr insts)
594 ; return (insts, not $ null insts)
596 | con1 /= con2 && not (isOpenSynTyCon con1 || isOpenSynTyCon con2)
597 -- not matching data constructors (of any flavour) are bad news
598 = do { env0 <- tcInitTidyEnv
599 ; let (env1, tidy_ty1) = tidyOpenType env0 ty1
600 (env2, tidy_ty2) = tidyOpenType env1 ty2
601 extra = sep [ppr tidy_ty1, char '~', ppr tidy_ty2]
603 ptext SLIT("Unsolvable equality constraint:")
604 ; failWithTcM (env2, hang msg 2 extra)
608 (idxTys1, tys1') = splitAt n tys1
609 (idxTys2, tys2') = splitAt n tys2
610 identicalHead = not (isOpenSynTyCon con1) ||
611 idxTys1 `tcEqTypes` idxTys2
613 go _ _ = return ([i], False)
615 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
616 topInsts :: [Inst] -> TcM ([Inst],Bool)
618 = do { (insts,bs) <- mapAndUnzipM topInst insts
619 ; return (insts,or bs)
624 -- >--> co1 :: t ~ t' / co2 :: s ~ s'
626 -- g1 := co1 * g2 * sym co2
627 topInst :: Inst -> TcM (Inst,Bool)
628 topInst i@(EqInst {})
629 = do { (coi1,ty1') <- tcNormalizeFamInst ty1
630 ; (coi2,ty2') <- tcNormalizeFamInst ty2
631 ; case (coi1,coi2) of
635 do { wg_co <- eitherEqInst i
636 -- old_co = co1 * new_co * sym co2
638 do { new_cotv <- newMetaTyVar TauTv (mkCoKind ty1 ty2)
639 ; let new_co = TyVarTy new_cotv
640 ; let old_coi = coi1 `mkTransCoI` ACo new_co `mkTransCoI` (mkSymCoI coi2)
641 ; writeMetaTyVar old_covar (fromACo old_coi)
642 ; return $ mkWantedCo new_cotv
644 -- new_co = sym co1 * old_co * co2
645 (\old_co -> return $ mkGivenCo $ fromACo $ mkSymCoI coi1 `mkTransCoI` ACo old_co `mkTransCoI` coi2)
646 ; new_inst <- mkEqInst (EqPred ty1' ty2') wg_co
647 ; return (new_inst,True)
652 ty2 = eqInstRightTy i
654 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
655 substInsts :: [Inst] -> TcM ([Inst],Bool)
656 substInsts insts = substInstsWorker insts []
658 substInstsWorker [] acc
660 substInstsWorker (i:is) acc
661 | (TyConApp con _) <- tci_left i, isOpenSynTyCon con
662 = do { (is',change) <- substInst i (acc ++ is)
664 then return ((i:is'),True)
665 else substInstsWorker is (i:acc)
668 = substInstsWorker is (i:acc)
672 -- forall g1 : s1{F c} ~ s2{F c}
674 -- g2 : s1{t} ~ s2{t}
675 -- g1 := s1{g} * g2 * sym s2{g} <=> g2 := sym s1{g} * g1 * s2{g}
678 substInst inst@(EqInst {tci_left = pattern, tci_right = target}) (i@(EqInst {tci_left = ty1, tci_right = ty2}):is)
679 = do { (is',changed) <- substInst inst is
680 ; (coi1,ty1') <- tcGenericNormalizeFamInst fun ty1
681 ; (coi2,ty2') <- tcGenericNormalizeFamInst fun ty2
682 ; case (coi1,coi2) of
684 return (i:is',changed)
686 do { gw_co <- eitherEqInst i
687 -- old_co := co1 * new_co * sym co2
689 do { new_cotv <- newMetaTyVar TauTv (mkCoKind ty1' ty2')
690 ; let new_co = TyVarTy new_cotv
691 ; let old_coi = coi1 `mkTransCoI` ACo new_co `mkTransCoI` (mkSymCoI coi2)
692 ; writeMetaTyVar old_covar (fromACo old_coi)
693 ; return $ mkWantedCo new_cotv
695 -- new_co := sym co1 * old_co * co2
696 (\old_co -> return $ mkGivenCo $ fromACo $ (mkSymCoI coi1) `mkTransCoI` ACo old_co `mkTransCoI` coi2)
697 ; new_inst <- mkEqInst (EqPred ty1' ty2') gw_co
698 ; return (new_inst:is',True)
701 where fun ty = return $ if tcEqType pattern ty then Just (target,coercion) else Nothing
703 coercion = eitherEqInst inst TyVarTy id
704 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
706 :: [Inst] -- wanted equations
709 = do { (insts',changeds) <- mapAndUnzipM unifyInst insts
710 ; return (concat insts',or changeds)
719 -- TOMDO: you should only do this for certain `meta' type variables
720 unifyInst i@(EqInst {tci_left = ty1, tci_right = ty2})
721 | TyVarTy tv1 <- ty1, isMetaTyVar tv1 = go ty2 tv1
722 | TyVarTy tv2 <- ty2, isMetaTyVar tv2 = go ty1 tv2
723 | otherwise = return ([i],False)
725 = do { let cotv = fromWantedCo "unifyInst" $ eqInstCoercion i
726 ; writeMetaTyVar tv ty -- alpha := t
727 ; writeMetaTyVar cotv ty -- g := t
731 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
732 occursCheckInsts :: [Inst] -> TcM ()
733 occursCheckInsts insts = mappM_ occursCheckInst insts
741 occursCheckInst :: Inst -> TcM ()
742 occursCheckInst i@(EqInst {tci_left = ty1, tci_right = ty2})
745 check ty = if ty `tcEqType` ty1
749 go (TyConApp con tys) = if isOpenSynTyCon con then return () else mappM_ check tys
750 go (FunTy arg res) = mappM_ check [arg,res]
751 go (AppTy fun arg) = mappM_ check [fun,arg]
754 occursError = do { env0 <- tcInitTidyEnv
755 ; let (env1, tidy_ty1) = tidyOpenType env0 ty1
756 (env2, tidy_ty2) = tidyOpenType env1 ty2
757 extra = sep [ppr tidy_ty1, char '~', ppr tidy_ty2]
758 ; failWithTcM (env2, hang msg 2 extra)
760 where msg = ptext SLIT("Occurs check: cannot construct the infinite type")
763 Normalises a set of dictionaries relative to a set of given equalities (which
764 are interpreted as rewrite rules). We only consider given equalities of the
769 where F is a type family.
772 substEqInDictInsts :: [Inst] -- given equalities (used as rewrite rules)
773 -> [Inst] -- dictinaries to be normalised
774 -> TcM ([Inst], TcDictBinds)
775 substEqInDictInsts eq_insts insts
776 = do { traceTc (text "substEqInDictInst <-" <+> ppr insts)
777 ; result <- foldlM rewriteWithOneEquality (insts, emptyBag) eq_insts
778 ; traceTc (text "substEqInDictInst ->" <+> ppr result)
782 -- (1) Given equality of form 'F ts ~ t': use for rewriting
783 rewriteWithOneEquality (insts, dictBinds)
784 inst@(EqInst {tci_left = pattern,
786 | isOpenSynTyConApp pattern
787 = do { (insts', moreDictBinds) <- genericNormaliseInsts True {- wanted -}
789 ; return (insts', dictBinds `unionBags` moreDictBinds)
792 applyThisEq = tcGenericNormalizeFamInstPred (return . matchResult)
794 -- rewrite in case of an exact match
795 matchResult ty | tcEqType pattern ty = Just (target, eqInstType inst)
796 | otherwise = Nothing
798 -- (2) Given equality has the wrong form: ignore
799 rewriteWithOneEquality (insts, dictBinds) _not_a_rewrite_rule
800 = return (insts, dictBinds)
803 %************************************************************************
805 Normalisation of Insts
807 %************************************************************************
809 Take a bunch of Insts (not EqInsts), and normalise them wrt the top-level
810 type-function equations, where
812 (norm_insts, binds) = normaliseInsts is_wanted insts
815 = True, (binds + norm_insts) defines insts (wanteds)
816 = False, (binds + insts) defines norm_insts (givens)
819 normaliseInsts :: Bool -- True <=> wanted insts
820 -> [Inst] -- wanted or given insts
821 -> TcM ([Inst], TcDictBinds) -- normalized insts and bindings
822 normaliseInsts isWanted insts
823 = genericNormaliseInsts isWanted tcNormalizeFamInstPred insts
825 genericNormaliseInsts :: Bool -- True <=> wanted insts
826 -> (TcPredType -> TcM (CoercionI, TcPredType))
828 -> [Inst] -- wanted or given insts
829 -> TcM ([Inst], TcDictBinds) -- normalized insts & binds
830 genericNormaliseInsts isWanted fun insts
831 = do { (insts', binds) <- mapAndUnzipM (normaliseOneInst isWanted fun) insts
832 ; return (insts', unionManyBags binds)
835 normaliseOneInst isWanted fun
836 dict@(Dict {tci_name = name,
839 = do { traceTc (text "genericNormaliseInst 1")
840 ; (coi, pred') <- fun pred
841 ; traceTc (text "genericNormaliseInst 2")
844 IdCo -> return (dict, emptyBag)
845 -- don't use pred' in this case; otherwise, we get
846 -- more unfolded closed type synonyms in error messages
848 do { -- an inst for the new pred
849 ; dict' <- newDictBndr loc pred'
850 -- relate the old inst to the new one
851 -- target_dict = source_dict `cast` st_co
852 ; let (target_dict, source_dict, st_co)
853 | isWanted = (dict, dict', mkSymCoercion co)
854 | otherwise = (dict', dict, co)
856 -- co :: dict ~ dict'
857 -- hence dict = dict' `cast` sym co
859 -- co :: dict ~ dict'
860 -- hence dict' = dict `cast` co
861 expr = HsVar $ instToId source_dict
862 cast_expr = HsWrap (WpCo st_co) expr
863 rhs = L (instLocSpan loc) cast_expr
864 binds = mkBind target_dict rhs
865 -- return the new inst
866 ; return (dict', binds)
870 -- TOMDO: treat other insts appropriately
871 normaliseOneInst isWanted fun inst
872 = do { inst' <- zonkInst inst
873 ; return (inst', emptyBag)
876 addBind binds inst rhs = binds `unionBags` mkBind inst rhs
878 mkBind inst rhs = unitBag (L (instSpan inst)
879 (VarBind (instToId inst) rhs))