summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--compiler/coreSyn/CoreLint.lhs13
-rw-r--r--compiler/coreSyn/ExternalCore.lhs3
-rw-r--r--compiler/coreSyn/MkExternalCore.lhs5
-rw-r--r--compiler/coreSyn/PprExternalCore.lhs4
-rw-r--r--compiler/coreSyn/TrieMap.lhs22
-rw-r--r--compiler/deSugar/DsBinds.lhs1
-rw-r--r--compiler/iface/BinIface.hs14
-rw-r--r--compiler/iface/IfaceType.lhs5
-rw-r--r--compiler/iface/TcIface.lhs1
-rw-r--r--compiler/typecheck/TcCanonical.lhs14
-rw-r--r--compiler/typecheck/TcEvidence.lhs14
-rw-r--r--compiler/typecheck/TcHsSyn.lhs1
-rw-r--r--compiler/typecheck/TcType.lhs1
-rw-r--r--compiler/types/Coercion.lhs31
-rw-r--r--compiler/types/OptCoercion.lhs56
15 files changed, 152 insertions, 33 deletions
diff --git a/compiler/coreSyn/CoreLint.lhs b/compiler/coreSyn/CoreLint.lhs
index dcd366f381..250efdd85d 100644
--- a/compiler/coreSyn/CoreLint.lhs
+++ b/compiler/coreSyn/CoreLint.lhs
@@ -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
diff --git a/compiler/coreSyn/ExternalCore.lhs b/compiler/coreSyn/ExternalCore.lhs
index d2f6691a7c..287f08049e 100644
--- a/compiler/coreSyn/ExternalCore.lhs
+++ b/compiler/coreSyn/ExternalCore.lhs
@@ -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
diff --git a/compiler/coreSyn/MkExternalCore.lhs b/compiler/coreSyn/MkExternalCore.lhs
index 21037088e1..8844818bdc 100644
--- a/compiler/coreSyn/MkExternalCore.lhs
+++ b/compiler/coreSyn/MkExternalCore.lhs
@@ -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 =
diff --git a/compiler/coreSyn/PprExternalCore.lhs b/compiler/coreSyn/PprExternalCore.lhs
index 26e64ee641..2290810fe1 100644
--- a/compiler/coreSyn/PprExternalCore.lhs
+++ b/compiler/coreSyn/PprExternalCore.lhs
@@ -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
diff --git a/compiler/coreSyn/TrieMap.lhs b/compiler/coreSyn/TrieMap.lhs
index 7170f1cede..6bc78a8272 100644
--- a/compiler/coreSyn/TrieMap.lhs
+++ b/compiler/coreSyn/TrieMap.lhs
@@ -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}
diff --git a/compiler/deSugar/DsBinds.lhs b/compiler/deSugar/DsBinds.lhs
index 803cdd886e..b418c8d592 100644
--- a/compiler/deSugar/DsBinds.lhs
+++ b/compiler/deSugar/DsBinds.lhs
@@ -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)
diff --git a/compiler/iface/BinIface.hs b/compiler/iface/BinIface.hs
index a319f6ed62..362df3fc35 100644
--- a/compiler/iface/BinIface.hs
+++ b/compiler/iface/BinIface.hs
@@ -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)
-------------------------------------------------------------------------
diff --git a/compiler/iface/IfaceType.lhs b/compiler/iface/IfaceType.lhs
index 225a3c812b..4a35f0049b 100644
--- a/compiler/iface/IfaceType.lhs
+++ b/compiler/iface/IfaceType.lhs
@@ -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 ]
diff --git a/compiler/iface/TcIface.lhs b/compiler/iface/TcIface.lhs
index 80c2029a70..eb9e5ddb80 100644
--- a/compiler/iface/TcIface.lhs
+++ b/compiler/iface/TcIface.lhs
@@ -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
diff --git a/compiler/typecheck/TcCanonical.lhs b/compiler/typecheck/TcCanonical.lhs
index e755d69c6b..dbb9de1365 100644
--- a/compiler/typecheck/TcCanonical.lhs
+++ b/compiler/typecheck/TcCanonical.lhs
@@ -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
diff --git a/compiler/typecheck/TcEvidence.lhs b/compiler/typecheck/TcEvidence.lhs
index 321809f91d..c88b350616 100644
--- a/compiler/typecheck/TcEvidence.lhs
+++ b/compiler/typecheck/TcEvidence.lhs
@@ -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)
diff --git a/compiler/typecheck/TcHsSyn.lhs b/compiler/typecheck/TcHsSyn.lhs
index d56f7af1ac..ef53f4e24d 100644
--- a/compiler/typecheck/TcHsSyn.lhs
+++ b/compiler/typecheck/TcHsSyn.lhs
@@ -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 )
diff --git a/compiler/typecheck/TcType.lhs b/compiler/typecheck/TcType.lhs
index 758573dd46..e129bac53c 100644
--- a/compiler/typecheck/TcType.lhs
+++ b/compiler/typecheck/TcType.lhs
@@ -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]
diff --git a/compiler/types/Coercion.lhs b/compiler/types/Coercion.lhs
index 42e54ba47b..30e71fd563 100644
--- a/compiler/types/Coercion.lhs
+++ b/compiler/types/Coercion.lhs
@@ -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
diff --git a/compiler/types/OptCoercion.lhs b/compiler/types/OptCoercion.lhs
index 7d707c33c4..c699163e74 100644
--- a/compiler/types/OptCoercion.lhs
+++ b/compiler/types/OptCoercion.lhs
@@ -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
View Lorry Controller Status