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

Implement 'left' and 'right' coercions

This patch finally adds 'left' and 'right' coercions back into
GHC.  Trac #7205 gives the details.

The main change is to add a new constructor to Coercion:

  data Coercion
    = ...
    | NthCo  Int         Coercion     -- OLD, still there
    | LRCo   LeftOrRight Coercion     -- NEW

  data LeftOrRight = CLeft | CRight

Plus:
  * Similar change to TcCoercion
  * Use LRCo when decomposing AppTys
  * Coercion optimisation needs to handle left/right

The rest is just knock-on effects.
parent 510f4394
......@@ -838,6 +838,19 @@ lintCoercion the_co@(NthCo n co)
_ -> failWithL (hang (ptext (sLit "Bad getNth:"))
2 (ppr the_co $$ ppr s $$ ppr t)) }
lintCoercion the_co@(LRCo lr co)
= do { (_,s,t) <- lintCoercion co
; case (splitAppTy_maybe s, splitAppTy_maybe t) of
(Just s_pr, Just t_pr)
-> return (k, s_pick, t_pick)
where
s_pick = pickLR lr s_pr
t_pick = pickLR lr t_pr
k = typeKind s_pick
_ -> failWithL (hang (ptext (sLit "Bad LRCo:"))
2 (ppr the_co $$ ppr s $$ ppr t)) }
lintCoercion (InstCo co arg_ty)
= do { (k,s,t) <- lintCoercion co
; arg_kind <- lintType arg_ty
......
......@@ -74,6 +74,9 @@ data Ty
| UnsafeCoercion Ty Ty
| InstCoercion Ty Ty
| NthCoercion Int Ty
| LRCoercion LeftOrRight Ty
data LeftOrRight = CLeft | CRight
data Kind
= Klifted
......
......@@ -326,8 +326,13 @@ make_co dflags (UnsafeCo t1 t2) = C.UnsafeCoercion (make_ty dflags t1) (mak
make_co dflags (SymCo co) = C.SymCoercion (make_co dflags co)
make_co dflags (TransCo c1 c2) = C.TransCoercion (make_co dflags c1) (make_co dflags c2)
make_co dflags (NthCo d co) = C.NthCoercion d (make_co dflags co)
make_co dflags (LRCo lr co) = C.LRCoercion (make_lr lr) (make_co dflags co)
make_co dflags (InstCo co ty) = C.InstCoercion (make_co dflags co) (make_ty dflags ty)
make_lr :: LeftOrRight -> C.LeftOrRight
make_lr CLeft = C.CLeft
make_lr CRight = C.CRight
-- Used for both tycon app coercions and axiom instantiations.
make_conAppCo :: DynFlags -> C.Qual C.Tcon -> [Coercion] -> C.Ty
make_conAppCo dflags con cos =
......
......@@ -114,6 +114,10 @@ pty (UnsafeCoercion t1 t2) =
sep [text "%unsafe", paty t1, paty t2]
pty (NthCoercion n t) =
sep [text "%nth", int n, paty t]
pty (LRCoercion CLeft t) =
sep [text "%left", paty t]
pty (LRCoercion CRight t) =
sep [text "%right", paty t]
pty (InstCoercion t1 t2) =
sep [text "%inst", paty t1, paty t2]
pty t = pbty t
......
......@@ -470,6 +470,8 @@ data CoercionMap a
, km_sym :: CoercionMap a
, km_trans :: CoercionMap (CoercionMap a)
, km_nth :: IntMap.IntMap (CoercionMap a)
, km_left :: CoercionMap a
, km_right :: CoercionMap a
, km_inst :: CoercionMap (TypeMap a) }
wrapEmptyKM :: CoercionMap a
......@@ -477,7 +479,8 @@ wrapEmptyKM = KM { km_refl = emptyTM, km_tc_app = emptyNameEnv
, km_app = emptyTM, km_forall = emptyTM
, km_var = emptyTM, km_axiom = emptyNameEnv
, km_unsafe = emptyTM, km_sym = emptyTM, km_trans = emptyTM
, km_nth = emptyTM, km_inst = emptyTM }
, km_nth = emptyTM, km_left = emptyTM, km_right = emptyTM
, km_inst = emptyTM }
instance TrieMap CoercionMap where
type Key CoercionMap = Coercion
......@@ -493,7 +496,8 @@ mapC f (KM { km_refl = krefl, km_tc_app = ktc
, km_app = kapp, km_forall = kforall
, km_var = kvar, km_axiom = kax
, km_unsafe = kunsafe, km_sym = ksym, km_trans = ktrans
, km_nth = knth, km_inst = kinst })
, km_nth = knth, km_left = kml, km_right = kmr
, km_inst = kinst })
= KM { km_refl = mapTM f krefl
, km_tc_app = mapNameEnv (mapTM f) ktc
, km_app = mapTM (mapTM f) kapp
......@@ -504,6 +508,8 @@ mapC f (KM { km_refl = krefl, km_tc_app = ktc
, km_sym = mapTM f ksym
, km_trans = mapTM (mapTM f) ktrans
, km_nth = IntMap.map (mapTM f) knth
, km_left = mapTM f kml
, km_right = mapTM f kmr
, km_inst = mapTM (mapTM f) kinst }
lkC :: CmEnv -> Coercion -> CoercionMap a -> Maybe a
......@@ -522,6 +528,8 @@ lkC env co m
go (CoVarCo v) = km_var >.> lkVar env v
go (SymCo c) = km_sym >.> lkC env c
go (NthCo n c) = km_nth >.> lookupTM n >=> lkC env c
go (LRCo CLeft c) = km_left >.> lkC env c
go (LRCo CRight c) = km_right >.> lkC env c
xtC :: CmEnv -> Coercion -> XT a -> CoercionMap a -> CoercionMap a
xtC env co f EmptyKM = xtC env co f wrapEmptyKM
......@@ -534,9 +542,11 @@ xtC env (UnsafeCo t1 t2) f m = m { km_unsafe = km_unsafe m |> xtT env t1 |>>
xtC env (InstCo c t) f m = m { km_inst = km_inst m |> xtC env c |>> xtT env t f }
xtC env (ForAllCo v c) f m = m { km_forall = km_forall m |> xtC (extendCME env v) c
|>> xtBndr env v f }
xtC env (CoVarCo v) f m = m { km_var = km_var m |> xtVar env v f }
xtC env (SymCo c) f m = m { km_sym = km_sym m |> xtC env c f }
xtC env (NthCo n c) f m = m { km_nth = km_nth m |> xtInt n |>> xtC env c f }
xtC env (CoVarCo v) f m = m { km_var = km_var m |> xtVar env v f }
xtC env (SymCo c) f m = m { km_sym = km_sym m |> xtC env c f }
xtC env (NthCo n c) f m = m { km_nth = km_nth m |> xtInt n |>> xtC env c f }
xtC env (LRCo CLeft c) f m = m { km_left = km_left m |> xtC env c f }
xtC env (LRCo CRight c) f m = m { km_right = km_right m |> xtC env c f }
fdC :: (a -> b -> b) -> CoercionMap a -> b -> b
fdC _ EmptyKM = \z -> z
......@@ -550,6 +560,8 @@ fdC k m = foldTM k (km_refl m)
. foldTM k (km_sym m)
. foldTM (foldTM k) (km_trans m)
. foldTM (foldTM k) (km_nth m)
. foldTM k (km_left m)
. foldTM k (km_right m)
. foldTM (foldTM k) (km_inst m)
\end{code}
......
......@@ -834,6 +834,7 @@ ds_tc_coercion subst tc_co
go (TcSymCo co) = mkSymCo (go co)
go (TcTransCo co1 co2) = mkTransCo (go co1) (go co2)
go (TcNthCo n co) = mkNthCo n (go co)
go (TcLRCo lr co) = mkLRCo lr (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)
......
......@@ -20,11 +20,12 @@ module BinIface (
#include "HsVersions.h"
import TcRnMonad
import TyCon (TyCon, tyConName, tupleTyConSort, tupleTyConArity, isTupleTyCon)
import TyCon
import DataCon (dataConName, dataConWorkId, dataConTyCon)
import PrelInfo (wiredInThings, basicKnownKeyNames)
import Id (idName, isDataConWorkId_maybe)
import CoreSyn (DFunArg(..))
import Coercion (LeftOrRight(..))
import TysWiredIn
import IfaceEnv
import HscTypes
......@@ -1037,6 +1038,15 @@ instance Binary IfaceTyCon where
put_ bh (IfaceTc ext) = put_ bh ext
get bh = liftM IfaceTc (get bh)
instance Binary LeftOrRight where
put_ bh CLeft = putByte bh 0
put_ bh CRight = putByte bh 1
get bh = do { h <- getByte bh
; case h of
0 -> return CLeft
_ -> return CRight }
instance Binary IfaceCoCon where
put_ bh (IfaceCoAx n) = do { putByte bh 0; put_ bh n }
put_ bh IfaceReflCo = putByte bh 1
......@@ -1045,6 +1055,7 @@ instance Binary IfaceCoCon where
put_ bh IfaceTransCo = putByte bh 4
put_ bh IfaceInstCo = putByte bh 5
put_ bh (IfaceNthCo d) = do { putByte bh 6; put_ bh d }
put_ bh (IfaceLRCo lr) = do { putByte bh 7; put_ bh lr }
get bh = do
h <- getByte bh
......@@ -1056,6 +1067,7 @@ instance Binary IfaceCoCon where
4 -> return IfaceTransCo
5 -> return IfaceInstCo
6 -> do { d <- get bh; return (IfaceNthCo d) }
7 -> do { lr <- get bh; return (IfaceLRCo lr) }
_ -> panic ("get IfaceCoCon " ++ show h)
-------------------------------------------------------------------------
......
......@@ -99,7 +99,7 @@ data IfaceCoCon
= IfaceCoAx IfExtName
| IfaceReflCo | IfaceUnsafeCo | IfaceSymCo
| IfaceTransCo | IfaceInstCo
| IfaceNthCo Int
| IfaceNthCo Int | IfaceLRCo LeftOrRight
\end{code}
%************************************************************************
......@@ -278,6 +278,7 @@ instance Outputable IfaceCoCon where
ppr IfaceTransCo = ptext (sLit "Trans")
ppr IfaceInstCo = ptext (sLit "Inst")
ppr (IfaceNthCo d) = ptext (sLit "Nth:") <> int d
ppr (IfaceLRCo lr) = ppr lr
instance Outputable IfaceTyLit where
ppr = ppr_tylit
......@@ -376,6 +377,8 @@ coToIfaceType (TransCo co1 co2) = IfaceCoConApp IfaceTransCo
, coToIfaceType co2 ]
coToIfaceType (NthCo d co) = IfaceCoConApp (IfaceNthCo d)
[ coToIfaceType co ]
coToIfaceType (LRCo lr co) = IfaceCoConApp (IfaceLRCo lr)
[ coToIfaceType co ]
coToIfaceType (InstCo co ty) = IfaceCoConApp IfaceInstCo
[ coToIfaceType co
, toIfaceType ty ]
......
......@@ -962,6 +962,7 @@ tcIfaceCoApp IfaceSymCo [t] = SymCo <$> tcIfaceCo t
tcIfaceCoApp IfaceTransCo [t1,t2] = TransCo <$> tcIfaceCo t1 <*> tcIfaceCo t2
tcIfaceCoApp IfaceInstCo [t1,t2] = InstCo <$> tcIfaceCo t1 <*> tcIfaceType t2
tcIfaceCoApp (IfaceNthCo d) [t] = NthCo d <$> tcIfaceCo t
tcIfaceCoApp (IfaceLRCo lr) [t] = LRCo lr <$> tcIfaceCo t
tcIfaceCoApp cc ts = pprPanic "toIfaceCoApp" (ppr cc <+> ppr ts)
tcIfaceCoVar :: FastString -> IfL CoVar
......
......@@ -809,19 +809,11 @@ canEqAppTy :: CtLoc -> CtEvidence
-> TcS StopOrContinue
canEqAppTy loc ev s1 t1 s2 t2
= ASSERT( not (isKind t1) && not (isKind t2) )
if isGiven ev then
do { traceTcS "canEq (app case)" $
text "Ommitting decomposition of given equality between: "
<+> ppr (AppTy s1 t1) <+> text "and" <+> ppr (AppTy s2 t2)
-- We cannot decompose given applications
-- because we no longer have 'left' and 'right'
; return Stop }
else
do { let xevcomp [x,y] = EvCoercion (mkTcAppCo (evTermCoercion x) (evTermCoercion y))
xevcomp _ = error "canEqAppTy: can't happen" -- Can't happen
xev = XEvTerm { ev_comp = xevcomp
, ev_decomp = error "canEqAppTy: can't happen" }
; ctevs <- xCtFlavor ev [mkTcEqPred s1 s2, mkTcEqPred t1 t2] xev
xevdecomp x = let xco = evTermCoercion x
in [EvCoercion (mkTcLRCo CLeft xco), EvCoercion (mkTcLRCo CRight xco)]
; ctevs <- xCtFlavor ev [mkTcEqPred s1 s2, mkTcEqPred t1 t2] (XEvTerm xevcomp xevdecomp)
; canEvVarsCreated loc ctevs }
canEqFailure :: CtLoc -> CtEvidence -> TcS StopOrContinue
......
......@@ -20,10 +20,10 @@ module TcEvidence (
EvLit(..), evTermCoercion,
-- TcCoercion
TcCoercion(..),
TcCoercion(..), LeftOrRight(..), pickLR,
mkTcReflCo, mkTcTyConAppCo, mkTcAppCo, mkTcAppCos, mkTcFunCo,
mkTcAxInstCo, mkTcForAllCo, mkTcForAllCos,
mkTcSymCo, mkTcTransCo, mkTcNthCo, mkTcInstCos,
mkTcSymCo, mkTcTransCo, mkTcNthCo, mkTcLRCo, mkTcInstCos,
tcCoercionKind, coVarsOfTcCo, isEqVar, mkTcCoVarCo,
isTcReflCo, isTcReflCo_maybe, getTcCoVar_maybe,
liftTcCoSubstWith
......@@ -32,7 +32,7 @@ module TcEvidence (
#include "HsVersions.h"
import Var
import Coercion( LeftOrRight(..), pickLR )
import PprCore () -- Instance OutputableBndr TyVar
import TypeRep -- Knows type representation
import TcType
......@@ -102,6 +102,7 @@ data TcCoercion
| TcSymCo TcCoercion
| TcTransCo TcCoercion TcCoercion
| TcNthCo Int TcCoercion
| TcLRCo LeftOrRight TcCoercion
| TcCastCo TcCoercion TcCoercion -- co1 |> co2
| TcLetCo TcEvBinds TcCoercion
deriving (Data.Data, Data.Typeable)
......@@ -167,6 +168,10 @@ mkTcNthCo :: Int -> TcCoercion -> TcCoercion
mkTcNthCo n (TcRefl ty) = TcRefl (tyConAppArgN n ty)
mkTcNthCo n co = TcNthCo n co
mkTcLRCo :: LeftOrRight -> TcCoercion -> TcCoercion
mkTcLRCo lr (TcRefl ty) = TcRefl (pickLR lr (tcSplitAppTy ty))
mkTcLRCo lr co = TcLRCo lr co
mkTcAppCos :: TcCoercion -> [TcCoercion] -> TcCoercion
mkTcAppCos co1 tys = foldl mkTcAppCo co1 tys
......@@ -211,6 +216,7 @@ tcCoercionKind co = go co
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
go (TcLRCo lr co) = (pickLR lr . tcSplitAppTy) <$> go co
-- c.f. Coercion.coercionKind
go_inst (TcInstCo co ty) tys = go_inst co (ty:tys)
......@@ -239,6 +245,7 @@ coVarsOfTcCo tc_co
go (TcSymCo co) = go co
go (TcTransCo co1 co2) = go co1 `unionVarSet` go co2
go (TcNthCo _ co) = go co
go (TcLRCo _ co) = go co
go (TcLetCo (EvBinds bs) co) = foldrBag (unionVarSet . go_bind) (go co) bs
`minusVarSet` get_bndrs bs
go (TcLetCo {}) = emptyVarSet -- Harumph. This does legitimately happen in the call
......@@ -306,6 +313,7 @@ ppr_co p (TcTransCo co1 co2) = maybeParen p FunPrec $
<+> ppr_co FunPrec co2
ppr_co p (TcSymCo co) = pprPrefixApp p (ptext (sLit "Sym")) [pprParendTcCo co]
ppr_co p (TcNthCo n co) = pprPrefixApp p (ptext (sLit "Nth:") <+> int n) [pprParendTcCo co]
ppr_co p (TcLRCo lr co) = pprPrefixApp p (ppr lr) [pprParendTcCo co]
ppr_fun_co :: Prec -> TcCoercion -> SDoc
ppr_fun_co p co = pprArrowChain p (split co)
......
......@@ -1357,6 +1357,7 @@ zonkTcLCoToLCo env co
; return (TcCastCo co1' co2') }
go (TcSymCo co) = do { co' <- go co; return (mkTcSymCo co') }
go (TcNthCo n co) = do { co' <- go co; return (mkTcNthCo n co') }
go (TcLRCo lr co) = do { co' <- go co; return (mkTcLRCo lr co') }
go (TcTransCo co1 co2) = do { co1' <- go co1; co2' <- go co2
; return (mkTcTransCo co1' co2') }
go (TcForAllCo tv co) = ASSERT( isImmutableTyVar tv )
......
......@@ -662,6 +662,7 @@ tidyCo env@(_, subst) co
go (SymCo co) = SymCo $! go co
go (TransCo co1 co2) = (TransCo $! go co1) $! go co2
go (NthCo d co) = NthCo d $! go co
go (LRCo lr co) = LRCo lr $! go co
go (InstCo co ty) = (InstCo $! go co) $! tidyType env ty
tidyCos :: TidyEnv -> [Coercion] -> [Coercion]
......
......@@ -17,6 +17,7 @@
module Coercion (
-- * Main data type
Coercion(..), Var, CoVar,
LeftOrRight(..), pickLR,
-- ** Functions over coercions
coVarKind,
......@@ -31,7 +32,7 @@ module Coercion (
mkReflCo, mkCoVarCo,
mkAxInstCo, mkAxInstRHS,
mkPiCo, mkPiCos, mkCoCast,
mkSymCo, mkTransCo, mkNthCo,
mkSymCo, mkTransCo, mkNthCo, mkLRCo,
mkInstCo, mkAppCo, mkTyConAppCo, mkFunCo,
mkForAllCo, mkUnsafeCo,
mkNewTypeCo,
......@@ -148,9 +149,17 @@ data Coercion
| TransCo Coercion Coercion
-- These are destructors
| NthCo Int Coercion -- Zero-indexed
| NthCo Int Coercion -- Zero-indexed; decomposes (T t0 ... tn)
| LRCo LeftOrRight Coercion -- Decomposes (t_left t_right)
| InstCo Coercion Type
deriving (Data.Data, Data.Typeable)
data LeftOrRight = CLeft | CRight
deriving( Eq, Data.Data, Data.Typeable )
pickLR :: LeftOrRight -> (a,a) -> a
pickLR CLeft (l,_) = l
pickLR CRight (_,r) = r
\end{code}
......@@ -337,6 +346,7 @@ tyCoVarsOfCo (UnsafeCo ty1 ty2) = tyVarsOfType ty1 `unionVarSet` tyVarsOfType t
tyCoVarsOfCo (SymCo co) = tyCoVarsOfCo co
tyCoVarsOfCo (TransCo co1 co2) = tyCoVarsOfCo co1 `unionVarSet` tyCoVarsOfCo co2
tyCoVarsOfCo (NthCo _ co) = tyCoVarsOfCo co
tyCoVarsOfCo (LRCo _ co) = tyCoVarsOfCo co
tyCoVarsOfCo (InstCo co ty) = tyCoVarsOfCo co `unionVarSet` tyVarsOfType ty
tyCoVarsOfCos :: [Coercion] -> VarSet
......@@ -354,6 +364,7 @@ coVarsOfCo (UnsafeCo _ _) = emptyVarSet
coVarsOfCo (SymCo co) = coVarsOfCo co
coVarsOfCo (TransCo co1 co2) = coVarsOfCo co1 `unionVarSet` coVarsOfCo co2
coVarsOfCo (NthCo _ co) = coVarsOfCo co
coVarsOfCo (LRCo _ co) = coVarsOfCo co
coVarsOfCo (InstCo co _) = coVarsOfCo co
coVarsOfCos :: [Coercion] -> VarSet
......@@ -370,6 +381,7 @@ coercionSize (UnsafeCo ty1 ty2) = typeSize ty1 + typeSize ty2
coercionSize (SymCo co) = 1 + coercionSize co
coercionSize (TransCo co1 co2) = 1 + coercionSize co1 + coercionSize co2
coercionSize (NthCo _ co) = 1 + coercionSize co
coercionSize (LRCo _ co) = 1 + coercionSize co
coercionSize (InstCo co ty) = 1 + coercionSize co + typeSize ty
\end{code}
......@@ -416,8 +428,12 @@ ppr_co p (InstCo co ty) = maybeParen p TyConPrec $
ppr_co p (UnsafeCo ty1 ty2) = pprPrefixApp p (ptext (sLit "UnsafeCo"))
[pprParendType ty1, pprParendType ty2]
ppr_co p (SymCo co) = pprPrefixApp p (ptext (sLit "Sym")) [pprParendCo co]
ppr_co p (NthCo n co) = pprPrefixApp p (ptext (sLit "Nth:") <+> int n) [pprParendCo co]
ppr_co p (NthCo n co) = pprPrefixApp p (ptext (sLit "Nth:") <> int n) [pprParendCo co]
ppr_co p (LRCo sel co) = pprPrefixApp p (ppr sel) [pprParendCo co]
instance Outputable LeftOrRight where
ppr CLeft = ptext (sLit "Left")
ppr CRight = ptext (sLit "Right")
ppr_fun_co :: Prec -> Coercion -> SDoc
ppr_fun_co p co = pprArrowChain p (split co)
......@@ -625,6 +641,10 @@ mkNthCo n co = ASSERT( ok_tc_app _ty1 n && ok_tc_app _ty2 n )
where
Pair _ty1 _ty2 = coercionKind co
mkLRCo :: LeftOrRight -> Coercion -> Coercion
mkLRCo lr (Refl ty) = Refl (pickLR lr (splitAppTy ty))
mkLRCo lr co = LRCo lr co
ok_tc_app :: Type -> Int -> Bool
ok_tc_app ty n = case splitTyConApp_maybe ty of
Just (_, tys) -> tys `lengthExceeds` n
......@@ -759,6 +779,8 @@ coreEqCoercion2 env (TransCo co11 co12) (TransCo co21 co22)
coreEqCoercion2 env (NthCo d1 co1) (NthCo d2 co2)
= d1 == d2 && coreEqCoercion2 env co1 co2
coreEqCoercion2 env (LRCo d1 co1) (LRCo d2 co2)
= d1 == d2 && coreEqCoercion2 env co1 co2
coreEqCoercion2 env (InstCo co1 ty1) (InstCo co2 ty2)
= coreEqCoercion2 env co1 co2 && eqTypeX env ty1 ty2
......@@ -900,6 +922,7 @@ subst_co subst co
go (SymCo co) = mkSymCo (go co)
go (TransCo co1 co2) = mkTransCo (go co1) (go co2)
go (NthCo d co) = mkNthCo d (go co)
go (LRCo lr co) = mkLRCo lr (go co)
go (InstCo co ty) = mkInstCo (go co) $! go_ty ty
substCoVar :: CvSubst -> CoVar -> Coercion
......@@ -1073,6 +1096,7 @@ seqCo (UnsafeCo ty1 ty2) = seqType ty1 `seq` seqType ty2
seqCo (SymCo co) = seqCo co
seqCo (TransCo co1 co2) = seqCo co1 `seq` seqCo co2
seqCo (NthCo _ co) = seqCo co
seqCo (LRCo _ co) = seqCo co
seqCo (InstCo co ty) = seqCo co `seq` seqType ty
seqCos :: [Coercion] -> ()
......@@ -1114,6 +1138,7 @@ coercionKind co = go co
go (SymCo co) = swap $ go co
go (TransCo co1 co2) = Pair (pFst $ go co1) (pSnd $ go co2)
go (NthCo d co) = tyConAppArgN d <$> go co
go (LRCo lr co) = (pickLR lr . splitAppTy) <$> go co
go (InstCo aco ty) = go_app aco [ty]
go_app :: Coercion -> [Type] -> Pair Type
......
......@@ -145,7 +145,7 @@ opt_co' env sym (TransCo co1 co2)
opt_co' env sym (NthCo n co)
| TyConAppCo tc cos <- co'
, isDecomposableTyCon tc -- Not synonym families
, isDecomposableTyCon tc -- Not synonym families
= ASSERT( n < length cos )
cos !! n
| otherwise
......@@ -153,6 +153,14 @@ opt_co' env sym (NthCo n co)
where
co' = opt_co env sym co
opt_co' env sym (LRCo lr co)
| Just pr_co <- splitAppCo_maybe co'
= pickLR lr pr_co
| otherwise
= LRCo lr co'
where
co' = opt_co env sym co
opt_co' env sym (InstCo co ty)
-- See if the first arg is already a forall
-- ...then we can just extend the current substitution
......@@ -165,7 +173,6 @@ opt_co' env sym (InstCo co ty)
= substCoWithTy (getCvInScope env) tv ty' co'_body
| otherwise = InstCo co' ty'
where
co' = opt_co env sym co
ty' = substTy env ty
......@@ -208,18 +215,19 @@ opt_trans2 _ co1 co2
-- Optimize coercions with a top-level use of transitivity.
opt_trans_rule :: InScopeSet -> NormalNonIdCo -> NormalNonIdCo -> Maybe NormalCo
-- push transitivity down through matching top-level constructors.
opt_trans_rule is in_co1@(TyConAppCo tc1 cos1) in_co2@(TyConAppCo tc2 cos2)
| tc1 == tc2 = fireTransRule "PushTyConApp" in_co1 in_co2 $
TyConAppCo tc1 (opt_transList is cos1 cos2)
-- push transitivity through matching destructors
-- Push transitivity through matching destructors
opt_trans_rule is in_co1@(NthCo d1 co1) in_co2@(NthCo d2 co2)
| d1 == d2
, co1 `compatible_co` co2
= fireTransRule "PushNth" in_co1 in_co2 $
mkNthCo d1 (opt_trans is co1 co2)
opt_trans_rule is in_co1@(LRCo d1 co1) in_co2@(LRCo d2 co2)
| d1 == d2
, co1 `compatible_co` co2
= fireTransRule "PushLR" in_co1 in_co2 $
mkLRCo d1 (opt_trans is co1 co2)
-- Push transitivity inside instantiation
opt_trans_rule is in_co1@(InstCo co1 ty1) in_co2@(InstCo co2 ty2)
| ty1 `eqType` ty2
......@@ -227,11 +235,17 @@ opt_trans_rule is in_co1@(InstCo co1 ty1) in_co2@(InstCo co2 ty2)
= fireTransRule "TrPushInst" in_co1 in_co2 $
mkInstCo (opt_trans is co1 co2) ty1
-- Push transitivity inside apply
-- Push transitivity down through matching top-level constructors.
opt_trans_rule is in_co1@(TyConAppCo tc1 cos1) in_co2@(TyConAppCo tc2 cos2)
| tc1 == tc2
= fireTransRule "PushTyConApp" in_co1 in_co2 $
TyConAppCo tc1 (opt_transList is cos1 cos2)
opt_trans_rule is in_co1@(AppCo co1a co1b) in_co2@(AppCo co2a co2b)
= fireTransRule "TrPushApp" in_co1 in_co2 $
mkAppCo (opt_trans is co1a co2a) (opt_trans is co1b co2b)
-- Eta rules
opt_trans_rule is co1@(TyConAppCo tc cos1) co2
| Just cos2 <- etaTyConAppCo_maybe tc co2
= ASSERT( length cos1 == length cos2 )
......@@ -244,6 +258,16 @@ opt_trans_rule is co1 co2@(TyConAppCo tc cos2)
fireTransRule "EtaCompR" co1 co2 $
TyConAppCo tc (opt_transList is cos1 cos2)
opt_trans_rule is co1@(AppCo co1a co1b) co2
| Just (co2a,co2b) <- etaAppCo_maybe co2
= fireTransRule "EtaAppL" co1 co2 $
mkAppCo (opt_trans is co1a co2a) (opt_trans is co1b co2b)
opt_trans_rule is co1 co2@(AppCo co2a co2b)
| Just (co1a,co1b) <- etaAppCo_maybe co1
= fireTransRule "EtaAppR" co1 co2 $
mkAppCo (opt_trans is co1a co2a) (opt_trans is co1b co2b)
-- Push transitivity inside forall
opt_trans_rule is co1 co2
| Just (tv1,r1) <- splitForAllCo_maybe co1
......@@ -359,6 +383,20 @@ etaForAllCo_maybe co
| otherwise
= Nothing
etaAppCo_maybe :: Coercion -> Maybe (Coercion,Coercion)
-- If possible, split a coercion
-- g :: t1a t1b ~ t2a t2b
-- into a pair of coercions (left g, right g)
etaAppCo_maybe co
| Just (co1,co2) <- splitAppCo_maybe co
= Just (co1,co2)
| Pair ty1 ty2 <- coercionKind co
, Just {} <- splitAppTy_maybe ty1
, Just {} <- splitAppTy_maybe ty2
= Just (LRCo CLeft co, LRCo CRight co)
| otherwise
= Nothing
etaTyConAppCo_maybe :: TyCon -> Coercion -> Maybe [Coercion]
-- If possible, split a coercion
-- g :: T s1 .. sn ~ T t1 .. tn
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment