Commit 04ef7649 authored by sheaf's avatar sheaf
Browse files

use coercion instead of dictionary evidence

parent 63725ae8
......@@ -144,7 +144,7 @@ module GHC.Builtin.Types (
-- ** FixedRuntimeRep
fixedRuntimeRepClass, fixedRuntimeRepTyCon,
fixedRuntimeRepTyConName, fixedRuntimeRepDataCon,
fixedRuntimeRepTyConName,
-- * Multiplicity and friends
multiplicityTyConName, oneDataConName, manyDataConName, multiplicityTy,
......@@ -1702,33 +1702,26 @@ unliftedRepTy = mkTyConApp boxedRepDataConTyCon [unliftedDataConTy]
-- type FixedRuntimeRep :: RuntimeRep -> Constraint
-- class FixedRuntimeRep rep where {}
fixedRuntimeRepTyConName, fixedRuntimeRepDataConName :: Name
fixedRuntimeRepTyConName :: Name
fixedRuntimeRepTyConName =
mkWiredInTyConName UserSyntax gHC_TYPES (fsLit "FixedRuntimeRep")
fixedRuntimeRepTyConKey fixedRuntimeRepTyCon
fixedRuntimeRepDataConName =
mkWiredInDataConName UserSyntax gHC_TYPES (fsLit "MkFixedRuntimeRep")
fixedRuntimeRepDataConKey fixedRuntimeRepDataCon
fixedRuntimeRepTyCon :: TyCon
fixedRuntimeRepClass :: Class
fixedRuntimeRepDataCon :: DataCon
(fixedRuntimeRepTyCon, fixedRuntimeRepClass, fixedRuntimeRepDataCon)
= (tycon, klass, datacon)
(fixedRuntimeRepTyCon, fixedRuntimeRepClass)
= (tycon, klass)
where
tycon = mkClassTyCon fixedRuntimeRepTyConName binders roles
rhs klass
(mkPrelTyConRepName fixedRuntimeRepTyConName)
klass = mkClass (tyConName tycon) (tyConTyVars tycon)
[] [] [] [] [] (mkAnd []) tycon
datacon = pcDataConW fixedRuntimeRepDataConName
tvs [unrestricted runtimeRepTy] tycon
-- Kind: RuntimeRep -> Constraint
binders = mkTemplateAnonTyConBinders [runtimeRepTy]
tvs = binderVars binders
roles = [Nominal]
rhs = mkDataTyConRhs [datacon]
rhs = mkDataTyConRhs []
{- *********************************************************************
* *
......
......@@ -31,7 +31,7 @@ module GHC.Core.Coercion (
mkAxInstCo, mkUnbranchedAxInstCo,
mkAxInstRHS, mkUnbranchedAxInstRHS,
mkAxInstLHS, mkUnbranchedAxInstLHS,
mkPiCo, mkPiCos, mkCoCast,
mkPiCo, mkPiCos,
mkSymCo, mkTransCo,
mkNthCo, mkNthCoFunCo, nthCoRole, mkLRCo,
mkInstCo, mkAppCo, mkAppCos, mkTyConAppCo, mkFunCo,
......@@ -1622,26 +1622,6 @@ mkPiCo r v co | isTyVar v = mkHomoForAllCos [v] co
mkFunCo r (multToCo (varMult v)) (mkReflCo r (varType v)) co
| otherwise = mkFunCo r (multToCo (varMult v)) (mkReflCo r (varType v)) co
-- mkCoCast (c :: s1 ~?r t1) (g :: (s1 ~?r t1) ~#R (s2 ~?r t2)) :: s2 ~?r t2
-- The first coercion might be lifted or unlifted; thus the ~? above
-- Lifted and unlifted equalities take different numbers of arguments,
-- so we have to make sure to supply the right parameter to decomposeCo.
-- Also, note that the role of the first coercion is the same as the role of
-- the equalities related by the second coercion. The second coercion is
-- itself always representational.
mkCoCast :: Coercion -> CoercionR -> Coercion
mkCoCast c g
| (g2:g1:_) <- reverse co_list
= mkSymCo g1 `mkTransCo` c `mkTransCo` g2
| otherwise
= pprPanic "mkCoCast" (ppr g $$ ppr (coercionKind g))
where
-- g :: (s1 ~# t1) ~# (s2 ~# t2)
-- g1 :: s1 ~# s2
-- g2 :: t1 ~# t2
(tc, _) = splitTyConApp (coercionLKind g)
co_list = decomposeCo (tyConArity tc) g (tyConRolesRepresentational tc)
{- Note [castCoercionKind1]
~~~~~~~~~~~~~~~~~~~~~~~~~~~
......
......@@ -9,7 +9,7 @@ Utility functions on @Core@ syntax
-- | Commonly useful utilities for manipulating the Core language
module GHC.Core.Utils (
-- * Constructing expressions
mkCast,
mkCast, mkCoCast,
mkTick, mkTicks, mkTickNoHNF, tickHNFArgs,
bindNonRec, needsCaseBinding,
mkAltExpr, mkDefaultCase, mkSingleAltCase,
......@@ -81,6 +81,7 @@ import GHC.Core.Multiplicity
import GHC.Builtin.Names (makeStaticName, unsafeEqualityProofName)
import GHC.Builtin.PrimOps
import GHC.Builtin.Types ( fixedRuntimeRepTyCon )
import GHC.Types.Var
import GHC.Types.SrcLoc
......@@ -304,6 +305,43 @@ applyTypeToArgs e op_ty args
************************************************************************
-}
-- mkCoCast (c :: s1 ~?r t1) (g :: (s1 ~?r t1) ~#R (s2 ~?r t2)) :: s2 ~?r t2
-- The first coercion might be lifted or unlifted; thus the ~? above
-- Lifted and unlifted equalities take different numbers of arguments,
-- so we have to make sure to supply the right parameter to decomposeCo.
-- Also, note that the role of the first coercion is the same as the role of
-- the equalities related by the second coercion. The second coercion is
-- itself always representational.
mkCoCast :: Coercion -> CoercionR -> Coercion
mkCoCast c g
-- SLD: phase 2 of FixedRuntimeRep
-- The evidence for "FixedRuntimeRep rr" is a coercion.
-- This means we can have:
-- ev = [W] hole{$dFixedRuntimeRep} :: FixedRuntimeRep rr
-- new_pred = FixedRuntimeRep IntRep
-- co = FixedRuntimeRep ...
| tc == fixedRuntimeRepTyCon
, [g1] <- co_list
= mkTyConAppCo Nominal fixedRuntimeRepTyCon [c `mkTransCo` g1]
| (g2:g1:_) <- reverse co_list
= mkSymCo g1 `mkTransCo` c `mkTransCo` g2
| otherwise
= pprPanic "mkCoCast" $ vcat
[ text "c =" <+> ppr c
, text "g =" <+> ppr g
, text "coercionKind g =" <+> ppr (coercionKind g)
, text "tc =" <+> ppr tc
, text "co_list =" <+> ppr co_list
]
where
-- g :: (s1 ~# t1) ~# (s2 ~# t2)
-- g1 :: s1 ~# s2
-- g2 :: t1 ~# t2
(tc, _) = splitTyConApp (coercionLKind g)
co_list = decomposeCo (tyConArity tc) g (tyConRolesRepresentational tc)
-- | Wrap the given expression in the coercion safely, dropping
-- identity coercions and coalescing nested coercions
mkCast :: CoreExpr -> CoercionR -> CoreExpr
......
......@@ -303,7 +303,7 @@ dsExpr (HsLamCase _ matches)
dsExpr e@(HsApp _ fun arg)
= do { fun' <- dsLExpr fun
-- SLD: handled in GHC.Tc.Gen.tcEValArg, test: T12973 (for example)
-- SLD: handled in GHC.Tc.Gen.App.tcEValArg, test: T12973 (for example)
-- See Note [Desugaring representation-polymorphic applications]
-- in GHC.HsToCore.Utils
; dsWhenNoErrs (hsExprType e) (dsLExprNoLP arg)
......
......@@ -21,6 +21,7 @@ import GHC.Tc.Utils.TcType
import GHC.Tc.Utils.Instantiate(instDFunType, tcInstType)
import GHC.Tc.Instance.Typeable
import GHC.Tc.Utils.TcMType
import GHC.Tc.Types.Constraint
import GHC.Tc.Types.Evidence
import GHC.Tc.Instance.Family( tcGetFamInstEnvs, tcInstNewTyCon_maybe, tcLookupDataFamInst )
import GHC.Tc.Types.Origin (CtOrigin(..), FRROrigin)
......@@ -30,17 +31,18 @@ import GHC.Builtin.Types
import GHC.Builtin.Types.Prim( eqPrimTyCon, eqReprPrimTyCon, tYPETyCon )
import GHC.Builtin.Names
import GHC.Types.Basic ( TypeOrKind(..) )
import GHC.Types.Name.Reader( lookupGRE_FieldLabel, greMangledName )
import GHC.Types.SafeHaskell
import GHC.Types.Name ( Name, pprDefinedAt )
import GHC.Types.Var.Env ( VarEnv )
import GHC.Types.Id
import GHC.Core.TyCo.Rep ( CoercionHole(..), Coercion(Refl) )
import GHC.Core.Predicate
import GHC.Core.InstEnv
import GHC.Core.Type
import GHC.Core.Make ( mkCharExpr, mkStringExprFS, mkNaturalExpr
, mkNilExpr, mkConsExpr, mkCoreConApps )
import GHC.Core.Make ( mkCharExpr, mkStringExprFS, mkNaturalExpr )
import GHC.Core.DataCon
import GHC.Core.TyCon
import GHC.Core.Class
......@@ -630,102 +632,115 @@ matchCoercible args = pprPanic "matchLiftedCoercible" (ppr args)
-- > ty :: TYPE (F x)
--
-- this function will emit a new Wanted 'FixedRuntimeRep' constraint.
hasFixedRuntimeRep :: FRROrigin -> Type -> TcM EvTerm
hasFixedRuntimeRep :: FRROrigin -> Type -> TcM FixedRuntimeRepHole
hasFixedRuntimeRep frrOrig ty = go ( typeKind ty )
where
orig :: CtOrigin
orig = FixedRuntimeRepOrigin frrOrig
go :: Kind -> TcM EvTerm
go :: Kind -> TcM FixedRuntimeRepHole
go ki
| Just ki' <- tcView ki
= go ki'
| Just (tc, [rep]) <- splitTyConApp_maybe ki
| Just (tc, [r]) <- splitTyConApp_maybe ki
, tc == tYPETyCon
= case getRuntimeRepExpr rep of
Just repExpr
-> pure $ EvExpr repExpr
_ -> emitWanted orig $ mkTyConApp fixedRuntimeRepTyCon [rep]
, let
pty :: PredType
pty = mkTyConApp fixedRuntimeRepTyCon [r]
= if isFixedRuntimeRep r
then
-- Create a filled coercion hole.
newFixedRuntimeRepHole pty ( Just $ Refl r )
else
-- Emit a new wanted constraint.
emitFRRWanted frrOrig pty
| otherwise
= pprPanic "hasFixedRuntimeRep: not of form 'TYPE rep'" $
vcat
[ text "orig =" <+> ppr orig
, text "ty =" <+> ppr ty
[ text "ty =" <+> ppr ty
, text "ki =" <+> ppr ki
, text "frrOrig =" <+> ppr frrOrig
]
type FixedRuntimeRepHole = CoercionHole
-- | Create a new coercion hole holding evidence
-- for a 'FixedRuntimeRep' constraint.
newFixedRuntimeRepHole :: PredType -> Maybe TcCoercion -> TcM FixedRuntimeRepHole
newFixedRuntimeRepHole pty mbFill = do
co_var <- newEvVar pty
traceTc "New FixedRuntimeRep coercion hole:" (ppr co_var)
ref <- newMutVar mbFill
pure $ CoercionHole { ch_co_var = co_var, ch_ref = ref }
-- | Emit a new "FixedRuntimeRep" constraint.
emitFRRWanted :: FRROrigin -> PredType -> TcM FixedRuntimeRepHole
emitFRRWanted frrOrig pty = do
loc <- getCtLocM (FixedRuntimeRepOrigin frrOrig) (Just KindLevel)
hole <- newFixedRuntimeRepHole pty Nothing
let
wantedCtEv :: CtEvidence
wantedCtEv =
CtWanted
{ ctev_dest = HoleDest hole
, ctev_pred = pty
, ctev_nosh = WDeriv
, ctev_loc = loc
}
emitSimple $ mkNonCanonical wantedCtEv
pure hole
matchFixedRuntimeRep :: [Type] -> TcM ClsInstResult
matchFixedRuntimeRep [ty]
| Just rep <- getRuntimeRepExpr ty
matchFixedRuntimeRep [rr]
| isFixedRuntimeRep rr
= return $ OneInst
{ cir_new_theta = []
, cir_mk_ev = \ _ -> evDataConApp fixedRuntimeRepDataCon [ty] [rep]
, cir_mk_ev = \ _ -> evCoercion $ Refl rr
, cir_what = BuiltinInstance }
| otherwise
= return NoInstance
matchFixedRuntimeRep args = pprPanic "matchFixedRuntimeRep" (ppr args)
getRuntimeRepExpr :: Type -> Maybe EvExpr
getRuntimeRepExpr ty = case splitTyConApp_maybe ty of
isFixedRuntimeRep :: Type -> Bool
isFixedRuntimeRep rr = case splitTyConApp_maybe rr of
Just (tc, args)
| tc == boxedRepDataConTyCon
, [l] <- args
-> ( \ x -> mkCoreConApps boxedRepDataCon [x] )
<$> getLevityExpr l
-> isFixedLevity l
| tc == vecRepDataConTyCon
, [count, elt] <- args
-> ( \ x y -> mkCoreConApps vecRepDataCon [x,y] )
<$> getVecCountExpr count
<*> getVecElemExpr elt
| tc == tupleRepDataConTyCon
, [reps] <- args
-> ( \ x -> mkCoreConApps tupleRepDataCon [x] )
<$> getRuntimeRepsExpr reps
| tc == sumRepDataConTyCon
-> isFixedVecCount count && isFixedVecElem elt
| tc == tupleRepDataConTyCon || tc == sumRepDataConTyCon
, [reps] <- args
-> ( \ x -> mkCoreConApps sumRepDataCon [x] )
<$> getRuntimeRepsExpr reps
-> isFixedRuntimeReps reps
| otherwise
-> lookupInNullaryDataCons tc runtimeRepSimpleDataCons
_ -> Nothing
-> any ( \ dc -> tc == promoteDataCon dc ) runtimeRepSimpleDataCons
_ -> False
getLevityExpr :: Type -> Maybe EvExpr
getLevityExpr ty = case splitTyConApp_maybe ty of
isFixedLevity :: Type -> Bool
isFixedLevity l = case splitTyConApp_maybe l of
Just (tc, [])
-> lookupInNullaryDataCons tc [liftedDataCon, unliftedDataCon]
_ -> Nothing
-> any ( \ dc -> tc == promoteDataCon dc ) [liftedDataCon, unliftedDataCon]
_ -> False
getVecCountExpr :: Type -> Maybe EvExpr
getVecCountExpr ty = case splitTyConApp_maybe ty of
isFixedVecCount :: Type -> Bool
isFixedVecCount ct = case splitTyConApp_maybe ct of
Just (tc, [])
-> lookupInNullaryDataCons tc vecCountDataCons
_ -> Nothing
-> any ( \ dc -> tc == promoteDataCon dc ) vecCountDataCons
_ -> False
getVecElemExpr :: Type -> Maybe EvExpr
getVecElemExpr ty = case splitTyConApp_maybe ty of
isFixedVecElem :: Type -> Bool
isFixedVecElem elt = case splitTyConApp_maybe elt of
Just (tc, [])
-> lookupInNullaryDataCons tc vecElemDataCons
_ -> Nothing
-> any ( \ dc -> tc == promoteDataCon dc ) vecElemDataCons
_ -> False
getRuntimeRepsExpr :: Type -> Maybe EvExpr
getRuntimeRepsExpr ty = case splitTyConApp_maybe ty of
isFixedRuntimeReps :: Type -> Bool
isFixedRuntimeReps rs = case splitTyConApp_maybe rs of
Just (tc, args)
| tc == promotedNilDataCon
, [_] <- args
-> Just $ mkNilExpr runtimeRepTy
-> True
| tc == promotedConsDataCon
, [_, rep, reps] <- args
-> ( \ r rs -> mkConsExpr runtimeRepTy r rs )
<$> getRuntimeRepExpr rep
<*> getRuntimeRepsExpr reps
_ -> Nothing
lookupInNullaryDataCons :: TyCon -> [DataCon] -> Maybe EvExpr
lookupInNullaryDataCons _ [] = Nothing
lookupInNullaryDataCons tc (dc:dcs)
| tc == promoteDataCon dc
= Just $ mkCoreConApps dc []
| otherwise
= lookupInNullaryDataCons tc dcs
-> isFixedRuntimeRep rep && isFixedRuntimeReps reps
_ -> False
{- ********************************************************************
* *
......
......@@ -39,7 +39,7 @@ import GHC.Types.Var.Set( delVarSetList, anyVarSet )
import GHC.Utils.Outputable
import GHC.Utils.Panic
import GHC.Utils.Panic.Plain
import GHC.Builtin.Types ( anyTypeOfKind )
import GHC.Builtin.Types ( anyTypeOfKind, fixedRuntimeRepClass )
import GHC.Types.Name.Set
import GHC.Types.Name.Reader
import GHC.Hs.Type( HsIPName(..) )
......@@ -205,6 +205,17 @@ canClass :: CtEvidence
-- Precondition: EvVar is class evidence
canClass ev cls tys pend_sc fds
-- SLD: phase 1 of FixedRuntimeRep
-- We don't allow a FixedRuntimeRep constraint to be rewritten.
| cls == fixedRuntimeRepClass
= return . ContinueWith $
CDictCan { cc_ev = ev
, cc_tyargs = tys
, cc_class = cls
, cc_pend_sc = False
, cc_fundeps = False
}
| otherwise
= -- all classes do *nominal* matching
assertPpr (ctEvRole ev == Nominal) (ppr ev $$ ppr cls $$ ppr tys) $
do { (xis, cos) <- rewriteArgsNom ev cls_tc tys
......@@ -3009,7 +3020,6 @@ rewriteEvidence ev@(CtWanted { ctev_dest = dest
, ctev_loc = loc }) new_pred co
= do { mb_new_ev <- newWanted_SI si loc new_pred
-- The "_SI" variant ensures that we make a new Wanted
-- with the same shadow-info as the existing one
-- with the same shadow-info as the existing one (#16735)
; massert (tcCoercionRole co == ctEvRole ev)
; setWantedEvTerm dest
......
......@@ -2011,7 +2011,8 @@ setWantedEq (EvVarDest ev) _ = pprPanic "setWantedEq" (ppr ev)
setWantedEvTerm :: TcEvDest -> EvTerm -> TcS ()
setWantedEvTerm (HoleDest hole) tm
| Just co <- evTermCoercion_maybe tm
= do { useVars (coVarsOfCo co)
= do { traceTcS "setWantedEvTerm, tm =" (ppr tm)
; useVars (coVarsOfCo co)
; fillCoercionHole hole co }
| otherwise
= -- See Note [Yukky eq_sel for a HoleDest]
......
......@@ -73,6 +73,7 @@ import GHC.Tc.Utils.TcType
import GHC.Core.Type
import GHC.Core.TyCon
import GHC.Core.DataCon ( DataCon, dataConWrapId )
import GHC.Core.Utils ( mkCoCast )
import GHC.Builtin.Names
import GHC.Types.Var.Env
import GHC.Types.Var.Set
......
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