{-# LANGUAGE BangPatterns #-}
{-# LANGUAGE BlockArguments #-}
{-# LANGUAGE CPP #-}
{-# LANGUAGE DerivingVia #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE NamedFieldPuns #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE TupleSections #-}
{-# LANGUAGE ViewPatterns #-}
module GHC.TcPlugin.API.Internal.Shim
( Reduction(..), mkReduction
, TcPluginSolveResult(TcPluginContradiction, TcPluginOk, ..), TcPluginRewriteResult(..)
, RewriteEnv(..)
, shimRewriter
)
where
import Prelude
hiding ( Floating(cos), iterate )
import Control.Monad
( forM, unless, when )
import Data.Foldable
( traverse_
#if !MIN_VERSION_ghc(9,2,0)
, foldlM
#endif
)
#if MIN_VERSION_ghc(9,2,0)
import Data.List.NonEmpty
( NonEmpty((:|)) )
#endif
import Data.Maybe
( fromMaybe )
import Control.Monad.Trans.Reader
( ReaderT(..) )
import Control.Monad.Trans.State.Strict
( StateT(..) )
import GHC.Core.Coercion
( coercionRole
, mkReflCo, mkSymCo
, mkAppCos, mkNomReflCo, mkSubCo
, mkTyConAppCo, tyConRolesX
, tyConRolesRepresentational
)
import GHC.Core.Predicate
( EqRel(..), eqRelRole )
import GHC.Core.TyCo.Rep
( Type(..), Kind, Coercion(..), MCoercion(..), TyCoBinder(..)
, isNamedBinder, mkTyVarTy
)
import GHC.Core.TyCon
( TyCon(..), TyConBinder, TyConBndrVis(..)
#if MIN_VERSION_ghc(9,2,0)
, isForgetfulSynTyCon
#endif
, isFamFreeTyCon, isTypeSynonymTyCon
, isTypeFamilyTyCon
, tyConBinders, tyConResKind
, tyConArity
)
import GHC.Core.Type
( TyVar
, tcView , mkTyConApp
#if MIN_VERSION_ghc(9,0,0)
, mkScaled, tymult
#endif
, coreView, tyVarKind
)
#if MIN_VERSION_ghc(9,2,0)
import GHC.Data.Maybe
( firstJustsM )
#endif
import GHC.Tc.Plugin
( newWanted, newDerived )
import GHC.Tc.Solver.Monad
( TcS
, zonkCo, zonkTcType
, isFilledMetaTyVar_maybe
, getInertEqs
, checkReductionDepth
, matchFam
, runTcPluginTcS, runTcSWithEvBinds
, traceTcS
, setWantedEvTerm
#if MIN_VERSION_ghc(9,2,0)
, lookupFamAppCache, lookupFamAppInert, extendFamAppCache
, pattern EqualCtList
#else
, lookupFlatCache, extendFlatCache
#endif
)
import GHC.Tc.Types
( TcPluginM
, unsafeTcPluginTcM, getEvBindsTcPluginM
)
import qualified GHC.Tc.Types as GHC
( TcPluginResult(..) )
import GHC.Tc.Types.Constraint
( Ct(..), CtEvidence(..)
, CtLoc, CtFlavour(..), CtFlavourRole, ShadowInfo(..)
#if MIN_VERSION_ghc(9,2,0)
, CanEqLHS(..)
#endif
, ctLoc, ctFlavour, ctEvidence, ctEqRel, ctEvPred
, ctEvExpr, ctEvCoercion, ctEvFlavour
, bumpCtLocDepth, eqCanRewriteFR, mkNonCanonical
)
import GHC.Tc.Types.Evidence
( EvTerm(..), Role(..)
, evCast, mkTcTransCo , mkTcTyConAppCo
)
import GHC.Tc.Utils.TcType
( TcTyCoVarSet
#if MIN_VERSION_ghc(9,2,0)
, tcSplitForAllTyVarBinders
#else
, tcSplitForAllVarBndrs
#endif
, tcSplitTyConApp_maybe
, tcTypeKind
, tyCoVarsOfType
)
import GHC.Types.Unique.FM
( UniqFM, lookupUFM, isNullUFM )
import GHC.Types.Var
( TcTyVar, VarBndr(..)
#if !MIN_VERSION_ghc(9,2,0)
, TyVarBinder
#endif
, updateTyVarKindM
)
import GHC.Types.Var.Env
( lookupDVarEnv )
import GHC.Types.Var.Set
( emptyVarSet )
import GHC.Utils.Misc
( dropList )
import GHC.Utils.Monad
( zipWith3M )
import GHC.Utils.Outputable
( Outputable(..), SDoc, empty )
import GHC.TcPlugin.API.Internal.Shim.Reduction
data RewriteEnv
= FE { RewriteEnv -> CtLoc
fe_loc :: !CtLoc
, RewriteEnv -> CtFlavour
fe_flavour :: !CtFlavour
, RewriteEnv -> EqRel
fe_eq_rel :: !EqRel
}
data TcPluginSolveResult
= TcPluginSolveResult
{
TcPluginSolveResult -> [Ct]
tcPluginInsolubleCts :: [Ct]
, TcPluginSolveResult -> [(EvTerm, Ct)]
tcPluginSolvedCts :: [(EvTerm, Ct)]
, TcPluginSolveResult -> [Ct]
tcPluginNewCts :: [Ct]
}
pattern TcPluginContradiction :: [Ct] -> TcPluginSolveResult
pattern $bTcPluginContradiction :: [Ct] -> TcPluginSolveResult
$mTcPluginContradiction :: forall r. TcPluginSolveResult -> ([Ct] -> r) -> (Void# -> r) -> r
TcPluginContradiction insols
= TcPluginSolveResult
{ tcPluginInsolubleCts = insols
, tcPluginSolvedCts = []
, tcPluginNewCts = [] }
pattern TcPluginOk :: [(EvTerm, Ct)] -> [Ct] -> TcPluginSolveResult
pattern $bTcPluginOk :: [(EvTerm, Ct)] -> [Ct] -> TcPluginSolveResult
$mTcPluginOk :: forall r.
TcPluginSolveResult
-> ([(EvTerm, Ct)] -> [Ct] -> r) -> (Void# -> r) -> r
TcPluginOk solved new
= TcPluginSolveResult
{ tcPluginInsolubleCts = []
, tcPluginSolvedCts = solved
, tcPluginNewCts = new }
adaptSolveResult :: Bool -> TcPluginSolveResult -> TcPluginM GHC.TcPluginResult
adaptSolveResult :: Bool -> TcPluginSolveResult -> TcPluginM TcPluginResult
adaptSolveResult Bool
doingGivens
( TcPluginSolveResult
{ tcPluginInsolubleCts :: TcPluginSolveResult -> [Ct]
tcPluginInsolubleCts = [Ct]
insols
, tcPluginSolvedCts :: TcPluginSolveResult -> [(EvTerm, Ct)]
tcPluginSolvedCts = [(EvTerm, Ct)]
solved
, tcPluginNewCts :: TcPluginSolveResult -> [Ct]
tcPluginNewCts = [Ct]
new
}
)
| [Ct] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Ct]
insols
= TcPluginResult -> TcPluginM TcPluginResult
forall (f :: * -> *) a. Applicative f => a -> f a
pure (TcPluginResult -> TcPluginM TcPluginResult)
-> TcPluginResult -> TcPluginM TcPluginResult
forall a b. (a -> b) -> a -> b
$ [(EvTerm, Ct)] -> [Ct] -> TcPluginResult
GHC.TcPluginOk [(EvTerm, Ct)]
solved [Ct]
new
| [(EvTerm, Ct)] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [(EvTerm, Ct)]
solved Bool -> Bool -> Bool
&& [Ct] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Ct]
new
= TcPluginResult -> TcPluginM TcPluginResult
forall (f :: * -> *) a. Applicative f => a -> f a
pure (TcPluginResult -> TcPluginM TcPluginResult)
-> TcPluginResult -> TcPluginM TcPluginResult
forall a b. (a -> b) -> a -> b
$ [Ct] -> TcPluginResult
GHC.TcPluginContradiction [Ct]
insols
| Bool
otherwise
= do
EvBindsVar
evBinds <- TcPluginM EvBindsVar
getEvBindsTcPluginM
TcM () -> TcPluginM ()
forall a. TcM a -> TcPluginM a
unsafeTcPluginTcM (TcM () -> TcPluginM ())
-> (TcS () -> TcM ()) -> TcS () -> TcPluginM ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. EvBindsVar -> TcS () -> TcM ()
forall a. EvBindsVar -> TcS a -> TcM a
runTcSWithEvBinds EvBindsVar
evBinds (TcS () -> TcPluginM ()) -> TcS () -> TcPluginM ()
forall a b. (a -> b) -> a -> b
$ do
Bool -> TcS () -> TcS ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless Bool
doingGivens (TcS () -> TcS ()) -> TcS () -> TcS ()
forall a b. (a -> b) -> a -> b
$ ((EvTerm, Ct) -> TcS ()) -> [(EvTerm, Ct)] -> TcS ()
forall (t :: * -> *) (f :: * -> *) a b.
(Foldable t, Applicative f) =>
(a -> f b) -> t a -> f ()
traverse_ ( (EvTerm -> Ct -> TcS ()) -> (EvTerm, Ct) -> TcS ()
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry EvTerm -> Ct -> TcS ()
setEv ) [(EvTerm, Ct)]
solved
TcPluginResult -> TcPluginM TcPluginResult
forall (f :: * -> *) a. Applicative f => a -> f a
pure (TcPluginResult -> TcPluginM TcPluginResult)
-> TcPluginResult -> TcPluginM TcPluginResult
forall a b. (a -> b) -> a -> b
$ [Ct] -> TcPluginResult
GHC.TcPluginContradiction [Ct]
insols
where
setEv :: EvTerm -> Ct -> TcS ()
setEv :: EvTerm -> Ct -> TcS ()
setEv EvTerm
ev ( Ct -> CtEvidence
ctEvidence -> CtWanted { ctev_dest :: CtEvidence -> TcEvDest
ctev_dest = TcEvDest
dest } )
= TcEvDest -> EvTerm -> TcS ()
setWantedEvTerm TcEvDest
dest EvTerm
ev
setEv EvTerm
_ Ct
_
= () -> TcS ()
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
data TcPluginRewriteResult
=
TcPluginNoRewrite
| TcPluginRewriteTo
{ TcPluginRewriteResult -> Reduction
tcPluginReduction :: !Reduction
, TcPluginRewriteResult -> [Ct]
tcRewriterWanteds :: [Ct]
}
type Rewriter = RewriteEnv -> [Ct] -> [Type] -> TcPluginM TcPluginRewriteResult
type Rewriters =
UniqFM
#if MIN_VERSION_ghc(9,0,0)
TyCon
#endif
Rewriter
shimRewriter :: [Ct] -> [Ct] -> [Ct]
-> Rewriters
-> ( [Ct] -> [Ct] -> [Ct] -> TcPluginM TcPluginSolveResult )
-> TcPluginM GHC.TcPluginResult
shimRewriter :: [Ct]
-> [Ct]
-> [Ct]
-> Rewriters
-> ([Ct] -> [Ct] -> [Ct] -> TcPluginM TcPluginSolveResult)
-> TcPluginM TcPluginResult
shimRewriter [Ct]
givens [Ct]
deriveds [Ct]
wanteds Rewriters
rws [Ct] -> [Ct] -> [Ct] -> TcPluginM TcPluginSolveResult
solver
| Rewriters -> Bool
forall elt. UniqFM elt -> Bool
isNullUFM Rewriters
rws
= Bool -> TcPluginSolveResult -> TcPluginM TcPluginResult
adaptSolveResult ([Ct] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Ct]
wanteds) (TcPluginSolveResult -> TcPluginM TcPluginResult)
-> TcPluginM TcPluginSolveResult -> TcPluginM TcPluginResult
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< [Ct] -> [Ct] -> [Ct] -> TcPluginM TcPluginSolveResult
solver [Ct]
givens [Ct]
deriveds [Ct]
wanteds
| Bool
otherwise
= do
TcPluginSolveResult
{ tcPluginInsolubleCts :: TcPluginSolveResult -> [Ct]
tcPluginInsolubleCts = [Ct]
contras
, tcPluginSolvedCts :: TcPluginSolveResult -> [(EvTerm, Ct)]
tcPluginSolvedCts = [(EvTerm, Ct)]
solved
, tcPluginNewCts :: TcPluginSolveResult -> [Ct]
tcPluginNewCts = [Ct]
new
} <- [Ct] -> [Ct] -> [Ct] -> TcPluginM TcPluginSolveResult
solver [Ct]
givens [Ct]
deriveds [Ct]
wanteds
( [Ct]
rewrittenDeriveds, [(EvTerm, Ct)]
solvedDeriveds, [Ct]
newCts1 ) <- (Ct -> TcPluginM (Maybe (Ct, (EvTerm, Ct)), [Ct]))
-> [Ct] -> TcPluginM ([Ct], [(EvTerm, Ct)], [Ct])
forall (m :: * -> *) a b c d.
Monad m =>
(a -> m (Maybe (b, c), [d])) -> [a] -> m ([b], [c], [d])
traverseCts ( Rewriters
-> [Ct] -> Ct -> TcPluginM (Maybe (Ct, (EvTerm, Ct)), [Ct])
reduceCt Rewriters
rws [Ct]
givens ) [Ct]
deriveds
( [Ct]
rewrittenWanteds , [(EvTerm, Ct)]
solvedWanteds , [Ct]
newCts2 ) <- (Ct -> TcPluginM (Maybe (Ct, (EvTerm, Ct)), [Ct]))
-> [Ct] -> TcPluginM ([Ct], [(EvTerm, Ct)], [Ct])
forall (m :: * -> *) a b c d.
Monad m =>
(a -> m (Maybe (b, c), [d])) -> [a] -> m ([b], [c], [d])
traverseCts ( Rewriters
-> [Ct] -> Ct -> TcPluginM (Maybe (Ct, (EvTerm, Ct)), [Ct])
reduceCt Rewriters
rws [Ct]
givens ) [Ct]
wanteds
Bool -> TcPluginSolveResult -> TcPluginM TcPluginResult
adaptSolveResult ([Ct] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Ct]
wanteds) (TcPluginSolveResult -> TcPluginM TcPluginResult)
-> TcPluginSolveResult -> TcPluginM TcPluginResult
forall a b. (a -> b) -> a -> b
$
TcPluginSolveResult :: [Ct] -> [(EvTerm, Ct)] -> [Ct] -> TcPluginSolveResult
TcPluginSolveResult
{ tcPluginInsolubleCts :: [Ct]
tcPluginInsolubleCts = [Ct]
contras
, tcPluginSolvedCts :: [(EvTerm, Ct)]
tcPluginSolvedCts = [(EvTerm, Ct)]
solved [(EvTerm, Ct)] -> [(EvTerm, Ct)] -> [(EvTerm, Ct)]
forall a. [a] -> [a] -> [a]
++ [(EvTerm, Ct)]
solvedDeriveds [(EvTerm, Ct)] -> [(EvTerm, Ct)] -> [(EvTerm, Ct)]
forall a. [a] -> [a] -> [a]
++ [(EvTerm, Ct)]
solvedWanteds
, tcPluginNewCts :: [Ct]
tcPluginNewCts = [Ct]
new [Ct] -> [Ct] -> [Ct]
forall a. [a] -> [a] -> [a]
++ [Ct]
newCts1 [Ct] -> [Ct] -> [Ct]
forall a. [a] -> [a] -> [a]
++ [Ct]
rewrittenDeriveds [Ct] -> [Ct] -> [Ct]
forall a. [a] -> [a] -> [a]
++ [Ct]
newCts2 [Ct] -> [Ct] -> [Ct]
forall a. [a] -> [a] -> [a]
++ [Ct]
rewrittenWanteds
}
reduceCt :: Rewriters
-> [Ct]
-> Ct
-> TcPluginM ( Maybe ( Ct, (EvTerm, Ct) ), [Ct] )
reduceCt :: Rewriters
-> [Ct] -> Ct -> TcPluginM (Maybe (Ct, (EvTerm, Ct)), [Ct])
reduceCt Rewriters
rws [Ct]
givens Ct
ct = do
let
predTy :: Type
predTy :: Type
predTy = CtEvidence -> Type
ctEvPred ( Ct -> CtEvidence
ctEvidence Ct
ct )
rwEnv :: RewriteEnv
rwEnv :: RewriteEnv
rwEnv = CtLoc -> CtFlavour -> EqRel -> RewriteEnv
FE ( Ct -> CtLoc
ctLoc Ct
ct ) ( Ct -> CtFlavour
ctFlavour Ct
ct ) ( Ct -> EqRel
ctEqRel Ct
ct )
shimRewriteEnv :: ShimRewriteEnv
shimRewriteEnv :: ShimRewriteEnv
shimRewriteEnv = Rewriters -> RewriteEnv -> [Ct] -> ShimRewriteEnv
ShimRewriteEnv Rewriters
rws RewriteEnv
rwEnv [Ct]
givens
( Maybe Reduction
res, [Ct]
newCts ) <- ShimRewriteEnv
-> RewriteM Reduction -> TcPluginM (Maybe Reduction, [Ct])
forall a. ShimRewriteEnv -> RewriteM a -> TcPluginM (Maybe a, [Ct])
runRewritePluginM ShimRewriteEnv
shimRewriteEnv ( Type -> RewriteM Reduction
rewrite_one Type
predTy )
case Maybe Reduction
res of
Maybe Reduction
Nothing -> (Maybe (Ct, (EvTerm, Ct)), [Ct])
-> TcPluginM (Maybe (Ct, (EvTerm, Ct)), [Ct])
forall (f :: * -> *) a. Applicative f => a -> f a
pure ( Maybe (Ct, (EvTerm, Ct))
forall a. Maybe a
Nothing, [Ct]
newCts )
Just ( Reduction Coercion
co Type
predTy' ) -> do
CtEvidence
ctEv' <- case Ct -> CtFlavour
ctFlavour Ct
ct of
CtFlavour
Given -> [Char] -> TcPluginM CtEvidence
forall a. HasCallStack => [Char] -> a
error [Char]
"ghc-tcplugin-api: unexpected Given in reduceCt"
Wanted {} -> CtLoc -> Type -> TcPluginM CtEvidence
newWanted ( Ct -> CtLoc
ctLoc Ct
ct ) Type
predTy'
CtFlavour
Derived -> CtLoc -> Type -> TcPluginM CtEvidence
newDerived ( Ct -> CtLoc
ctLoc Ct
ct ) Type
predTy'
let
role :: Role
role :: Role
role = Coercion -> Role
coercionRole Coercion
co
cast_co :: Coercion
cast_co :: Coercion
cast_co = Coercion -> Coercion
mkSymCo (Coercion -> Coercion) -> Coercion -> Coercion
forall a b. (a -> b) -> a -> b
$ case Role
role of
Role
Nominal -> Coercion -> Coercion
mkSubCo Coercion
co
Role
_ -> Coercion
co
(Maybe (Ct, (EvTerm, Ct)), [Ct])
-> TcPluginM (Maybe (Ct, (EvTerm, Ct)), [Ct])
forall (f :: * -> *) a. Applicative f => a -> f a
pure ( (Ct, (EvTerm, Ct)) -> Maybe (Ct, (EvTerm, Ct))
forall a. a -> Maybe a
Just
( CtEvidence -> Ct
mkNonCanonical CtEvidence
ctEv'
, ( EvExpr -> Coercion -> EvTerm
evCast ( CtEvidence -> EvExpr
ctEvExpr CtEvidence
ctEv' ) Coercion
cast_co, Ct
ct )
)
, [Ct]
newCts
)
traverseCts :: Monad m
=> ( a -> m ( Maybe (b, c), [d] ) )
-> [a]
-> m ( [b], [c], [d] )
traverseCts :: (a -> m (Maybe (b, c), [d])) -> [a] -> m ([b], [c], [d])
traverseCts a -> m (Maybe (b, c), [d])
_ [] = ([b], [c], [d]) -> m ([b], [c], [d])
forall (f :: * -> *) a. Applicative f => a -> f a
pure ( [], [], [] )
traverseCts a -> m (Maybe (b, c), [d])
f (a
a : [a]
as) = do
( Maybe (b, c)
mb_bc, [d]
ds ) <- a -> m (Maybe (b, c), [d])
f a
a
( [b]
bs, [c]
cs, [d]
dss ) <- (a -> m (Maybe (b, c), [d])) -> [a] -> m ([b], [c], [d])
forall (m :: * -> *) a b c d.
Monad m =>
(a -> m (Maybe (b, c), [d])) -> [a] -> m ([b], [c], [d])
traverseCts a -> m (Maybe (b, c), [d])
f [a]
as
case Maybe (b, c)
mb_bc of
Maybe (b, c)
Nothing -> ([b], [c], [d]) -> m ([b], [c], [d])
forall (f :: * -> *) a. Applicative f => a -> f a
pure ( [b]
bs, [c]
cs, [d]
ds [d] -> [d] -> [d]
forall a. [a] -> [a] -> [a]
++ [d]
dss )
Just (b
b,c
c) -> ([b], [c], [d]) -> m ([b], [c], [d])
forall (f :: * -> *) a. Applicative f => a -> f a
pure ( b
b b -> [b] -> [b]
forall a. a -> [a] -> [a]
: [b]
bs, c
c c -> [c] -> [c]
forall a. a -> [a] -> [a]
: [c]
cs, [d]
ds [d] -> [d] -> [d]
forall a. [a] -> [a] -> [a]
++ [d]
dss )
rewrite_one :: Type -> RewriteM Reduction
rewrite_one :: Type -> RewriteM Reduction
rewrite_one Type
ty
| Just Type
ty' <- Type -> Maybe Type
rewriterView Type
ty
= Type -> RewriteM Reduction
rewrite_one Type
ty'
rewrite_one xi :: Type
xi@(LitTy {})
= do { Role
role <- RewriteM Role
getRole
; Reduction -> RewriteM Reduction
forall (m :: * -> *) a. Monad m => a -> m a
return (Reduction -> RewriteM Reduction)
-> Reduction -> RewriteM Reduction
forall a b. (a -> b) -> a -> b
$ Role -> Type -> Reduction
mkReflRedn Role
role Type
xi }
rewrite_one (TyVarTy Var
tv)
= Var -> RewriteM Reduction
rewriteTyVar Var
tv
rewrite_one (AppTy Type
ty1 Type
ty2)
= Type -> [Type] -> RewriteM Reduction
rewrite_app_tys Type
ty1 [Type
ty2]
rewrite_one (TyConApp TyCon
tc [Type]
tys)
| TyCon -> Bool
isTypeFamilyTyCon TyCon
tc
= TyCon -> [Type] -> RewriteM Reduction
rewrite_fam_app TyCon
tc [Type]
tys
| Bool
otherwise
= TyCon -> [Type] -> RewriteM Reduction
rewrite_ty_con_app TyCon
tc [Type]
tys
rewrite_one
(FunTy
#if MIN_VERSION_ghc(8,10,0)
AnonArgFlag
vis
#endif
#if MIN_VERSION_ghc(9,0,0)
mult
#endif
Type
ty1
Type
ty2
)
= do { Reduction
arg_redn <- Type -> RewriteM Reduction
rewrite_one Type
ty1
; Reduction
res_redn <- Type -> RewriteM Reduction
rewrite_one Type
ty2
#if MIN_VERSION_ghc(9,0,0)
; w_redn <- setEqRel NomEq $ rewrite_one mult
#endif
; Role
role <- RewriteM Role
getRole
; Reduction -> RewriteM Reduction
forall (m :: * -> *) a. Monad m => a -> m a
return (Reduction -> RewriteM Reduction)
-> Reduction -> RewriteM Reduction
forall a b. (a -> b) -> a -> b
$
Role -> AnonArgFlag -> Reduction -> Reduction -> Reduction
mkFunRedn
Role
role
#if MIN_VERSION_ghc(8,10,0)
AnonArgFlag
vis
#endif
#if MIN_VERSION_ghc(9,0,0)
w_redn
#endif
Reduction
arg_redn
Reduction
res_redn
}
rewrite_one ty :: Type
ty@(ForAllTy {})
= do { let ([TyVarBinder]
bndrs, Type
rho) = Type -> ([TyVarBinder], Type)
tcSplitForAllTyVarBinders Type
ty
; Reduction
redn <- Type -> RewriteM Reduction
rewrite_one Type
rho
; Reduction -> RewriteM Reduction
forall (m :: * -> *) a. Monad m => a -> m a
return (Reduction -> RewriteM Reduction)
-> Reduction -> RewriteM Reduction
forall a b. (a -> b) -> a -> b
$ [TyVarBinder] -> Reduction -> Reduction
mkHomoForAllRedn [TyVarBinder]
bndrs Reduction
redn }
rewrite_one (CastTy Type
ty Coercion
g)
= do { Reduction
redn <- Type -> RewriteM Reduction
rewrite_one Type
ty
; Coercion
g' <- Coercion -> RewriteM Coercion
rewrite_co Coercion
g
; Role
role <- RewriteM Role
getRole
; Reduction -> RewriteM Reduction
forall (m :: * -> *) a. Monad m => a -> m a
return (Reduction -> RewriteM Reduction)
-> Reduction -> RewriteM Reduction
forall a b. (a -> b) -> a -> b
$ Role -> Type -> Coercion -> Reduction -> Reduction
mkCastRedn1 Role
role Type
ty Coercion
g' Reduction
redn }
rewrite_one (CoercionTy Coercion
co)
= do { Coercion
co' <- Coercion -> RewriteM Coercion
rewrite_co Coercion
co
; Role
role <- RewriteM Role
getRole
; Reduction -> RewriteM Reduction
forall (m :: * -> *) a. Monad m => a -> m a
return (Reduction -> RewriteM Reduction)
-> Reduction -> RewriteM Reduction
forall a b. (a -> b) -> a -> b
$ Role -> Coercion -> Reduction
mkReflCoRedn Role
role Coercion
co' }
rewrite_reduction :: Reduction -> RewriteM Reduction
rewrite_reduction :: Reduction -> RewriteM Reduction
rewrite_reduction (Reduction Coercion
co Type
xi) = do
Reduction
redn <- RewriteM Reduction -> RewriteM Reduction
forall a. RewriteM a -> RewriteM a
bumpDepth (RewriteM Reduction -> RewriteM Reduction)
-> RewriteM Reduction -> RewriteM Reduction
forall a b. (a -> b) -> a -> b
$ Type -> RewriteM Reduction
rewrite_one Type
xi
Reduction -> RewriteM Reduction
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Reduction -> RewriteM Reduction)
-> Reduction -> RewriteM Reduction
forall a b. (a -> b) -> a -> b
$ Coercion
co Coercion -> Reduction -> Reduction
`mkTransRedn` Reduction
redn
rewrite_app_tys :: Type -> [Type] -> RewriteM Reduction
rewrite_app_tys :: Type -> [Type] -> RewriteM Reduction
rewrite_app_tys (AppTy Type
ty1 Type
ty2) [Type]
tys = Type -> [Type] -> RewriteM Reduction
rewrite_app_tys Type
ty1 (Type
ty2Type -> [Type] -> [Type]
forall a. a -> [a] -> [a]
:[Type]
tys)
rewrite_app_tys Type
fun_ty [Type]
arg_tys
= do { Reduction
redn <- Type -> RewriteM Reduction
rewrite_one Type
fun_ty
; Reduction -> [Type] -> RewriteM Reduction
rewrite_app_ty_args Reduction
redn [Type]
arg_tys }
rewrite_app_ty_args :: Reduction -> [Type] -> RewriteM Reduction
rewrite_app_ty_args :: Reduction -> [Type] -> RewriteM Reduction
rewrite_app_ty_args Reduction
redn []
= Reduction -> RewriteM Reduction
forall (m :: * -> *) a. Monad m => a -> m a
return Reduction
redn
rewrite_app_ty_args fun_redn :: Reduction
fun_redn@(Reduction Coercion
fun_co Type
fun_xi) [Type]
arg_tys
= do { HetReduction
het_redn <- case HasCallStack => Type -> Maybe (TyCon, [Type])
Type -> Maybe (TyCon, [Type])
tcSplitTyConApp_maybe Type
fun_xi of
Just (TyCon
tc, [Type]
xis) ->
do { let tc_roles :: [Role]
tc_roles = TyCon -> [Role]
tyConRolesRepresentational TyCon
tc
arg_roles :: [Role]
arg_roles = [Type] -> [Role] -> [Role]
forall b a. [b] -> [a] -> [a]
dropList [Type]
xis [Role]
tc_roles
; ArgsReductions (Reductions [Coercion]
arg_cos [Type]
arg_xis) MCoercion
kind_co
<- Type -> [Role] -> [Type] -> RewriteM ArgsReductions
rewrite_vector (HasDebugCallStack => Type -> Type
Type -> Type
tcTypeKind Type
fun_xi) [Role]
arg_roles [Type]
arg_tys
; EqRel
eq_rel <- RewriteM EqRel
getEqRel
; let app_xi :: Type
app_xi = TyCon -> [Type] -> Type
mkTyConApp TyCon
tc ([Type]
xis [Type] -> [Type] -> [Type]
forall a. [a] -> [a] -> [a]
++ [Type]
arg_xis)
app_co :: Coercion
app_co = case EqRel
eq_rel of
EqRel
NomEq -> Coercion -> [Coercion] -> Coercion
mkAppCos Coercion
fun_co [Coercion]
arg_cos
EqRel
ReprEq -> Coercion -> [Coercion] -> Coercion
mkAppCos Coercion
fun_co ((Type -> Coercion) -> [Type] -> [Coercion]
forall a b. (a -> b) -> [a] -> [b]
map Type -> Coercion
mkNomReflCo [Type]
arg_tys)
Coercion -> Coercion -> Coercion
`mkTcTransCo`
Role -> TyCon -> [Coercion] -> Coercion
mkTcTyConAppCo Role
Representational TyCon
tc
((Role -> Type -> Coercion) -> [Role] -> [Type] -> [Coercion]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith Role -> Type -> Coercion
mkReflCo [Role]
tc_roles [Type]
xis [Coercion] -> [Coercion] -> [Coercion]
forall a. [a] -> [a] -> [a]
++ [Coercion]
arg_cos)
; HetReduction -> RewriteM HetReduction
forall (m :: * -> *) a. Monad m => a -> m a
return (HetReduction -> RewriteM HetReduction)
-> HetReduction -> RewriteM HetReduction
forall a b. (a -> b) -> a -> b
$
Reduction -> MCoercion -> HetReduction
mkHetReduction
(Coercion -> Type -> Reduction
mkReduction Coercion
app_co Type
app_xi )
MCoercion
kind_co }
Maybe (TyCon, [Type])
Nothing ->
do { ArgsReductions Reductions
redns MCoercion
kind_co
<- Type -> [Role] -> [Type] -> RewriteM ArgsReductions
rewrite_vector (HasDebugCallStack => Type -> Type
Type -> Type
tcTypeKind Type
fun_xi) (Role -> [Role]
forall a. a -> [a]
repeat Role
Nominal) [Type]
arg_tys
; HetReduction -> RewriteM HetReduction
forall (m :: * -> *) a. Monad m => a -> m a
return (HetReduction -> RewriteM HetReduction)
-> HetReduction -> RewriteM HetReduction
forall a b. (a -> b) -> a -> b
$ Reduction -> MCoercion -> HetReduction
mkHetReduction (Reduction -> Reductions -> Reduction
mkAppRedns Reduction
fun_redn Reductions
redns) MCoercion
kind_co }
; Role
role <- RewriteM Role
getRole
; Reduction -> RewriteM Reduction
forall (m :: * -> *) a. Monad m => a -> m a
return (Role -> HetReduction -> Reduction
homogeniseHetRedn Role
role HetReduction
het_redn) }
{-# INLINE rewrite_args_tc #-}
rewrite_args_tc :: TyCon -> Maybe [Role] -> [Type] -> RewriteM ArgsReductions
rewrite_args_tc :: TyCon -> Maybe [Role] -> [Type] -> RewriteM ArgsReductions
rewrite_args_tc TyCon
tc = [TyCoBinder]
-> Bool
-> Type
-> TcTyCoVarSet
-> Maybe [Role]
-> [Type]
-> RewriteM ArgsReductions
rewrite_args [TyCoBinder]
all_bndrs Bool
any_named_bndrs Type
inner_ki TcTyCoVarSet
emptyVarSet
where
([TyCoBinder]
bndrs, Bool
named)
= [TyConBinder] -> ([TyCoBinder], Bool)
ty_con_binders_ty_binders' (TyCon -> [TyConBinder]
tyConBinders TyCon
tc)
([TyCoBinder]
inner_bndrs, Type
inner_ki, Bool
inner_named) = Type -> ([TyCoBinder], Type, Bool)
split_pi_tys' (TyCon -> Type
tyConResKind TyCon
tc)
!all_bndrs :: [TyCoBinder]
all_bndrs = [TyCoBinder]
bndrs [TyCoBinder] -> [TyCoBinder] -> [TyCoBinder]
forall a. [a] -> [a] -> [a]
`chkAppend` [TyCoBinder]
inner_bndrs
!any_named_bndrs :: Bool
any_named_bndrs = Bool
named Bool -> Bool -> Bool
|| Bool
inner_named
rewrite_fam_app :: TyCon -> [Type] -> RewriteM Reduction
rewrite_fam_app :: TyCon -> [Type] -> RewriteM Reduction
rewrite_fam_app TyCon
tc [Type]
tys = do
let ([Type]
tys1, [Type]
tys_rest) = Int -> [Type] -> ([Type], [Type])
forall a. Int -> [a] -> ([a], [a])
splitAt (TyCon -> Int
tyConArity TyCon
tc) [Type]
tys
Reduction
redn <- TyCon -> [Type] -> RewriteM Reduction
rewrite_exact_fam_app TyCon
tc [Type]
tys1
Reduction -> [Type] -> RewriteM Reduction
rewrite_app_ty_args Reduction
redn [Type]
tys_rest
rewrite_exact_fam_app :: TyCon -> [Type] -> RewriteM Reduction
rewrite_exact_fam_app :: TyCon -> [Type] -> RewriteM Reduction
rewrite_exact_fam_app TyCon
tc [Type]
tys = do
Type -> RewriteM ()
checkStackDepth (Type -> RewriteM ()) -> Type -> RewriteM ()
forall a b. (a -> b) -> a -> b
$ TyCon -> [Type] -> Type
mkTyConApp TyCon
tc [Type]
tys
Rewriters
rws <- RewriteM Rewriters
getRewriters
let
mbRewriter :: Maybe Rewriter
mbRewriter :: Maybe Rewriter
mbRewriter = Rewriters -> TyCon -> Maybe Rewriter
forall key elt. Uniquable key => UniqFM elt -> key -> Maybe elt
lookupUFM Rewriters
rws TyCon
tc
Maybe Reduction
result1 <- TyCon -> [Type] -> Maybe Rewriter -> RewriteM (Maybe Reduction)
try_to_reduce TyCon
tc [Type]
tys Maybe Rewriter
mbRewriter
case Maybe Reduction
result1 of
Just Reduction
redn -> Bool -> Reduction -> RewriteM Reduction
finish Bool
False Reduction
redn
Maybe Reduction
_ -> do
EqRel
eq_rel <- RewriteM EqRel
getEqRel
ArgsReductions (Reductions [Coercion]
cos [Type]
xis) MCoercion
kind_co <-
if EqRel
eq_rel EqRel -> EqRel -> Bool
forall a. Eq a => a -> a -> Bool
== EqRel
NomEq
then TyCon -> Maybe [Role] -> [Type] -> RewriteM ArgsReductions
rewrite_args_tc TyCon
tc Maybe [Role]
forall a. Maybe a
Nothing [Type]
tys
else EqRel -> RewriteM ArgsReductions -> RewriteM ArgsReductions
forall a. EqRel -> RewriteM a -> RewriteM a
setEqRel EqRel
NomEq (RewriteM ArgsReductions -> RewriteM ArgsReductions)
-> RewriteM ArgsReductions -> RewriteM ArgsReductions
forall a b. (a -> b) -> a -> b
$
TyCon -> Maybe [Role] -> [Type] -> RewriteM ArgsReductions
rewrite_args_tc TyCon
tc Maybe [Role]
forall a. Maybe a
Nothing [Type]
tys
let
role :: Role
role = EqRel -> Role
eqRelRole EqRel
eq_rel
args_co :: Coercion
args_co = HasDebugCallStack => Role -> TyCon -> [Coercion] -> Coercion
Role -> TyCon -> [Coercion] -> Coercion
mkTyConAppCo Role
role TyCon
tc [Coercion]
cos
homogenise :: Reduction -> Reduction
homogenise :: Reduction -> Reduction
homogenise Reduction
redn
= Role -> HetReduction -> Reduction
homogeniseHetRedn Role
role
(HetReduction -> Reduction) -> HetReduction -> Reduction
forall a b. (a -> b) -> a -> b
$ Reduction -> MCoercion -> HetReduction
mkHetReduction
(Coercion
args_co Coercion -> Reduction -> Reduction
`mkTransRedn` Reduction
redn)
MCoercion
kind_co
give_up :: Reduction
give_up :: Reduction
give_up = Reduction -> Reduction
homogenise (Reduction -> Reduction) -> Reduction -> Reduction
forall a b. (a -> b) -> a -> b
$ Role -> Type -> Reduction
mkReflRedn Role
role (TyCon -> [Type] -> Type
mkTyConApp TyCon
tc [Type]
xis)
Maybe (Coercion, Type, CtFlavourRole)
result2 <- TcS (Maybe (Coercion, Type, CtFlavourRole))
-> RewriteM (Maybe (Coercion, Type, CtFlavourRole))
forall a. TcS a -> RewriteM a
liftTcS (TcS (Maybe (Coercion, Type, CtFlavourRole))
-> RewriteM (Maybe (Coercion, Type, CtFlavourRole)))
-> TcS (Maybe (Coercion, Type, CtFlavourRole))
-> RewriteM (Maybe (Coercion, Type, CtFlavourRole))
forall a b. (a -> b) -> a -> b
$ TyCon -> [Type] -> TcS (Maybe (Coercion, Type, CtFlavourRole))
lookupFamAppInert TyCon
tc [Type]
xis
CtFlavour
flavour <- RewriteM CtFlavour
getFlavour
case Maybe (Coercion, Type, CtFlavourRole)
result2 of
Just (Coercion
co, Type
xi, fr :: CtFlavourRole
fr@(CtFlavour
_, EqRel
inert_eq_rel))
| CtFlavourRole
fr CtFlavourRole -> CtFlavourRole -> Bool
`eqCanRewriteFR` (CtFlavour
flavour, EqRel
eq_rel)
, let
redn :: Reduction
redn :: Reduction
redn = Coercion -> Type -> Reduction
Reduction (Coercion -> Coercion
mkSymCo Coercion
co) Type
xi
-> Bool -> Reduction -> RewriteM Reduction
finish Bool
True (Reduction -> Reduction
homogenise (Reduction -> Reduction) -> Reduction -> Reduction
forall a b. (a -> b) -> a -> b
$ Role -> Role -> Reduction -> Reduction
downgradeRedn Role
role' Role
inert_role Reduction
redn)
where
inert_role :: Role
inert_role = EqRel -> Role
eqRelRole EqRel
inert_eq_rel
role' :: Role
role' = EqRel -> Role
eqRelRole EqRel
eq_rel
Maybe (Coercion, Type, CtFlavourRole)
_ -> do
Maybe Reduction
result3 <- TyCon -> [Type] -> Maybe Rewriter -> RewriteM (Maybe Reduction)
try_to_reduce TyCon
tc [Type]
xis Maybe Rewriter
mbRewriter
case Maybe Reduction
result3 of
Just Reduction
redn -> Bool -> Reduction -> RewriteM Reduction
finish Bool
True (Reduction -> Reduction
homogenise Reduction
redn)
Maybe Reduction
_ -> Reduction -> RewriteM Reduction
forall (m :: * -> *) a. Monad m => a -> m a
return Reduction
give_up
where
finish :: Bool -> Reduction -> RewriteM Reduction
finish :: Bool -> Reduction -> RewriteM Reduction
finish Bool
use_cache (Reduction Coercion
co Type
xi) = do
Reduction Coercion
fully_co Type
fully <- RewriteM Reduction -> RewriteM Reduction
forall a. RewriteM a -> RewriteM a
bumpDepth (RewriteM Reduction -> RewriteM Reduction)
-> RewriteM Reduction -> RewriteM Reduction
forall a b. (a -> b) -> a -> b
$ Type -> RewriteM Reduction
rewrite_one Type
xi
let final_redn :: Reduction
final_redn@(Reduction Coercion
final_co Type
final_xi) = Coercion -> Type -> Reduction
Reduction (Coercion
fully_co Coercion -> Coercion -> Coercion
`mkTcTransCo` Coercion
co) Type
fully
EqRel
eq_rel <- RewriteM EqRel
getEqRel
CtFlavour
flavour <- RewriteM CtFlavour
getFlavour
Bool -> RewriteM () -> RewriteM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Bool
use_cache Bool -> Bool -> Bool
&& EqRel
eq_rel EqRel -> EqRel -> Bool
forall a. Eq a => a -> a -> Bool
== EqRel
NomEq Bool -> Bool -> Bool
&& CtFlavour
flavour CtFlavour -> CtFlavour -> Bool
forall a. Eq a => a -> a -> Bool
/= CtFlavour
Derived) (RewriteM () -> RewriteM ()) -> RewriteM () -> RewriteM ()
forall a b. (a -> b) -> a -> b
$
TcS () -> RewriteM ()
forall a. TcS a -> RewriteM a
liftTcS (TcS () -> RewriteM ()) -> TcS () -> RewriteM ()
forall a b. (a -> b) -> a -> b
$
TyCon -> [Type] -> (Coercion, Type) -> CtFlavour -> TcS ()
extendFamAppCache TyCon
tc [Type]
tys
( Coercion -> Coercion
mkSymCo Coercion
final_co, Type
final_xi )
#if !MIN_VERSION_ghc(9,2,0)
CtFlavour
flavour
#endif
Reduction -> RewriteM Reduction
forall (m :: * -> *) a. Monad m => a -> m a
return Reduction
final_redn
{-# INLINE finish #-}
try_to_reduce :: TyCon -> [Type] -> Maybe Rewriter
-> RewriteM (Maybe Reduction)
try_to_reduce :: TyCon -> [Type] -> Maybe Rewriter -> RewriteM (Maybe Reduction)
try_to_reduce TyCon
tc [Type]
tys Maybe Rewriter
mb_rewriter = do
Maybe Reduction
result <-
[RewriteM (Maybe Reduction)] -> RewriteM (Maybe Reduction)
forall (m :: * -> *) (f :: * -> *) a.
(Monad m, Foldable f) =>
f (m (Maybe a)) -> m (Maybe a)
firstJustsM
[ Maybe Rewriter -> [Type] -> RewriteM (Maybe Reduction)
runTcPluginRewriter Maybe Rewriter
mb_rewriter [Type]
tys
, TcS (Maybe Reduction) -> RewriteM (Maybe Reduction)
forall a. TcS a -> RewriteM a
liftTcS (TcS (Maybe Reduction) -> RewriteM (Maybe Reduction))
-> TcS (Maybe Reduction) -> RewriteM (Maybe Reduction)
forall a b. (a -> b) -> a -> b
$ Maybe (Coercion, Type) -> Maybe Reduction
mkRed (Maybe (Coercion, Type) -> Maybe Reduction)
-> TcS (Maybe (Coercion, Type)) -> TcS (Maybe Reduction)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TyCon -> [Type] -> TcS (Maybe (Coercion, Type))
lookupFamAppCache TyCon
tc [Type]
tys
, TcS (Maybe Reduction) -> RewriteM (Maybe Reduction)
forall a. TcS a -> RewriteM a
liftTcS (TcS (Maybe Reduction) -> RewriteM (Maybe Reduction))
-> TcS (Maybe Reduction) -> RewriteM (Maybe Reduction)
forall a b. (a -> b) -> a -> b
$ Maybe (Coercion, Type) -> Maybe Reduction
mkRed (Maybe (Coercion, Type) -> Maybe Reduction)
-> TcS (Maybe (Coercion, Type)) -> TcS (Maybe Reduction)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TyCon -> [Type] -> TcS (Maybe (Coercion, Type))
matchFam TyCon
tc [Type]
tys ]
Maybe Reduction
-> (Reduction -> RewriteM Reduction) -> RewriteM (Maybe Reduction)
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM Maybe Reduction
result Reduction -> RewriteM Reduction
downgrade
where
mkRed :: Maybe (Coercion, Type) -> Maybe Reduction
mkRed :: Maybe (Coercion, Type) -> Maybe Reduction
mkRed = ((Coercion, Type) -> Reduction)
-> Maybe (Coercion, Type) -> Maybe Reduction
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (((Coercion, Type) -> Reduction)
-> Maybe (Coercion, Type) -> Maybe Reduction)
-> ((Coercion, Type) -> Reduction)
-> Maybe (Coercion, Type)
-> Maybe Reduction
forall a b. (a -> b) -> a -> b
$ (Coercion -> Type -> Reduction) -> (Coercion, Type) -> Reduction
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry Coercion -> Type -> Reduction
Reduction
downgrade :: Reduction -> RewriteM Reduction
downgrade :: Reduction -> RewriteM Reduction
downgrade redn :: Reduction
redn@(Reduction Coercion
co Type
xi) = do
EqRel
eq_rel <- RewriteM EqRel
getEqRel
case EqRel
eq_rel of
EqRel
NomEq -> Reduction -> RewriteM Reduction
forall (m :: * -> *) a. Monad m => a -> m a
return Reduction
redn
EqRel
ReprEq -> Reduction -> RewriteM Reduction
forall (m :: * -> *) a. Monad m => a -> m a
return (Reduction -> RewriteM Reduction)
-> Reduction -> RewriteM Reduction
forall a b. (a -> b) -> a -> b
$ Coercion -> Type -> Reduction
Reduction (Coercion -> Coercion
mkSubCo Coercion
co) Type
xi
runTcPluginRewriter :: Maybe Rewriter
-> [Type]
-> RewriteM (Maybe Reduction)
runTcPluginRewriter :: Maybe Rewriter -> [Type] -> RewriteM (Maybe Reduction)
runTcPluginRewriter Maybe Rewriter
mbRewriter [Type]
tys =
case Maybe Rewriter
mbRewriter of
Maybe Rewriter
Nothing -> Maybe Reduction -> RewriteM (Maybe Reduction)
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe Reduction
forall a. Maybe a
Nothing
Just Rewriter
rewriter -> do
[Char] -> SDoc -> RewriteM ()
traceRewriteM [Char]
"runTcPluginRewriter { " SDoc
empty
Maybe Reduction
res <- Rewriter -> RewriteM (Maybe Reduction)
runRewriter Rewriter
rewriter
[Char] -> SDoc -> RewriteM ()
traceRewriteM [Char]
"runTcPluginRewriter }" ( Maybe Reduction -> SDoc
forall a. Outputable a => a -> SDoc
ppr Maybe Reduction
res )
Maybe Reduction -> RewriteM (Maybe Reduction)
forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe Reduction
res
where
runRewriter :: Rewriter -> RewriteM (Maybe Reduction)
runRewriter :: Rewriter -> RewriteM (Maybe Reduction)
runRewriter Rewriter
rewriter = do
TcPluginRewriteResult
rewriteResult <- (ShimRewriteEnv
-> RewriteState -> TcS (TcPluginRewriteResult, RewriteState))
-> RewriteM TcPluginRewriteResult
forall a.
(ShimRewriteEnv -> RewriteState -> TcS (a, RewriteState))
-> RewriteM a
RewriteM \ ShimRewriteEnv
env RewriteState
s -> do
TcPluginRewriteResult
res <- TcPluginM TcPluginRewriteResult -> TcS TcPluginRewriteResult
forall a. TcPluginM a -> TcS a
runTcPluginTcS ( Rewriter
rewriter ( ShimRewriteEnv -> RewriteEnv
rewriteEnv ShimRewriteEnv
env ) ( ShimRewriteEnv -> [Ct]
rewriteGivens ShimRewriteEnv
env ) [Type]
tys )
(TcPluginRewriteResult, RewriteState)
-> TcS (TcPluginRewriteResult, RewriteState)
forall (f :: * -> *) a. Applicative f => a -> f a
pure ( TcPluginRewriteResult
res, RewriteState
s )
case TcPluginRewriteResult
rewriteResult of
TcPluginRewriteTo
{ tcPluginReduction :: TcPluginRewriteResult -> Reduction
tcPluginReduction = Reduction
redn
, tcRewriterWanteds :: TcPluginRewriteResult -> [Ct]
tcRewriterWanteds = [Ct]
wanteds
} -> Maybe Reduction -> [Ct] -> RewriteM (Maybe Reduction)
addRewriting ( Reduction -> Maybe Reduction
forall a. a -> Maybe a
Just Reduction
redn ) [Ct]
wanteds
TcPluginNoRewrite { }
-> Maybe Reduction -> [Ct] -> RewriteM (Maybe Reduction)
addRewriting Maybe Reduction
forall a. Maybe a
Nothing []
rewrite_ty_con_app :: TyCon -> [Type] -> RewriteM Reduction
rewrite_ty_con_app :: TyCon -> [Type] -> RewriteM Reduction
rewrite_ty_con_app TyCon
tc [Type]
tys
= do { Role
role <- RewriteM Role
getRole
; let m_roles :: Maybe [Role]
m_roles | Role
Nominal <- Role
role = Maybe [Role]
forall a. Maybe a
Nothing
| Bool
otherwise = [Role] -> Maybe [Role]
forall a. a -> Maybe a
Just ([Role] -> Maybe [Role]) -> [Role] -> Maybe [Role]
forall a b. (a -> b) -> a -> b
$ Role -> TyCon -> [Role]
tyConRolesX Role
role TyCon
tc
; ArgsReductions Reductions
redns MCoercion
kind_co <- TyCon -> Maybe [Role] -> [Type] -> RewriteM ArgsReductions
rewrite_args_tc TyCon
tc Maybe [Role]
m_roles [Type]
tys
; let tyconapp_redn :: HetReduction
tyconapp_redn
= Reduction -> MCoercion -> HetReduction
mkHetReduction
(Role -> TyCon -> Reductions -> Reduction
mkTyConAppRedn Role
role TyCon
tc Reductions
redns)
MCoercion
kind_co
; Reduction -> RewriteM Reduction
forall (m :: * -> *) a. Monad m => a -> m a
return (Reduction -> RewriteM Reduction)
-> Reduction -> RewriteM Reduction
forall a b. (a -> b) -> a -> b
$ Role -> HetReduction -> Reduction
homogeniseHetRedn Role
role HetReduction
tyconapp_redn }
rewrite_co :: Coercion -> RewriteM Coercion
rewrite_co :: Coercion -> RewriteM Coercion
rewrite_co Coercion
co = TcS Coercion -> RewriteM Coercion
forall a. TcS a -> RewriteM a
liftTcS (TcS Coercion -> RewriteM Coercion)
-> TcS Coercion -> RewriteM Coercion
forall a b. (a -> b) -> a -> b
$ Coercion -> TcS Coercion
zonkCo Coercion
co
rewriterView :: Type -> Maybe Type
rewriterView :: Type -> Maybe Type
rewriterView ty :: Type
ty@(TyConApp TyCon
tc [Type]
_)
| ( TyCon -> Bool
isTypeSynonymTyCon TyCon
tc Bool -> Bool -> Bool
&& Bool -> Bool
not (TyCon -> Bool
isFamFreeTyCon TyCon
tc) )
#if MIN_VERSION_ghc(9,2,0)
|| isForgetfulSynTyCon tc
#endif
= Type -> Maybe Type
tcView Type
ty
rewriterView Type
_other = Maybe Type
forall a. Maybe a
Nothing
rewriteTyVar :: TyVar -> RewriteM Reduction
rewriteTyVar :: Var -> RewriteM Reduction
rewriteTyVar Var
tv = do
RewriteTvResult
mb_yes <- Var -> RewriteM RewriteTvResult
rewrite_tyvar1 Var
tv
case RewriteTvResult
mb_yes of
RTRFollowed Reduction
redn -> Reduction -> RewriteM Reduction
rewrite_reduction Reduction
redn
RewriteTvResult
RTRNotFollowed -> do
Var
tv' <- TcS Var -> RewriteM Var
forall a. TcS a -> RewriteM a
liftTcS (TcS Var -> RewriteM Var) -> TcS Var -> RewriteM Var
forall a b. (a -> b) -> a -> b
$ (Type -> TcS Type) -> Var -> TcS Var
forall (m :: * -> *). Monad m => (Type -> m Type) -> Var -> m Var
updateTyVarKindM Type -> TcS Type
zonkTcType Var
tv
Role
role <- RewriteM Role
getRole
let ty' :: Type
ty' = Var -> Type
mkTyVarTy Var
tv'
Reduction -> RewriteM Reduction
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Reduction -> RewriteM Reduction)
-> Reduction -> RewriteM Reduction
forall a b. (a -> b) -> a -> b
$ Role -> Type -> Reduction
mkReflRedn Role
role Type
ty'
data RewriteTvResult
= RTRNotFollowed
| RTRFollowed !Reduction
rewrite_tyvar1 :: TcTyVar -> RewriteM RewriteTvResult
rewrite_tyvar1 :: Var -> RewriteM RewriteTvResult
rewrite_tyvar1 Var
tv = do
Maybe Type
mb_ty <- TcS (Maybe Type) -> RewriteM (Maybe Type)
forall a. TcS a -> RewriteM a
liftTcS (TcS (Maybe Type) -> RewriteM (Maybe Type))
-> TcS (Maybe Type) -> RewriteM (Maybe Type)
forall a b. (a -> b) -> a -> b
$ Var -> TcS (Maybe Type)
isFilledMetaTyVar_maybe Var
tv
case Maybe Type
mb_ty of
Just Type
ty -> do
Role
role <- RewriteM Role
getRole
RewriteTvResult -> RewriteM RewriteTvResult
forall (m :: * -> *) a. Monad m => a -> m a
return (RewriteTvResult -> RewriteM RewriteTvResult)
-> RewriteTvResult -> RewriteM RewriteTvResult
forall a b. (a -> b) -> a -> b
$ Reduction -> RewriteTvResult
RTRFollowed (Reduction -> RewriteTvResult) -> Reduction -> RewriteTvResult
forall a b. (a -> b) -> a -> b
$ Role -> Type -> Reduction
mkReflRedn Role
role Type
ty
Maybe Type
Nothing -> do
CtFlavourRole
fr <- RewriteM CtFlavourRole
getFlavourRole
Var -> CtFlavourRole -> RewriteM RewriteTvResult
rewrite_tyvar2 Var
tv CtFlavourRole
fr
rewrite_tyvar2 :: TcTyVar -> CtFlavourRole -> RewriteM RewriteTvResult
rewrite_tyvar2 :: Var -> CtFlavourRole -> RewriteM RewriteTvResult
rewrite_tyvar2 Var
tv fr :: CtFlavourRole
fr@(CtFlavour
_, EqRel
eq_rel) = do
DTyVarEnv [Ct]
ieqs <- TcS (DTyVarEnv [Ct]) -> RewriteM (DTyVarEnv [Ct])
forall a. TcS a -> RewriteM a
liftTcS (TcS (DTyVarEnv [Ct]) -> RewriteM (DTyVarEnv [Ct]))
-> TcS (DTyVarEnv [Ct]) -> RewriteM (DTyVarEnv [Ct])
forall a b. (a -> b) -> a -> b
$ TcS (DTyVarEnv [Ct])
getInertEqs
case DTyVarEnv [Ct] -> Var -> Maybe [Ct]
forall a. DVarEnv a -> Var -> Maybe a
lookupDVarEnv DTyVarEnv [Ct]
ieqs Var
tv of
#if MIN_VERSION_ghc(9,2,0)
Just (EqualCtList (ct :| _))
| CEqCan { cc_ev = ctev, cc_lhs = TyVarLHS {}
, cc_rhs = rhs_ty, cc_eq_rel = ct_eq_rel } <- ct
#else
Just (Ct
ct : [Ct]
_)
| CTyEqCan { cc_ev :: Ct -> CtEvidence
cc_ev = CtEvidence
ctev
, cc_rhs :: Ct -> Type
cc_rhs = Type
rhs_ty, cc_eq_rel :: Ct -> EqRel
cc_eq_rel = EqRel
ct_eq_rel } <- Ct
ct
#endif
, let ct_fr :: CtFlavourRole
ct_fr = (CtEvidence -> CtFlavour
ctEvFlavour CtEvidence
ctev, EqRel
ct_eq_rel)
, CtFlavourRole
ct_fr CtFlavourRole -> CtFlavourRole -> Bool
`eqCanRewriteFR` CtFlavourRole
fr
-> do
let rewriting_co1 :: Coercion
rewriting_co1 = HasDebugCallStack => CtEvidence -> Coercion
CtEvidence -> Coercion
ctEvCoercion CtEvidence
ctev
rewriting_co :: Coercion
rewriting_co = case (EqRel
ct_eq_rel, EqRel
eq_rel) of
(EqRel
ReprEq, EqRel
_rel) -> Coercion
rewriting_co1
(EqRel
NomEq, EqRel
NomEq) -> Coercion
rewriting_co1
(EqRel
NomEq, EqRel
ReprEq) -> Coercion -> Coercion
mkSubCo Coercion
rewriting_co1
RewriteTvResult -> RewriteM RewriteTvResult
forall (m :: * -> *) a. Monad m => a -> m a
return (RewriteTvResult -> RewriteM RewriteTvResult)
-> RewriteTvResult -> RewriteM RewriteTvResult
forall a b. (a -> b) -> a -> b
$ Reduction -> RewriteTvResult
RTRFollowed (Reduction -> RewriteTvResult) -> Reduction -> RewriteTvResult
forall a b. (a -> b) -> a -> b
$ Coercion -> Type -> Reduction
mkReduction Coercion
rewriting_co Type
rhs_ty
Maybe [Ct]
_other -> RewriteTvResult -> RewriteM RewriteTvResult
forall (m :: * -> *) a. Monad m => a -> m a
return RewriteTvResult
RTRNotFollowed
rewrite_vector :: Kind
-> [Role]
-> [Type]
-> RewriteM ArgsReductions
rewrite_vector :: Type -> [Role] -> [Type] -> RewriteM ArgsReductions
rewrite_vector Type
ki [Role]
roles [Type]
tys
= do { EqRel
eq_rel <- RewriteM EqRel
getEqRel
; let mb_roles :: Maybe [Role]
mb_roles = case EqRel
eq_rel of { EqRel
NomEq -> Maybe [Role]
forall a. Maybe a
Nothing; EqRel
ReprEq -> [Role] -> Maybe [Role]
forall a. a -> Maybe a
Just [Role]
roles }
; [TyCoBinder]
-> Bool
-> Type
-> TcTyCoVarSet
-> Maybe [Role]
-> [Type]
-> RewriteM ArgsReductions
rewrite_args [TyCoBinder]
bndrs Bool
any_named_bndrs Type
inner_ki TcTyCoVarSet
fvs Maybe [Role]
mb_roles [Type]
tys
}
where
([TyCoBinder]
bndrs, Type
inner_ki, Bool
any_named_bndrs) = Type -> ([TyCoBinder], Type, Bool)
split_pi_tys' Type
ki
fvs :: TcTyCoVarSet
fvs = Type -> TcTyCoVarSet
tyCoVarsOfType Type
ki
{-# INLINE rewrite_vector #-}
split_pi_tys' :: Type -> ([TyCoBinder], Type, Bool)
split_pi_tys' :: Type -> ([TyCoBinder], Type, Bool)
split_pi_tys' Type
ty = Type -> Type -> ([TyCoBinder], Type, Bool)
split Type
ty Type
ty
where
split :: Type -> Type -> ([TyCoBinder], Type, Bool)
split Type
_ (ForAllTy TyVarBinder
b Type
res) =
let !([TyCoBinder]
bs, Type
ty', Bool
_) = Type -> Type -> ([TyCoBinder], Type, Bool)
split Type
res Type
res
in (TyVarBinder -> TyCoBinder
Named TyVarBinder
b TyCoBinder -> [TyCoBinder] -> [TyCoBinder]
forall a. a -> [a] -> [a]
: [TyCoBinder]
bs, Type
ty', Bool
True)
split Type
_
(FunTy
#if MIN_VERSION_ghc(8,10,0)
AnonArgFlag
af
#endif
#if MIN_VERSION_ghc(9,0,0)
w
#endif
Type
arg
Type
res
) =
let !([TyCoBinder]
bs, Type
ty', Bool
named) = Type -> Type -> ([TyCoBinder], Type, Bool)
split Type
res Type
res
in ( AnonArgFlag -> Type -> TyCoBinder
Anon
#if MIN_VERSION_ghc(8,10,0)
AnonArgFlag
af
#endif
#if MIN_VERSION_ghc(9,0,0)
(mkScaled w arg)
#else
Type
arg
#endif
TyCoBinder -> [TyCoBinder] -> [TyCoBinder]
forall a. a -> [a] -> [a]
: [TyCoBinder]
bs
, Type
ty', Bool
named
)
split Type
orig_ty Type
ty' | Just Type
ty'' <- Type -> Maybe Type
coreView Type
ty' = Type -> Type -> ([TyCoBinder], Type, Bool)
split Type
orig_ty Type
ty''
split Type
orig_ty Type
_ = ([], Type
orig_ty, Bool
False)
{-# INLINE split_pi_tys' #-}
ty_con_binders_ty_binders' :: [TyConBinder] -> ([TyCoBinder], Bool)
ty_con_binders_ty_binders' :: [TyConBinder] -> ([TyCoBinder], Bool)
ty_con_binders_ty_binders' = (TyConBinder -> ([TyCoBinder], Bool) -> ([TyCoBinder], Bool))
-> ([TyCoBinder], Bool) -> [TyConBinder] -> ([TyCoBinder], Bool)
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr TyConBinder -> ([TyCoBinder], Bool) -> ([TyCoBinder], Bool)
go ([], Bool
False)
where
go :: TyConBinder -> ([TyCoBinder], Bool) -> ([TyCoBinder], Bool)
go (Bndr Var
tv (NamedTCB ArgFlag
vis)) ([TyCoBinder]
bndrs, Bool
_)
= (TyVarBinder -> TyCoBinder
Named (Var -> ArgFlag -> TyVarBinder
forall var argf. var -> argf -> VarBndr var argf
Bndr Var
tv ArgFlag
vis) TyCoBinder -> [TyCoBinder] -> [TyCoBinder]
forall a. a -> [a] -> [a]
: [TyCoBinder]
bndrs, Bool
True)
go (Bndr Var
tv
(AnonTCB
#if MIN_VERSION_ghc(8,10,0)
AnonArgFlag
af
#endif
)
) ([TyCoBinder]
bndrs, Bool
n)
= (AnonArgFlag -> Type -> TyCoBinder
Anon
#if MIN_VERSION_ghc(8,10,0)
AnonArgFlag
af
#endif
(
#if MIN_VERSION_ghc(9,0,0)
tymult
#endif
(Var -> Type
tyVarKind Var
tv)
)
TyCoBinder -> [TyCoBinder] -> [TyCoBinder]
forall a. a -> [a] -> [a]
: [TyCoBinder]
bndrs
, Bool
n)
{-# INLINE go #-}
{-# INLINE ty_con_binders_ty_binders' #-}
{-# INLINE rewrite_args #-}
rewrite_args :: [TyCoBinder] -> Bool
-> Kind -> TcTyCoVarSet
-> Maybe [Role] -> [Type]
-> RewriteM ArgsReductions
rewrite_args :: [TyCoBinder]
-> Bool
-> Type
-> TcTyCoVarSet
-> Maybe [Role]
-> [Type]
-> RewriteM ArgsReductions
rewrite_args [TyCoBinder]
orig_binders
Bool
any_named_bndrs
Type
orig_inner_ki
TcTyCoVarSet
orig_fvs
Maybe [Role]
orig_m_roles
[Type]
orig_tys
= case (Maybe [Role]
orig_m_roles, Bool
any_named_bndrs) of
(Maybe [Role]
Nothing, Bool
False) -> [Type] -> RewriteM ArgsReductions
rewrite_args_fast [Type]
orig_tys
(Maybe [Role], Bool)
_ -> [TyCoBinder]
-> Type
-> TcTyCoVarSet
-> [Role]
-> [Type]
-> RewriteM ArgsReductions
rewrite_args_slow [TyCoBinder]
orig_binders Type
orig_inner_ki TcTyCoVarSet
orig_fvs [Role]
orig_roles [Type]
orig_tys
where orig_roles :: [Role]
orig_roles = [Role] -> Maybe [Role] -> [Role]
forall a. a -> Maybe a -> a
fromMaybe (Role -> [Role]
forall a. a -> [a]
repeat Role
Nominal) Maybe [Role]
orig_m_roles
{-# INLINE rewrite_args_fast #-}
rewrite_args_fast :: [Type] -> RewriteM ArgsReductions
rewrite_args_fast :: [Type] -> RewriteM ArgsReductions
rewrite_args_fast [Type]
orig_tys
= (Reductions -> ArgsReductions)
-> RewriteM Reductions -> RewriteM ArgsReductions
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Reductions -> ArgsReductions
finish ([Type] -> RewriteM Reductions
iterate [Type]
orig_tys)
where
iterate :: [Type] -> RewriteM Reductions
iterate :: [Type] -> RewriteM Reductions
iterate (Type
ty : [Type]
tys) = do
Reduction Coercion
co Type
xi <- Type -> RewriteM Reduction
rewrite_one Type
ty
Reductions [Coercion]
cos [Type]
xis <- [Type] -> RewriteM Reductions
iterate [Type]
tys
Reductions -> RewriteM Reductions
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Reductions -> RewriteM Reductions)
-> Reductions -> RewriteM Reductions
forall a b. (a -> b) -> a -> b
$ [Coercion] -> [Type] -> Reductions
Reductions (Coercion
co Coercion -> [Coercion] -> [Coercion]
forall a. a -> [a] -> [a]
: [Coercion]
cos) (Type
xi Type -> [Type] -> [Type]
forall a. a -> [a] -> [a]
: [Type]
xis)
iterate [] = Reductions -> RewriteM Reductions
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Reductions -> RewriteM Reductions)
-> Reductions -> RewriteM Reductions
forall a b. (a -> b) -> a -> b
$ [Coercion] -> [Type] -> Reductions
Reductions [] []
{-# INLINE finish #-}
finish :: Reductions -> ArgsReductions
finish :: Reductions -> ArgsReductions
finish Reductions
redns = Reductions -> MCoercion -> ArgsReductions
ArgsReductions Reductions
redns MCoercion
MRefl
{-# INLINE rewrite_args_slow #-}
rewrite_args_slow :: [TyCoBinder] -> Kind -> TcTyCoVarSet
-> [Role] -> [Type]
-> RewriteM ArgsReductions
rewrite_args_slow :: [TyCoBinder]
-> Type
-> TcTyCoVarSet
-> [Role]
-> [Type]
-> RewriteM ArgsReductions
rewrite_args_slow [TyCoBinder]
binders Type
inner_ki TcTyCoVarSet
fvs [Role]
roles [Type]
tys
= do { [Reduction]
rewritten_args <- (Bool -> Role -> Type -> RewriteM Reduction)
-> [Bool] -> [Role] -> [Type] -> RewriteM [Reduction]
forall (m :: * -> *) a b c d.
Monad m =>
(a -> b -> c -> m d) -> [a] -> [b] -> [c] -> m [d]
zipWith3M Bool -> Role -> Type -> RewriteM Reduction
fl ((TyCoBinder -> Bool) -> [TyCoBinder] -> [Bool]
forall a b. (a -> b) -> [a] -> [b]
map TyCoBinder -> Bool
isNamedBinder [TyCoBinder]
binders [Bool] -> [Bool] -> [Bool]
forall a. [a] -> [a] -> [a]
++ Bool -> [Bool]
forall a. a -> [a]
repeat Bool
True)
[Role]
roles [Type]
tys
; ArgsReductions -> RewriteM ArgsReductions
forall (m :: * -> *) a. Monad m => a -> m a
return (ArgsReductions -> RewriteM ArgsReductions)
-> ArgsReductions -> RewriteM ArgsReductions
forall a b. (a -> b) -> a -> b
$ [TyCoBinder]
-> Type -> TcTyCoVarSet -> [Role] -> [Reduction] -> ArgsReductions
simplifyArgsWorker [TyCoBinder]
binders Type
inner_ki TcTyCoVarSet
fvs [Role]
roles [Reduction]
rewritten_args }
where
{-# INLINE fl #-}
fl :: Bool
-> Role -> Type -> RewriteM Reduction
fl :: Bool -> Role -> Type -> RewriteM Reduction
fl Bool
True Role
r Type
ty = RewriteM Reduction -> RewriteM Reduction
forall a. RewriteM a -> RewriteM a
noBogusCoercions (RewriteM Reduction -> RewriteM Reduction)
-> RewriteM Reduction -> RewriteM Reduction
forall a b. (a -> b) -> a -> b
$ Role -> Type -> RewriteM Reduction
fl1 Role
r Type
ty
fl Bool
False Role
r Type
ty = Role -> Type -> RewriteM Reduction
fl1 Role
r Type
ty
{-# INLINE fl1 #-}
fl1 :: Role -> Type -> RewriteM Reduction
fl1 :: Role -> Type -> RewriteM Reduction
fl1 Role
Nominal Type
ty
= EqRel -> RewriteM Reduction -> RewriteM Reduction
forall a. EqRel -> RewriteM a -> RewriteM a
setEqRel EqRel
NomEq (RewriteM Reduction -> RewriteM Reduction)
-> RewriteM Reduction -> RewriteM Reduction
forall a b. (a -> b) -> a -> b
$
Type -> RewriteM Reduction
rewrite_one Type
ty
fl1 Role
Representational Type
ty
= EqRel -> RewriteM Reduction -> RewriteM Reduction
forall a. EqRel -> RewriteM a -> RewriteM a
setEqRel EqRel
ReprEq (RewriteM Reduction -> RewriteM Reduction)
-> RewriteM Reduction -> RewriteM Reduction
forall a b. (a -> b) -> a -> b
$
Type -> RewriteM Reduction
rewrite_one Type
ty
fl1 Role
Phantom Type
ty
= do { Type
ty' <- TcS Type -> RewriteM Type
forall a. TcS a -> RewriteM a
liftTcS (TcS Type -> RewriteM Type) -> TcS Type -> RewriteM Type
forall a b. (a -> b) -> a -> b
$ Type -> TcS Type
zonkTcType Type
ty
; Reduction -> RewriteM Reduction
forall (m :: * -> *) a. Monad m => a -> m a
return (Reduction -> RewriteM Reduction)
-> Reduction -> RewriteM Reduction
forall a b. (a -> b) -> a -> b
$ Role -> Type -> Reduction
mkReflRedn Role
Phantom Type
ty' }
noBogusCoercions :: RewriteM a -> RewriteM a
noBogusCoercions :: RewriteM a -> RewriteM a
noBogusCoercions RewriteM a
thing_inside
= (ShimRewriteEnv -> RewriteState -> TcS (a, RewriteState))
-> RewriteM a
forall a.
(ShimRewriteEnv -> RewriteState -> TcS (a, RewriteState))
-> RewriteM a
RewriteM \ ShimRewriteEnv
env RewriteState
s ->
let !renv :: RewriteEnv
renv = ShimRewriteEnv -> RewriteEnv
rewriteEnv ShimRewriteEnv
env
!renv' :: RewriteEnv
renv' = case RewriteEnv -> CtFlavour
fe_flavour RewriteEnv
renv of
CtFlavour
Derived -> RewriteEnv
renv { fe_flavour :: CtFlavour
fe_flavour = ShadowInfo -> CtFlavour
Wanted ShadowInfo
WDeriv }
CtFlavour
_ -> RewriteEnv
renv
!env' :: ShimRewriteEnv
env' = ShimRewriteEnv
env { rewriteEnv :: RewriteEnv
rewriteEnv = RewriteEnv
renv' }
in
RewriteM a
-> ShimRewriteEnv -> RewriteState -> TcS (a, RewriteState)
forall a.
RewriteM a
-> ShimRewriteEnv -> RewriteState -> TcS (a, RewriteState)
runRewriteM RewriteM a
thing_inside ShimRewriteEnv
env' RewriteState
s
chkAppend :: [a] -> [a] -> [a]
chkAppend :: [a] -> [a] -> [a]
chkAppend [a]
xs [a]
ys
| [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [a]
ys = [a]
xs
| Bool
otherwise = [a]
xs [a] -> [a] -> [a]
forall a. [a] -> [a] -> [a]
++ [a]
ys
data ReduceQ = NoReduction | DidReduce
instance Semigroup ReduceQ where
ReduceQ
NoReduction <> :: ReduceQ -> ReduceQ -> ReduceQ
<> ReduceQ
NoReduction = ReduceQ
NoReduction
ReduceQ
_ <> ReduceQ
_ = ReduceQ
DidReduce
instance Monoid ReduceQ where
mempty :: ReduceQ
mempty = ReduceQ
NoReduction
data RewriteState =
RewriteState
{ RewriteState -> [Ct]
rewrittenCts :: ![ Ct ]
, RewriteState -> ReduceQ
reductionOccurred :: !ReduceQ
}
data ShimRewriteEnv
= ShimRewriteEnv
{ ShimRewriteEnv -> Rewriters
rewriters :: !Rewriters
, ShimRewriteEnv -> RewriteEnv
rewriteEnv :: !RewriteEnv
, ShimRewriteEnv -> [Ct]
rewriteGivens :: ![ Ct ]
}
newtype RewriteM a
= RewriteM
{ RewriteM a
-> ShimRewriteEnv -> RewriteState -> TcS (a, RewriteState)
runRewriteM
:: ShimRewriteEnv
-> RewriteState
-> TcS ( a, RewriteState )
}
deriving ( a -> RewriteM b -> RewriteM a
(a -> b) -> RewriteM a -> RewriteM b
(forall a b. (a -> b) -> RewriteM a -> RewriteM b)
-> (forall a b. a -> RewriteM b -> RewriteM a) -> Functor RewriteM
forall a b. a -> RewriteM b -> RewriteM a
forall a b. (a -> b) -> RewriteM a -> RewriteM b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
<$ :: a -> RewriteM b -> RewriteM a
$c<$ :: forall a b. a -> RewriteM b -> RewriteM a
fmap :: (a -> b) -> RewriteM a -> RewriteM b
$cfmap :: forall a b. (a -> b) -> RewriteM a -> RewriteM b
Functor, Functor RewriteM
a -> RewriteM a
Functor RewriteM
-> (forall a. a -> RewriteM a)
-> (forall a b. RewriteM (a -> b) -> RewriteM a -> RewriteM b)
-> (forall a b c.
(a -> b -> c) -> RewriteM a -> RewriteM b -> RewriteM c)
-> (forall a b. RewriteM a -> RewriteM b -> RewriteM b)
-> (forall a b. RewriteM a -> RewriteM b -> RewriteM a)
-> Applicative RewriteM
RewriteM a -> RewriteM b -> RewriteM b
RewriteM a -> RewriteM b -> RewriteM a
RewriteM (a -> b) -> RewriteM a -> RewriteM b
(a -> b -> c) -> RewriteM a -> RewriteM b -> RewriteM c
forall a. a -> RewriteM a
forall a b. RewriteM a -> RewriteM b -> RewriteM a
forall a b. RewriteM a -> RewriteM b -> RewriteM b
forall a b. RewriteM (a -> b) -> RewriteM a -> RewriteM b
forall a b c.
(a -> b -> c) -> RewriteM a -> RewriteM b -> RewriteM c
forall (f :: * -> *).
Functor f
-> (forall a. a -> f a)
-> (forall a b. f (a -> b) -> f a -> f b)
-> (forall a b c. (a -> b -> c) -> f a -> f b -> f c)
-> (forall a b. f a -> f b -> f b)
-> (forall a b. f a -> f b -> f a)
-> Applicative f
<* :: RewriteM a -> RewriteM b -> RewriteM a
$c<* :: forall a b. RewriteM a -> RewriteM b -> RewriteM a
*> :: RewriteM a -> RewriteM b -> RewriteM b
$c*> :: forall a b. RewriteM a -> RewriteM b -> RewriteM b
liftA2 :: (a -> b -> c) -> RewriteM a -> RewriteM b -> RewriteM c
$cliftA2 :: forall a b c.
(a -> b -> c) -> RewriteM a -> RewriteM b -> RewriteM c
<*> :: RewriteM (a -> b) -> RewriteM a -> RewriteM b
$c<*> :: forall a b. RewriteM (a -> b) -> RewriteM a -> RewriteM b
pure :: a -> RewriteM a
$cpure :: forall a. a -> RewriteM a
$cp1Applicative :: Functor RewriteM
Applicative, Applicative RewriteM
a -> RewriteM a
Applicative RewriteM
-> (forall a b. RewriteM a -> (a -> RewriteM b) -> RewriteM b)
-> (forall a b. RewriteM a -> RewriteM b -> RewriteM b)
-> (forall a. a -> RewriteM a)
-> Monad RewriteM
RewriteM a -> (a -> RewriteM b) -> RewriteM b
RewriteM a -> RewriteM b -> RewriteM b
forall a. a -> RewriteM a
forall a b. RewriteM a -> RewriteM b -> RewriteM b
forall a b. RewriteM a -> (a -> RewriteM b) -> RewriteM b
forall (m :: * -> *).
Applicative m
-> (forall a b. m a -> (a -> m b) -> m b)
-> (forall a b. m a -> m b -> m b)
-> (forall a. a -> m a)
-> Monad m
return :: a -> RewriteM a
$creturn :: forall a. a -> RewriteM a
>> :: RewriteM a -> RewriteM b -> RewriteM b
$c>> :: forall a b. RewriteM a -> RewriteM b -> RewriteM b
>>= :: RewriteM a -> (a -> RewriteM b) -> RewriteM b
$c>>= :: forall a b. RewriteM a -> (a -> RewriteM b) -> RewriteM b
$cp1Monad :: Applicative RewriteM
Monad )
via ( ReaderT ShimRewriteEnv
( StateT RewriteState TcS )
)
runRewritePluginM :: ShimRewriteEnv
-> RewriteM a
-> TcPluginM ( Maybe a, [Ct] )
runRewritePluginM :: ShimRewriteEnv -> RewriteM a -> TcPluginM (Maybe a, [Ct])
runRewritePluginM ShimRewriteEnv
env ( RewriteM { runRewriteM :: forall a.
RewriteM a
-> ShimRewriteEnv -> RewriteState -> TcS (a, RewriteState)
runRewriteM = ShimRewriteEnv -> RewriteState -> TcS (a, RewriteState)
run } ) = do
EvBindsVar
evBindsVar <- TcPluginM EvBindsVar
getEvBindsTcPluginM
( a
a, RewriteState { [Ct]
rewrittenCts :: [Ct]
rewrittenCts :: RewriteState -> [Ct]
rewrittenCts, ReduceQ
reductionOccurred :: ReduceQ
reductionOccurred :: RewriteState -> ReduceQ
reductionOccurred } )
<- TcM (a, RewriteState) -> TcPluginM (a, RewriteState)
forall a. TcM a -> TcPluginM a
unsafeTcPluginTcM
(TcM (a, RewriteState) -> TcPluginM (a, RewriteState))
-> TcM (a, RewriteState) -> TcPluginM (a, RewriteState)
forall a b. (a -> b) -> a -> b
$ EvBindsVar -> TcS (a, RewriteState) -> TcM (a, RewriteState)
forall a. EvBindsVar -> TcS a -> TcM a
runTcSWithEvBinds EvBindsVar
evBindsVar
(TcS (a, RewriteState) -> TcM (a, RewriteState))
-> TcS (a, RewriteState) -> TcM (a, RewriteState)
forall a b. (a -> b) -> a -> b
$ ShimRewriteEnv -> RewriteState -> TcS (a, RewriteState)
run ShimRewriteEnv
env ( [Ct] -> ReduceQ -> RewriteState
RewriteState [] ReduceQ
NoReduction )
let
mb_a :: Maybe a
mb_a = case ReduceQ
reductionOccurred of
ReduceQ
NoReduction -> Maybe a
forall a. Maybe a
Nothing
ReduceQ
DidReduce -> a -> Maybe a
forall a. a -> Maybe a
Just a
a
(Maybe a, [Ct]) -> TcPluginM (Maybe a, [Ct])
forall (f :: * -> *) a. Applicative f => a -> f a
pure ( Maybe a
mb_a, [Ct]
rewrittenCts )
addRewriting :: Maybe Reduction -> [Ct] -> RewriteM ( Maybe Reduction )
addRewriting :: Maybe Reduction -> [Ct] -> RewriteM (Maybe Reduction)
addRewriting Maybe Reduction
mbRedn [Ct]
newCts = (ShimRewriteEnv
-> RewriteState -> TcS (Maybe Reduction, RewriteState))
-> RewriteM (Maybe Reduction)
forall a.
(ShimRewriteEnv -> RewriteState -> TcS (a, RewriteState))
-> RewriteM a
RewriteM \ ShimRewriteEnv
_ ( RewriteState [Ct]
cts ReduceQ
s ) ->
let
s' :: ReduceQ
s' :: ReduceQ
s'
| Just Reduction
_ <- Maybe Reduction
mbRedn
= ReduceQ
DidReduce
| Bool
otherwise
= ReduceQ
s
in (Maybe Reduction, RewriteState)
-> TcS (Maybe Reduction, RewriteState)
forall (f :: * -> *) a. Applicative f => a -> f a
pure ( Maybe Reduction
mbRedn , [Ct] -> ReduceQ -> RewriteState
RewriteState ( [Ct]
cts [Ct] -> [Ct] -> [Ct]
forall a. Semigroup a => a -> a -> a
<> [Ct]
newCts ) ReduceQ
s' )
getRewriters :: RewriteM Rewriters
getRewriters :: RewriteM Rewriters
getRewriters = (ShimRewriteEnv -> RewriteState -> TcS (Rewriters, RewriteState))
-> RewriteM Rewriters
forall a.
(ShimRewriteEnv -> RewriteState -> TcS (a, RewriteState))
-> RewriteM a
RewriteM \ ShimRewriteEnv
env RewriteState
s -> (Rewriters, RewriteState) -> TcS (Rewriters, RewriteState)
forall (f :: * -> *) a. Applicative f => a -> f a
pure ( ShimRewriteEnv -> Rewriters
rewriters ShimRewriteEnv
env, RewriteState
s )
getRewriteEnvField :: (RewriteEnv -> a) -> RewriteM a
getRewriteEnvField :: (RewriteEnv -> a) -> RewriteM a
getRewriteEnvField RewriteEnv -> a
accessor = (ShimRewriteEnv -> RewriteState -> TcS (a, RewriteState))
-> RewriteM a
forall a.
(ShimRewriteEnv -> RewriteState -> TcS (a, RewriteState))
-> RewriteM a
RewriteM \ ShimRewriteEnv
env RewriteState
s ->
(a, RewriteState) -> TcS (a, RewriteState)
forall (f :: * -> *) a. Applicative f => a -> f a
pure ( RewriteEnv -> a
accessor ( ShimRewriteEnv -> RewriteEnv
rewriteEnv ShimRewriteEnv
env ), RewriteState
s )
getEqRel :: RewriteM EqRel
getEqRel :: RewriteM EqRel
getEqRel = (RewriteEnv -> EqRel) -> RewriteM EqRel
forall a. (RewriteEnv -> a) -> RewriteM a
getRewriteEnvField RewriteEnv -> EqRel
fe_eq_rel
getRole :: RewriteM Role
getRole :: RewriteM Role
getRole = EqRel -> Role
eqRelRole (EqRel -> Role) -> RewriteM EqRel -> RewriteM Role
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> RewriteM EqRel
getEqRel
getFlavour :: RewriteM CtFlavour
getFlavour :: RewriteM CtFlavour
getFlavour = (RewriteEnv -> CtFlavour) -> RewriteM CtFlavour
forall a. (RewriteEnv -> a) -> RewriteM a
getRewriteEnvField RewriteEnv -> CtFlavour
fe_flavour
getFlavourRole :: RewriteM CtFlavourRole
getFlavourRole :: RewriteM CtFlavourRole
getFlavourRole = do
CtFlavour
flavour <- RewriteM CtFlavour
getFlavour
EqRel
eq_rel <- RewriteM EqRel
getEqRel
CtFlavourRole -> RewriteM CtFlavourRole
forall (m :: * -> *) a. Monad m => a -> m a
return (CtFlavour
flavour, EqRel
eq_rel)
setEqRel :: EqRel -> RewriteM a -> RewriteM a
setEqRel :: EqRel -> RewriteM a -> RewriteM a
setEqRel EqRel
new_eq_rel RewriteM a
thing_inside = (ShimRewriteEnv -> RewriteState -> TcS (a, RewriteState))
-> RewriteM a
forall a.
(ShimRewriteEnv -> RewriteState -> TcS (a, RewriteState))
-> RewriteM a
RewriteM \ ShimRewriteEnv
env RewriteState
s ->
if EqRel
new_eq_rel EqRel -> EqRel -> Bool
forall a. Eq a => a -> a -> Bool
== RewriteEnv -> EqRel
fe_eq_rel ( ShimRewriteEnv -> RewriteEnv
rewriteEnv ShimRewriteEnv
env )
then RewriteM a
-> ShimRewriteEnv -> RewriteState -> TcS (a, RewriteState)
forall a.
RewriteM a
-> ShimRewriteEnv -> RewriteState -> TcS (a, RewriteState)
runRewriteM RewriteM a
thing_inside ShimRewriteEnv
env RewriteState
s
else RewriteM a
-> ShimRewriteEnv -> RewriteState -> TcS (a, RewriteState)
forall a.
RewriteM a
-> ShimRewriteEnv -> RewriteState -> TcS (a, RewriteState)
runRewriteM RewriteM a
thing_inside ( ShimRewriteEnv -> ShimRewriteEnv
setEqRel' ShimRewriteEnv
env ) RewriteState
s
where
setEqRel' :: ShimRewriteEnv -> ShimRewriteEnv
setEqRel' :: ShimRewriteEnv -> ShimRewriteEnv
setEqRel' ShimRewriteEnv
env = ShimRewriteEnv
env { rewriteEnv :: RewriteEnv
rewriteEnv = ( ShimRewriteEnv -> RewriteEnv
rewriteEnv ShimRewriteEnv
env ) { fe_eq_rel :: EqRel
fe_eq_rel = EqRel
new_eq_rel } }
{-# INLINE setEqRel #-}
liftTcS :: TcS a -> RewriteM a
liftTcS :: TcS a -> RewriteM a
liftTcS TcS a
thing_inside = (ShimRewriteEnv -> RewriteState -> TcS (a, RewriteState))
-> RewriteM a
forall a.
(ShimRewriteEnv -> RewriteState -> TcS (a, RewriteState))
-> RewriteM a
RewriteM \ ShimRewriteEnv
_env RewriteState
s -> do
a
a <- TcS a
thing_inside
(a, RewriteState) -> TcS (a, RewriteState)
forall (f :: * -> *) a. Applicative f => a -> f a
pure ( a
a, RewriteState
s )
traceRewriteM :: String -> SDoc -> RewriteM ()
traceRewriteM :: [Char] -> SDoc -> RewriteM ()
traceRewriteM [Char]
herald SDoc
doc = TcS () -> RewriteM ()
forall a. TcS a -> RewriteM a
liftTcS (TcS () -> RewriteM ()) -> TcS () -> RewriteM ()
forall a b. (a -> b) -> a -> b
$ [Char] -> SDoc -> TcS ()
traceTcS [Char]
herald SDoc
doc
{-# INLINE traceRewriteM #-}
getLoc :: RewriteM CtLoc
getLoc :: RewriteM CtLoc
getLoc = (RewriteEnv -> CtLoc) -> RewriteM CtLoc
forall a. (RewriteEnv -> a) -> RewriteM a
getRewriteEnvField RewriteEnv -> CtLoc
fe_loc
checkStackDepth :: Type -> RewriteM ()
checkStackDepth :: Type -> RewriteM ()
checkStackDepth Type
ty = do
CtLoc
loc <- RewriteM CtLoc
getLoc
TcS () -> RewriteM ()
forall a. TcS a -> RewriteM a
liftTcS (TcS () -> RewriteM ()) -> TcS () -> RewriteM ()
forall a b. (a -> b) -> a -> b
$ CtLoc -> Type -> TcS ()
checkReductionDepth CtLoc
loc Type
ty
bumpDepth :: RewriteM a -> RewriteM a
bumpDepth :: RewriteM a -> RewriteM a
bumpDepth (RewriteM ShimRewriteEnv -> RewriteState -> TcS (a, RewriteState)
thing_inside) = (ShimRewriteEnv -> RewriteState -> TcS (a, RewriteState))
-> RewriteM a
forall a.
(ShimRewriteEnv -> RewriteState -> TcS (a, RewriteState))
-> RewriteM a
RewriteM \ ShimRewriteEnv
env RewriteState
s -> do
let !renv :: RewriteEnv
renv = ShimRewriteEnv -> RewriteEnv
rewriteEnv ShimRewriteEnv
env
!renv' :: RewriteEnv
renv' = RewriteEnv
renv { fe_loc :: CtLoc
fe_loc = CtLoc -> CtLoc
bumpCtLocDepth ( RewriteEnv -> CtLoc
fe_loc RewriteEnv
renv ) }
!env' :: ShimRewriteEnv
env' = ShimRewriteEnv
env { rewriteEnv :: RewriteEnv
rewriteEnv = RewriteEnv
renv' }
ShimRewriteEnv -> RewriteState -> TcS (a, RewriteState)
thing_inside ShimRewriteEnv
env' RewriteState
s
#if !MIN_VERSION_ghc(9,2,0)
firstJustsM :: (Monad m, Foldable f) => f (m (Maybe a)) -> m (Maybe a)
firstJustsM :: f (m (Maybe a)) -> m (Maybe a)
firstJustsM = (Maybe a -> m (Maybe a) -> m (Maybe a))
-> Maybe a -> f (m (Maybe a)) -> m (Maybe a)
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldlM Maybe a -> m (Maybe a) -> m (Maybe a)
forall (m :: * -> *) a.
Monad m =>
Maybe a -> m (Maybe a) -> m (Maybe a)
go Maybe a
forall a. Maybe a
Nothing where
go :: Monad m => Maybe a -> m (Maybe a) -> m (Maybe a)
go :: Maybe a -> m (Maybe a) -> m (Maybe a)
go Maybe a
Nothing m (Maybe a)
action = m (Maybe a)
action
go result :: Maybe a
result@(Just a
_) m (Maybe a)
_action = Maybe a -> m (Maybe a)
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe a
result
lookupFamAppCache :: TyCon -> [Type] -> TcS (Maybe (Coercion, Type))
lookupFamAppCache :: TyCon -> [Type] -> TcS (Maybe (Coercion, Type))
lookupFamAppCache TyCon
fam_tc [Type]
tys = do
Maybe (Coercion, Type, CtFlavour)
res <- TyCon -> [Type] -> TcS (Maybe (Coercion, Type, CtFlavour))
lookupFlatCache TyCon
fam_tc [Type]
tys
Maybe (Coercion, Type) -> TcS (Maybe (Coercion, Type))
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Maybe (Coercion, Type) -> TcS (Maybe (Coercion, Type)))
-> Maybe (Coercion, Type) -> TcS (Maybe (Coercion, Type))
forall a b. (a -> b) -> a -> b
$ case Maybe (Coercion, Type, CtFlavour)
res of
Maybe (Coercion, Type, CtFlavour)
Nothing -> Maybe (Coercion, Type)
forall a. Maybe a
Nothing
Just ( Coercion
co, Type
ty, CtFlavour
_ ) -> (Coercion, Type) -> Maybe (Coercion, Type)
forall a. a -> Maybe a
Just ( Coercion
co, Type
ty )
extendFamAppCache :: TyCon -> [Type] -> (Coercion, Type) -> CtFlavour -> TcS ()
extendFamAppCache :: TyCon -> [Type] -> (Coercion, Type) -> CtFlavour -> TcS ()
extendFamAppCache TyCon
tc [Type]
xi_args (Coercion
co, Type
ty) CtFlavour
f = TyCon -> [Type] -> (Coercion, Type, CtFlavour) -> TcS ()
extendFlatCache TyCon
tc [Type]
xi_args (Coercion
co, Type
ty, CtFlavour
f)
lookupFamAppInert :: TyCon -> [Type] -> TcS (Maybe (Coercion, Type, CtFlavourRole))
lookupFamAppInert :: TyCon -> [Type] -> TcS (Maybe (Coercion, Type, CtFlavourRole))
lookupFamAppInert TyCon
tc [Type]
tys = do
Maybe (Coercion, Type, CtFlavour)
res <- TyCon -> [Type] -> TcS (Maybe (Coercion, Type, CtFlavour))
lookupFlatCache TyCon
tc [Type]
tys
Maybe (Coercion, Type, CtFlavourRole)
-> TcS (Maybe (Coercion, Type, CtFlavourRole))
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Maybe (Coercion, Type, CtFlavourRole)
-> TcS (Maybe (Coercion, Type, CtFlavourRole)))
-> Maybe (Coercion, Type, CtFlavourRole)
-> TcS (Maybe (Coercion, Type, CtFlavourRole))
forall a b. (a -> b) -> a -> b
$ case Maybe (Coercion, Type, CtFlavour)
res of
Maybe (Coercion, Type, CtFlavour)
Nothing -> Maybe (Coercion, Type, CtFlavourRole)
forall a. Maybe a
Nothing
Just ( Coercion
co, Type
ty, CtFlavour
f ) -> (Coercion, Type, CtFlavourRole)
-> Maybe (Coercion, Type, CtFlavourRole)
forall a. a -> Maybe a
Just ( Coercion
co, Type
ty, (CtFlavour
f, EqRel
NomEq) )
tcSplitForAllTyVarBinders :: Type -> ([TyVarBinder], Type)
tcSplitForAllTyVarBinders :: Type -> ([TyVarBinder], Type)
tcSplitForAllTyVarBinders = Type -> ([TyVarBinder], Type)
tcSplitForAllVarBndrs
#endif