Commit f7e246b5 authored by Simon Peyton Jones's avatar Simon Peyton Jones
Browse files

Merge branch 'ghc-new-flavor'

parents 4b089dba ff106127
......@@ -187,15 +187,7 @@ mkCast (Coercion e_co) co
-- The guard here checks that g has a (~#) on both sides,
-- otherwise decomposeCo fails. Can in principle happen
-- with unsafeCoerce
= Coercion new_co
where
-- g :: (s1 ~# s2) ~# (t1 ~# t2)
-- g1 :: s1 ~# t1
-- g2 :: s2 ~# t2
new_co = mkSymCo g1 `mkTransCo` e_co `mkTransCo` g2
[_reflk, g1, g2] = decomposeCo 3 co
-- Remember, (~#) :: forall k. k -> k -> *
-- so it takes *three* arguments, not two
= Coercion (mkCoCast e_co co)
mkCast (Cast expr co2) co
= ASSERT(let { Pair from_ty _to_ty = coercionKind co;
......
......@@ -18,7 +18,7 @@ lower levels it is preserved with @let@/@letrec@s).
-- for details
module DsBinds ( dsTopLHsBinds, dsLHsBinds, decomposeRuleLhs, dsSpec,
dsHsWrapper, dsTcEvBinds, dsEvBinds, dsTcCoercion
dsHsWrapper, dsTcEvBinds, dsEvBinds
) where
#include "HsVersions.h"
......@@ -32,7 +32,6 @@ import DsUtils
import HsSyn -- lots of things
import CoreSyn -- lots of things
import HscTypes ( MonadThings )
import Literal ( Literal(MachStr) )
import CoreSubst
import MkCore
......@@ -40,6 +39,8 @@ import CoreUtils
import CoreArity ( etaExpand )
import CoreUnfold
import CoreFVs
import UniqSupply
import Unique( Unique )
import Digraph
......@@ -52,7 +53,7 @@ import TysWiredIn ( eqBoxDataCon, tupleCon )
import Id
import Class
import DataCon ( dataConWorkId )
import Name ( Name, localiseName )
import Name
import MkId ( seqId )
import Var
import VarSet
......@@ -662,7 +663,7 @@ but it seems better to reject the program because it's almost certainly
a mistake. That's what the isDeadBinder call detects.
Note [Constant rule dicts]
~~~~~~~~~~~~~~~~~~~~~~~
~~~~~~~~~~~~~~~~~~~~~~~~~~
When the LHS of a specialisation rule, (/\as\ds. f es) has a free dict,
which is presumably in scope at the function definition site, we can quantify
over it too. *Any* dict with that type will do.
......@@ -695,23 +696,23 @@ as the old one, but with an Internal name and no IdInfo.
\begin{code}
dsHsWrapper :: MonadThings m => HsWrapper -> CoreExpr -> m CoreExpr
dsHsWrapper :: HsWrapper -> CoreExpr -> DsM CoreExpr
dsHsWrapper WpHole e = return e
dsHsWrapper (WpTyApp ty) e = return $ App e (Type ty)
dsHsWrapper (WpLet ev_binds) e = do bs <- dsTcEvBinds ev_binds
return (mkCoreLets bs e)
dsHsWrapper (WpCompose c1 c2) e = dsHsWrapper c1 =<< dsHsWrapper c2 e
dsHsWrapper (WpCast co) e = return $ dsTcCoercion co (mkCast e)
dsHsWrapper (WpCast co) e = dsTcCoercion co (mkCast e)
dsHsWrapper (WpEvLam ev) e = return $ Lam ev e
dsHsWrapper (WpTyLam tv) e = return $ Lam tv e
dsHsWrapper (WpEvApp evtrm) e = liftM (App e) (dsEvTerm evtrm)
--------------------------------------
dsTcEvBinds :: MonadThings m => TcEvBinds -> m [CoreBind]
dsTcEvBinds :: TcEvBinds -> DsM [CoreBind]
dsTcEvBinds (TcEvBinds {}) = panic "dsEvBinds" -- Zonker has got rid of this
dsTcEvBinds (EvBinds bs) = dsEvBinds bs
dsEvBinds :: MonadThings m => Bag EvBind -> m [CoreBind]
dsEvBinds :: Bag EvBind -> DsM [CoreBind]
dsEvBinds bs = mapM ds_scc (sccEvBinds bs)
where
ds_scc (AcyclicSCC (EvBind v r)) = liftM (NonRec v) (dsEvTerm r)
......@@ -726,39 +727,51 @@ sccEvBinds bs = stronglyConnCompFromEdgedVertices edges
edges = foldrBag ((:) . mk_node) [] bs
mk_node :: EvBind -> (EvBind, EvVar, [EvVar])
mk_node b@(EvBind var term) = (b, var, evVarsOfTerm term)
mk_node b@(EvBind var term) = (b, var, varSetElems (evVarsOfTerm term))
---------------------------------------
dsEvTerm :: MonadThings m => EvTerm -> m CoreExpr
dsEvTerm :: EvTerm -> DsM CoreExpr
dsEvTerm (EvId v) = return (Var v)
dsEvTerm (EvCast v co)
= return $ dsTcCoercion co $ mkCast (Var v) -- 'v' is always a lifted evidence variable so it is
-- unnecessary to call varToCoreExpr v here.
dsEvTerm (EvCast tm co)
= do { tm' <- dsEvTerm tm
; dsTcCoercion co $ mkCast tm' }
-- 'v' is always a lifted evidence variable so it is
-- unnecessary to call varToCoreExpr v here.
dsEvTerm (EvKindCast v co)
= return $ dsTcCoercion co $ (\_ -> Var v)
= do { v' <- dsEvTerm v
; dsTcCoercion co $ (\_ -> v') }
dsEvTerm (EvDFunApp df tys vars) = return (Var df `mkTyApps` tys `mkVarApps` vars)
dsEvTerm (EvCoercion co) = return $ dsTcCoercion co mkEqBox
dsEvTerm (EvDFunApp df tys tms) = do { tms' <- mapM dsEvTerm tms
; return (Var df `mkTyApps` tys `mkApps` tms') }
dsEvTerm (EvCoercion co) = dsTcCoercion co mkEqBox
dsEvTerm (EvTupleSel v n)
= ASSERT( isTupleTyCon tc )
return $
Case (Var v) (mkWildValBinder (varType v)) (tys !! n) [(DataAlt dc, xs, Var v')]
where
(tc, tys) = splitTyConApp (evVarPred v)
Just [dc] = tyConDataCons_maybe tc
v' = v `setVarType` ty_want
xs = map mkWildValBinder tys_before ++ v' : map mkWildValBinder tys_after
(tys_before, ty_want:tys_after) = splitAt n tys
dsEvTerm (EvTupleMk vs) = return $ Var (dataConWorkId dc) `mkTyApps` tys `mkVarApps` vs
where dc = tupleCon ConstraintTuple (length vs)
tys = map varType vs
= do { tm' <- dsEvTerm v
; let scrut_ty = exprType tm'
(tc, tys) = splitTyConApp scrut_ty
Just [dc] = tyConDataCons_maybe tc
xs = mkTemplateLocals tys
the_x = xs !! n
; ASSERT( isTupleTyCon tc )
return $
Case tm' (mkWildValBinder scrut_ty) (idType the_x) [(DataAlt dc, xs, Var the_x)] }
dsEvTerm (EvTupleMk tms)
= do { tms' <- mapM dsEvTerm tms
; let tys = map exprType tms'
; return $ Var (dataConWorkId dc) `mkTyApps` tys `mkApps` tms' }
where
dc = tupleCon ConstraintTuple (length tms)
dsEvTerm (EvSuperClass d n)
= return $ Var sc_sel_id `mkTyApps` tys `App` Var d
= do { d' <- dsEvTerm d
; let (cls, tys) = getClassPredTys (exprType d')
sc_sel_id = classSCSelId cls n -- Zero-indexed
; return $ Var sc_sel_id `mkTyApps` tys `App` d' }
where
sc_sel_id = classSCSelId cls n -- Zero-indexed
(cls, tys) = getClassPredTys (evVarPred d)
dsEvTerm (EvDelayedError ty msg) = return $ Var errorId `mkTyApps` [ty] `mkApps` [litMsg]
where
errorId = rUNTIME_ERROR_ID
......@@ -770,7 +783,7 @@ dsEvTerm (EvLit l) =
EvStr s -> mkStringExprFS s
---------------------------------------
dsTcCoercion :: TcCoercion -> (Coercion -> CoreExpr) -> CoreExpr
dsTcCoercion :: TcCoercion -> (Coercion -> CoreExpr) -> DsM CoreExpr
-- This is the crucial function that moves
-- from TcCoercions to Coercions; see Note [TcCoercions] in Coercion
-- e.g. dsTcCoercion (trans g1 g2) k
......@@ -778,22 +791,28 @@ dsTcCoercion :: TcCoercion -> (Coercion -> CoreExpr) -> CoreExpr
-- case g2 of EqBox g2# ->
-- k (trans g1# g2#)
dsTcCoercion co thing_inside
= foldr wrap_in_case result_expr eqvs_covs
where
result_expr = thing_inside (ds_tc_coercion subst co)
result_ty = exprType result_expr
= do { us <- newUniqueSupply
; let eqvs_covs :: [(EqVar,CoVar)]
eqvs_covs = zipWith mk_co_var (varSetElems (coVarsOfTcCo co))
(uniqsFromSupply us)
-- We use the same uniques for the EqVars and the CoVars, and just change
-- the type. So the CoVars shadow the EqVars
subst = mkCvSubst emptyInScopeSet [(eqv, mkCoVarCo cov) | (eqv, cov) <- eqvs_covs]
result_expr = thing_inside (ds_tc_coercion subst co)
result_ty = exprType result_expr
eqvs_covs :: [(EqVar,CoVar)]
eqvs_covs = [(eqv, eqv `setIdType` mkCoercionType ty1 ty2)
| eqv <- varSetElems (coVarsOfTcCo co)
, let (ty1, ty2) = getEqPredTys (evVarPred eqv)]
subst = mkCvSubst emptyInScopeSet [(eqv, mkCoVarCo cov) | (eqv, cov) <- eqvs_covs]
wrap_in_case (eqv, cov) body
; return (foldr (wrap_in_case result_ty) result_expr eqvs_covs) }
where
mk_co_var :: Id -> Unique -> (Id, Id)
mk_co_var eqv uniq = (eqv, mkUserLocal occ uniq ty loc)
where
eq_nm = idName eqv
occ = nameOccName eq_nm
loc = nameSrcSpan eq_nm
ty = mkCoercionType ty1 ty2
(ty1, ty2) = getEqPredTys (evVarPred eqv)
wrap_in_case result_ty (eqv, cov) body
= Case (Var eqv) eqv result_ty [(DataAlt eqBoxDataCon, [cov], body)]
ds_tc_coercion :: CvSubst -> TcCoercion -> Coercion
......@@ -816,6 +835,7 @@ ds_tc_coercion subst tc_co
go (TcNthCo n co) = mkNthCo n (go co)
go (TcInstCo co ty) = mkInstCo (go co) ty
go (TcLetCo bs co) = ds_tc_coercion (ds_co_binds bs) co
go (TcCastCo co1 co2) = mkCoCast (go co1) (go co2)
go (TcCoVarCo v) = ds_ev_id subst v
ds_co_binds :: TcEvBinds -> CvSubst
......
......@@ -83,10 +83,11 @@ emitWanteds :: CtOrigin -> TcThetaType -> TcM [EvVar]
emitWanteds origin theta = mapM (emitWanted origin) theta
emitWanted :: CtOrigin -> TcPredType -> TcM EvVar
emitWanted origin pred = do { loc <- getCtLoc origin
; ev <- newWantedEvVar pred
; emitFlat (mkNonCanonical (Wanted loc ev))
; return ev }
emitWanted origin pred
= do { loc <- getCtLoc origin
; ev <- newWantedEvVar pred
; emitFlat (mkNonCanonical (Wanted { ctev_wloc = loc, ctev_pred = pred, ctev_evar = ev }))
; return ev }
newMethodFromName :: CtOrigin -> Name -> TcRhoType -> TcM (HsExpr TcId)
-- Used when Name is the wired-in name for a wired-in class method,
......@@ -530,7 +531,7 @@ tyVarsOfCt (CFunEqCan { cc_tyargs = tys, cc_rhs = xi }) = tyVarsOfTypes (xi:tys)
tyVarsOfCt (CDictCan { cc_tyargs = tys }) = tyVarsOfTypes tys
tyVarsOfCt (CIPCan { cc_ip_ty = ty }) = tyVarsOfType ty
tyVarsOfCt (CIrredEvCan { cc_ty = ty }) = tyVarsOfType ty
tyVarsOfCt (CNonCanonical { cc_flavor = fl }) = tyVarsOfType (ctFlavPred fl)
tyVarsOfCt (CNonCanonical { cc_ev = fl }) = tyVarsOfType (ctEvPred fl)
tyVarsOfCDict :: Ct -> TcTyVarSet
tyVarsOfCDict (CDictCan { cc_tyargs = tys }) = tyVarsOfTypes tys
......@@ -564,24 +565,22 @@ tyVarsOfBag tvs_of = foldrBag (unionVarSet . tvs_of) emptyVarSet
---------------- Tidying -------------------------
tidyCt :: TidyEnv -> Ct -> Ct
-- Used only in error reporting
-- Also converts it to non-canonical
tidyCt env ct
= CNonCanonical { cc_flavor = tidy_flavor env (cc_flavor ct)
= CNonCanonical { cc_ev = tidy_flavor env (cc_ev ct)
, cc_depth = cc_depth ct }
where tidy_flavor :: TidyEnv -> CtFlavor -> CtFlavor
tidy_flavor env (Given { flav_gloc = gloc, flav_evar = evar })
= Given { flav_gloc = tidyGivenLoc env gloc
, flav_evar = tidyEvVar env evar }
tidy_flavor env (Solved { flav_gloc = gloc
, flav_evar = evar })
= Solved { flav_gloc = tidyGivenLoc env gloc
, flav_evar = tidyEvVar env evar }
tidy_flavor env (Wanted { flav_wloc = wloc
, flav_evar = evar })
= Wanted { flav_wloc = wloc -- Interesting: no tidying needed?
, flav_evar = tidyEvVar env evar }
tidy_flavor env (Derived { flav_wloc = wloc, flav_der_pty = pty })
= Derived { flav_wloc = wloc, flav_der_pty = tidyType env pty }
where
tidy_flavor :: TidyEnv -> CtEvidence -> CtEvidence
-- NB: we do not tidy the ctev_evtm/var field because we don't
-- show it in error messages
tidy_flavor env ctev@(Given { ctev_gloc = gloc, ctev_pred = pred })
= ctev { ctev_gloc = tidyGivenLoc env gloc
, ctev_pred = tidyType env pred }
tidy_flavor env ctev@(Wanted { ctev_pred = pred })
= ctev { ctev_pred = tidyType env pred }
tidy_flavor env ctev@(Derived { ctev_pred = pred })
= ctev { ctev_pred = tidyType env pred }
tidyEvVar :: TidyEnv -> EvVar -> EvVar
tidyEvVar env var = setVarType var (tidyType env (varType var))
......@@ -604,6 +603,10 @@ tidySkolemInfo env (UnifyForAllSkol skol_tvs ty)
tidySkolemInfo _ info = info
---------------- Substitution -------------------------
-- This is used only in TcSimpify, for substituations that are *also*
-- reflected in the unification variables. So we don't substitute
-- in the evidence.
substCt :: TvSubst -> Ct -> Ct
-- Conservatively converts it to non-canonical:
-- Postcondition: if the constraint does not get rewritten
......@@ -611,9 +614,9 @@ substCt subst ct
| pty <- ctPred ct
, sty <- substTy subst pty
= if sty `eqType` pty then
ct { cc_flavor = substFlavor subst (cc_flavor ct) }
ct { cc_ev = substFlavor subst (cc_ev ct) }
else
CNonCanonical { cc_flavor = substFlavor subst (cc_flavor ct)
CNonCanonical { cc_ev = substFlavor subst (cc_ev ct)
, cc_depth = cc_depth ct }
substWC :: TvSubst -> WantedConstraints -> WantedConstraints
......@@ -637,21 +640,16 @@ substImplication subst implic@(Implic { ic_skols = tvs
substEvVar :: TvSubst -> EvVar -> EvVar
substEvVar subst var = setVarType var (substTy subst (varType var))
substFlavor :: TvSubst -> CtFlavor -> CtFlavor
substFlavor subst (Given { flav_gloc = gloc, flav_evar = evar })
= Given { flav_gloc = substGivenLoc subst gloc
, flav_evar = substEvVar subst evar }
substFlavor subst (Solved { flav_gloc = gloc, flav_evar = evar })
= Solved { flav_gloc = substGivenLoc subst gloc
, flav_evar = substEvVar subst evar }
substFlavor subst (Wanted { flav_wloc = wloc, flav_evar = evar })
= Wanted { flav_wloc = wloc
, flav_evar = substEvVar subst evar }
substFlavor subst (Derived { flav_wloc = wloc, flav_der_pty = pty })
= Derived { flav_wloc = wloc
, flav_der_pty = substTy subst pty }
substFlavor :: TvSubst -> CtEvidence -> CtEvidence
substFlavor subst ctev@(Given { ctev_gloc = gloc, ctev_pred = pred })
= ctev { ctev_gloc = substGivenLoc subst gloc
, ctev_pred = substTy subst pred }
substFlavor subst ctev@(Wanted { ctev_pred = pred })
= ctev { ctev_pred = substTy subst pred }
substFlavor subst ctev@(Derived { ctev_pred = pty })
= ctev { ctev_pred = substTy subst pty }
substGivenLoc :: TvSubst -> GivenLoc -> GivenLoc
substGivenLoc subst (CtLoc skol span ctxt)
......
This diff is collapsed.
......@@ -158,17 +158,15 @@ reportTidyWanteds ctxt insols flats implics
deferToRuntime :: EvBindsVar -> ReportErrCtxt -> (ReportErrCtxt -> Ct -> TcM ErrMsg)
-> Ct -> TcM ()
deferToRuntime ev_binds_var ctxt mk_err_msg ct
| fl <- cc_flavor ct
, Wanted loc _ <- fl
| Wanted { ctev_wloc = loc, ctev_pred = pred, ctev_evar = ev_id } <- cc_ev ct
= do { err <- setCtLoc loc $
mk_err_msg ctxt ct
; let ev_id = ctId ct -- Prec satisfied: Wanted
err_msg = pprLocErrMsg err
; let err_msg = pprLocErrMsg err
err_fs = mkFastString $ showSDoc $
err_msg $$ text "(deferred type error)"
-- Create the binding
; addTcEvBind ev_binds_var ev_id (EvDelayedError (idType ev_id) err_fs)
; addTcEvBind ev_binds_var ev_id (EvDelayedError pred err_fs)
-- And emit a warning
; reportWarning (makeIntoWarning err) }
......@@ -231,7 +229,7 @@ type Reporter = [Ct] -> TcM ()
mkReporter :: (Ct -> TcM ErrMsg) -> [Ct] -> TcM ()
-- Reports errors one at a time
mkReporter mk_err = mapM_ (\ct -> do { err <- setCtFlavorLoc (cc_flavor ct) $
mkReporter mk_err = mapM_ (\ct -> do { err <- setCtFlavorLoc (cc_ev ct) $
mk_err ct;
; reportError err })
......@@ -316,15 +314,15 @@ groupErrs mk_err (ct1 : rest)
; reportError err
; groupErrs mk_err others }
where
flavor = cc_flavor ct1
flavor = cc_ev ct1
cts = ct1 : friends
(friends, others) = partition is_friend rest
is_friend friend = cc_flavor friend `same_group` flavor
is_friend friend = cc_ev friend `same_group` flavor
same_group :: CtFlavor -> CtFlavor -> Bool
same_group (Given l1 _) (Given l2 _) = same_loc l1 l2
same_group (Derived l1 _) (Derived l2 _) = same_loc l1 l2
same_group (Wanted l1 _) (Wanted l2 _) = same_loc l1 l2
same_group :: CtEvidence -> CtEvidence -> Bool
same_group (Given {ctev_gloc = l1}) (Given {ctev_gloc = l2}) = same_loc l1 l2
same_group (Wanted {ctev_wloc = l1}) (Wanted {ctev_wloc = l2}) = same_loc l1 l2
same_group (Derived {ctev_wloc = l1}) (Derived {ctev_wloc = l2}) = same_loc l1 l2
same_group _ _ = False
same_loc :: CtLoc o -> CtLoc o -> Bool
......@@ -425,7 +423,7 @@ mkEqErr _ [] = panic "mkEqErr"
mkEqErr1 :: ReportErrCtxt -> Ct -> TcM ErrMsg
-- Wanted constraints only!
mkEqErr1 ctxt ct
= if isGivenOrSolved flav then
= if isGiven flav then
let ctx2 = ctxt { cec_extra = cec_extra ctxt $$ inaccessible_msg flav }
in mkEqErr_help ctx2 ct False ty1 ty2
else
......@@ -434,10 +432,11 @@ mkEqErr1 ctxt ct
; mk_err ctxt1 orig' }
where
flav = cc_flavor ct
flav = cc_ev ct
inaccessible_msg (Given loc _) = hang (ptext (sLit "Inaccessible code in"))
2 (ppr (ctLocOrigin loc))
inaccessible_msg (Given { ctev_gloc = loc })
= hang (ptext (sLit "Inaccessible code in"))
2 (ppr (ctLocOrigin loc))
-- If a Solved then we should not report inaccessible code
inaccessible_msg _ = empty
......@@ -571,7 +570,7 @@ misMatchOrCND :: ReportErrCtxt -> Ct -> Bool -> TcType -> TcType -> SDoc
misMatchOrCND ctxt ct oriented ty1 ty2
| null givens ||
(isRigid ty1 && isRigid ty2) ||
isGivenOrSolved (cc_flavor ct)
isGiven (cc_ev ct)
-- If the equality is unconditionally insoluble
-- or there is no context, don't report the context
= misMatchMsg oriented ty1 ty2
......@@ -1066,7 +1065,7 @@ solverDepthErrorTcS depth stack
| null stack -- Shouldn't happen unless you say -fcontext-stack=0
= failWith msg
| otherwise
= setCtFlavorLoc (cc_flavor top_item) $
= setCtFlavorLoc (cc_ev top_item) $
do { zstack <- mapM zonkCt stack
; env0 <- tcInitTidyEnv
; let zstack_tvs = foldr (unionVarSet . tyVarsOfCt) emptyVarSet zstack
......@@ -1079,7 +1078,7 @@ solverDepthErrorTcS depth stack
, ptext (sLit "Use -fcontext-stack=N to increase stack size to N") ]
{- DV: Changing this because Derived's no longer have ids ... Kind of a corner case ...
= setCtFlavorLoc (cc_flavor top_item) $
= setCtFlavorLoc (cc_ev top_item) $
do { ev_vars <- mapM (zonkEvVar . cc_id) stack
; env0 <- tcInitTidyEnv
; let tidy_env = tidyFreeTyVars env0 (tyVarsOfEvVars ev_vars)
......@@ -1092,7 +1091,7 @@ solverDepthErrorTcS depth stack
-}
flattenForAllErrorTcS :: CtFlavor -> TcType -> TcM a
flattenForAllErrorTcS :: CtEvidence -> TcType -> TcM a
flattenForAllErrorTcS fl ty
= setCtFlavorLoc fl $
do { env0 <- tcInitTidyEnv
......@@ -1109,11 +1108,10 @@ flattenForAllErrorTcS fl ty
%************************************************************************
\begin{code}
setCtFlavorLoc :: CtFlavor -> TcM a -> TcM a
setCtFlavorLoc (Wanted loc _) thing = setCtLoc loc thing
setCtFlavorLoc (Derived loc _) thing = setCtLoc loc thing
setCtFlavorLoc (Given loc _) thing = setCtLoc loc thing
setCtFlavorLoc (Solved loc _) thing = setCtLoc loc thing
setCtFlavorLoc :: CtEvidence -> TcM a -> TcM a
setCtFlavorLoc (Wanted { ctev_wloc = loc }) thing = setCtLoc loc thing
setCtFlavorLoc (Derived { ctev_wloc = loc }) thing = setCtLoc loc thing
setCtFlavorLoc (Given { ctev_gloc = loc }) thing = setCtLoc loc thing
\end{code}
%************************************************************************
......
......@@ -17,7 +17,7 @@ module TcEvidence (
EvBind(..), emptyTcEvBinds, isEmptyTcEvBinds,
EvTerm(..), mkEvCast, evVarsOfTerm, mkEvKindCast,
EvLit(..),
EvLit(..), evTermCoercion,
-- TcCoercion
TcCoercion(..),
......@@ -36,7 +36,7 @@ import Var
import PprCore () -- Instance OutputableBndr TyVar
import TypeRep -- Knows type representation
import TcType
import Type( tyConAppArgN, getEqPredTys_maybe, tyConAppTyCon_maybe )
import Type( tyConAppArgN, getEqPredTys_maybe, tyConAppTyCon_maybe, getEqPredTys )
import TysPrim( funTyCon )
import TyCon
import PrelNames
......@@ -102,6 +102,7 @@ data TcCoercion
| TcSymCo TcCoercion
| TcTransCo TcCoercion TcCoercion
| TcNthCo Int TcCoercion
| TcCastCo TcCoercion TcCoercion -- co1 |> co2
| TcLetCo TcEvBinds TcCoercion
deriving (Data.Data, Data.Typeable)
......@@ -199,6 +200,8 @@ tcCoercionKind co = go co
where
go (TcRefl ty) = Pair ty ty
go (TcLetCo _ co) = go co
go (TcCastCo _ co) = case getEqPredTys (pSnd (go co)) of
(ty1,ty2) -> Pair ty1 ty2
go (TcTyConAppCo tc cos) = mkTyConApp tc <$> (sequenceA $ map go cos)
go (TcAppCo co1 co2) = mkAppTy <$> go co1 <*> go co2
go (TcForAllCo tv co) = mkForAllTy tv <$> go co
......@@ -206,8 +209,8 @@ tcCoercionKind co = go co
go (TcCoVarCo cv) = eqVarKind cv
go (TcAxiomInstCo ax tys) = Pair (substTyWith (co_ax_tvs ax) tys (co_ax_lhs ax))
(substTyWith (co_ax_tvs ax) tys (co_ax_rhs ax))
go (TcSymCo co) = swap $ go co
go (TcTransCo co1 co2) = Pair (pFst $ go co1) (pSnd $ go co2)
go (TcSymCo co) = swap (go co)
go (TcTransCo co1 co2) = Pair (pFst (go co1)) (pSnd (go co2))
go (TcNthCo d co) = tyConAppArgN d <$> go co
-- c.f. Coercion.coercionKind
......@@ -219,7 +222,7 @@ eqVarKind cv
| Just (tc, [_kind,ty1,ty2]) <- tcSplitTyConApp_maybe (varType cv)
= ASSERT (tc `hasKey` eqTyConKey)
Pair ty1 ty2
| otherwise = panic "eqVarKind, non coercion variable"
| otherwise = pprPanic "eqVarKind, non coercion variable" (ppr cv <+> dcolon <+> ppr (varType cv))
coVarsOfTcCo :: TcCoercion -> VarSet
-- Only works on *zonked* coercions, because of TcLetCo
......@@ -229,6 +232,7 @@ coVarsOfTcCo tc_co
go (TcRefl _) = emptyVarSet
go (TcTyConAppCo _ cos) = foldr (unionVarSet . go) emptyVarSet cos
go (TcAppCo co1 co2) = go co1 `unionVarSet` go co2
go (TcCastCo co1 co2) = go co1 `unionVarSet` go co2
go (TcForAllCo _ co) = go co
go (TcInstCo co _) = go co
go (TcCoVarCo v) = unitVarSet v
......@@ -263,7 +267,7 @@ liftTcCoSubstWith tvs cos ty
Nothing -> mkTcReflCo ty
go (AppTy t1 t2) = mkTcAppCo (go t1) (go t2)
go (TyConApp tc tys) = mkTcTyConAppCo tc (map go tys)
go ty@(LitTy {}) = mkTcReflCo ty
go ty@(LitTy {}) = mkTcReflCo ty
go (ForAllTy tv ty) = mkTcForAllCo tv (go ty)
go (FunTy t1 t2) = mkTcFunCo (go t1) (go t2)
\end{code}
......@@ -289,6 +293,8 @@ ppr_co p (TcLetCo bs co) = maybeParen p TopPrec $
sep [ptext (sLit "let") <+> braces (ppr bs), ppr co]
ppr_co p (TcAppCo co1 co2) = maybeParen p TyConPrec $
pprTcCo co1 <+> ppr_co TyConPrec co2
ppr_co p (TcCastCo co1 co2) = maybeParen p FunPrec $
ppr_co FunPrec co1 <+> ptext (sLit "|>") <+> ppr_co FunPrec co2
ppr_co p co@(TcForAllCo {}) = ppr_forall_co p co
ppr_co p (TcInstCo co ty) = maybeParen p TyConPrec $
pprParendTcCo co <> ptext (sLit "@") <> pprType ty
......@@ -454,24 +460,24 @@ data EvTerm
| EvCoercion TcCoercion -- (Boxed) coercion bindings
| EvCast EvVar TcCoercion -- d |> co
| EvCast EvTerm TcCoercion -- d |> co
| EvDFunApp DFunId -- Dictionary instance application
[Type] [EvVar]
[Type] [EvTerm]
| EvTupleSel EvId Int -- n'th component of the tuple
| EvTupleSel EvTerm Int -- n'th component of the tuple, 0-indexed
| EvTupleMk [EvId] -- tuple built from this stuff
| EvTupleMk [EvTerm] -- tuple built from this stuff
| EvDelayedError Type FastString -- Used with Opt_DeferTypeErrors
-- See Note [Deferring coercion errors to runtime]
-- in TcSimplify
| EvSuperClass DictId Int -- n'th superclass. Used for both equalities and
| EvSuperClass EvTerm Int -- n'th superclass. Used for both equalities and
-- dictionaries, even though the former have no
-- selector Id. We count up from _0_
| EvKindCast EvVar TcCoercion -- See Note [EvKindCast]
| EvKindCast EvTerm TcCoercion -- See Note [EvKindCast]
| EvLit EvLit -- Dictionary for class "SingI" for type lits.
-- Note [EvLit]
......@@ -555,14 +561,14 @@ and another to make it into "SingI" evidence.
\begin{code}
mkEvCast :: EvVar -> TcCoercion -> EvTerm
mkEvCast :: EvTerm -> TcCoercion -> EvTerm
mkEvCast ev lco
| isTcReflCo lco = EvId ev
| isTcReflCo lco = ev
| otherwise = EvCast ev lco
mkEvKindCast :: EvVar -> TcCoercion -> EvTerm
mkEvKindCast :: EvTerm -> TcCoercion -> EvTerm
mkEvKindCast ev lco
| isTcReflCo lco = EvId ev
| isTcReflCo lco = ev
| otherwise = EvKindCast ev lco
emptyTcEvBinds :: TcEvBinds
......@@ -573,17 +579,27 @@ isEmptyTcEvBinds (EvBinds b) = isEmptyBag b
isEmptyTcEvBinds (TcEvBinds {}) = panic "isEmptyTcEvBinds"
evVarsOfTerm :: EvTerm -> [EvVar]
evVarsOfTerm (EvId v) = [v]
evVarsOfTerm (EvCoercion co) = varSetElems (coVarsOfTcCo co)
evVarsOfTerm (EvDFunApp _ _ evs) = evs
evVarsOfTerm (EvTupleSel v _) = [v]
evVarsOfTerm (EvSuperClass v _) = [v]
evVarsOfTerm (EvCast v co) = v : varSetElems (coVarsOfTcCo co)
evVarsOfTerm (EvTupleMk evs) = evs
evVarsOfTerm (EvDelayedError _ _) = []
evVarsOfTerm (EvKindCast v co) = v : varSetElems (coVarsOfTcCo co)
evVarsOfTerm (EvLit _) = []
evTermCoercion :: EvTerm -> TcCoercion
-- Applied only to EvTerms of type (s~t)
evTermCoercion (EvId v) = mkTcCoVarCo v
evTermCoercion (EvCoercion co) = co
evTermCoercion (EvCast tm co) = TcCastCo (evTermCoercion tm) co
evTermCoercion tm = pprPanic "evTermCoercion" (ppr tm)
evVarsOfTerm :: EvTerm -> VarSet
evVarsOfTerm (EvId v) = unitVarSet v
evVarsOfTerm (EvCoercion co) = coVarsOfTcCo co
evVarsOfTerm (EvDFunApp _ _ evs) = evVarsOfTerms evs
evVarsOfTerm (EvTupleSel v _) = evVarsOfTerm v
evVarsOfTerm (EvSuperClass v _) = evVarsOfTerm v
evVarsOfTerm (EvCast tm co) = evVarsOfTerm tm `unionVarSet` coVarsOfTcCo co
evVarsOfTerm (EvTupleMk evs) = evVarsOfTerms evs
evVarsOfTerm (EvDelayedError _ _) = emptyVarSet
evVarsOfTerm (EvKindCast v co) = coVarsOfTcCo co `unionVarSet` evVarsOfTerm v
evVarsOfTerm (EvLit _) = emptyVarSet
evVarsOfTerms :: [EvTerm] -> VarSet
evVarsOfTerms = foldr (unionVarSet . evVarsOfTerm) emptyVarSet
\end{code}
......
......@@ -1095,21 +1095,24 @@ zonkEvTerm env (EvId v) = ASSERT2( isId v, ppr v )
return (EvId (zonkIdOcc env v))
zonkEvTerm env (EvCoercion co) = do { co' <- zonkTcLCoToLCo env co
; return (EvCoercion co') }
zonkEvTerm env (EvCast v co) = ASSERT( isId v)
do { co' <- zonkTcLCoToLCo env co
; return (mkEvCast (zonkIdOcc env v) co') }
zonkEvTerm env (EvKindCast v co) = ASSERT( isId v)
do { co' <- zonkTcLCoToLCo env co
; return (mkEvKindCast (zonkIdOcc env v) co') }
zonkEvTerm env (EvTupleSel v n) = return (EvTupleSel (zonkIdOcc env v) n)
zonkEvTerm env (EvTupleMk vs) = return (EvTupleMk (map (zonkIdOcc env) vs))
zonkEvTerm env (EvCast tm co) = do { tm' <- zonkEvTerm env tm
; co' <- zonkTcLCoToLCo env co
; return (mkEvCast tm' co') }