Commit 17a868af authored by Joachim Breitner's avatar Joachim Breitner
Browse files

Introduce coerce :: Coercible a b -> a -> b

This is the result of the design at
http://ghc.haskell.org/trac/ghc/wiki/NewtypeWrappers

The goal is to be able to convert between, say [First Int] and [Last
Int] with zero run-time overhead. To that end, we introduce a special
two parameter type class Coercible whose instances are created
automatically and on-the fly. This relies on and exploits the recent
addition of roles to core.
parent 638da2fe
......@@ -137,7 +137,8 @@ ghcPrimIds
unsafeCoerceId,
nullAddrId,
seqId,
magicSingIId
magicSingIId,
coerceId
]
\end{code}
......@@ -1036,7 +1037,7 @@ they can unify with both unlifted and lifted types. Hence we provide
another gun with which to shoot yourself in the foot.
\begin{code}
lazyIdName, unsafeCoerceName, nullAddrName, seqName, realWorldName, coercionTokenName, magicSingIName :: Name
lazyIdName, unsafeCoerceName, nullAddrName, seqName, realWorldName, coercionTokenName, magicSingIName, coerceName :: Name
unsafeCoerceName = mkWiredInIdName gHC_PRIM (fsLit "unsafeCoerce#") unsafeCoerceIdKey unsafeCoerceId
nullAddrName = mkWiredInIdName gHC_PRIM (fsLit "nullAddr#") nullAddrIdKey nullAddrId
seqName = mkWiredInIdName gHC_PRIM (fsLit "seq") seqIdKey seqId
......@@ -1044,6 +1045,7 @@ realWorldName = mkWiredInIdName gHC_PRIM (fsLit "realWorld#") realWorldPr
lazyIdName = mkWiredInIdName gHC_MAGIC (fsLit "lazy") lazyIdKey lazyId
coercionTokenName = mkWiredInIdName gHC_PRIM (fsLit "coercionToken#") coercionTokenIdKey coercionTokenId
magicSingIName = mkWiredInIdName gHC_PRIM (fsLit "magicSingI") magicSingIKey magicSingIId
coerceName = mkWiredInIdName gHC_PRIM (fsLit "coerce") coerceKey coerceId
\end{code}
\begin{code}
......@@ -1118,6 +1120,21 @@ magicSingIId = pcMiscPrelId magicSingIName ty info
info = noCafIdInfo `setInlinePragInfo` neverInlinePragma
ty = mkForAllTys [alphaTyVar] alphaTy
--------------------------------------------------------------------------------
coerceId :: Id
coerceId = pcMiscPrelId coerceName ty info
where
info = noCafIdInfo `setInlinePragInfo` alwaysInlinePragma
`setUnfoldingInfo` mkCompulsoryUnfolding rhs
eqRTy = mkTyConApp coercibleTyCon [alphaTy, betaTy]
eqRPrimTy = mkTyConApp eqReprPrimTyCon [liftedTypeKind, alphaTy, betaTy]
ty = mkForAllTys [alphaTyVar, betaTyVar] (mkFunTys [eqRTy, alphaTy] betaTy)
[eqR,x,eq] = mkTemplateLocals [eqRTy, alphaTy,eqRPrimTy]
rhs = mkLams [alphaTyVar,betaTyVar,eqR,x] $
mkWildCase (Var eqR) eqRTy betaTy $
[(DataAlt coercibleDataCon, [eq], Cast (Var x) (CoVarCo eq))]
\end{code}
Note [Unsafe coerce magic]
......
......@@ -28,6 +28,9 @@ module MkCore (
-- * Constructing/deconstructing equality evidence boxes
mkEqBox,
-- * Constructing Coercible evidence
mkCoercible,
-- * Constructing general big tuples
-- $big_tuples
mkChunkified,
......@@ -305,6 +308,11 @@ mkEqBox co = ASSERT2( typeKind ty2 `eqKind` k, ppr co $$ ppr ty1 $$ ppr ty2 $$ p
where Pair ty1 ty2 = coercionKind co
k = typeKind ty1
mkCoercible :: Coercion -> CoreExpr
mkCoercible co = ASSERT2( typeKind ty2 `eqKind` k, ppr co $$ ppr ty1 $$ ppr ty2 $$ ppr (typeKind ty1) $$ ppr (typeKind ty2) )
Var (dataConWorkId coercibleDataCon) `mkTyApps` [ty1, ty2] `App` Coercion co
where Pair ty1 ty2 = coercionKind co
k = typeKind ty1
\end{code}
%************************************************************************
......
......@@ -44,12 +44,12 @@ import Unique( Unique )
import Digraph
import TyCon ( isTupleTyCon, tyConDataCons_maybe )
import TyCon ( isTupleTyCon, tyConDataCons_maybe, unwrapNewTyCon_maybe )
import TcEvidence
import TcType
import Type
import Coercion hiding (substCo)
import TysWiredIn ( eqBoxDataCon, tupleCon )
import TysWiredIn ( eqBoxDataCon, coercibleTyCon, coercibleDataCon, tupleCon )
import Id
import Class
import DataCon ( dataConWorkId )
......@@ -785,6 +785,49 @@ dsEvTerm (EvLit l) =
EvNum n -> mkIntegerExpr n
EvStr s -> mkStringExprFS s
-- Note [Coercible Instances]
dsEvTerm (EvCoercible (EvCoercibleRefl ty)) = do
return $ mkCoercible $ mkReflCo Representational ty
dsEvTerm (EvCoercible (EvCoercibleTyCon tyCon evs)) = do
ntEvs <- mapM (mapEvCoercibleArgM dsEvTerm) evs
wrapInEqRCases ntEvs $ \cos -> do
return $ mkCoercible $
mkTyConAppCo Representational tyCon cos
dsEvTerm (EvCoercible (EvCoercibleNewType lor tyCon tys v)) = do
ntEv <- dsEvTerm v
wrapInEqRCase ntEv $ \co -> do
return $ mkCoercible $
connect lor co $
mkUnbranchedAxInstCo Representational coAxiom tys
where Just (_, _, coAxiom) = unwrapNewTyCon_maybe tyCon
connect CLeft co2 co1 = mkTransCo co1 co2
connect CRight co2 co1 = mkTransCo co2 (mkSymCo co1)
wrapInEqRCase :: CoreExpr -> (Coercion -> DsM CoreExpr) -> DsM CoreExpr
wrapInEqRCase e mkBody = do
cov <- newSysLocalDs (mkCoercionType Representational ty1 ty2)
body' <- mkBody (mkCoVarCo cov)
return $
ASSERT (tc == coercibleTyCon)
mkWildCase
e
(exprType e)
(exprType body')
[(DataAlt coercibleDataCon, [cov], body')]
where
Just (tc, [ty1, ty2]) = splitTyConApp_maybe (exprType e)
wrapInEqRCases :: [EvCoercibleArg CoreExpr] -> ([Coercion] -> DsM CoreExpr) -> DsM CoreExpr
wrapInEqRCases (EvCoercibleArgN t:es) mkBody =
wrapInEqRCases es (\cos -> mkBody (mkReflCo Nominal t:cos))
wrapInEqRCases (EvCoercibleArgR e:es) mkBody = wrapInEqRCase e $ \co ->
wrapInEqRCases es (\cos -> mkBody (co:cos))
wrapInEqRCases (EvCoercibleArgP t1 t2:es) mkBody =
wrapInEqRCases es (\cos -> mkBody (mkUnivCo Phantom t1 t2:cos))
wrapInEqRCases [] mkBody = mkBody []
---------------------------------------
dsTcCoercion :: Role -> TcCoercion -> (Coercion -> CoreExpr) -> DsM CoreExpr
-- This is the crucial function that moves
......
......@@ -130,7 +130,7 @@ ghcPrimExports
= map (Avail . idName) ghcPrimIds ++
map (Avail . idName . primOpId) allThePrimOps ++
[ AvailTC n [n]
| tc <- funTyCon : primTyCons, let n = tyConName tc ]
| tc <- funTyCon : coercibleTyCon : primTyCons, let n = tyConName tc ]
\end{code}
......
......@@ -352,7 +352,7 @@ genericTyConNames = [
pRELUDE :: Module
pRELUDE = mkBaseModule_ pRELUDE_NAME
gHC_PRIM, gHC_PRIMWRAPPERS, gHC_TYPES, gHC_GENERICS, gHC_MAGIC,
gHC_PRIM, gHC_PRIMWRAPPERS, gHC_TYPES, gHC_GENERICS, gHC_MAGIC, gHC_COERCIBLE,
gHC_CLASSES, gHC_BASE, gHC_ENUM, gHC_GHCI, gHC_CSTRING,
gHC_SHOW, gHC_READ, gHC_NUM, gHC_INTEGER_TYPE, gHC_LIST,
gHC_TUPLE, dATA_TUPLE, dATA_EITHER, dATA_STRING, dATA_FOLDABLE, dATA_TRAVERSABLE, dATA_MONOID,
......@@ -370,6 +370,7 @@ gHC_TYPES = mkPrimModule (fsLit "GHC.Types")
gHC_MAGIC = mkPrimModule (fsLit "GHC.Magic")
gHC_CSTRING = mkPrimModule (fsLit "GHC.CString")
gHC_CLASSES = mkPrimModule (fsLit "GHC.Classes")
gHC_COERCIBLE = mkPrimModule (fsLit "GHC.Coercible")
gHC_BASE = mkBaseModule (fsLit "GHC.Base")
gHC_ENUM = mkBaseModule (fsLit "GHC.Enum")
......@@ -1486,6 +1487,11 @@ doubleX2PrimTyConKey = mkPreludeTyConUnique 171
int32X4PrimTyConKey = mkPreludeTyConUnique 172
int64X2PrimTyConKey = mkPreludeTyConUnique 173
ntTyConKey:: Unique
ntTyConKey = mkPreludeTyConUnique 174
coercibleTyConKey :: Unique
coercibleTyConKey = mkPreludeTyConUnique 175
---------------- Template Haskell -------------------
-- USES TyConUniques 200-299
-----------------------------------------------------
......@@ -1504,7 +1510,7 @@ unitTyConKey = mkTupleTyConUnique BoxedTuple 0
charDataConKey, consDataConKey, doubleDataConKey, falseDataConKey,
floatDataConKey, intDataConKey, nilDataConKey, ratioDataConKey,
stableNameDataConKey, trueDataConKey, wordDataConKey,
ioDataConKey, integerDataConKey, eqBoxDataConKey :: Unique
ioDataConKey, integerDataConKey, eqBoxDataConKey, coercibleDataConKey :: Unique
charDataConKey = mkPreludeDataConUnique 1
consDataConKey = mkPreludeDataConUnique 2
doubleDataConKey = mkPreludeDataConUnique 3
......@@ -1544,6 +1550,8 @@ gtDataConKey = mkPreludeDataConUnique 29
integerGmpSDataConKey, integerGmpJDataConKey :: Unique
integerGmpSDataConKey = mkPreludeDataConUnique 30
integerGmpJDataConKey = mkPreludeDataConUnique 31
coercibleDataConKey = mkPreludeDataConUnique 32
\end{code}
%************************************************************************
......@@ -1710,6 +1718,9 @@ undefinedKey = mkPreludeMiscIdUnique 155
magicSingIKey :: Unique
magicSingIKey = mkPreludeMiscIdUnique 156
coerceKey :: Unique
coerceKey = mkPreludeMiscIdUnique 157
\end{code}
Certain class operations from Prelude classes. They get their own
......
......@@ -68,6 +68,7 @@ module TysWiredIn (
-- * Equality predicates
eqTyCon_RDR, eqTyCon, eqTyConName, eqBoxDataCon,
coercibleTyCon, coercibleDataCon, coercibleClass,
mkWiredInTyConName -- This is used in TcTypeNats to define the
-- built-in functions for evaluation.
......@@ -88,6 +89,7 @@ import Type ( mkTyConApp )
import DataCon
import Var
import TyCon
import Class ( Class, mkClass )
import TypeRep
import RdrName
import Name
......@@ -147,6 +149,7 @@ wiredInTyCons = [ unitTyCon -- Not treated like other tuples, because
, listTyCon
, parrTyCon
, eqTyCon
, coercibleTyCon
, typeNatKindCon
, typeSymbolKindCon
]
......@@ -172,6 +175,10 @@ eqTyConName, eqBoxDataConName :: Name
eqTyConName = mkWiredInTyConName BuiltInSyntax gHC_TYPES (fsLit "~") eqTyConKey eqTyCon
eqBoxDataConName = mkWiredInDataConName UserSyntax gHC_TYPES (fsLit "Eq#") eqBoxDataConKey eqBoxDataCon
coercibleTyConName, coercibleDataConName :: Name
coercibleTyConName = mkWiredInTyConName UserSyntax gHC_TYPES (fsLit "Coercible") coercibleTyConKey coercibleTyCon
coercibleDataConName = mkWiredInDataConName UserSyntax gHC_TYPES (fsLit "MkCoercible") coercibleDataConKey coercibleDataCon
charTyConName, charDataConName, intTyConName, intDataConName :: Name
charTyConName = mkWiredInTyConName UserSyntax gHC_TYPES (fsLit "Char") charTyConKey charTyCon
charDataConName = mkWiredInDataConName UserSyntax gHC_TYPES (fsLit "C#") charDataConKey charDataCon
......@@ -451,6 +458,26 @@ eqBoxDataCon = pcDataCon eqBoxDataConName args [TyConApp eqPrimTyCon (map mkTyVa
k = mkTyVarTy kv
a:b:_ = tyVarList k
args = [kv, a, b]
coercibleTyCon :: TyCon
coercibleTyCon = mkClassTyCon
coercibleTyConName kind tvs [Representational, Representational]
rhs coercibleClass NonRecursive
where kind = mkArrowKinds [liftedTypeKind, liftedTypeKind] constraintKind
a:b:_ = tyVarList liftedTypeKind
tvs = [a, b]
rhs = DataTyCon [coercibleDataCon] False
coercibleDataCon :: DataCon
coercibleDataCon = pcDataCon coercibleDataConName args [TyConApp eqReprPrimTyCon (liftedTypeKind : map mkTyVarTy args)] coercibleTyCon
where
a:b:_ = tyVarList liftedTypeKind
args = [a, b]
coercibleClass :: Class
coercibleClass = mkClass (tyConTyVars coercibleTyCon) [] [] [] [] [] coercibleTyCon
\end{code}
\begin{code}
......
......@@ -2279,6 +2279,62 @@ primop TraceMarkerOp "traceMarker#" GenPrimOp
has_side_effects = True
out_of_line = True
------------------------------------------------------------------------
section "Safe coercions"
------------------------------------------------------------------------
pseudoop "coerce"
Coercible a b => a -> b
{ The function {\tt coerce} allows you to safely convert between values of
types that have the same representation with no run-time overhead. In the
simplest case you can use it instead of a newtype constructor, to go from
the newtype's concrete type to the abstract type. But it also works in
more complicated settings, e.g. converting a list of newtypes to a list of
concrete types.
}
primclass Coercible a b
{ This two-parameter class has instances for types {\tt a} and {\tt b} if
the compiler can infer that they have the same representation. This class
does not have regular instances; instead they are created on-the-fly during
type-checking. Trying to manually declare an instance of {\tt Coercible}
is an error.
Nevertheless one can pretend that the following three kinds of instances
exist. First, as a trivial base-case:
{\tt instance a a}
Furthermore, for every type constructor there is
an instance that allows to coerce under the type constructor. For
example, let {\tt D} be a prototypical type constructor ({\tt data} or {\tt
newtype}) with three type arguments, which have roles Nominal,
Representational resp. Phantom. Then there is an instance of the form
{\tt instance Coercible b b' => Coercible (D a b c) (D a b' c')}
Note that the nominal type arguments are equal, the representational type
arguments can differ, but need to have a {\tt Coercible} instance
themself, and the phantom type arguments can be changed arbitrarily.
In SafeHaskell code, this instance is only usable if the constructors of
every type constructor used in the definition of {\tt D} (including
those of {\tt D} itself) is in scope.
The third kind of instance exists for every {\tt newtype NT = MkNT T} and
comes in two variants, namely
{\tt instance Coercible a T => Coercible a NT}
{\tt instance Coercible T b => Coercible NT b}
This instance is only usable if the constructor {\tt MkNT} is in scope.
If, as a library author of a type constructor like {\tt Set a}, you
want to prevent a user of your module to write
{\tt coerce :: Set T -> Set NT},
you need to set the role of {\tt Set}'s type parameter to Nominal.
}
------------------------------------------------------------------------
section "Float SIMD Vectors"
......
......@@ -27,8 +27,11 @@ import Unify ( tcMatchTys )
import Inst
import InstEnv
import TyCon
import DataCon
import TcEvidence
import TysWiredIn ( coercibleClass )
import Name
import RdrName ( lookupGRE_Name )
import Id
import Var
import VarSet
......@@ -42,7 +45,7 @@ import FastString
import Outputable
import SrcLoc
import DynFlags
import Data.List ( partition, mapAccumL )
import Data.List ( partition, mapAccumL, zip4 )
\end{code}
%************************************************************************
......@@ -934,7 +937,9 @@ mk_dict_err ctxt (ct, (matches, unifiers, safe_haskell))
= do { let (is_ambig, ambig_msg) = mkAmbigMsg ct
; (ctxt, binds_msg) <- relevantBindings True ctxt ct
; traceTc "mk_dict_err" (ppr ct $$ ppr is_ambig $$ ambig_msg)
; return (ctxt, cannot_resolve_msg is_ambig binds_msg ambig_msg) }
; safe_mod <- safeLanguageOn `fmap` getDynFlags
; rdr_env <- getGlobalRdrEnv
; return (ctxt, cannot_resolve_msg safe_mod rdr_env is_ambig binds_msg ambig_msg) }
| not safe_haskell -- Some matches => overlap errors
= return (ctxt, overlap_msg)
......@@ -949,8 +954,9 @@ mk_dict_err ctxt (ct, (matches, unifiers, safe_haskell))
givens = getUserGivens ctxt
all_tyvars = all isTyVarTy tys
cannot_resolve_msg has_ambig_tvs binds_msg ambig_msg
= vcat [ addArising orig (no_inst_herald <+> pprParendType pred)
cannot_resolve_msg safe_mod rdr_env has_ambig_tvs binds_msg ambig_msg
= vcat [ addArising orig (no_inst_herald <+> pprParendType pred $$
coercible_msg safe_mod rdr_env)
, vcat (pp_givens givens)
, ppWhen (has_ambig_tvs && not (null unifiers && null givens))
(vcat [ ambig_msg, binds_msg, potential_msg ])
......@@ -1064,6 +1070,78 @@ mk_dict_err ctxt (ct, (matches, unifiers, safe_haskell))
]
]
-- This function tries to reconstruct why a "Coercible ty1 ty2" constraint
-- is left over. Therefore its logic has to stay in sync with
-- getCoericbleInst in TcInteract. See Note [Coercible Instances]
coercible_msg safe_mod rdr_env
| clas /= coercibleClass = empty
| Just (tc1,tyArgs1) <- splitTyConApp_maybe ty1,
Just (tc2,tyArgs2) <- splitTyConApp_maybe ty2,
tc1 == tc2
= nest 2 $ vcat $
-- Only for safe haskell: First complain if tc is abstract, only if
-- not check if the type constructors therein are abstract
(if safe_mod
then case tyConAbstractMsg rdr_env tc1 empty of
Just msg ->
[ msg $$ ptext (sLit "as required in SafeHaskell mode") ]
Nothing ->
[ msg
| tc <- tyConsOfTyCon tc1
, Just msg <- return $
tyConAbstractMsg rdr_env tc $
parens $ ptext (sLit "used within") <+> quotes (ppr tc1)
]
else []
) ++
[ fsep [ hsep [ ptext $ sLit "because the", speakNth n, ptext $ sLit "type argument"]
, hsep [ ptext $ sLit "of", quotes (ppr tc1), ptext $ sLit "has role Nominal,"]
, ptext $ sLit "but the arguments"
, quotes (ppr t1)
, ptext $ sLit "and"
, quotes (ppr t2)
, ptext $ sLit "differ" ]
| (n,Nominal,t1,t2) <- zip4 [1..] (tyConRoles tc1) tyArgs1 tyArgs2
, not (t1 `eqType` t2)
]
| Just (tc,_) <- splitTyConApp_maybe ty1,
Just msg <- coercible_msg_for_tycon rdr_env tc
= msg
| Just (tc,_) <- splitTyConApp_maybe ty2,
Just msg <- coercible_msg_for_tycon rdr_env tc
= msg
| otherwise
= nest 2 $ hsep [ ptext $ sLit "because", quotes (ppr ty1),
ptext $ sLit "and", quotes (ppr ty2),
ptext $ sLit "are different types." ]
where
(clas, ~[ty1,ty2]) = getClassPredTys (ctPred ct)
dataConMissing rdr_env tc =
all (null . lookupGRE_Name rdr_env) (map dataConName (tyConDataCons tc))
coercible_msg_for_tycon rdr_env tc
| isRecursiveTyCon tc
= Just $ nest 2 $ hsep [ ptext $ sLit "because", quotes (ppr tc)
, ptext $ sLit "is a recursive type constuctor" ]
| isNewTyCon tc
= tyConAbstractMsg rdr_env tc empty
| otherwise
= Nothing
tyConAbstractMsg rdr_env tc occExpl
| isAbstractTyCon tc || dataConMissing rdr_env tc = Just $ vcat $
[ fsep [ ptext $ sLit "because the type constructor", quotes (ppr tc) <+> occExpl
, ptext $ sLit "is abstract" ]
| isAbstractTyCon tc
] ++
[ fsep [ ptext (sLit "because the constructor") <> plural (tyConDataCons tc)
, ptext (sLit "of") <+> quotes (ppr tc) <+> occExpl
, isOrAre (tyConDataCons tc) <+> ptext (sLit "not imported") ]
| dataConMissing rdr_env tc
]
| otherwise = Nothing
show_fixes :: [SDoc] -> SDoc
show_fixes [] = empty
show_fixes (f:fs) = sep [ ptext (sLit "Possible fix:")
......
......@@ -16,6 +16,7 @@ module TcEvidence (
EvBind(..), emptyTcEvBinds, isEmptyTcEvBinds,
EvTerm(..), mkEvCast, evVarsOfTerm,
EvLit(..), evTermCoercion,
EvCoercible(..), EvCoercibleArg(..), mapEvCoercibleArgM,
-- TcCoercion
TcCoercion(..), LeftOrRight(..), pickLR,
......@@ -534,6 +535,9 @@ data EvTerm
| EvLit EvLit -- Dictionary for class "SingI" for type lits.
-- Note [SingI and EvLit]
| EvCoercible EvCoercible -- Dictionary for "Coercible a b"
-- Note [Coercible Instances]
deriving( Data.Data, Data.Typeable)
......@@ -542,6 +546,22 @@ data EvLit
| EvStr FastString
deriving( Data.Data, Data.Typeable)
data EvCoercible
= EvCoercibleRefl Type
| EvCoercibleTyCon TyCon [EvCoercibleArg EvTerm]
| EvCoercibleNewType LeftOrRight TyCon [Type] EvTerm
deriving( Data.Data, Data.Typeable)
data EvCoercibleArg a
= EvCoercibleArgN Type
| EvCoercibleArgR a
| EvCoercibleArgP Type Type
deriving( Data.Data, Data.Typeable)
mapEvCoercibleArgM :: Monad m => (a -> m b) -> EvCoercibleArg a -> m (EvCoercibleArg b)
mapEvCoercibleArgM _ (EvCoercibleArgN t) = return (EvCoercibleArgN t)
mapEvCoercibleArgM f (EvCoercibleArgR v) = do { v' <- f v; return (EvCoercibleArgR v') }
mapEvCoercibleArgM _ (EvCoercibleArgP t1 t2) = return (EvCoercibleArgP t1 t2)
\end{code}
Note [Coercion evidence terms]
......@@ -654,6 +674,12 @@ evVarsOfTerm (EvCast tm co) = evVarsOfTerm tm `unionVarSet` coVarsOfTcCo c
evVarsOfTerm (EvTupleMk evs) = evVarsOfTerms evs
evVarsOfTerm (EvDelayedError _ _) = emptyVarSet
evVarsOfTerm (EvLit _) = emptyVarSet
evVarsOfTerm (EvCoercible evnt) = evVarsOfEvCoercible evnt
evVarsOfEvCoercible :: EvCoercible -> VarSet
evVarsOfEvCoercible (EvCoercibleRefl _) = emptyVarSet
evVarsOfEvCoercible (EvCoercibleTyCon _ evs) = evVarsOfTerms [v | EvCoercibleArgR v <- evs ]
evVarsOfEvCoercible (EvCoercibleNewType _ _ _ v) = evVarsOfTerm v
evVarsOfTerms :: [EvTerm] -> VarSet
evVarsOfTerms = foldr (unionVarSet . evVarsOfTerm) emptyVarSet
......@@ -716,11 +742,23 @@ instance Outputable EvTerm where
ppr (EvSuperClass d n) = ptext (sLit "sc") <> parens (ppr (d,n))
ppr (EvDFunApp df tys ts) = ppr df <+> sep [ char '@' <> ppr tys, ppr ts ]
ppr (EvLit l) = ppr l
ppr (EvCoercible co) = ptext (sLit "Coercible") <+> ppr co
ppr (EvDelayedError ty msg) = ptext (sLit "error")
<+> sep [ char '@' <> ppr ty, ppr msg ]
instance Outputable EvLit where
ppr (EvNum n) = integer n
ppr (EvStr s) = text (show s)
instance Outputable EvCoercible where
ppr (EvCoercibleRefl ty) = ppr ty
ppr (EvCoercibleTyCon tyCon evs) = ppr tyCon <+> hsep (map ppr evs)
ppr (EvCoercibleNewType CLeft tyCon tys v) = ppr (tyCon `mkTyConApp` tys) <+> char ';' <+> ppr v
ppr (EvCoercibleNewType CRight tyCon tys v) =ppr v <+> char ';' <+> ppr (tyCon `mkTyConApp` tys)
instance Outputable a => Outputable (EvCoercibleArg a) where
ppr (EvCoercibleArgN t) = ptext (sLit "N:") <+> ppr t
ppr (EvCoercibleArgR v) = ptext (sLit "R:") <+> ppr v
ppr (EvCoercibleArgP t1 t2) = ptext (sLit "P:") <+> parens (ppr (t1,t2))
\end{code}
......@@ -1178,6 +1178,9 @@ zonkEvTerm env (EvTupleSel tm n) = do { tm' <- zonkEvTerm env tm
zonkEvTerm env (EvTupleMk tms) = do { tms' <- mapM (zonkEvTerm env) tms
; return (EvTupleMk tms') }
zonkEvTerm _ (EvLit l) = return (EvLit l)
zonkEvTerm env (EvCoercible evnt) = do { evnt' <- zonkEvCoercible env evnt
; return (EvCoercible evnt')
}
zonkEvTerm env (EvSuperClass d n) = do { d' <- zonkEvTerm env d
; return (EvSuperClass d' n) }
zonkEvTerm env (EvDFunApp df tys tms)
......@@ -1188,6 +1191,16 @@ zonkEvTerm env (EvDelayedError ty msg)
= do { ty' <- zonkTcTypeToType env ty
; return (EvDelayedError ty' msg) }
zonkEvCoercible :: ZonkEnv -> EvCoercible -> TcM EvCoercible
zonkEvCoercible _ (EvCoercibleRefl ty) = return (EvCoercibleRefl ty)
zonkEvCoercible env (EvCoercibleTyCon tyCon evs) = do
evs' <- mapM (mapEvCoercibleArgM (zonkEvTerm env)) evs
return (EvCoercibleTyCon tyCon evs')
zonkEvCoercible env (EvCoercibleNewType l tyCon tys v) = do
v' <- zonkEvTerm env v
return (EvCoercibleNewType l tyCon tys v')
zonkTcEvBinds :: ZonkEnv -> TcEvBinds -> TcM (ZonkEnv, TcEvBinds)
zonkTcEvBinds env (TcEvBinds var) = do { (env', bs') <- zonkEvBindsVar env var
; return (env', EvBinds bs') }
......
......@@ -26,11 +26,14 @@ import InstEnv( lookupInstEnv, instanceDFunId )
import Var
import TcType
import PrelNames (singIClassName, ipClassNameKey )
import TysWiredIn ( coercibleClass )
import Id( idType )
import Class
import TyCon
import DataCon
import Name
import RdrName ( GlobalRdrEnv, lookupGRE_Name, mkRdrQual, is_as,
is_decl, Provenance(Imported), gre_prov )
import FunDeps
import TcEvidence
......@@ -45,7 +48,7 @@ import Maybes( orElse )
import Bag
import Control.Monad ( foldM )
import Data.Maybe(catMaybes)
import Data.Maybe ( catMaybes, mapPaybe )
import VarEnv
......@@ -1724,6 +1727,11 @@ data LookupInstResult
= NoInstance
| GenInst [CtEvidence] EvTerm
instance Outputable LookupInstResult where
ppr NoInstance = text "NoInstance"
ppr (GenInst ev t) = text "GenInst" <+> ppr ev <+> ppr t
matchClassInst :: InertSet -> Class -> [Type] -> CtLoc -> TcS LookupInstResult
matchClassInst _ clas [ k, ty ] _
......@@ -1768,6 +1776,15 @@ matchClassInst _ clas [ k, ty ] _
unexpected = panicTcS (text "Unexpected evidence for SingI")
matchClassInst _ clas [ ty1, ty2 ] _
| clas == coercibleClass = do
traceTcS "matchClassInst for" $ ppr clas <+> ppr ty1 <+> ppr ty2
rdr_env <- getGlobalRdrEnvTcS
safeMode <- safeLanguageOn `fmap` getDynFlags
ev <- getCoericbleInst safeMode rdr_env ty1 ty2
traceTcS "matchClassInst returned" $ ppr ev
return ev
matchClassInst inerts clas tys loc
= do { dflags <- getDynFlags
; untch <- getUntouchables
......@@ -1848,8 +1865,117 @@ matchClassInst inerts clas tys loc
| otherwise = False -- No overlap with a solved, already been taken care of
-- by the overlap check with the instance environment.
matchable _tys ct = pprPanic "Expecting dictionary!" (ppr ct)
-- See Note [Coercible Instances]
-- Changes to this logic should likely be reflected in coercible_msg in TcErrors.
getCoericbleInst :: Bool -> GlobalRdrEnv -> TcType -> TcType -> TcS LookupInstResult
getCoericbleInst safeMode rdr_env ty1 ty2
| ty1 `eqType` ty2
= do return $ GenInst []
$ EvCoercible (EvCoercibleRefl ty1)
| Just (tc1,tyArgs1) <- splitTyConApp_maybe ty1,
Just (tc2,tyArgs2) <- splitTyConApp_maybe ty2,
tc1 == tc2,
nominalArgsAgree tc1 tyArgs1 tyArgs2,
not safeMode || all (dataConsInScope rdr_env) (tyConsOfTyCon tc1)
= do -- Mark all used data constructors as used
when safeMode $ mapM_ (markDataConsAsUsed rdr_env) (tyConsOfTyCon tc1)
-- We want evidence for all type arguments of role R
arg_evs <- flip mapM (zip3 (tyConRoles tc1) tyArgs1 tyArgs2) $ \(r,ta1,ta2) ->
case r of Nominal -> return (Nothing, EvCoercibleArgN ta1 {- == ta2, due to nominalArgsAgree -})
Representational -> do
ct_ev <- requestCoercible ta1 ta2
return (freshGoal ct_ev, EvCoercibleArgR (getEvTerm ct_ev))
Phantom -> do
return (Nothing, EvCoercibleArgP ta1 ta2)
return $ GenInst (mapMaybe fst arg_evs)
$ EvCoercible (EvCoercibleTyCon tc1 (map snd arg_evs))
| Just (tc,tyArgs) <- splitTyConApp_maybe ty1,
Just (_, _, _) <- unwrapNewTyCon_maybe tc,
not (isRecursiveTyCon tc),
dataConsInScope rdr_env tc -- Do noot look at all tyConsOfTyCon
= do markDataConsAsUsed rdr_env tc