1 Normalisation of type terms relative to type instances as well as
2 normalisation and entailment checking of equality constraints.
8 normaliseGivenEqs, normaliseGivenDicts,
9 normaliseWantedEqs, normaliseWantedDicts,
14 eqInstMisMatch, misMatchMsg,
18 #include "HsVersions.h"
30 import TypeRep ( Type(..) )
38 import SrcLoc ( Located(..) )
43 import Control.Monad (liftM)
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 { -- we only use the indexing arguments for matching,
71 -- not the additional ones
72 ; maybeFamInst <- tcLookupFamInst tycon idxTys
73 ; case maybeFamInst of
74 Nothing -> return Nothing
75 Just (rep_tc, rep_tys) -> return $ Just (mkTyConApp rep_tc tys',
76 mkTyConApp coe_tc tys')
78 tys' = rep_tys ++ restTys
79 coe_tc = expectJust "TcTyFun.tcUnfoldSynFamInst"
80 (tyConFamilyCoercion_maybe rep_tc)
84 (idxTys, restTys) = splitAt n tys
85 tcUnfoldSynFamInst _other = return Nothing
88 Normalise 'Type's and 'PredType's by unfolding type family applications where
89 possible (ie, we treat family instances as a TRS). Also zonk meta variables.
91 tcNormaliseFamInst ty = (co, ty')
95 tcNormaliseFamInst :: TcType -> TcM (CoercionI, TcType)
96 tcNormaliseFamInst = tcGenericNormaliseFamInst tcUnfoldSynFamInst
98 tcNormaliseFamInstPred :: TcPredType -> TcM (CoercionI, TcPredType)
99 tcNormaliseFamInstPred = tcGenericNormaliseFamInstPred tcUnfoldSynFamInst
102 An elementary rewrite is a properly oriented equality with associated coercion
103 that has one of the following two forms:
105 (1) co :: F t1..tn ~ t
106 (2) co :: a ~ t , where t /= F t1..tn
108 The following functions takes an equality instance and turns it into an
109 elementary rewrite if possible.
112 data Rewrite = Rewrite TcType -- lhs of rewrite rule
113 TcType -- rhs of rewrite rule
114 TcType -- coercion witnessing the rewrite rule
116 eqInstToRewrite :: Inst -> Maybe (Rewrite, Bool)
117 -- True iff rewrite swapped equality
119 = ASSERT( isEqInst inst )
120 go (eqInstLeftTy inst) (eqInstRightTy inst) (eqInstType inst)
122 -- look through synonyms
123 go ty1 ty2 co | Just ty1' <- tcView ty1 = go ty1' ty2 co
124 go ty1 ty2 co | Just ty2' <- tcView ty2 = go ty1 ty2' co
126 -- left-to-right rule with type family head
127 go ty1@(TyConApp con _) ty2 co
129 = Just (Rewrite ty1 ty2 co, False) -- not swapped
131 -- left-to-right rule with type variable head
132 go ty1@(TyVarTy tv) ty2 co
134 = Just (Rewrite ty1 ty2 co, False) -- not swapped
136 -- right-to-left rule with type family head, only after
137 -- having checked whether we can work left-to-right
138 go ty1 ty2@(TyConApp con _) co
140 = Just (Rewrite ty2 ty1 (mkSymCoercion co), True) -- swapped
142 -- right-to-left rule with type variable head, only after
143 -- having checked whether we can work left-to-right
144 go ty1 ty2@(TyVarTy tv) co
146 = Just (Rewrite ty2 ty1 (mkSymCoercion co), True) -- swapped
148 -- this equality is not a rewrite rule => ignore
152 Normalise a type relative to an elementary rewrite implied by an EqInst or an
153 explicitly given elementary rewrite.
157 -- Precondition: the EqInst passes the occurs check
158 tcEqInstNormaliseFamInst :: Inst -> TcType -> TcM (CoercionI, TcType)
159 tcEqInstNormaliseFamInst inst ty
160 = case eqInstToRewrite inst of
161 Just (rewrite, _) -> tcEqRuleNormaliseFamInst rewrite ty
162 Nothing -> return (IdCo, ty)
164 -- Rewrite by equality rewrite rule
165 tcEqRuleNormaliseFamInst :: Rewrite -- elementary rewrite
166 -> TcType -- type to rewrite
167 -> TcM (CoercionI, -- witnessing coercion
168 TcType) -- rewritten type
169 tcEqRuleNormaliseFamInst (Rewrite pat rhs co) ty
170 = tcGenericNormaliseFamInst matchEqRule ty
172 matchEqRule sty | pat `tcEqType` sty = return $ Just (rhs, co)
173 | otherwise = return $ Nothing
176 Generic normalisation of 'Type's and 'PredType's; ie, walk the type term and
177 apply the normalisation function gives as the first argument to every TyConApp
178 and every TyVarTy subterm.
180 tcGenericNormaliseFamInst fun ty = (co, ty')
183 This function is (by way of using smart constructors) careful to ensure that
184 the returned coercion is exactly IdCo (and not some semantically equivalent,
185 but syntactically different coercion) whenever (ty' `tcEqType` ty). This
186 makes it easy for the caller to determine whether the type changed. BUT
187 even if we return IdCo, ty' may be *syntactically* different from ty due to
188 unfolded closed type synonyms (by way of tcCoreView). In the interest of
189 good error messages, callers should discard ty' in favour of ty in this case.
192 tcGenericNormaliseFamInst :: (TcType -> TcM (Maybe (TcType, Coercion)))
193 -- what to do with type functions and tyvars
194 -> TcType -- old type
195 -> TcM (CoercionI, TcType) -- (coercion, new type)
196 tcGenericNormaliseFamInst fun ty
197 | Just ty' <- tcView ty = tcGenericNormaliseFamInst fun ty'
198 tcGenericNormaliseFamInst fun (TyConApp tyCon tys)
199 = do { (cois, ntys) <- mapAndUnzipM (tcGenericNormaliseFamInst fun) tys
200 ; let tycon_coi = mkTyConAppCoI tyCon ntys cois
201 ; maybe_ty_co <- fun (mkTyConApp tyCon ntys) -- use normalised args!
202 ; case maybe_ty_co of
203 -- a matching family instance exists
205 do { let first_coi = mkTransCoI tycon_coi (ACo co)
206 ; (rest_coi, nty) <- tcGenericNormaliseFamInst fun ty'
207 ; let fix_coi = mkTransCoI first_coi rest_coi
208 ; return (fix_coi, nty)
210 -- no matching family instance exists
211 -- we do not do anything
212 Nothing -> return (tycon_coi, mkTyConApp tyCon ntys)
214 tcGenericNormaliseFamInst fun (AppTy ty1 ty2)
215 = do { (coi1,nty1) <- tcGenericNormaliseFamInst fun ty1
216 ; (coi2,nty2) <- tcGenericNormaliseFamInst fun ty2
217 ; return (mkAppTyCoI nty1 coi1 nty2 coi2, mkAppTy nty1 nty2)
219 tcGenericNormaliseFamInst fun (FunTy ty1 ty2)
220 = do { (coi1,nty1) <- tcGenericNormaliseFamInst fun ty1
221 ; (coi2,nty2) <- tcGenericNormaliseFamInst fun ty2
222 ; return (mkFunTyCoI nty1 coi1 nty2 coi2, mkFunTy nty1 nty2)
224 tcGenericNormaliseFamInst fun (ForAllTy tyvar ty1)
225 = do { (coi,nty1) <- tcGenericNormaliseFamInst fun ty1
226 ; return (mkForAllTyCoI tyvar coi, mkForAllTy tyvar nty1)
228 tcGenericNormaliseFamInst fun (NoteTy note ty1)
229 = do { (coi,nty1) <- tcGenericNormaliseFamInst fun ty1
230 ; return (mkNoteTyCoI note coi, NoteTy note nty1)
232 tcGenericNormaliseFamInst fun ty@(TyVarTy tv)
234 = do { traceTc (text "tcGenericNormaliseFamInst" <+> ppr ty)
235 ; res <- lookupTcTyVar tv
238 do { maybe_ty' <- fun ty
240 Nothing -> return (IdCo, ty)
242 do { (coi2, ty'') <- tcGenericNormaliseFamInst fun ty'
243 ; return (ACo co1 `mkTransCoI` coi2, ty'')
246 IndirectTv ty' -> tcGenericNormaliseFamInst fun ty'
250 tcGenericNormaliseFamInst fun (PredTy predty)
251 = do { (coi, pred') <- tcGenericNormaliseFamInstPred fun predty
252 ; return (coi, PredTy pred') }
254 ---------------------------------
255 tcGenericNormaliseFamInstPred :: (TcType -> TcM (Maybe (TcType,Coercion)))
257 -> TcM (CoercionI, TcPredType)
259 tcGenericNormaliseFamInstPred fun (ClassP cls tys)
260 = do { (cois, tys')<- mapAndUnzipM (tcGenericNormaliseFamInst fun) tys
261 ; return (mkClassPPredCoI cls tys' cois, ClassP cls tys')
263 tcGenericNormaliseFamInstPred fun (IParam ipn ty)
264 = do { (coi, ty') <- tcGenericNormaliseFamInst fun ty
265 ; return $ (mkIParamPredCoI ipn coi, IParam ipn ty')
267 tcGenericNormaliseFamInstPred fun (EqPred ty1 ty2)
268 = do { (coi1, ty1') <- tcGenericNormaliseFamInst fun ty1
269 ; (coi2, ty2') <- tcGenericNormaliseFamInst fun ty2
270 ; return (mkEqPredCoI ty1' coi1 ty2' coi2, EqPred ty1' ty2') }
274 %************************************************************************
276 \section{Normalisation of equality constraints}
278 %************************************************************************
280 Note [Inconsistencies in equality constraints]
281 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
282 We guarantee that we raise an error if we discover any inconsistencies (i.e.,
283 equalities that if presented to the unifer in TcUnify would result in an
284 error) during normalisation of wanted constraints. This is especially so that
285 we don't solve wanted constraints under an inconsistent given set. In
286 particular, we don't want to permit signatures, such as
288 bad :: (Int ~ Bool => Int) -> a -> a
291 normaliseGivenEqs :: [Inst] -> TcM ([Inst], TcM ())
292 normaliseGivenEqs givens
293 = do { traceTc (text "normaliseGivenEqs <-" <+> ppr givens)
294 ; (result, deSkolem) <-
295 rewriteToFixedPoint (Just ("(SkolemOccurs)", skolemOccurs))
296 [ ("(ZONK)", dontRerun $ zonkInsts)
297 , ("(TRIVIAL)", dontRerun $ trivialRule)
298 , ("(DECOMP)", decompRule)
300 , ("(SUBST)", substRule) -- incl. occurs check
302 ; traceTc (text "normaliseGivenEqs ->" <+> ppr result)
303 ; return (result, deSkolem)
308 normaliseWantedEqs :: [Inst] -> TcM [Inst]
309 normaliseWantedEqs insts
310 = do { traceTc (text "normaliseWantedEqs <-" <+> ppr insts)
311 ; result <- liftM fst $ rewriteToFixedPoint Nothing
312 [ ("(ZONK)", dontRerun $ zonkInsts)
313 , ("(TRIVIAL)", dontRerun $ trivialRule)
314 , ("(DECOMP)", decompRule)
316 , ("(UNIFY)", unifyMetaRule) -- incl. occurs check
317 , ("(SUBST)", substRule) -- incl. occurs check
319 ; traceTc (text "normaliseWantedEqs ->" <+> ppr result)
325 %************************************************************************
327 \section{Solving of wanted constraints with respect to a given set}
329 %************************************************************************
331 The set of given equalities must have been normalised already.
334 solveWantedEqs :: [Inst] -- givens
336 -> TcM [Inst] -- irreducible wanteds
337 solveWantedEqs givens wanteds
338 = do { traceTc $ text "solveWantedEqs <-" <+> ppr wanteds <+> text "with" <+>
340 ; result <- liftM fst $ rewriteToFixedPoint Nothing
341 [ ("(ZONK)", dontRerun $ zonkInsts)
342 , ("(TRIVIAL)", dontRerun $ trivialRule)
343 , ("(DECOMP)", decompRule)
345 , ("(GIVEN)", substGivens givens) -- incl. occurs check
346 , ("(UNIFY)", unifyMetaRule) -- incl. occurs check
348 ; traceTc (text "solveWantedEqs ->" <+> ppr result)
352 -- Use `substInst' with every given on all the wanteds.
353 substGivens :: [Inst] -> [Inst] -> TcM ([Inst], Bool)
354 substGivens [] wanteds = return (wanteds, False)
355 substGivens (g:gs) wanteds
356 = do { (wanteds1, changed1) <- substGivens gs wanteds
357 ; (wanteds2, changed2) <- substInst g wanteds1
358 ; return (wanteds2, changed1 || changed2)
363 %************************************************************************
365 \section{Normalisation of non-equality dictionaries}
367 %************************************************************************
370 normaliseGivenDicts, normaliseWantedDicts
371 :: [Inst] -- given equations
372 -> [Inst] -- dictionaries
373 -> TcM ([Inst],TcDictBinds)
375 normaliseGivenDicts eqs dicts = normalise_dicts eqs dicts False
376 normaliseWantedDicts eqs dicts = normalise_dicts eqs dicts True
379 :: [Inst] -- given equations
380 -> [Inst] -- dictionaries
381 -> Bool -- True <=> the dicts are wanted
382 -- Fals <=> they are given
383 -> TcM ([Inst],TcDictBinds)
384 normalise_dicts given_eqs dicts is_wanted
385 = do { traceTc $ text "normalise???Dicts <-" <+> ppr dicts <+>
386 text "with" <+> ppr given_eqs
387 ; (dicts0, binds0) <- normaliseInsts is_wanted dicts
388 ; (dicts1, binds1) <- substEqInDictInsts given_eqs dicts0
389 ; let binds01 = binds0 `unionBags` binds1
390 ; if isEmptyBag binds1
391 then return (dicts1, binds01)
392 else do { (dicts2, binds2) <- normaliseGivenDicts given_eqs dicts1
393 ; return (dicts2, binds01 `unionBags` binds2) } }
397 %************************************************************************
399 \section{Normalisation rules and iterative rule application}
401 %************************************************************************
403 We have three kinds of normalising rewrite rules:
405 (1) Normalisation rules that rewrite a set of insts and return a flag indicating
406 whether any changes occurred during rewriting that necessitate re-running
407 the current rule set.
409 (2) Precondition rules that rewrite a set of insts and return a monadic action
410 that reverts the effect of preconditioning.
412 (3) Idempotent normalisation rules that never require re-running the rule set.
415 type RewriteRule = [Inst] -> TcM ([Inst], Bool) -- rewrite, maybe re-run
416 type PrecondRule = [Inst] -> TcM ([Inst], TcM ()) -- rewrite, revertable
417 type IdemRewriteRule = [Inst] -> TcM [Inst] -- rewrite, don't re-run
419 type NamedRule = (String, RewriteRule) -- rule with description
420 type NamedPreRule = (String, PrecondRule) -- precond with desc
423 Template lifting idempotent rules to full rules (which can be put into a rule
427 dontRerun :: IdemRewriteRule -> RewriteRule
428 dontRerun rule insts = liftM addFalse $ rule insts
430 addFalse x = (x, False)
433 The following function applies a set of rewrite rules until a fixed point is
434 reached; i.e., none of the `RewriteRule's require re-running the rule set.
435 Optionally, there may be a pre-conditing rule that is applied before any other
436 rules are applied and before the rule set is re-run.
438 The result is the set of rewritten (i.e., normalised) insts and, in case of a
439 pre-conditing rule, a monadic action that reverts the effects of
440 pre-conditioning - specifically, this is removing introduced skolems.
443 rewriteToFixedPoint :: Maybe NamedPreRule -- optional preconditioning rule
444 -> [NamedRule] -- rule set
445 -> [Inst] -- insts to rewrite
446 -> TcM ([Inst], TcM ())
447 rewriteToFixedPoint precondRule rules insts
448 = completeRewrite (return ()) precondRule insts
450 completeRewrite :: TcM () -> Maybe NamedPreRule -> [Inst]
451 -> TcM ([Inst], TcM ())
452 completeRewrite dePrecond (Just (precondName, precond)) insts
453 = do { traceTc $ text precondName <+> text " <- " <+> ppr insts
454 ; (insts', dePrecond') <- precond insts
455 ; traceTc $ text precondName <+> text " -> " <+> ppr insts'
456 ; tryRules (dePrecond >> dePrecond') rules insts'
458 completeRewrite dePrecond Nothing insts
459 = tryRules dePrecond rules insts
461 tryRules dePrecond _ [] = return ([] , dePrecond)
462 tryRules dePrecond [] insts = return (insts, dePrecond)
463 tryRules dePrecond ((name, rule):rules) insts
464 = do { traceTc $ text name <+> text " <- " <+> ppr insts
465 ; (insts', rerun) <- rule insts
466 ; traceTc $ text name <+> text " -> " <+> ppr insts'
467 ; if rerun then completeRewrite dePrecond precondRule insts'
468 else tryRules dePrecond rules insts'
473 %************************************************************************
475 \section{Different forms of Inst rewrite rules}
477 %************************************************************************
479 Splitting of non-terminating given constraints: skolemOccurs
480 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
481 This is a preconditioning rule exclusively applied to given constraints.
482 Moreover, its rewriting is only temporary, as it is undone by way of
483 side-effecting mutable type variables after simplification and constraint
484 entailment has been completed.
486 This version is an (attempt at, yet unproven, an) *unflattened* version of
487 the SubstL-Ev completion rule.
489 The above rule is essential to catch non-terminating rules that cannot be
490 oriented properly, like
496 The left-to-right orientiation is not suitable because it does not
497 terminate. The right-to-left orientation is not suitable because it
498 does not have a type-function on the left. This is undesirable because
499 it would hide information. E.g. assume
503 then rewriting C [G (F a)] to C (F a) is bad because we cannot now
504 see that the C [x] instance applies.
506 The rule also caters for badly-oriented rules of the form:
510 for which other solutions are possible, but this one will do too.
514 co : ty1 ~ ty2{F ty1}
517 sym (F co) : F ty2{b} ~ b
518 where b is a fresh skolem variable
520 We also cater for the symmetric situation *if* the rule cannot be used as a
521 left-to-right rewrite rule.
523 We also return an action (b := ty1) which is used to eliminate b
524 after the dust of normalisation with the completed rewrite system
527 A subtle point of this transformation is that both coercions in the results
528 are strictly speaking incorrect. However, they are correct again after the
529 action {B := ty1} has removed the skolem again. This happens immediately
530 after constraint entailment has been checked; ie, code outside of the
531 simplification and entailment checking framework will never see these
532 temporarily incorrect coercions.
534 NB: We perform this transformation for multiple occurences of ty1 under one
535 or multiple family applications on the left-hand side at once (ie, the
536 rule doesn't need to be applied multiple times at a single inst). As a
537 result we can get two or more insts back.
540 skolemOccurs :: PrecondRule
542 = do { (instss, undoSkolems) <- mapAndUnzipM oneSkolemOccurs insts
543 ; return (concat instss, sequence_ undoSkolems)
547 = ASSERT( isEqInst inst )
548 case eqInstToRewrite inst of
549 Just (rewrite, swapped) -> breakRecursion rewrite swapped
550 Nothing -> return ([inst], return ())
552 -- inst is an elementary rewrite rule, check whether we need to break
554 breakRecursion (Rewrite pat body _) swapped
556 -- skolemOccurs does not apply, leave as is
558 = return ([inst], return ())
560 -- recursive occurence of pat in body under a type family application
562 = do { traceTc $ text "oneSkolemOccurs[TLO]:" <+> ppr tysToLiftOut
563 ; skTvs <- mapM (newMetaTyVar TauTv . typeKind) tysToLiftOut
564 ; let skTvs_tysTLO = zip skTvs tysToLiftOut
565 insertSkolems = return . replace skTvs_tysTLO
566 ; (_, body') <- tcGenericNormaliseFamInst insertSkolems body
567 ; inst' <- if swapped then mkEqInst (EqPred body' pat) co
568 else mkEqInst (EqPred pat body') co
569 -- ensure to reconstruct the inst in the
570 -- original orientation
571 ; traceTc $ text "oneSkolemOccurs[inst']:" <+> ppr inst'
572 ; (insts, undoSk) <- mapAndUnzipM (mkSkolemInst inst')
574 ; return (inst':insts, sequence_ undoSk)
577 co = eqInstCoercion inst
579 -- all subtypes that are (1) type family instances and (2) contain
580 -- the lhs type as part of the type arguments of the type family
582 tysToLiftOut = [mkTyConApp tc tys | (tc, tys) <- tyFamInsts body
583 , any (pat `tcPartOfType`) tys]
585 replace :: [(TcTyVar, Type)] -> Type -> Maybe (Type, Coercion)
586 replace [] _ = Nothing
587 replace ((skTv, tyTLO):rest) ty
588 | tyTLO `tcEqType` ty = Just (mkTyVarTy skTv, undefined)
589 | otherwise = replace rest ty
591 -- create the EqInst for the equality determining the skolem and a
592 -- TcM action undoing the skolem introduction
593 mkSkolemInst inst' (skTv, tyTLO)
594 = do { (co, tyLiftedOut) <- tcEqInstNormaliseFamInst inst' tyTLO
595 ; inst <- mkEqInst (EqPred tyLiftedOut (mkTyVarTy skTv))
596 (mkGivenCo $ mkSymCoercion (fromACo co))
597 -- co /= IdCo due to construction of inst'
598 ; return (inst, writeMetaTyVar skTv tyTLO)
603 Removal of trivial equalities: trivialRule
604 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
605 The following rules exploits the reflexivity of equality:
613 trivialRule :: IdemRewriteRule
615 = liftM catMaybes $ mappM trivial insts
618 | ASSERT( isEqInst inst )
620 = do { eitherEqInst inst
621 (\cotv -> writeMetaTyVar cotv ty1)
628 ty1 = eqInstLeftTy inst
629 ty2 = eqInstRightTy inst
633 Decomposition of data type constructors: decompRule
634 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
635 Whenever, the same *data* constructors occurs on both sides of an equality, we
636 can decompose as in standard unification.
641 g21 : c1 ~ d1, ..., g2n : cn ~ dn
644 Works also for the case where T is actually an application of a type family
645 constructor to a set of types, provided the applications on both sides of the
646 ~ are identical; see also Note [OpenSynTyCon app] in TcUnify.
648 We guarantee to raise an error for any inconsistent equalities;
649 cf Note [Inconsistencies in equality constraints].
652 decompRule :: RewriteRule
654 = do { (insts, changed) <- mapAndUnzipM decomp insts
655 ; return (concat insts, or changed)
659 = ASSERT( isEqInst inst )
660 go (eqInstLeftTy inst) (eqInstRightTy inst)
663 | Just ty1' <- tcView ty1 = go ty1' ty2
664 | Just ty2' <- tcView ty2 = go ty1 ty2'
666 go (TyConApp con1 tys1) (TyConApp con2 tys2)
667 | con1 == con2 && identicalHead
668 = mkArgInsts (mkTyConApp con1) tys1 tys2
670 | con1 /= con2 && not (isOpenSynTyCon con1 || isOpenSynTyCon con2)
671 -- not matching data constructors (of any flavour) are bad news
672 = eqInstMisMatch inst
675 (idxTys1, _) = splitAt n tys1
676 (idxTys2, _) = splitAt n tys2
677 identicalHead = not (isOpenSynTyCon con1) ||
678 idxTys1 `tcEqTypes` idxTys2
680 go (FunTy fun1 arg1) (FunTy fun2 arg2)
681 = mkArgInsts (\[funCo, argCo] -> mkFunTy funCo argCo) [fun1, arg1]
684 -- Applications need a bit of care!
685 -- They can match FunTy and TyConApp, so use splitAppTy_maybe
687 | Just (s2, t2) <- tcSplitAppTy_maybe ty2
688 = mkArgInsts (\[s, t] -> mkAppTy s t) [s1, t1] [s2, t2]
692 | Just (s1, t1) <- tcSplitAppTy_maybe ty1
693 = mkArgInsts (\[s, t] -> mkAppTy s t) [s1, t1] [s2, t2]
695 -- We already covered all the consistent cases of rigid types on both
696 -- sides; so, if we see two rigid types here, we discovered an
699 | isRigid ty1 && isRigid ty2
700 = eqInstMisMatch inst
702 -- We can neither assert consistency nor inconsistency => defer
703 go _ _ = return ([inst], False)
705 isRigid (TyConApp con _) = not (isOpenSynTyCon con)
706 isRigid (FunTy _ _) = True
707 isRigid (AppTy _ _) = True
710 -- Create insts for matching argument positions (ie, the bit after
711 -- '>-->' in the rule description above)
712 mkArgInsts con tys1 tys2
713 = do { cos <- eitherEqInst inst
714 -- old_co := Con1 cos
716 do { cotvs <- zipWithM newMetaCoVar tys1 tys2
717 ; let cos = map mkTyVarTy cotvs
718 ; writeMetaTyVar old_covar (con cos)
719 ; return $ map mkWantedCo cotvs
721 -- co_i := Con_i old_co
723 return $ map mkGivenCo $
724 mkRightCoercions (length tys1) old_co)
725 ; insts <- zipWithM mkEqInst (zipWith EqPred tys1 tys2) cos
726 ; traceTc (text "decomp identicalHead" <+> ppr insts)
727 ; return (insts, not $ null insts)
732 Rewriting with type instances: topRule
733 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
734 We use (toplevel) type instances to normalise both sides of equalities.
738 >--> co1 :: t ~ t' / co2 :: s ~ s'
740 g1 := co1 * g2 * sym co2
743 topRule :: RewriteRule
745 = do { (insts, changed) <- mapAndUnzipM top insts
746 ; return (insts, or changed)
750 = ASSERT( isEqInst inst )
751 do { (coi1, ty1') <- tcNormaliseFamInst ty1
752 ; (coi2, ty2') <- tcNormaliseFamInst ty2
753 ; case (coi1, coi2) of
754 (IdCo, IdCo) -> return (inst, False)
758 -- old_co = co1 * new_co * sym co2
760 do { new_cotv <- newMetaCoVar ty1' ty2'
761 ; let new_co = mkTyVarTy new_cotv
762 old_coi = coi1 `mkTransCoI`
763 ACo new_co `mkTransCoI`
765 ; writeMetaTyVar old_covar (fromACo old_coi)
766 ; return $ mkWantedCo new_cotv
768 -- new_co = sym co1 * old_co * co2
773 mkSymCoI coi1 `mkTransCoI`
774 ACo old_co `mkTransCoI` coi2)
775 ; new_inst <- mkEqInst (EqPred ty1' ty2') wg_co
776 ; return (new_inst, True)
780 ty1 = eqInstLeftTy inst
781 ty2 = eqInstRightTy inst
785 Rewriting with equalities: substRule
786 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
787 From a set of insts, use all insts that can be read as rewrite rules to
788 rewrite the types in all other insts.
792 forall g1 : s1{F c} ~ s2{F c}
795 g1 := s1{g} * g2 * sym s2{g} <=> g2 := sym s1{g} * g1 * s2{g}
797 Alternatively, the rewrite rule may have the form (g : a ~ t).
799 To avoid having to swap rules of the form (g : t ~ F c) and (g : t ~ a),
800 where t is neither a variable nor a type family application, we use them for
801 rewriting from right-to-left. However, it is crucial to only apply rules
802 from right-to-left if they cannot be used left-to-right.
804 The workhorse is substInst, which performs an occurs check before actually
805 using an equality for rewriting. If the type pattern occurs in the type we
806 substitute for the pattern, normalisation would diverge.
809 substRule :: RewriteRule
810 substRule insts = tryAllInsts insts []
812 -- for every inst check whether it can be used to rewrite the others
813 -- (we make an effort to keep the insts in order; it makes debugging
815 tryAllInsts [] triedInsts = return (reverse triedInsts, False)
816 tryAllInsts (inst:insts) triedInsts
817 = do { (insts', changed) <- substInst inst (reverse triedInsts ++ insts)
818 ; if changed then return (insertAt (length triedInsts) inst insts',
820 else tryAllInsts insts (inst:triedInsts)
823 insertAt n x xs = let (xs1, xs2) = splitAt n xs
826 -- Use the given inst as a rewrite rule to normalise the insts in the second
827 -- argument. Don't do anything if the inst cannot be used as a rewrite rule,
828 -- but do apply it right-to-left, if possible, and if it cannot be used
831 substInst :: Inst -> [Inst] -> TcM ([Inst], Bool)
833 = case eqInstToRewrite inst of
834 Just (rewrite, _) -> substEquality rewrite insts
835 Nothing -> return (insts, False)
837 substEquality :: Rewrite -- elementary rewrite
838 -> [Inst] -- insts to rewrite
839 -> TcM ([Inst], Bool)
840 substEquality eqRule@(Rewrite pat rhs _) insts
841 | pat `tcPartOfType` rhs -- occurs check!
842 = occurCheckErr pat rhs
844 = do { (insts', changed) <- mapAndUnzipM substOne insts
845 ; return (insts', or changed)
849 = ASSERT( isEqInst inst )
850 do { (coi1, ty1') <- tcEqRuleNormaliseFamInst eqRule ty1
851 ; (coi2, ty2') <- tcEqRuleNormaliseFamInst eqRule ty2
852 ; case (coi1, coi2) of
853 (IdCo, IdCo) -> return (inst, False)
857 -- old_co := co1 * new_co * sym co2
859 do { new_cotv <- newMetaCoVar ty1' ty2'
860 ; let new_co = mkTyVarTy new_cotv
861 old_coi = coi1 `mkTransCoI`
862 ACo new_co `mkTransCoI`
864 ; writeMetaTyVar old_covar (fromACo old_coi)
865 ; return $ mkWantedCo new_cotv
867 -- new_co := sym co1 * old_co * co2
872 mkSymCoI coi1 `mkTransCoI`
873 ACo old_co `mkTransCoI` coi2)
874 ; new_inst <- mkEqInst (EqPred ty1' ty2') gw_co
875 ; return (new_inst, True)
879 ty1 = eqInstLeftTy inst
880 ty2 = eqInstRightTy inst
884 Instantiate meta variables: unifyMetaRule
885 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
886 If an equality equates a meta type variable with a type, we simply instantiate
895 Meta variables can only appear in wanted constraints, and this rule should
896 only be applied to wanted constraints. We also know that t definitely is
897 distinct from alpha (as the trivialRule) has been run on the insts beforehand.
899 NB: We cannot assume that meta tyvars are empty. They may have been updated
900 by another inst in the currently processed wanted list. We need to be very
901 careful when updateing type variables (see TcUnify.uUnfilledVar), but at least
902 we know that we have no boxes. It's unclear that it would be an advantage to
903 common up the code in TcUnify and the code below. Firstly, we don't want
904 calls to TcUnify.defer_unification here, and secondly, TcUnify import the
905 current module, so we would have to move everything here (Yuk!) or to
906 TcMType. Besides, the code here is much simpler due to the lack of boxes.
909 unifyMetaRule :: RewriteRule
911 = do { (insts', changed) <- mapAndUnzipM unifyMeta insts
912 ; return (concat insts', or changed)
916 = ASSERT( isEqInst inst )
917 go (eqInstLeftTy inst) (eqInstRightTy inst)
918 (fromWantedCo "unifyMetaRule" $ eqInstCoercion inst)
921 | Just ty1' <- tcView ty1 = go ty1' ty2 cotv
922 | Just ty2' <- tcView ty2 = go ty1 ty2' cotv
925 , isMetaTyVar tv1 = do { lookupTV <- lookupTcTyVar tv1
926 ; uMeta False tv1 lookupTV ty2 cotv
929 , isMetaTyVar tv2 = do { lookupTV <- lookupTcTyVar tv2
930 ; uMeta True tv2 lookupTV ty1 cotv
932 | otherwise = return ([inst], False)
934 -- meta variable has been filled already
935 -- => ignore this inst (we'll come around again, after zonking)
936 uMeta _swapped _tv (IndirectTv _) _ty _cotv
937 = return ([inst], False)
939 -- signature skolem meets non-variable type
941 uMeta _swapped _tv (DoneTv (MetaTv (SigTv _) _)) ty _cotv
943 = return ([inst], False)
945 -- type variable meets type variable
946 -- => check that tv2 hasn't been updated yet and choose which to update
947 uMeta swapped tv1 (DoneTv details1) (TyVarTy tv2) cotv
948 = do { lookupTV2 <- lookupTcTyVar tv2
950 IndirectTv ty -> uMeta swapped tv1 (DoneTv details1) ty cotv
952 uMetaVar swapped tv1 details1 tv2 details2 cotv
955 -- updatable meta variable meets non-variable type
956 -- => occurs check, monotype check, and kinds match check, then update
957 uMeta swapped tv (DoneTv (MetaTv _ ref)) ty cotv
958 = do { mb_ty' <- checkTauTvUpdate tv ty -- occurs + monotype check
960 Nothing -> return ([inst], False) -- tv occurs in faminst
962 do { checkUpdateMeta swapped tv ref ty' -- update meta var
963 ; writeMetaTyVar cotv ty' -- update co var
968 uMeta _ _ _ _ _ = panic "uMeta"
970 -- meta variable meets skolem
972 uMetaVar swapped tv1 (MetaTv _ ref) tv2 (SkolemTv _) cotv
973 = do { checkUpdateMeta swapped tv1 ref (mkTyVarTy tv2)
974 ; writeMetaTyVar cotv (mkTyVarTy tv2)
978 -- meta variable meets meta variable
979 -- => be clever about which of the two to update
980 -- (from TcUnify.uUnfilledVars minus boxy stuff)
981 uMetaVar swapped tv1 (MetaTv info1 ref1) tv2 (MetaTv info2 ref2) cotv
982 = do { case (info1, info2) of
983 -- Avoid SigTvs if poss
984 (SigTv _, _ ) | k1_sub_k2 -> update_tv2
985 (_, SigTv _) | k2_sub_k1 -> update_tv1
987 (_, _) | k1_sub_k2 -> if k2_sub_k1 && nicer_to_update_tv1
988 then update_tv1 -- Same kinds
990 | k2_sub_k1 -> update_tv1
991 | otherwise -> kind_err
992 -- Update the variable with least kind info
993 -- See notes on type inference in Kind.lhs
994 -- The "nicer to" part only applies if the two kinds are the same,
995 -- so we can choose which to do.
997 ; writeMetaTyVar cotv (mkTyVarTy tv2)
1001 -- Kinds should be guaranteed ok at this point
1002 update_tv1 = updateMeta tv1 ref1 (mkTyVarTy tv2)
1003 update_tv2 = updateMeta tv2 ref2 (mkTyVarTy tv1)
1005 kind_err = addErrCtxtM (unifyKindCtxt swapped tv1 (mkTyVarTy tv2)) $
1006 unifyKindMisMatch k1 k2
1010 k1_sub_k2 = k1 `isSubKind` k2
1011 k2_sub_k1 = k2 `isSubKind` k1
1013 nicer_to_update_tv1 = isSystemName (Var.varName tv1)
1014 -- Try to update sys-y type variables in preference to ones
1015 -- gotten (say) by instantiating a polymorphic function with
1016 -- a user-written type sig
1018 uMetaVar _ _ _ _ _ _ = panic "uMetaVar"
1022 %************************************************************************
1024 \section{Normalisation of Insts}
1026 %************************************************************************
1028 Normalises a set of dictionaries relative to a set of given equalities (which
1029 are interpreted as rewrite rules). We only consider given equalities of the
1034 where F is a type family.
1037 substEqInDictInsts :: [Inst] -- given equalities (used as rewrite rules)
1038 -> [Inst] -- dictinaries to be normalised
1039 -> TcM ([Inst], TcDictBinds)
1040 substEqInDictInsts eqInsts dictInsts
1041 = do { traceTc (text "substEqInDictInst <-" <+> ppr dictInsts)
1043 foldlM rewriteWithOneEquality (dictInsts, emptyBag) eqInsts
1044 ; traceTc (text "substEqInDictInst ->" <+> ppr dictInsts')
1048 -- (1) Given equality of form 'F ts ~ t' or 'a ~ t': use for rewriting
1049 rewriteWithOneEquality (dictInsts, dictBinds)
1050 eqInst@(EqInst {tci_left = pattern,
1051 tci_right = target})
1052 | isOpenSynTyConApp pattern || isTyVarTy pattern
1053 = do { (dictInsts', moreDictBinds) <-
1054 genericNormaliseInsts True {- wanted -} applyThisEq dictInsts
1055 ; return (dictInsts', dictBinds `unionBags` moreDictBinds)
1058 applyThisEq = tcGenericNormaliseFamInstPred (return . matchResult)
1060 -- rewrite in case of an exact match
1061 matchResult ty | tcEqType pattern ty = Just (target, eqInstType eqInst)
1062 | otherwise = Nothing
1064 -- (2) Given equality has the wrong form: ignore
1065 rewriteWithOneEquality (dictInsts, dictBinds) _not_a_rewrite_rule
1066 = return (dictInsts, dictBinds)
1070 Take a bunch of Insts (not EqInsts), and normalise them wrt the top-level
1071 type-function equations, where
1073 (norm_insts, binds) = normaliseInsts is_wanted insts
1076 = True, (binds + norm_insts) defines insts (wanteds)
1077 = False, (binds + insts) defines norm_insts (givens)
1079 Ie, in the case of normalising wanted dictionaries, we use the normalised
1080 dictionaries to define the originally wanted ones. However, in the case of
1081 given dictionaries, we use the originally given ones to define the normalised
1085 normaliseInsts :: Bool -- True <=> wanted insts
1086 -> [Inst] -- wanted or given insts
1087 -> TcM ([Inst], TcDictBinds) -- normalised insts and bindings
1088 normaliseInsts isWanted insts
1089 = genericNormaliseInsts isWanted tcNormaliseFamInstPred insts
1091 genericNormaliseInsts :: Bool -- True <=> wanted insts
1092 -> (TcPredType -> TcM (CoercionI, TcPredType))
1094 -> [Inst] -- wanted or given insts
1095 -> TcM ([Inst], TcDictBinds) -- normalised insts & binds
1096 genericNormaliseInsts isWanted fun insts
1097 = do { (insts', binds) <- mapAndUnzipM (normaliseOneInst isWanted fun) insts
1098 ; return (insts', unionManyBags binds)
1101 normaliseOneInst isWanted fun
1102 dict@(Dict {tci_pred = pred,
1104 = do { traceTc $ text "genericNormaliseInst <-" <+> ppr dict
1105 ; (coi, pred') <- fun pred
1109 do { traceTc $ text "genericNormaliseInst ->" <+> ppr dict
1110 ; return (dict, emptyBag)
1112 -- don't use pred' in this case; otherwise, we get
1113 -- more unfolded closed type synonyms in error messages
1115 do { -- an inst for the new pred
1116 ; dict' <- newDictBndr loc pred'
1117 -- relate the old inst to the new one
1118 -- target_dict = source_dict `cast` st_co
1119 ; let (target_dict, source_dict, st_co)
1120 | isWanted = (dict, dict', mkSymCoercion co)
1121 | otherwise = (dict', dict, co)
1123 -- co :: dict ~ dict'
1124 -- hence, if isWanted
1125 -- dict = dict' `cast` sym co
1127 -- dict' = dict `cast` co
1128 expr = HsVar $ instToId source_dict
1129 cast_expr = HsWrap (WpCo st_co) expr
1130 rhs = L (instLocSpan loc) cast_expr
1131 binds = instToDictBind target_dict rhs
1132 -- return the new inst
1133 ; traceTc $ text "genericNormaliseInst ->" <+> ppr dict'
1134 ; return (dict', binds)
1138 -- TOMDO: What do we have to do about ImplicInst, Method, and LitInst??
1139 normaliseOneInst _isWanted _fun inst
1140 = do { inst' <- zonkInst inst
1141 ; return (inst', emptyBag)
1146 %************************************************************************
1150 %************************************************************************
1152 The infamous couldn't match expected type soandso against inferred type
1153 somethingdifferent message.
1156 eqInstMisMatch :: Inst -> TcM a
1158 = ASSERT( isEqInst inst )
1159 do { (env, msg) <- misMatchMsg ty_act ty_exp
1161 failWithTcM (env, msg)
1164 ty_act = eqInstLeftTy inst
1165 ty_exp = eqInstRightTy inst
1166 InstLoc _ _ ctxt = instLoc inst
1168 -----------------------
1169 misMatchMsg :: TcType -> TcType -> TcM (TidyEnv, SDoc)
1170 -- Generate the message when two types fail to match,
1171 -- going to some trouble to make it helpful.
1172 -- The argument order is: actual type, expected type
1173 misMatchMsg ty_act ty_exp
1174 = do { env0 <- tcInitTidyEnv
1175 ; ty_exp <- zonkTcType ty_exp
1176 ; ty_act <- zonkTcType ty_act
1177 ; (env1, pp_exp, extra_exp) <- ppr_ty env0 ty_exp
1178 ; (env2, pp_act, extra_act) <- ppr_ty env1 ty_act
1180 sep [sep [ptext SLIT("Couldn't match expected type") <+> pp_exp,
1182 ptext SLIT("against inferred type") <+> pp_act],
1183 nest 2 (extra_exp $$ extra_act)]) }
1185 ppr_ty :: TidyEnv -> TcType -> TcM (TidyEnv, SDoc, SDoc)
1187 = do { let (env1, tidy_ty) = tidyOpenType env ty
1188 ; (env2, extra) <- ppr_extra env1 tidy_ty
1189 ; return (env2, quotes (ppr tidy_ty), extra) }
1191 -- (ppr_extra env ty) shows extra info about 'ty'
1192 ppr_extra :: TidyEnv -> Type -> TcM (TidyEnv, SDoc)
1193 ppr_extra env (TyVarTy tv)
1194 | isSkolemTyVar tv || isSigTyVar tv
1195 = return (env1, pprSkolTvBinding tv1)
1197 (env1, tv1) = tidySkolemTyVar env tv
1199 ppr_extra env _ty = return (env, empty) -- Normal case