\begin{code}
-{-# OPTIONS_GHC -w #-}
--- The above warning supression flag is a temporary kludge.
--- While working on this module you are encouraged to remove it and fix
--- any warnings in the module. See
--- http://hackage.haskell.org/trac/ghc/wiki/WorkingConventions#Warnings
--- for details
-
-module TcTyFuns(
- finalizeEqInst,
- partitionWantedEqInsts, partitionGivenEqInsts,
-
+module TcTyFuns (
tcNormalizeFamInst,
normaliseGivens, normaliseGivenDicts,
import TcRnMonad
import TcEnv
import Inst
-import FamInstEnv
import TcType
import TcMType
import Coercion
import TypeRep ( Type(..) )
import TyCon
-import Var ( mkCoVar, isTcTyVar )
+import Var ( isTcTyVar )
import Type
-import HscTypes ( ExternalPackageState(..) )
import Bag
import Outputable
import SrcLoc ( Located(..) )
import Maybes
import Data.List
-\end{code}
-
-%************************************************************************
-%* *
-\section{Eq Insts}
-%* *
-%************************************************************************
-
-%************************************************************************
-%* *
-\section{Utility Code}
-%* *
-%************************************************************************
-
-\begin{code}
-partitionWantedEqInsts
- :: [Inst] -- wanted insts
- -> ([Inst],[Inst]) -- (wanted equations,wanted dicts)
-partitionWantedEqInsts = partitionEqInsts True
-
-partitionGivenEqInsts
- :: [Inst] -- given insts
- -> ([Inst],[Inst]) -- (given equations,given dicts)
-partitionGivenEqInsts = partitionEqInsts False
-
-
-partitionEqInsts
- :: Bool -- <=> wanted
- -> [Inst] -- insts
- -> ([Inst],[Inst]) -- (equations,dicts)
-partitionEqInsts wanted []
- = ([],[])
-partitionEqInsts wanted (i:is)
- | isEqInst i
- = (i:es,ds)
- | otherwise
- = (es,i:ds)
- where (es,ds) = partitionEqInsts wanted is
-
-isEqDict :: Inst -> Bool
-isEqDict (Dict {tci_pred = EqPred _ _}) = True
-isEqDict _ = False
-
+import Control.Monad (liftM)
\end{code}
| not (isOpenSynTyCon tycon) -- unfold *only* _synonym_ family instances
= return Nothing
| otherwise
- = do { maybeFamInst <- tcLookupFamInst tycon tys
+ = do { -- we only use the indexing arguments for matching,
+ -- not the additional ones
+ ; maybeFamInst <- tcLookupFamInst tycon idxTys
; case maybeFamInst of
Nothing -> return Nothing
- Just (rep_tc, rep_tys) -> return $ Just (mkTyConApp rep_tc rep_tys,
- mkTyConApp coe_tc rep_tys)
+ Just (rep_tc, rep_tys) -> return $ Just (mkTyConApp rep_tc tys',
+ mkTyConApp coe_tc tys')
where
+ tys' = rep_tys ++ restTys
coe_tc = expectJust "TcTyFun.tcUnfoldSynFamInst"
(tyConFamilyCoercion_maybe rep_tc)
}
+ where
+ n = tyConArity tycon
+ (idxTys, restTys) = splitAt n tys
tcUnfoldSynFamInst _other = return Nothing
\end{code}
then co : ty ~ ty'
\begin{code}
-tcNormalizeFamInst :: Type -> TcM (CoercionI, Type)
+tcNormalizeFamInst :: TcType -> TcM (CoercionI, TcType)
tcNormalizeFamInst = tcGenericNormalizeFamInst tcUnfoldSynFamInst
tcNormalizeFamInstPred :: TcPredType -> TcM (CoercionI, TcPredType)
tcNormalizeFamInstPred = tcGenericNormalizeFamInstPred tcUnfoldSynFamInst
\end{code}
+Normalise a type relative to the rewrite rule implied by one EqInst.
+
+\begin{code}
+tcEqInstNormalizeFamInst :: Inst -> TcType -> TcM (CoercionI, Type)
+tcEqInstNormalizeFamInst inst = ASSERT( isEqInst inst )
+ tcGenericNormalizeFamInst matchInst
+ where
+ pat = eqInstLeftTy inst
+ rhs = eqInstRightTy inst
+ co = eitherEqInst inst TyVarTy id
+ --
+ matchInst ty | pat `tcEqType` ty = return $ Just (rhs, co)
+ | otherwise = return $ Nothing
+\end{code}
+
Generic normalisation of 'Type's and 'PredType's; ie, walk the type term and
apply the normalisation function gives as the first argument to every TyConApp
and every TyVarTy subterm.
good error messages, callers should discard ty' in favour of ty in this case.
\begin{code}
-tcGenericNormalizeFamInst :: (TcType -> TcM (Maybe (TcType,Coercion)))
+tcGenericNormalizeFamInst :: (TcType -> TcM (Maybe (TcType, Coercion)))
-- what to do with type functions and tyvars
-> TcType -- old type
- -> TcM (CoercionI, Type) -- (coercion, new type)
+ -> TcM (CoercionI, TcType) -- (coercion, new type)
tcGenericNormalizeFamInst fun ty
| Just ty' <- tcView ty = tcGenericNormalizeFamInst fun ty'
-tcGenericNormalizeFamInst fun ty@(TyConApp tyCon tys)
+tcGenericNormalizeFamInst fun (TyConApp tyCon tys)
= do { (cois, ntys) <- mapAndUnzipM (tcGenericNormalizeFamInst fun) tys
; let tycon_coi = mkTyConAppCoI tyCon ntys cois
; maybe_ty_co <- fun (TyConApp tyCon ntys) -- use normalised args!
-- we do not do anything
Nothing -> return (tycon_coi, TyConApp tyCon ntys)
}
-tcGenericNormalizeFamInst fun ty@(AppTy ty1 ty2)
+tcGenericNormalizeFamInst fun (AppTy ty1 ty2)
= do { (coi1,nty1) <- tcGenericNormalizeFamInst fun ty1
; (coi2,nty2) <- tcGenericNormalizeFamInst fun ty2
; return (mkAppTyCoI nty1 coi1 nty2 coi2, AppTy nty1 nty2)
}
-tcGenericNormalizeFamInst fun ty@(FunTy ty1 ty2)
+tcGenericNormalizeFamInst fun (FunTy ty1 ty2)
= do { (coi1,nty1) <- tcGenericNormalizeFamInst fun ty1
; (coi2,nty2) <- tcGenericNormalizeFamInst fun ty2
; return (mkFunTyCoI nty1 coi1 nty2 coi2, FunTy nty1 nty2)
}
-tcGenericNormalizeFamInst fun ty@(ForAllTy tyvar ty1)
+tcGenericNormalizeFamInst fun (ForAllTy tyvar ty1)
= do { (coi,nty1) <- tcGenericNormalizeFamInst fun ty1
; return (mkForAllTyCoI tyvar coi,ForAllTy tyvar nty1)
}
-tcGenericNormalizeFamInst fun ty@(NoteTy note ty1)
+tcGenericNormalizeFamInst fun (NoteTy note ty1)
= do { (coi,nty1) <- tcGenericNormalizeFamInst fun ty1
; return (mkNoteTyCoI note coi,NoteTy note nty1)
}
%************************************************************************
%* *
-\section{Normalisation of Wanteds}
+\section{Normalisation of wanteds constraints}
%* *
%************************************************************************
\begin{code}
normaliseWanteds :: [Inst] -> TcM [Inst]
normaliseWanteds insts
- = do { traceTc (text "normaliseWanteds" <+> ppr insts)
- ; result <- eq_rewrite
- [ ("(Occurs)", simple_rewrite_check $ occursCheckInsts)
- , ("(ZONK)", simple_rewrite $ zonkInsts)
+ = do { traceTc (text "normaliseWanteds <-" <+> ppr insts)
+ ; result <- liftM fst $ rewriteToFixedPoint Nothing
+ [ ("(Occurs)", noChange $ occursCheckInsts)
+ , ("(ZONK)", dontRerun $ zonkInsts)
, ("(TRIVIAL)", trivialInsts)
- , ("(SWAP)", swapInsts)
+ -- no `swapInsts'; it messes up error messages and should
+ -- not be necessary -=chak
, ("(DECOMP)", decompInsts)
, ("(TOP)", topInsts)
, ("(SUBST)", substInsts)
}
\end{code}
+
%************************************************************************
%* *
-\section{Normalisation of Givens}
+\section{Normalisation of givens constraints}
%* *
%************************************************************************
\begin{code}
+normaliseGivens :: [Inst] -> TcM ([Inst], TcM ())
+normaliseGivens givens
+ = do { traceTc (text "normaliseGivens <-" <+> ppr givens)
+ ; (result, deSkolem) <-
+ rewriteToFixedPoint (Just ("(SkolemOccurs)", skolemOccurs))
+ [ ("(Occurs)", noChange $ occursCheckInsts)
+ , ("(ZONK)", dontRerun $ zonkInsts)
+ , ("(TRIVIAL)", trivialInsts)
+ , ("(SWAP)", swapInsts)
+ , ("(DECOMP)", decompInsts)
+ , ("(TOP)", topInsts)
+ , ("(SUBST)", substInsts)
+ ] givens
+ ; traceTc (text "normaliseGivens ->" <+> ppr result)
+ ; return (result, deSkolem)
+ }
+\end{code}
-normaliseGivens :: [Inst] -> TcM ([Inst],TcM ())
-normaliseGivens givens =
- do { traceTc (text "normaliseGivens <-" <+> ppr givens)
- ; (result,action) <- given_eq_rewrite
- ("(SkolemOccurs)", skolemOccurs)
- (return ())
- [("(Occurs)", simple_rewrite_check $ occursCheckInsts),
- ("(ZONK)", simple_rewrite $ zonkInsts),
- ("(TRIVIAL)", trivialInsts),
- ("(SWAP)", swapInsts),
- ("(DECOMP)", decompInsts),
- ("(TOP)", topInsts),
- ("(SUBST)", substInsts)]
- givens
- ; traceTc (text "normaliseGivens ->" <+> ppr result)
- ; return (result,action)
- }
-skolemOccurs :: [Inst] -> TcM ([Inst],TcM ())
-skolemOccurs [] = return ([], return ())
-skolemOccurs (inst@(EqInst {}):insts)
- = do { (insts',actions) <- skolemOccurs insts
- -- check whether the current inst co :: ty1 ~ ty2 suffers
- -- from the occurs check issue: F ty1 \in ty2
- ; let occurs = go False ty2
- ; if occurs
- then
- -- if it does generate two new coercions:
- do { skolem_var <- newMetaTyVar TauTv (typeKind ty1)
- ; let skolem_ty = TyVarTy skolem_var
- -- ty1 :: ty1 ~ b
- ; inst1 <- mkEqInst (EqPred ty1 skolem_ty) (mkGivenCo ty1)
- -- sym co :: ty2 ~ b
- ; inst2 <- mkEqInst (EqPred ty2 skolem_ty) (mkGivenCo $ fromACo $ mkSymCoI $ ACo $ fromGivenCo co)
- -- to replace the old one
- -- the corresponding action is
- -- b := ty1
- ; let action = writeMetaTyVar skolem_var ty1
- ; return (inst1:inst2:insts', action >> actions)
- }
- else
- return (inst:insts', actions)
- }
- where
- ty1 = eqInstLeftTy inst
- ty2 = eqInstRightTy inst
- co = eqInstCoercion inst
- check :: Bool -> TcType -> Bool
- check flag ty
- = if flag && ty1 `tcEqType` ty
- then True
- else go flag ty
-
- go flag (TyConApp con tys) = or $ map (check (isOpenSynTyCon con || flag)) tys
- go flag (FunTy arg res) = or $ map (check flag) [arg,res]
- go flag (AppTy fun arg) = or $ map (check flag) [fun,arg]
- go flag ty = False
+This is an (attempt at, yet unproven, an) *unflattened* version of
+the SubstL-Ev completion rule.
+
+The above rule is essential to catch non-terminating
+rules that cannot be oriented properly, like
+
+ F a ~ [G (F a)]
+ or even
+ a ~ [G a]
+
+The left-to-right orientiation is not suitable because it does not
+terminate.
+The right-to-left orientation is not suitable because it
+does not have a type-function on the left. This is undesirable because
+it would hide information. E.g. assume
+ instance C [x]
+then rewriting C [G (F a)] to C (F a) is bad because we cannot now
+see that the C [x] instance applies.
+
+The rule also caters for badly-oriented rules of the form:
+ F a ~ G (F a)
+for which other solutions are possible, but this one will do too.
+
+It's behavior is:
+ co : ty1 ~ ty2{F ty1}
+ >-->
+ co : ty1 ~ ty2{b}
+ sym (F co) : F ty2{b} ~ b
+ where b is a fresh skolem variable
+
+We also return an action (b := ty1) which is used to eliminate b
+after the dust of normalisation with the completed rewrite system
+has settled.
+
+A subtle point of this transformation is that both coercions in the results
+are strictly speaking incorrect. However, they are correct again after the
+action {B := ty1} has removed the skolem again. This happens immediately
+after constraint entailment has been checked; ie, code outside of the
+simplification and entailment checking framework will never see these
+temporarily incorrect coercions.
+
+NB: We perform this transformation for multiple occurences of ty1 under one
+ or multiple family applications on the left-hand side at once (ie, the
+ rule doesn't need to be applied multiple times at a single inst). As a
+ result we can get two or more insts back.
+
+\begin{code}
+skolemOccurs :: PrecondRule
+skolemOccurs insts
+ = do { (instss, undoSkolems) <- mapAndUnzipM oneSkolemOccurs insts
+ ; return (concat instss, sequence_ undoSkolems)
+ }
+ where
+ oneSkolemOccurs inst
+ | null tysToLiftOut
+ = return ([inst], return ())
+ | otherwise
+ = do { skTvs <- mapM (newMetaTyVar TauTv . typeKind) tysToLiftOut
+ ; let skTvs_tysTLO = zip skTvs tysToLiftOut
+ insertSkolems = return . replace skTvs_tysTLO
+ ; (_, ty2') <- tcGenericNormalizeFamInst insertSkolems ty2
+ ; inst' <- mkEqInst (EqPred ty1 ty2') co
+ ; (insts, undoSk) <- mapAndUnzipM (mkSkolemInst inst') skTvs_tysTLO
+ ; return (inst':insts, sequence_ undoSk)
+ }
+ where
+ ty1 = eqInstLeftTy inst
+ ty2 = eqInstRightTy inst
+ co = eqInstCoercion inst
+
+ -- all subtypes that are (1) type family instances and (2) contain the
+ -- lhs type as part of the type arguments of the type family constructor
+ tysToLiftOut = ASSERT( isEqInst inst )
+ [mkTyConApp tc tys | (tc, tys) <- tyFamInsts ty2
+ , any (ty1 `tcPartOfType`) tys]
+
+ replace :: [(TcTyVar, Type)] -> Type -> Maybe (Type, Coercion)
+ replace [] _ = Nothing
+ replace ((skTv, tyTLO):rest) ty
+ | tyTLO `tcEqType` ty = Just (mkTyVarTy skTv, undefined)
+ | otherwise = replace rest ty
+
+ -- create the EqInst for the equality determining the skolem and a
+ -- TcM action undoing the skolem introduction
+ mkSkolemInst inst' (skTv, tyTLO)
+ = do { (co, tyLiftedOut) <- tcEqInstNormalizeFamInst inst' tyTLO
+ ; inst <- mkEqInst (EqPred tyLiftedOut (mkTyVarTy skTv))
+ (mkGivenCo $ mkSymCoercion (fromACo co))
+ ; return (inst, writeMetaTyVar skTv tyTLO)
+ }
\end{code}
+
%************************************************************************
%* *
-\section{Solving of Wanteds}
+\section{Solving of wanted constraints with respect to a given set}
%* *
%************************************************************************
\begin{code}
-solveWanteds ::
- [Inst] -> -- givens
- [Inst] -> -- wanteds
- TcM [Inst] -- irreducible wanteds
-solveWanteds givens wanteds =
- do { traceTc (text "solveWanteds <-" <+> ppr wanteds <+> text "with" <+> ppr givens)
- ; result <- eq_rewrite
- [("(Occurs)", simple_rewrite_check $ occursCheckInsts),
- ("(TRIVIAL)", trivialInsts),
- ("(DECOMP)", decompInsts),
- ("(TOP)", topInsts),
- ("(GIVEN)", givenInsts givens),
- ("(UNIFY)", unifyInsts)]
- wanteds
- ; traceTc (text "solveWanteds ->" <+> ppr result)
- ; return result
+solveWanteds :: [Inst] -- givens
+ -> [Inst] -- wanteds
+ -> TcM [Inst] -- irreducible wanteds
+solveWanteds givens wanteds
+ = do { traceTc $ text "solveWanteds <-" <+> ppr wanteds <+> text "with" <+>
+ ppr givens
+ ; result <- liftM fst $ rewriteToFixedPoint Nothing
+ [ ("(Occurs)", noChange $ occursCheckInsts)
+ , ("(TRIVIAL)", trivialInsts)
+ , ("(DECOMP)", decompInsts)
+ , ("(TOP)", topInsts)
+ , ("(GIVEN)", givenInsts givens)
+ , ("(UNIFY)", unifyInsts)
+ ] wanteds
+ ; traceTc (text "solveWanteds ->" <+> ppr result)
+ ; return result
+ }
+ where
+ -- Use `substInst' with every given on all the wanteds.
+ givenInsts :: [Inst] -> [Inst] -> TcM ([Inst],Bool)
+ givenInsts [] wanteds = return (wanteds,False)
+ givenInsts (g:gs) wanteds
+ = do { (wanteds1, changed1) <- givenInsts gs wanteds
+ ; (wanteds2, changed2) <- substInst g wanteds1
+ ; return (wanteds2, changed1 || changed2)
}
+\end{code}
-givenInsts :: [Inst] -> [Inst] -> TcM ([Inst],Bool)
-givenInsts [] wanteds
- = return (wanteds,False)
-givenInsts (g:gs) wanteds
- = do { (wanteds1,changed1) <- givenInsts gs wanteds
- ; (wanteds2,changed2) <- substInst g wanteds1
- ; return (wanteds2,changed1 || changed2)
- }
+%************************************************************************
+%* *
+\section{Normalisation rules and iterative rule application}
+%* *
+%************************************************************************
+We have four kinds of normalising rewrite rules:
+(1) Normalisation rules that rewrite a set of insts and return a flag indicating
+ whether any changes occurred during rewriting that necessitate re-running
+ the current rule set.
- -- fixpoint computation
- -- of a number of rewrites of equalities
-eq_rewrite ::
- [(String,[Inst] -> TcM ([Inst],Bool))] -> -- rewrite functions and descriptions
- [Inst] -> -- initial equations
- TcM [Inst] -- final equations (at fixed point)
-eq_rewrite rewrites insts
- = go rewrites insts
- where
- go _ [] -- return quickly when there's nothing to be done
- = return []
- go [] insts
- = return insts
- go ((desc,r):rs) insts
- = do { (insts',changed) <- r insts
- ; traceTc (text desc <+> ppr insts')
- ; if changed
- then loop insts'
- else go rs insts'
- }
- loop = eq_rewrite rewrites
-
- -- fixpoint computation
- -- of a number of rewrites of equalities
-given_eq_rewrite ::
-
- (String,[Inst] -> TcM ([Inst],TcM ())) ->
- (TcM ()) ->
- [(String,[Inst] -> TcM ([Inst],Bool))] -> -- rewrite functions and descriptions
- [Inst] -> -- initial equations
- TcM ([Inst],TcM ()) -- final equations (at fixed point)
-given_eq_rewrite p@(desc,start) acc rewrites insts
- = do { (insts',acc') <- start insts
- ; go (acc >> acc') rewrites insts'
- }
- where
- go acc _ [] -- return quickly when there's nothing to be done
- = return ([],acc)
- go acc [] insts
- = return (insts,acc)
- go acc ((desc,r):rs) insts
- = do { (insts',changed) <- r insts
- ; traceTc (text desc <+> ppr insts')
- ; if changed
- then loop acc insts'
- else go acc rs insts'
- }
- loop acc = given_eq_rewrite p acc rewrites
-
-simple_rewrite ::
- ([Inst] -> TcM [Inst]) ->
- ([Inst] -> TcM ([Inst],Bool))
-simple_rewrite r insts
- = do { insts' <- r insts
- ; return (insts',False)
- }
+(2) Precondition rules that rewrite a set of insts and return a monadic action
+ that reverts the effect of preconditioning.
+
+(3) Idempotent normalisation rules that never require re-running the rule set.
+
+(4) Checking rule that does not alter the set of insts.
+
+\begin{code}
+type RewriteRule = [Inst] -> TcM ([Inst], Bool) -- rewrite, maybe re-run
+type PrecondRule = [Inst] -> TcM ([Inst], TcM ()) -- rewrite, revertable
+type IdemRewriteRule = [Inst] -> TcM [Inst] -- rewrite, don't re-run
+type CheckRule = [Inst] -> TcM () -- check
+
+type NamedRule = (String, RewriteRule) -- rule with description
+type NamedPreRule = (String, PrecondRule) -- precond with desc
+\end{code}
+
+Templates lifting idempotent and checking rules to full rules (which can be put
+into a rule set).
+
+\begin{code}
+dontRerun :: IdemRewriteRule -> RewriteRule
+dontRerun rule insts = liftM addFalse $ rule insts
+ where
+ addFalse x = (x, False)
+
+noChange :: CheckRule -> RewriteRule
+noChange rule insts = rule insts >> return (insts, False)
+\end{code}
+
+The following function applies a set of rewrite rules until a fixed point is
+reached; i.e., none of the `RewriteRule's require re-running the rule set.
+Optionally, there may be a pre-conditing rule that is applied before any other
+rules are applied and before the rule set is re-run.
-simple_rewrite_check ::
- ([Inst] -> TcM ()) ->
- ([Inst] -> TcM ([Inst],Bool))
-simple_rewrite_check check insts
- = check insts >> return (insts,False)
-
+The result is the set of rewritten (i.e., normalised) insts and, in case of a
+pre-conditing rule, a monadic action that reverts the effects of
+pre-conditioning - specifically, this is removing introduced skolems.
+\begin{code}
+rewriteToFixedPoint :: Maybe NamedPreRule -- optional preconditioning rule
+ -> [NamedRule] -- rule set
+ -> [Inst] -- insts to rewrite
+ -> TcM ([Inst], TcM ())
+rewriteToFixedPoint precondRule rules insts
+ = completeRewrite (return ()) precondRule insts
+ where
+ completeRewrite :: TcM () -> Maybe NamedPreRule -> [Inst]
+ -> TcM ([Inst], TcM ())
+ completeRewrite dePrecond (Just (precondName, precond)) insts
+ = do { (insts', dePrecond') <- precond insts
+ ; traceTc $ text precondName <+> ppr insts'
+ ; tryRules (dePrecond >> dePrecond') rules insts'
+ }
+ completeRewrite dePrecond Nothing insts
+ = tryRules dePrecond rules insts
+
+ tryRules dePrecond _ [] = return ([] , dePrecond)
+ tryRules dePrecond [] insts = return (insts, dePrecond)
+ tryRules dePrecond ((name, rule):rules) insts
+ = do { (insts', rerun) <- rule insts
+ ; traceTc $ text name <+> ppr insts'
+ ; if rerun then completeRewrite dePrecond precondRule insts'
+ else tryRules dePrecond rules insts'
+ }
\end{code}
+
%************************************************************************
%* *
\section{Different forms of Inst rewritings}
-- >-->
-- g1 := t
--
-trivialInsts ::
- [Inst] -> -- equations
- TcM ([Inst],Bool) -- remaining equations, any changes?
+trivialInsts :: RewriteRule
trivialInsts []
= return ([],False)
trivialInsts (i@(EqInst {}):is)
where
ty1 = eqInstLeftTy i
ty2 = eqInstRightTy i
+trivialInsts _ = panic "TcTyFuns.trivialInsts: not EqInst"
-- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-swapInsts :: [Inst] -> TcM ([Inst],Bool)
+swapInsts :: RewriteRule
-- All the inputs and outputs are equalities
-swapInsts insts = mapAndUnzipM swapInst insts >>= \(insts',changeds) -> return (insts',or changeds)
-
+swapInsts insts
+ = do { (insts', changeds) <- mapAndUnzipM swapInst insts
+ ; return (insts', or changeds)
+ }
-- (Swap)
- -- g1 : c ~ Fd
+ -- g1 : c ~ F d
-- >-->
- -- g2 : Fd ~ c
+ -- g2 : F d ~ c
-- g1 := sym g2
+ -- where c isn't a function call
+ -- and
--
+ -- g1 : c ~ a
+ -- >-->
+ -- g2 : a ~ c
+ -- g1 := sym g2
+ -- where c isn't a function call or other variable
+swapInst :: Inst -> TcM (Inst, Bool)
swapInst i@(EqInst {})
= go ty1 ty2
where
-- we should swap!
go ty1 ty2@(TyConApp tyCon _)
| isOpenSynTyCon tyCon
- = do { wg_co <- eitherEqInst i
+ = actual_swap ty1 ty2
+ go ty1@(TyConApp _ _) ty2@(TyVarTy _)
+ = actual_swap ty1 ty2
+ go _ _ = return (i,False)
+
+ actual_swap ty1 ty2 = do { wg_co <- eitherEqInst i
-- old_co := sym new_co
(\old_covar ->
do { new_cotv <- newMetaTyVar TauTv (mkCoKind ty2 ty1)
; new_inst <- mkEqInst (EqPred ty2 ty1) wg_co
; return (new_inst,True)
}
- go _ _ = return (i,False)
+swapInst _ = panic "TcTyFuns.swapInst: not EqInst"
-- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-decompInsts :: [Inst] -> TcM ([Inst],Bool)
+decompInsts :: RewriteRule
decompInsts insts = do { (insts,bs) <- mapAndUnzipM decompInst insts
; return (concat insts,or bs)
}
do { cotvs <- zipWithM (\t1 t2 ->
newMetaTyVar TauTv
(mkCoKind t1 t2))
- tys1' tys2'
+ tys1 tys2
; let cos = map TyVarTy cotvs
; writeMetaTyVar old_covar (TyConApp con1 cos)
; return $ map mkWantedCo cotvs
-- co_i := Con_i old_co
(\old_co -> return $
map mkGivenCo $
- mkRightCoercions (length tys1') old_co)
- ; insts <- zipWithM mkEqInst (zipWith EqPred tys1' tys2') cos
- ; return (insts, not $ null insts)
+ mkRightCoercions (length tys1) old_co)
+ ; insts <- zipWithM mkEqInst (zipWith EqPred tys1 tys2) cos
+ ; traceTc (text "decomp identicalHead" <+> ppr insts)
+ ; return (insts, not $ null insts)
}
| con1 /= con2 && not (isOpenSynTyCon con1 || isOpenSynTyCon con2)
-- not matching data constructors (of any flavour) are bad news
= do { env0 <- tcInitTidyEnv
- ; let (env1, tidy_ty1) = tidyOpenType env0 ty1
- (env2, tidy_ty2) = tidyOpenType env1 ty2
- extra = sep [ppr tidy_ty1, char '~', ppr tidy_ty2]
- msg = ptext SLIT("Couldn't match expected type against inferred type")
+ ; let (env1, tidy_ty1) = tidyOpenType env0 ty1
+ (env2, tidy_ty2) = tidyOpenType env1 ty2
+ extra = sep [ppr tidy_ty1, char '~', ppr tidy_ty2]
+ msg =
+ ptext SLIT("Unsolvable equality constraint:")
; failWithTcM (env2, hang msg 2 extra)
}
where
- n = tyConArity con1
- (idxTys1, tys1') = splitAt n tys1
- (idxTys2, tys2') = splitAt n tys2
- identicalHead = not (isOpenSynTyCon con1) ||
- idxTys1 `tcEqTypes` idxTys2
+ n = tyConArity con1
+ (idxTys1, _) = splitAt n tys1
+ (idxTys2, _) = splitAt n tys2
+ identicalHead = not (isOpenSynTyCon con1) ||
+ idxTys1 `tcEqTypes` idxTys2
go _ _ = return ([i], False)
+decompInst _ = panic "TcTyFuns.decompInst: not EqInst"
-- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-topInsts :: [Inst] -> TcM ([Inst],Bool)
+topInsts :: RewriteRule
topInsts insts
= do { (insts,bs) <- mapAndUnzipM topInst insts
; return (insts,or bs)
where
ty1 = eqInstLeftTy i
ty2 = eqInstRightTy i
+topInst _ = panic "TcTyFuns.topInsts: not EqInst"
-- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-substInsts :: [Inst] -> TcM ([Inst],Bool)
+substInsts :: RewriteRule
substInsts insts = substInstsWorker insts []
+substInstsWorker :: [Inst] -> [Inst] -> TcM ([Inst],Bool)
substInstsWorker [] acc
= return (acc,False)
substInstsWorker (i:is) acc
then return ((i:is'),True)
else substInstsWorker is (i:acc)
}
+ | (TyVarTy _) <- tci_left i
+ = do { (is',change) <- substInst i (acc ++ is)
+ ; if change
+ then return ((i:is'),True)
+ else substInstsWorker is (i:acc)
+ }
| otherwise
= substInstsWorker is (i:acc)
-- >-->
-- g2 : s1{t} ~ s2{t}
-- g1 := s1{g} * g2 * sym s2{g} <=> g2 := sym s1{g} * g1 * s2{g}
-substInst inst []
- = return ([],False)
-substInst inst@(EqInst {tci_left = pattern, tci_right = target}) (i@(EqInst {tci_left = ty1, tci_right = ty2}):is)
+substInst :: Inst -> [Inst] -> TcM ([Inst], Bool)
+substInst _inst [] = return ([],False)
+substInst inst (i@(EqInst {tci_left = ty1, tci_right = ty2}):is)
= do { (is',changed) <- substInst inst is
- ; (coi1,ty1') <- tcGenericNormalizeFamInst fun ty1
- ; (coi2,ty2') <- tcGenericNormalizeFamInst fun ty2
+ ; (coi1,ty1') <- normalise ty1
+ ; (coi2,ty2') <- normalise ty2
; case (coi1,coi2) of
(IdCo,IdCo) ->
return (i:is',changed)
; return (new_inst:is',True)
}
}
- where fun ty = return $ if tcEqType pattern ty then Just (target,coercion) else Nothing
+ where
+ normalise = tcEqInstNormalizeFamInst inst
+substInst _ _ = panic "TcTyFuns.substInst: not EqInst"
- coercion = eitherEqInst inst TyVarTy id
-- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-unifyInsts
- :: [Inst] -- wanted equations
- -> TcM ([Inst],Bool)
+unifyInsts :: RewriteRule
unifyInsts insts
= do { (insts',changeds) <- mapAndUnzipM unifyInst insts
; return (concat insts',or changeds)
-- g := t
--
-- TOMDO: you should only do this for certain `meta' type variables
+unifyInst :: Inst -> TcM ([Inst], Bool)
unifyInst i@(EqInst {tci_left = ty1, tci_right = ty2})
| TyVarTy tv1 <- ty1, isMetaTyVar tv1 = go ty2 tv1
| TyVarTy tv2 <- ty2, isMetaTyVar tv2 = go ty1 tv2
; writeMetaTyVar cotv ty -- g := t
; return ([],True)
}
+unifyInst _ = panic "TcTyFuns.unifyInst: not EqInst"
-- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-occursCheckInsts :: [Inst] -> TcM ()
+occursCheckInsts :: CheckRule
occursCheckInsts insts = mappM_ occursCheckInst insts
-- fail
--
occursCheckInst :: Inst -> TcM ()
-occursCheckInst i@(EqInst {tci_left = ty1, tci_right = ty2})
+occursCheckInst (EqInst {tci_left = ty1, tci_right = ty2})
= go ty2
where
check ty = if ty `tcEqType` ty1
; failWithTcM (env2, hang msg 2 extra)
}
where msg = ptext SLIT("Occurs check: cannot construct the infinite type")
+occursCheckInst _ = panic "TcTyFuns.occursCheckInst: not eqInst"
\end{code}
Normalises a set of dictionaries relative to a set of given equalities (which
}
where
normaliseOneInst isWanted fun
- dict@(Dict {tci_name = name,
- tci_pred = pred,
+ dict@(Dict {tci_pred = pred,
tci_loc = loc})
= do { traceTc (text "genericNormaliseInst 1")
; (coi, pred') <- fun pred
}
-- TOMDO: treat other insts appropriately
- normaliseOneInst isWanted fun inst
+ normaliseOneInst _isWanted _fun inst
= do { inst' <- zonkInst inst
; return (inst', emptyBag)
}
+addBind :: Bag (LHsBind TcId) -> Inst -> LHsExpr TcId -> Bag (LHsBind TcId)
addBind binds inst rhs = binds `unionBags` mkBind inst rhs
+mkBind :: Inst -> LHsExpr TcId -> Bag (LHsBind TcId)
mkBind inst rhs = unitBag (L (instSpan inst)
(VarBind (instToId inst) rhs))
\end{code}
projects / ghc-hetmet.git / blobdiff