{-# LANGUAGE BangPatterns    #-}
{-# LANGUAGE BlockArguments  #-}
{-# LANGUAGE CPP             #-}
{-# LANGUAGE DerivingVia     #-}
{-# LANGUAGE LambdaCase      #-}
{-# LANGUAGE NamedFieldPuns  #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE TupleSections   #-}
{-# LANGUAGE ViewPatterns    #-}

{-|
Module: GHC.TcPlugin.API.Internal.Shim

This module defines a compatibility shim which allows
the library to support a limited form of type-family rewriting
in typechecking plugins on GHC 9.0 and 9.2.
-}

module GHC.TcPlugin.API.Internal.Shim
  ( Reduction(..), mkReduction
  , TcPluginSolveResult(TcPluginContradiction, TcPluginOk, ..), TcPluginRewriteResult(..)
  , RewriteEnv(..)
  , shimRewriter
  )
  where

-- base

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 )

-- transformers

import Control.Monad.Trans.Reader
  ( ReaderT(..) )
import Control.Monad.Trans.State.Strict
  ( StateT(..) )

-- ghc

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 )

-- ghc-tcplugin-api

import GHC.TcPlugin.API.Internal.Shim.Reduction

--------------------------------------------------------------------------------


-- | The type-family rewriting environment.

data RewriteEnv
  = FE { RewriteEnv -> CtLoc
fe_loc     :: !CtLoc
       , RewriteEnv -> CtFlavour
fe_flavour :: !CtFlavour
       , RewriteEnv -> EqRel
fe_eq_rel  :: !EqRel
       }

-- | Result of running a solver plugin.

data TcPluginSolveResult
  = TcPluginSolveResult
  { -- | Insoluble constraints found by the plugin.

    --

    -- These constraints will be added to the inert set,

    -- and reported as insoluble to the user.

    TcPluginSolveResult -> [Ct]
tcPluginInsolubleCts :: [Ct]
    -- | Solved constraints, together with their evidence.

    --

    -- These are removed from the inert set, and the

    -- evidence for them is recorded.

  , TcPluginSolveResult -> [(EvTerm, Ct)]
tcPluginSolvedCts :: [(EvTerm, Ct)]
    -- | New constraints that the plugin wishes to emit.

    --

    -- These will be added to the work list.

  , TcPluginSolveResult -> [Ct]
tcPluginNewCts :: [Ct]
  }

-- | The plugin found a contradiction.

-- The returned constraints are removed from the inert set,

-- and recorded as insoluble.

--

-- The returned list of constraints should never be empty.

pattern TcPluginContradiction :: [Ct] -> TcPluginSolveResult
pattern $bTcPluginContradiction :: [Ct] -> TcPluginSolveResult
$mTcPluginContradiction :: forall {r}. TcPluginSolveResult -> ([Ct] -> r) -> ((# #) -> r) -> r
TcPluginContradiction insols
  = TcPluginSolveResult
  { tcPluginInsolubleCts = insols
  , tcPluginSolvedCts    = []
  , tcPluginNewCts       = [] }

-- | The plugin has not found any contradictions,

--

-- The first field is for constraints that were solved.

-- The second field contains new work, that should be processed by

-- the constraint solver.

pattern TcPluginOk :: [(EvTerm, Ct)] -> [Ct] -> TcPluginSolveResult
pattern $bTcPluginOk :: [(EvTerm, Ct)] -> [Ct] -> TcPluginSolveResult
$mTcPluginOk :: forall {r}.
TcPluginSolveResult
-> ([(EvTerm, Ct)] -> [Ct] -> r) -> ((# #) -> r) -> r
TcPluginOk solved new
  = TcPluginSolveResult
  { tcPluginInsolubleCts = []
  , tcPluginSolvedCts    = solved
  , tcPluginNewCts       = new }

-- The 'TcPluginSolveResult' datatype changed in GHC 9.4,

-- allowing users to return solved and new constraints even in case of

-- a contradiction.

--

-- This function simply drops the solved and new constraints on older versions,

-- although it does at least still bind the evidence in case of solved Wanteds.

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
    }
  )
    | forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Ct]
insols
    = forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ [(EvTerm, Ct)] -> [Ct] -> TcPluginResult
GHC.TcPluginOk [(EvTerm, Ct)]
solved [Ct]
new
    | forall (t :: * -> *) a. Foldable t => t a -> Bool
null [(EvTerm, Ct)]
solved Bool -> Bool -> Bool
&& forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Ct]
new
    = forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ [Ct] -> TcPluginResult
GHC.TcPluginContradiction [Ct]
insols
    | Bool
otherwise
    = do
      EvBindsVar
evBinds <- TcPluginM EvBindsVar
getEvBindsTcPluginM
      forall a. TcM a -> TcPluginM a
unsafeTcPluginTcM forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. EvBindsVar -> TcS a -> TcM a
runTcSWithEvBinds EvBindsVar
evBinds forall a b. (a -> b) -> a -> b
$ do
        forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless Bool
doingGivens forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) (f :: * -> *) a b.
(Foldable t, Applicative f) =>
(a -> f b) -> t a -> f ()
traverse_ ( forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry EvTerm -> Ct -> TcS ()
setEv ) [(EvTerm, Ct)]
solved
        --updInertCans (removeInertCts $ fmap snd solved) -- These don't do anything, as the inert set and work list

        --emitWork new                                    -- are confined to this run of the plugin.

      forall (f :: * -> *) a. Applicative f => a -> f a
pure 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
_
      = forall (f :: * -> *) a. Applicative f => a -> f a
pure ()

data TcPluginRewriteResult
  =
  -- | The plugin does not rewrite the type family application.

    TcPluginNoRewrite

  -- | The plugin rewrites the type family application

  -- providing a rewriting together with evidence.

  --

  -- The plugin can also emit additional wanted constraints.

  | 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

-- | Emulate type-family rewriting functionality in a constraint solving plugin,

-- by traversing through all the constraints and rewriting any type-family applications

-- inside them.

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
  | forall key elt. UniqFM key elt -> Bool
isNullUFM Rewriters
rws
  = Bool -> TcPluginSolveResult -> TcPluginM TcPluginResult
adaptSolveResult (forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Ct]
wanteds) 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 ) <- 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 ) <- 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 (forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Ct]
wanteds) forall a b. (a -> b) -> a -> b
$
      TcPluginSolveResult
        { tcPluginInsolubleCts :: [Ct]
tcPluginInsolubleCts = [Ct]
contras
        , tcPluginSolvedCts :: [(EvTerm, Ct)]
tcPluginSolvedCts    = [(EvTerm, Ct)]
solved forall a. [a] -> [a] -> [a]
++ [(EvTerm, Ct)]
solvedDeriveds forall a. [a] -> [a] -> [a]
++ [(EvTerm, Ct)]
solvedWanteds
        , tcPluginNewCts :: [Ct]
tcPluginNewCts       = [Ct]
new forall a. [a] -> [a] -> [a]
++ [Ct]
newCts1 forall a. [a] -> [a] -> [a]
++ [Ct]
rewrittenDeriveds forall a. [a] -> [a] -> [a]
++ [Ct]
newCts2 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 ) <- 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 -> forall (f :: * -> *) a. Applicative f => a -> f a
pure ( 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     -> 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 forall a b. (a -> b) -> a -> b
$ case Role
role of
          Role
Nominal -> HasDebugCallStack => Coercion -> Coercion
mkSubCo Coercion
co
          Role
_       -> Coercion
co
      forall (f :: * -> *) a. Applicative f => a -> f a
pure ( 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 :: 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])
_ [] = 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 ) <- 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    -> forall (f :: * -> *) a. Applicative f => a -> f a
pure ( [b]
bs, [c]
cs, [d]
ds forall a. [a] -> [a] -> [a]
++ [d]
dss )
    Just (b
b,c
c) -> forall (f :: * -> *) a. Applicative f => a -> f a
pure ( b
b forall a. a -> [a] -> [a]
: [b]
bs, c
c forall a. a -> [a] -> [a]
: [c]
cs, [d]
ds forall a. [a] -> [a] -> [a]
++ [d]
dss )

--------------------------------------------------------------------------------

-- The following is (mostly) copied from GHC 9.4's GHC.Tc.Solver.Rewrite module.


rewrite_one :: Type -> RewriteM Reduction
rewrite_one :: Type -> RewriteM Reduction
rewrite_one Type
ty
  | Just Type
ty' <- Type -> Maybe Type
rewriterView Type
ty  -- See Note [Rewriting synonyms]

  = Type -> RewriteM Reduction
rewrite_one Type
ty'

rewrite_one xi :: Type
xi@(LitTy {})
  = do { Role
role <- RewriteM Role
getRole
       ; forall (m :: * -> *) a. Monad m => a -> m a
return 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)
    Type
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)
       ; Reduction
w_redn <- forall a. EqRel -> RewriteM a -> RewriteM a
setEqRel EqRel
NomEq forall a b. (a -> b) -> a -> b
$ Type -> RewriteM Reduction
rewrite_one Type
mult
#endif
       ; Role
role <- RewriteM Role
getRole
       ; forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$
           Role
-> AnonArgFlag -> Reduction -> Reduction -> Reduction -> Reduction
mkFunRedn
             Role
role
#if MIN_VERSION_ghc(8,10,0)
             AnonArgFlag
vis
#endif
#if MIN_VERSION_ghc(9,0,0)
             Reduction
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
       ; forall (m :: * -> *) a. Monad m => a -> m a
return 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
       ; forall (m :: * -> *) a. Monad m => a -> m a
return 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
       ; forall (m :: * -> *) a. Monad m => a -> m a
return 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 <- forall a. RewriteM a -> RewriteM a
bumpDepth forall a b. (a -> b) -> a -> b
$ Type -> RewriteM Reduction
rewrite_one Type
xi
  forall (f :: * -> *) a. Applicative f => a -> f a
pure 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
ty2forall 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 []
  = 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])
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 = 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
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 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 (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
                                    (forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith Role -> Type -> Coercion
mkReflCo [Role]
tc_roles [Type]
xis forall a. [a] -> [a] -> [a]
++ [Coercion]
arg_cos)

                ; forall (m :: * -> *) a. Monad m => a -> m a
return 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
tcTypeKind Type
fun_xi) (forall a. a -> [a]
repeat Role
Nominal) [Type]
arg_tys
                ; forall (m :: * -> *) a. Monad m => a -> m a
return 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
       ; 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
  -- NB: TyCon kinds are always closed

  where
  -- There are many bang patterns in here. It's been observed that they

  -- greatly improve performance of an optimized build.

  -- The T9872 test cases are good witnesses of this fact.


    ([TyCoBinder]
bndrs, Bool
named)
      = [TyConBinder] -> ([TyCoBinder], Bool)
ty_con_binders_ty_binders' (TyCon -> [TyConBinder]
tyConBinders TyCon
tc)
    -- it's possible that the result kind has arrows (for, e.g., a type family)

    -- so we must split it

    ([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 forall a. [a] -> [a] -> [a]
`chkAppend` [TyCoBinder]
inner_bndrs
    !any_named_bndrs :: Bool
any_named_bndrs                     = Bool
named Bool -> Bool -> Bool
|| Bool
inner_named
    -- NB: Those bangs there drop allocations in T9872{a,c,d} by 8%.


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) = 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 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 = forall key elt. Uniquable key => UniqFM key 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 forall a. Eq a => a -> a -> Bool
== EqRel
NomEq
        then TyCon -> Maybe [Role] -> [Type] -> RewriteM ArgsReductions
rewrite_args_tc TyCon
tc forall a. Maybe a
Nothing [Type]
tys
        else forall a. EqRel -> RewriteM a -> RewriteM a
setEqRel EqRel
NomEq forall a b. (a -> b) -> a -> b
$
             TyCon -> Maybe [Role] -> [Type] -> RewriteM ArgsReductions
rewrite_args_tc TyCon
tc 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
mkTyConAppCo Role
role TyCon
tc [Coercion]
cos
        homogenise :: Reduction -> Reduction
        homogenise :: Reduction -> Reduction
homogenise Reduction
redn
          = Role -> HetReduction -> Reduction
homogeniseHetRedn Role
role
          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 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 <- forall a. TcS a -> RewriteM a
liftTcS 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
mkSymCoOnGHC92 Coercion
co) Type
xi
          -> Bool -> Reduction -> RewriteM Reduction
finish Bool
True (Reduction -> Reduction
homogenise 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
_         -> 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 <- forall a. RewriteM a -> RewriteM a
bumpDepth 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
co Coercion -> Coercion -> Coercion
`mkTcTransCo` Coercion
fully_co) Type
fully
      EqRel
eq_rel <- RewriteM EqRel
getEqRel
      CtFlavour
flavour <- RewriteM CtFlavour
getFlavour
      forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Bool
use_cache Bool -> Bool -> Bool
&& EqRel
eq_rel forall a. Eq a => a -> a -> Bool
== EqRel
NomEq Bool -> Bool -> Bool
&& CtFlavour
flavour forall a. Eq a => a -> a -> Bool
/= CtFlavour
Derived) forall a b. (a -> b) -> a -> b
$
        forall a. TcS a -> RewriteM a
liftTcS forall a b. (a -> b) -> a -> b
$
          TyCon -> [Type] -> (Coercion, Type) -> TcS ()
extendFamAppCache TyCon
tc [Type]
tys
            ( Coercion -> Coercion
mkSymCoOnGHC92 Coercion
final_co, Type
final_xi )
#if !MIN_VERSION_ghc(9,2,0)
            flavour
#endif
      forall (m :: * -> *) a. Monad m => a -> m a
return Reduction
final_redn
    {-# INLINE finish #-}

-- On GHC 9.2, lookupFamAppCache and matchFam

-- use a coercion that goes from right to left.

-- On GHC 9.0 (and GHC 9.4 and above), the coercions

-- always go from left to right.

-- (Recall: this module is only used for GHC 9.2 and below.)

mkSymCoOnGHC92 :: Coercion -> Coercion
mkSymCoOnGHC92 :: Coercion -> Coercion
mkSymCoOnGHC92 Coercion
co =
#if MIN_VERSION_ghc(9,2,0)
  Coercion -> Coercion
mkSymCo Coercion
co
#else
  co
#endif

-- Returned coercion is output ~r input, where r is the role in the RewriteM monad

-- See Note [How to normalise a family application]

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 <-
    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
      , forall a. TcS a -> RewriteM a
liftTcS forall a b. (a -> b) -> a -> b
$ Maybe (Coercion, Type) -> Maybe Reduction
mkRed forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TyCon -> [Type] -> TcS (Maybe (Coercion, Type))
lookupFamAppCache TyCon
tc [Type]
tys
      , forall a. TcS a -> RewriteM a
liftTcS forall a b. (a -> b) -> a -> b
$ Maybe (Coercion, Type) -> Maybe Reduction
mkRed forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TyCon -> [Type] -> TcS (Maybe (Coercion, Type))
matchFam TyCon
tc [Type]
tys ]
  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 = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a b. (a -> b) -> a -> b
$ \ (Coercion
co, Type
ty) -> Coercion -> Type -> Reduction
Reduction (Coercion -> Coercion
mkSymCoOnGHC92 Coercion
co) Type
ty
      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  -> forall (m :: * -> *) a. Monad m => a -> m a
return Reduction
redn
          EqRel
ReprEq -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Coercion -> Type -> Reduction
Reduction (HasDebugCallStack => 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 -> forall (m :: * -> *) a. Monad m => a -> m a
return 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 }" ( forall a. Outputable a => a -> SDoc
ppr Maybe Reduction
res )
      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 <- forall a.
(ShimRewriteEnv -> RewriteState -> TcS (a, RewriteState))
-> RewriteM a
RewriteM \ ShimRewriteEnv
env RewriteState
s -> do
      TcPluginRewriteResult
res <- forall a. TcPluginM a -> TcS a
runTcPluginTcS ( Rewriter
rewriter ( ShimRewriteEnv -> RewriteEnv
rewriteEnv ShimRewriteEnv
env ) ( ShimRewriteEnv -> [Ct]
rewriteGivens ShimRewriteEnv
env ) [Type]
tys )
      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 ( forall a. a -> Maybe a
Just Reduction
redn ) [Ct]
wanteds
      TcPluginNoRewrite { }
          -> Maybe Reduction -> [Ct] -> RewriteM (Maybe Reduction)
addRewriting 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 = forall a. Maybe a
Nothing
                     | Bool
otherwise       = forall a. a -> Maybe a
Just 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
       ; forall (m :: * -> *) a. Monad m => a -> m a
return 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 = forall a. TcS a -> RewriteM a
liftTcS 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)
  Bool -> Bool -> Bool
|| TyCon -> Bool
isForgetfulSynTyCon TyCon
tc
#endif
  = Type -> Maybe Type
tcView Type
ty
rewriterView Type
_other = 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' <- forall a. TcS a -> RewriteM a
liftTcS forall a b. (a -> b) -> a -> b
$ 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'
      forall (f :: * -> *) a. Applicative f => a -> f a
pure 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 <- forall a. TcS a -> RewriteM a
liftTcS 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
      forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Reduction -> RewriteTvResult
RTRFollowed 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 EqualCtList
ieqs <- forall a. TcS a -> RewriteM a
liftTcS forall a b. (a -> b) -> a -> b
$ TcS (DTyVarEnv EqualCtList)
getInertEqs
  case forall a. DVarEnv a -> Var -> Maybe a
lookupDVarEnv DTyVarEnv EqualCtList
ieqs Var
tv of
#if MIN_VERSION_ghc(9,2,0)
    Just (EqualCtList (Ct
ct :| [Ct]
_))
      | CEqCan { cc_ev :: Ct -> CtEvidence
cc_ev = CtEvidence
ctev, cc_lhs :: Ct -> CanEqLHS
cc_lhs = TyVarLHS {}
               , cc_rhs :: Ct -> Type
cc_rhs = Type
rhs_ty, cc_eq_rel :: Ct -> EqRel
cc_eq_rel = EqRel
ct_eq_rel } <- Ct
ct
#else
    Just (ct : _)
      | CTyEqCan { cc_ev = ctev
                 , cc_rhs = rhs_ty, cc_eq_rel = ct_eq_rel } <- 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
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) -> HasDebugCallStack => Coercion -> Coercion
mkSubCo Coercion
rewriting_co1
          forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Reduction -> RewriteTvResult
RTRFollowed forall a b. (a -> b) -> a -> b
$ Coercion -> Type -> Reduction
mkReduction Coercion
rewriting_co Type
rhs_ty 
    Maybe EqualCtList
_other -> 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 -> forall a. Maybe a
Nothing; EqRel
ReprEq -> 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 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)
      Type
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 -> Scaled Type -> TyCoBinder
Anon
#if MIN_VERSION_ghc(8,10,0)
          AnonArgFlag
af
#endif
#if MIN_VERSION_ghc(9,0,0)
          (forall a. Type -> a -> Scaled a
mkScaled Type
w Type
arg)
#else
          arg
#endif
          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' = 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 (forall var argf. var -> argf -> VarBndr var argf
Bndr Var
tv ArgFlag
vis) 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 -> Scaled Type -> TyCoBinder
Anon
#if MIN_VERSION_ghc(8,10,0)
          AnonArgFlag
af
#endif
          (
#if MIN_VERSION_ghc(9,0,0)
            forall a. a -> Scaled a
tymult
#endif
             (Var -> Type
tyVarKind Var
tv)
          )
          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 = forall a. a -> Maybe a -> a
fromMaybe (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
  = 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
      forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ [Coercion] -> [Type] -> Reductions
Reductions (Coercion
co forall a. a -> [a] -> [a]
: [Coercion]
cos) (Type
xi forall a. a -> [a] -> [a]
: [Type]
xis)
    iterate [] = forall (f :: * -> *) a. Applicative f => a -> f a
pure 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 <- 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 (forall a b. (a -> b) -> [a] -> [b]
map TyCoBinder -> Bool
isNamedBinder [TyCoBinder]
binders forall a. [a] -> [a] -> [a]
++ forall a. a -> [a]
repeat Bool
True)
                                        [Role]
roles [Type]
tys
       ; forall (m :: * -> *) a. Monad m => a -> m a
return 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   -- must we ensure to produce a real coercion here?

                 -- see comment at top of function

       -> Role -> Type -> RewriteM Reduction
    fl :: Bool -> Role -> Type -> RewriteM Reduction
fl Bool
True  Role
r Type
ty = forall a. RewriteM a -> RewriteM a
noBogusCoercions 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
      = forall a. EqRel -> RewriteM a -> RewriteM a
setEqRel EqRel
NomEq forall a b. (a -> b) -> a -> b
$
        Type -> RewriteM Reduction
rewrite_one Type
ty

    fl1 Role
Representational Type
ty
      = forall a. EqRel -> RewriteM a -> RewriteM a
setEqRel EqRel
ReprEq forall a b. (a -> b) -> a -> b
$
        Type -> RewriteM Reduction
rewrite_one Type
ty

    fl1 Role
Phantom Type
ty
      = do { Type
ty' <- forall a. TcS a -> RewriteM a
liftTcS forall a b. (a -> b) -> a -> b
$ Type -> TcS Type
zonkTcType Type
ty
           ; forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Role -> Type -> Reduction
mkReflRedn Role
Phantom Type
ty' }

noBogusCoercions :: RewriteM a -> RewriteM a
noBogusCoercions :: forall a. RewriteM a -> RewriteM a
noBogusCoercions RewriteM a
thing_inside
  = 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
    forall a.
RewriteM a
-> ShimRewriteEnv -> RewriteState -> TcS (a, RewriteState)
runRewriteM RewriteM a
thing_inside ShimRewriteEnv
env' RewriteState
s

chkAppend :: [a] -> [a] -> [a]
chkAppend :: forall a. [a] -> [a] -> [a]
chkAppend [a]
xs [a]
ys
  | forall (t :: * -> *) a. Foldable t => t a -> Bool
null [a]
ys   = [a]
xs
  | Bool
otherwise = [a]
xs 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
  { forall a.
RewriteM a
-> ShimRewriteEnv -> RewriteState -> TcS (a, RewriteState)
runRewriteM
    :: ShimRewriteEnv
    -> RewriteState
    -> TcS ( a, RewriteState )
  }
  deriving ( 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
<$ :: forall a b. a -> RewriteM b -> RewriteM a
$c<$ :: forall a b. a -> RewriteM b -> RewriteM a
fmap :: forall a b. (a -> b) -> RewriteM a -> RewriteM b
$cfmap :: forall a b. (a -> b) -> RewriteM a -> RewriteM b
Functor, Functor RewriteM
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
<* :: forall a b. RewriteM a -> RewriteM b -> RewriteM a
$c<* :: forall a b. RewriteM a -> RewriteM b -> RewriteM a
*> :: forall a b. RewriteM a -> RewriteM b -> RewriteM b
$c*> :: forall a b. RewriteM a -> RewriteM b -> RewriteM b
liftA2 :: forall a b c.
(a -> b -> c) -> RewriteM a -> RewriteM b -> RewriteM c
$cliftA2 :: forall a b c.
(a -> b -> c) -> RewriteM a -> RewriteM b -> RewriteM c
<*> :: forall a b. RewriteM (a -> b) -> RewriteM a -> RewriteM b
$c<*> :: forall a b. RewriteM (a -> b) -> RewriteM a -> RewriteM b
pure :: forall a. a -> RewriteM a
$cpure :: forall a. a -> RewriteM a
Applicative, Applicative RewriteM
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 :: forall a. a -> RewriteM a
$creturn :: forall a. a -> RewriteM a
>> :: forall a b. RewriteM a -> RewriteM b -> RewriteM b
$c>> :: forall a b. RewriteM a -> RewriteM b -> RewriteM b
>>= :: forall a b. RewriteM a -> (a -> RewriteM b) -> RewriteM b
$c>>= :: forall a b. RewriteM a -> (a -> RewriteM b) -> RewriteM b
Monad )
    via ( ReaderT ShimRewriteEnv
          ( StateT RewriteState TcS )
        )

runRewritePluginM :: ShimRewriteEnv
                  -> RewriteM a
                  -> TcPluginM ( Maybe a, [Ct] )
runRewritePluginM :: forall a. 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 } )
    <- forall a. TcM a -> TcPluginM a
unsafeTcPluginTcM
     forall a b. (a -> b) -> a -> b
$ forall a. EvBindsVar -> TcS a -> TcM a
runTcSWithEvBinds EvBindsVar
evBindsVar
     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 -> forall a. Maybe a
Nothing
      ReduceQ
DidReduce   -> forall a. a -> Maybe a
Just a
a
  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 = 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 forall (f :: * -> *) a. Applicative f => a -> f a
pure ( Maybe Reduction
mbRedn , [Ct] -> ReduceQ -> RewriteState
RewriteState ( [Ct]
cts forall a. Semigroup a => a -> a -> a
<> [Ct]
newCts ) ReduceQ
s' )

getRewriters :: RewriteM Rewriters
getRewriters :: RewriteM Rewriters
getRewriters = forall a.
(ShimRewriteEnv -> RewriteState -> TcS (a, RewriteState))
-> RewriteM a
RewriteM \ ShimRewriteEnv
env RewriteState
s -> forall (f :: * -> *) a. Applicative f => a -> f a
pure ( ShimRewriteEnv -> Rewriters
rewriters ShimRewriteEnv
env, RewriteState
s )

getRewriteEnvField :: (RewriteEnv -> a) -> RewriteM a
getRewriteEnvField :: forall a. (RewriteEnv -> a) -> RewriteM a
getRewriteEnvField RewriteEnv -> a
accessor = forall a.
(ShimRewriteEnv -> RewriteState -> TcS (a, RewriteState))
-> RewriteM a
RewriteM \ ShimRewriteEnv
env RewriteState
s ->
  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 = forall a. (RewriteEnv -> a) -> RewriteM a
getRewriteEnvField RewriteEnv -> EqRel
fe_eq_rel

getRole :: RewriteM Role
getRole :: RewriteM Role
getRole = EqRel -> Role
eqRelRole forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> RewriteM EqRel
getEqRel

getFlavour :: RewriteM CtFlavour
getFlavour :: RewriteM CtFlavour
getFlavour = 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
  forall (m :: * -> *) a. Monad m => a -> m a
return (CtFlavour
flavour, EqRel
eq_rel)

setEqRel :: EqRel -> RewriteM a -> RewriteM a
setEqRel :: forall a. EqRel -> RewriteM a -> RewriteM a
setEqRel EqRel
new_eq_rel RewriteM a
thing_inside = forall a.
(ShimRewriteEnv -> RewriteState -> TcS (a, RewriteState))
-> RewriteM a
RewriteM \ ShimRewriteEnv
env RewriteState
s ->
  if EqRel
new_eq_rel forall a. Eq a => a -> a -> Bool
== RewriteEnv -> EqRel
fe_eq_rel ( ShimRewriteEnv -> RewriteEnv
rewriteEnv ShimRewriteEnv
env )
  then forall a.
RewriteM a
-> ShimRewriteEnv -> RewriteState -> TcS (a, RewriteState)
runRewriteM RewriteM a
thing_inside ShimRewriteEnv
env RewriteState
s
  else 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 :: forall a. TcS a -> RewriteM a
liftTcS TcS a
thing_inside = forall a.
(ShimRewriteEnv -> RewriteState -> TcS (a, RewriteState))
-> RewriteM a
RewriteM \ ShimRewriteEnv
_env RewriteState
s -> do
  a
a <- TcS a
thing_inside
  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 = forall a. TcS a -> RewriteM a
liftTcS forall a b. (a -> b) -> a -> b
$ [Char] -> SDoc -> TcS ()
traceTcS [Char]
herald SDoc
doc
{-# INLINE traceRewriteM #-}

getLoc :: RewriteM CtLoc
getLoc :: RewriteM CtLoc
getLoc = 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
  forall a. TcS a -> RewriteM a
liftTcS forall a b. (a -> b) -> a -> b
$ CtLoc -> Type -> TcS ()
checkReductionDepth CtLoc
loc Type
ty

bumpDepth :: RewriteM a -> RewriteM a
bumpDepth :: forall a. RewriteM a -> RewriteM a
bumpDepth (RewriteM ShimRewriteEnv -> RewriteState -> TcS (a, RewriteState)
thing_inside) = 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)
--------------------------------------------------------------------------------

-- GHC 9.0 compatibility.


firstJustsM :: (Monad m, Foldable f) => f (m (Maybe a)) -> m (Maybe a)
firstJustsM = foldlM go Nothing where
  go :: Monad m => Maybe a -> m (Maybe a) -> m (Maybe a)
  go Nothing         action  = action
  go result@(Just _) _action = return result

lookupFamAppCache :: TyCon -> [Type] -> TcS (Maybe (Coercion, Type))
lookupFamAppCache fam_tc tys = do
  res <- lookupFlatCache fam_tc tys
  pure $ case res of
    Nothing -> Nothing
    Just  ( co, ty, _ ) -> Just ( co, ty )

extendFamAppCache :: TyCon -> [Type] -> (Coercion, Type) -> CtFlavour -> TcS ()
extendFamAppCache tc xi_args (co, ty) f = extendFlatCache tc xi_args (co, ty, f)

lookupFamAppInert :: TyCon -> [Type] -> TcS (Maybe (Coercion, Type, CtFlavourRole))
lookupFamAppInert tc tys = do
  res <- lookupFlatCache tc tys
  pure $ case res of
    Nothing -> Nothing
    Just ( co, ty, f ) -> Just ( co, ty, (f, NomEq) )

tcSplitForAllTyVarBinders :: Type -> ([TyVarBinder], Type)
tcSplitForAllTyVarBinders = tcSplitForAllVarBndrs

#endif