{-# LANGUAGE BangPatterns #-}
{-# LANGUAGE CPP #-}

module GHC.TcPlugin.API.Internal.Shim.Reduction where

-- base
import Prelude
  hiding (Floating(cos))

-- ghc
import GHC.Core.Class
  ( Class(classTyCon) )
import GHC.Core.Coercion
  ( Coercion, CoercionN, MCoercion(..)
  , Role(Nominal), LiftingContext
#if MIN_VERSION_ghc(9,0,0)
  , castCoercionKind1, castCoercionKind2
  , coercionLKind, coercionRKind
#else
  , mkCoherenceLeftCo, mkNomReflCo
#endif
  , coercionKind
#if MIN_VERSION_ghc(8,10,0)
  , coToMCo
#else
  , isReflCo
#endif
  , decomposePiCos, downgradeRole
  , liftCoSubst, emptyLiftingContext, extendLiftingContextAndInScope, zapLiftingContext
  , mkAppCo, mkAppCos
  , mkCoherenceRightCo
  , mkForAllCo, mkFunCo
  , mkGReflLeftCo, mkGReflRightCo
  , mkHomoForAllCos, mkProofIrrelCo
  , mkReflCo, mkSubCo, mkSymCo, mkTransCo, mkTyConAppCo
  )
import GHC.Core.Predicate
  ( mkClassPred )
import GHC.Core.TyCo.Rep
  ( TyCoBinder, mkFunTy
#if !MIN_VERSION_ghc(9,0,0)
  , Coercion(..)
#endif
  )
import GHC.Core.TyCon
  ( TyCon )
import GHC.Core.Type
  ( ArgFlag, Kind, Type, TyVar, TyVarBinder
#if MIN_VERSION_ghc(8,10,0)
  , AnonArgFlag
#endif
  , binderVars
  , mkAppTy, mkAppTys, mkCastTy, mkCoercionTy, mkForAllTy, mkForAllTys
  , mkTyConApp, mkPiTys
  , noFreeVarsOfType
  , splitPiTys, tyCoBinderType, tyCoBinderVar_maybe
  )
import GHC.Data.Pair
  ( Pair(Pair) )
import GHC.Types.Var
  ( setTyVarKind )
import GHC.Types.Var.Env
  ( mkInScopeSet )
import GHC.Types.Var.Set
  ( TyCoVarSet )
import GHC.Utils.Outputable
  ( Outputable(ppr), (<+>)
  , braces, text, vcat
  )

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


-- | A 'Reduction' is the result of an operation that rewrites a type @ty_in@.
-- The 'Reduction' includes the rewritten type @ty_out@ and a 'Coercion' @co@
-- such that @co :: ty_in ~ ty_out@, where the role of the coercion is determined
-- by the context. That is, the LHS type of the coercion is the original type
-- @ty_in@, while its RHS type is the rewritten type @ty_out@.
--
-- A Reduction is always homogeneous, unless it is wrapped inside a 'HetReduction',
-- which separately stores the kind coercion.
data Reduction =
  Reduction
    { Reduction -> Coercion
reductionCoercion    :: Coercion
    , Reduction -> Type
reductionReducedType :: !Type
    }

-- | Stores a heterogeneous reduction.
--
-- The stored kind coercion must relate the kinds of the
-- stored reduction. That is, in @HetReduction (Reduction co xi) kco@,
-- we must have:
--
-- >  co :: ty ~ xi
-- > kco :: typeKind ty ~ typeKind xi
data HetReduction =
  HetReduction
    Reduction
    MCoercion

-- | Create a heterogeneous reduction.
--
-- Pre-condition: the provided kind coercion (second argument)
-- relates the kinds of the stored reduction.
-- That is, if the coercion stored in the 'Reduction' is of the form
--
-- > co :: ty ~ xi
--
-- Then the kind coercion supplied must be of the form:
--
-- > kco :: typeKind ty ~ typeKind xi
mkHetReduction :: Reduction  -- ^ heterogeneous reduction
               -> MCoercion  -- ^ kind coercion
               -> HetReduction
mkHetReduction :: Reduction -> MCoercion -> HetReduction
mkHetReduction Reduction
redn MCoercion
mco = Reduction -> MCoercion -> HetReduction
HetReduction Reduction
redn MCoercion
mco
{-# INLINE mkHetReduction #-}

-- | Homogenise a heterogeneous reduction.
--
-- Given @HetReduction (Reduction co xi) kco@, with
--
-- >  co :: ty ~ xi
-- > kco :: typeKind(ty) ~ typeKind(xi)
--
-- this returns the homogeneous reduction:
--
-- > hco :: ty ~ ( xi |> sym kco )
homogeniseHetRedn :: Role -> HetReduction -> Reduction
homogeniseHetRedn :: Role -> HetReduction -> Reduction
homogeniseHetRedn Role
role (HetReduction Reduction
redn MCoercion
kco)
  = Role -> Reduction -> MCoercion -> Reduction
mkCoherenceRightMRedn Role
role Reduction
redn (MCoercion -> MCoercion
mkSymMCo MCoercion
kco)
{-# INLINE homogeniseHetRedn #-}

-- | Create a 'Reduction' from a pair of a 'Coercion' and a 'Type.
--
-- Pre-condition: the RHS type of the coercion matches the provided type
-- (perhaps up to zonking).
--
-- Use 'coercionRedn' when you only have the coercion.
mkReduction :: Coercion -> Type -> Reduction
mkReduction :: Coercion -> Type -> Reduction
mkReduction Coercion
co Type
ty = Coercion -> Type -> Reduction
Reduction Coercion
co Type
ty
{-# INLINE mkReduction #-}

instance Outputable Reduction where
  ppr :: Reduction -> SDoc
ppr Reduction
redn =
    SDoc -> SDoc
braces forall a b. (a -> b) -> a -> b
$ [SDoc] -> SDoc
vcat
      [ String -> SDoc
text String
"reductionOriginalType:" SDoc -> SDoc -> SDoc
<+> forall a. Outputable a => a -> SDoc
ppr (Reduction -> Type
reductionOriginalType Reduction
redn)
      , String -> SDoc
text String
" reductionReducedType:" SDoc -> SDoc -> SDoc
<+> forall a. Outputable a => a -> SDoc
ppr (Reduction -> Type
reductionReducedType Reduction
redn)
      , String -> SDoc
text String
"    reductionCoercion:" SDoc -> SDoc -> SDoc
<+> forall a. Outputable a => a -> SDoc
ppr (Reduction -> Coercion
reductionCoercion Reduction
redn)
      ]

-- | A 'Reduction' in which the 'Coercion' has 'Nominal' role.
type ReductionN = Reduction

-- | A 'Reduction' in which the 'Coercion' has 'Representational' role.
type ReductionR = Reduction

-- | Get the original, unreduced type corresponding to a 'Reduction'.
--
-- This is obtained by computing the LHS kind of the stored coercion,
-- which may be slow.
reductionOriginalType :: Reduction -> Type
reductionOriginalType :: Reduction -> Type
reductionOriginalType = Coercion -> Type
coercionLKind forall b c a. (b -> c) -> (a -> b) -> a -> c
. Reduction -> Coercion
reductionCoercion
{-# INLINE reductionOriginalType #-}

-- | Turn a 'Coercion' into a 'Reduction'
-- by inspecting the RHS type of the coercion.
--
-- Prefer using 'mkReduction' when you already know
-- the RHS type of the coercion, to avoid computing it anew.
coercionRedn :: Coercion -> Reduction
coercionRedn :: Coercion -> Reduction
coercionRedn Coercion
co = Coercion -> Type -> Reduction
Reduction Coercion
co (Coercion -> Type
coercionRKind Coercion
co)
{-# INLINE coercionRedn #-}

-- | Downgrade the role of the coercion stored in the 'Reduction'.
downgradeRedn :: Role -- ^ desired role
              -> Role -- ^ current role
              -> Reduction
              -> Reduction
downgradeRedn :: Role -> Role -> Reduction -> Reduction
downgradeRedn Role
new_role Role
old_role redn :: Reduction
redn@(Reduction Coercion
co Type
_)
  = Reduction
redn { reductionCoercion :: Coercion
reductionCoercion = Role -> Role -> Coercion -> Coercion
downgradeRole Role
new_role Role
old_role Coercion
co }
{-# INLINE downgradeRedn #-}

-- | Downgrade the role of the coercion stored in the 'Reduction',
-- from 'Nominal' to 'Representational'.
mkSubRedn :: Reduction -> Reduction
mkSubRedn :: Reduction -> Reduction
mkSubRedn redn :: Reduction
redn@(Reduction Coercion
co Type
_) = Reduction
redn { reductionCoercion :: Coercion
reductionCoercion = HasDebugCallStack => Coercion -> Coercion
mkSubCo Coercion
co }
{-# INLINE mkSubRedn #-}

-- | Compose a reduction with a coercion on the left.
--
-- Pre-condition: the provided coercion's RHS type must match the LHS type
-- of the coercion that is stored in the reduction.
mkTransRedn :: Coercion -> Reduction -> Reduction
mkTransRedn :: Coercion -> Reduction -> Reduction
mkTransRedn Coercion
co1 redn :: Reduction
redn@(Reduction Coercion
co2 Type
_)
  = Reduction
redn { reductionCoercion :: Coercion
reductionCoercion = Coercion
co1 Coercion -> Coercion -> Coercion
`mkTransCo` Coercion
co2 }
{-# INLINE mkTransRedn #-}

-- | The reflexive reduction.
mkReflRedn :: Role -> Type -> Reduction
mkReflRedn :: Role -> Type -> Reduction
mkReflRedn Role
r Type
ty = Coercion -> Type -> Reduction
mkReduction (Role -> Type -> Coercion
mkReflCo Role
r Type
ty) Type
ty

-- | Create a 'Reduction' from a kind cast, in which
-- the casted type is the rewritten type.
--
-- Given @ty :: k1@, @mco :: k1 ~ k2@,
-- produces the 'Reduction' @ty ~res_co~> (ty |> mco)@
-- at the given 'Role'.
mkGReflRightRedn :: Role -> Type -> CoercionN -> Reduction
mkGReflRightRedn :: Role -> Type -> Coercion -> Reduction
mkGReflRightRedn Role
role Type
ty Coercion
co
  = Coercion -> Type -> Reduction
mkReduction
      (Role -> Type -> Coercion -> Coercion
mkGReflRightCo Role
role Type
ty Coercion
co)
      (Type -> Coercion -> Type
mkCastTy Type
ty Coercion
co)
{-# INLINE mkGReflRightRedn #-}

-- | Create a 'Reduction' from a kind cast, in which
-- the casted type is the rewritten type.
--
-- Given @ty :: k1@, @mco :: k1 ~ k2@,
-- produces the 'Reduction' @ty ~res_co~> (ty |> mco)@
-- at the given 'Role'.
mkGReflRightMRedn :: Role -> Type -> MCoercion -> Reduction
mkGReflRightMRedn :: Role -> Type -> MCoercion -> Reduction
mkGReflRightMRedn Role
role Type
ty MCoercion
mco
  = Coercion -> Type -> Reduction
mkReduction
      (Role -> Type -> MCoercion -> Coercion
mkGReflRightMCo Role
role Type
ty MCoercion
mco)
      (Type -> MCoercion -> Type
mkCastTyMCo Type
ty MCoercion
mco)
{-# INLINE mkGReflRightMRedn #-}

-- | Create a 'Reduction' from a kind cast, in which
-- the casted type is the original (non-rewritten) type.
--
-- Given @ty :: k1@, @mco :: k1 ~ k2@,
-- produces the 'Reduction' @(ty |> mco) ~res_co~> ty@
-- at the given 'Role'.
mkGReflLeftRedn :: Role -> Type -> CoercionN -> Reduction
mkGReflLeftRedn :: Role -> Type -> Coercion -> Reduction
mkGReflLeftRedn Role
role Type
ty Coercion
co
  = Coercion -> Type -> Reduction
mkReduction
      (Role -> Type -> Coercion -> Coercion
mkGReflLeftCo Role
role Type
ty Coercion
co)
      Type
ty
{-# INLINE mkGReflLeftRedn #-}

-- | Create a 'Reduction' from a kind cast, in which
-- the casted type is the original (non-rewritten) type.
--
-- Given @ty :: k1@, @mco :: k1 ~ k2@,
-- produces the 'Reduction' @(ty |> mco) ~res_co~> ty@
-- at the given 'Role'.
mkGReflLeftMRedn :: Role -> Type -> MCoercion -> Reduction
mkGReflLeftMRedn :: Role -> Type -> MCoercion -> Reduction
mkGReflLeftMRedn Role
role Type
ty MCoercion
mco
  = Coercion -> Type -> Reduction
mkReduction
      (Role -> Type -> MCoercion -> Coercion
mkGReflLeftMCo Role
role Type
ty MCoercion
mco)
      Type
ty
{-# INLINE mkGReflLeftMRedn #-}

-- | Apply a cast to the result of a 'Reduction'.
--
-- Given a 'Reduction' @ty1 ~co1~> (ty2 :: k2)@ and a kind coercion @kco@
-- with LHS kind @k2@, produce a new 'Reduction' @ty1 ~co2~> ( ty2 |> kco )@
-- of the given 'Role' (which must match the role of the coercion stored
-- in the 'Reduction' argument).
mkCoherenceRightRedn :: Role -> Reduction -> CoercionN -> Reduction
mkCoherenceRightRedn :: Role -> Reduction -> Coercion -> Reduction
mkCoherenceRightRedn Role
r (Reduction Coercion
co1 Type
ty2) Coercion
kco
  = Coercion -> Type -> Reduction
mkReduction
      (Role -> Type -> Coercion -> Coercion -> Coercion
mkCoherenceRightCo Role
r Type
ty2 Coercion
kco Coercion
co1)
      (Type -> Coercion -> Type
mkCastTy Type
ty2 Coercion
kco)
{-# INLINE mkCoherenceRightRedn #-}

-- | Apply a cast to the result of a 'Reduction', using an 'MCoercionN'.
--
-- Given a 'Reduction' @ty1 ~co1~> (ty2 :: k2)@ and a kind coercion @mco@
-- with LHS kind @k2@, produce a new 'Reduction' @ty1 ~co2~> ( ty2 |> mco )@
-- of the given 'Role' (which must match the role of the coercion stored
-- in the 'Reduction' argument).
mkCoherenceRightMRedn :: Role -> Reduction -> MCoercion -> Reduction
mkCoherenceRightMRedn :: Role -> Reduction -> MCoercion -> Reduction
mkCoherenceRightMRedn Role
r (Reduction Coercion
co1 Type
ty2) MCoercion
kco
  = Coercion -> Type -> Reduction
mkReduction
      (Role -> Type -> MCoercion -> Coercion -> Coercion
mkCoherenceRightMCo Role
r Type
ty2 MCoercion
kco Coercion
co1)
      (Type -> MCoercion -> Type
mkCastTyMCo Type
ty2 MCoercion
kco)
{-# INLINE mkCoherenceRightMRedn #-}

-- | Apply a cast to a 'Reduction', casting both the original and the reduced type.
--
-- Given @cast_co@ and 'Reduction' @ty ~co~> xi@, this function returns
-- the 'Reduction' @(ty |> cast_co) ~return_co~> (xi |> cast_co)@
-- of the given 'Role' (which must match the role of the coercion stored
-- in the 'Reduction' argument).
--
-- Pre-condition: the 'Type' passed in is the same as the LHS type
-- of the coercion stored in the 'Reduction'.
mkCastRedn1 :: Role
            -> Type      -- ^ original type
            -> CoercionN -- ^ coercion to cast with
            -> Reduction -- ^ rewritten type, with rewriting coercion
            -> Reduction
mkCastRedn1 :: Role -> Type -> Coercion -> Reduction -> Reduction
mkCastRedn1 Role
r Type
ty Coercion
cast_co (Reduction Coercion
co Type
xi)
  -- co :: ty ~r ty'
  -- return_co :: (ty |> cast_co) ~r (ty' |> cast_co)
  = Coercion -> Type -> Reduction
mkReduction
      (Coercion -> Role -> Type -> Type -> Coercion -> Coercion
castCoercionKind1 Coercion
co Role
r Type
ty Type
xi Coercion
cast_co)
      (Type -> Coercion -> Type
mkCastTy Type
xi Coercion
cast_co)
{-# INLINE mkCastRedn1 #-}

-- | Apply casts on both sides of a 'Reduction' (of the given 'Role').
--
-- Use 'mkCastRedn1' when you want to cast both the original and reduced types
-- in a 'Reduction' using the same coercion.
--
-- Pre-condition: the 'Type' passed in is the same as the LHS type
-- of the coercion stored in the 'Reduction'.
mkCastRedn2 :: Role
            -> Type      -- ^ original type
            -> CoercionN -- ^ coercion to cast with on the left
            -> Reduction -- ^ rewritten type, with rewriting coercion
            -> CoercionN -- ^ coercion to cast with on the right
            -> Reduction
mkCastRedn2 :: Role -> Type -> Coercion -> Reduction -> Coercion -> Reduction
mkCastRedn2 Role
r Type
ty Coercion
cast_co (Reduction Coercion
nco Type
nty) Coercion
cast_co'
  = Coercion -> Type -> Reduction
mkReduction
      (Coercion
-> Role -> Type -> Type -> Coercion -> Coercion -> Coercion
castCoercionKind2 Coercion
nco Role
r Type
ty Type
nty Coercion
cast_co Coercion
cast_co')
      (Type -> Coercion -> Type
mkCastTy Type
nty Coercion
cast_co')
{-# INLINE mkCastRedn2 #-}

-- | Apply one 'Reduction' to another.
--
-- Combines 'mkAppCo' and 'mkAppTy`.
mkAppRedn :: Reduction -> Reduction -> Reduction
mkAppRedn :: Reduction -> Reduction -> Reduction
mkAppRedn (Reduction Coercion
co1 Type
ty1) (Reduction Coercion
co2 Type
ty2)
  = Coercion -> Type -> Reduction
mkReduction (Coercion -> Coercion -> Coercion
mkAppCo Coercion
co1 Coercion
co2) (Type -> Type -> Type
mkAppTy Type
ty1 Type
ty2)
{-# INLINE mkAppRedn #-}

-- | Create a function 'Reduction'.
--
-- Combines 'mkFunCo' and 'mkFunTy'.
mkFunRedn :: Role
#if MIN_VERSION_ghc(8,10,0)
          -> AnonArgFlag
#endif
#if MIN_VERSION_ghc(9,0,0)
          -> ReductionN -- ^ multiplicity reduction
#endif
          -> Reduction  -- ^ argument reduction
          -> Reduction  -- ^ result reduction
          -> Reduction
mkFunRedn :: Role
-> AnonArgFlag -> Reduction -> Reduction -> Reduction -> Reduction
mkFunRedn Role
r
#if MIN_VERSION_ghc(8,10,0)
  AnonArgFlag
vis
#endif
#if MIN_VERSION_ghc(9,0,0)
  (Reduction Coercion
w_co Type
w_ty)
#endif
  (Reduction Coercion
arg_co Type
arg_ty)
  (Reduction Coercion
res_co Type
res_ty)
    = Coercion -> Type -> Reduction
mkReduction
        ( Role -> Coercion -> Coercion -> Coercion -> Coercion
mkFunCo
            Role
r
#if MIN_VERSION_ghc(9,0,0)
            Coercion
w_co
#endif
            Coercion
arg_co
            Coercion
res_co
        )
        ( AnonArgFlag -> Type -> Type -> Type -> Type
mkFunTy
#if MIN_VERSION_ghc(8,10,0)
            AnonArgFlag
vis
#endif
#if MIN_VERSION_ghc(9,0,0)
            Type
w_ty
#endif
            Type
arg_ty
            Type
res_ty
        )
{-# INLINE mkFunRedn #-}

-- | Create a 'Reduction' associated to a Π type,
-- from a kind 'Reduction' and a body 'Reduction'.
--
-- Combines 'mkForAllCo' and 'mkForAllTy'.
mkForAllRedn :: ArgFlag
             -> TyVar
             -> ReductionN -- ^ kind reduction
             -> Reduction  -- ^ body reduction
             -> Reduction
mkForAllRedn :: ArgFlag -> TyVar -> Reduction -> Reduction -> Reduction
mkForAllRedn ArgFlag
vis TyVar
tv1 (Reduction Coercion
h Type
ki') (Reduction Coercion
co Type
ty)
  = Coercion -> Type -> Reduction
mkReduction
      (TyVar -> Coercion -> Coercion -> Coercion
mkForAllCo TyVar
tv1 Coercion
h Coercion
co)
      (TyVar -> ArgFlag -> Type -> Type
mkForAllTy TyVar
tv2 ArgFlag
vis Type
ty)
  where
    tv2 :: TyVar
tv2 = TyVar -> Type -> TyVar
setTyVarKind TyVar
tv1 Type
ki'
{-# INLINE mkForAllRedn #-}

-- | Create a 'Reduction' of a quantified type from a
-- 'Reduction' of the body.
--
-- Combines 'mkHomoForAllCos' and 'mkForAllTys'.
mkHomoForAllRedn :: [TyVarBinder] -> Reduction -> Reduction
mkHomoForAllRedn :: [TyVarBinder] -> Reduction -> Reduction
mkHomoForAllRedn [TyVarBinder]
bndrs (Reduction Coercion
co Type
ty)
  = Coercion -> Type -> Reduction
mkReduction
      ([TyVar] -> Coercion -> Coercion
mkHomoForAllCos (forall tv argf. [VarBndr tv argf] -> [tv]
binderVars [TyVarBinder]
bndrs) Coercion
co)
      ([TyVarBinder] -> Type -> Type
mkForAllTys [TyVarBinder]
bndrs Type
ty)
{-# INLINE mkHomoForAllRedn #-}

-- | Create a 'Reduction' from a coercion between coercions.
--
-- Combines 'mkProofIrrelCo' and 'mkCoercionTy'.
mkProofIrrelRedn :: Role      -- ^ role of the created coercion, "r"
                 -> CoercionN -- ^ co :: phi1 ~N phi2
                 -> Coercion  -- ^ g1 :: phi1
                 -> Coercion  -- ^ g2 :: phi2
                 -> Reduction -- ^ res_co :: g1 ~r g2
mkProofIrrelRedn :: Role -> Coercion -> Coercion -> Coercion -> Reduction
mkProofIrrelRedn Role
role Coercion
co Coercion
g1 Coercion
g2
  = Coercion -> Type -> Reduction
mkReduction
      (Role -> Coercion -> Coercion -> Coercion -> Coercion
mkProofIrrelCo Role
role Coercion
co Coercion
g1 Coercion
g2)
      (Coercion -> Type
mkCoercionTy Coercion
g2)
{-# INLINE mkProofIrrelRedn #-}

-- | Create a reflexive 'Reduction' whose RHS is the given 'Coercion',
-- with the specified 'Role'.
mkReflCoRedn :: Role -> Coercion -> Reduction
mkReflCoRedn :: Role -> Coercion -> Reduction
mkReflCoRedn Role
role Coercion
co
  = Coercion -> Type -> Reduction
mkReduction
      (Role -> Type -> Coercion
mkReflCo Role
role Type
co_ty)
      Type
co_ty
  where
    co_ty :: Type
co_ty = Coercion -> Type
mkCoercionTy Coercion
co
{-# INLINE mkReflCoRedn #-}

-- | A collection of 'Reduction's where the coercions and the types are stored separately.
--
-- Use 'unzipRedns' to obtain 'Reductions' from a list of 'Reduction's.
--
-- This datatype is used in 'mkAppRedns', 'mkClassPredRedns' and 'mkTyConAppRedn',
-- which expect separate types and coercions.
--
-- Invariant: the two stored lists are of the same length,
-- and the RHS type of each coercion is the corresponding type.
data Reductions = Reductions [Coercion] [Type]

-- | Create 'Reductions' from individual lists of coercions and types.
--
-- The lists should be of the same length, and the RHS type of each coercion
-- should match the specified type in the other list.
mkReductions :: [Coercion] -> [Type] -> Reductions
mkReductions :: [Coercion] -> [Type] -> Reductions
mkReductions [Coercion]
cos [Type]
tys = [Coercion] -> [Type] -> Reductions
Reductions [Coercion]
cos [Type]
tys
{-# INLINE mkReductions #-}

-- | Combines 'mkAppCos' and 'mkAppTys'.
mkAppRedns :: Reduction -> Reductions -> Reduction
mkAppRedns :: Reduction -> Reductions -> Reduction
mkAppRedns (Reduction Coercion
co Type
ty) (Reductions [Coercion]
cos [Type]
tys)
  = Coercion -> Type -> Reduction
mkReduction (Coercion -> [Coercion] -> Coercion
mkAppCos Coercion
co [Coercion]
cos) (Type -> [Type] -> Type
mkAppTys Type
ty [Type]
tys)
{-# INLINE mkAppRedns #-}

-- | 'TyConAppCo' for 'Reduction's: combines 'mkTyConAppCo' and `mkTyConApp`.
mkTyConAppRedn :: Role -> TyCon -> Reductions -> Reduction
mkTyConAppRedn :: Role -> TyCon -> Reductions -> Reduction
mkTyConAppRedn Role
role TyCon
tc (Reductions [Coercion]
cos [Type]
tys)
  = Coercion -> Type -> Reduction
mkReduction (HasDebugCallStack => Role -> TyCon -> [Coercion] -> Coercion
mkTyConAppCo Role
role TyCon
tc [Coercion]
cos) (TyCon -> [Type] -> Type
mkTyConApp TyCon
tc [Type]
tys)
{-# INLINE mkTyConAppRedn #-}

-- | Reduce the arguments of a 'Class' 'TyCon'.
mkClassPredRedn :: Class -> Reductions -> Reduction
mkClassPredRedn :: Class -> Reductions -> Reduction
mkClassPredRedn Class
cls (Reductions [Coercion]
cos [Type]
tys)
  = Coercion -> Type -> Reduction
mkReduction
      (HasDebugCallStack => Role -> TyCon -> [Coercion] -> Coercion
mkTyConAppCo Role
Nominal (Class -> TyCon
classTyCon Class
cls) [Coercion]
cos)
      (Class -> [Type] -> Type
mkClassPred Class
cls [Type]
tys)
{-# INLINE mkClassPredRedn #-}

-- | Obtain 'Reductions' from a list of 'Reduction's by unzipping.
unzipRedns :: [Reduction] -> Reductions
unzipRedns :: [Reduction] -> Reductions
unzipRedns = forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr Reduction -> Reductions -> Reductions
accRedn ([Coercion] -> [Type] -> Reductions
Reductions [] [])
  where
    accRedn :: Reduction -> Reductions -> Reductions
    accRedn :: Reduction -> Reductions -> Reductions
accRedn (Reduction Coercion
co Type
xi) (Reductions [Coercion]
cos [Type]
xis)
      = [Coercion] -> [Type] -> Reductions
Reductions (Coercion
coforall a. a -> [a] -> [a]
:[Coercion]
cos) (Type
xiforall a. a -> [a] -> [a]
:[Type]
xis)
{-# INLINE unzipRedns #-}

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

data ArgsReductions =
  ArgsReductions
    {-# UNPACK #-} !Reductions
    !MCoercion

{-# INLINE simplifyArgsWorker #-}
simplifyArgsWorker :: [TyCoBinder] -> Kind -> TyCoVarSet -> [Role] -> [Reduction] -> ArgsReductions
simplifyArgsWorker :: [TyCoBinder]
-> Type -> TyCoVarSet -> [Role] -> [Reduction] -> ArgsReductions
simplifyArgsWorker [TyCoBinder]
orig_ki_binders Type
orig_inner_ki TyCoVarSet
orig_fvs
                   [Role]
orig_roles [Reduction]
orig_simplified_args
  = LiftingContext
-> [TyCoBinder] -> Type -> [Role] -> [Reduction] -> ArgsReductions
go LiftingContext
orig_lc
       [TyCoBinder]
orig_ki_binders Type
orig_inner_ki
       [Role]
orig_roles [Reduction]
orig_simplified_args
  where
    orig_lc :: LiftingContext
orig_lc = InScopeSet -> LiftingContext
emptyLiftingContext forall a b. (a -> b) -> a -> b
$ TyCoVarSet -> InScopeSet
mkInScopeSet forall a b. (a -> b) -> a -> b
$ TyCoVarSet
orig_fvs

    go :: LiftingContext -> [TyCoBinder] -> Kind -> [Role] -> [Reduction] -> ArgsReductions
    go :: LiftingContext
-> [TyCoBinder] -> Type -> [Role] -> [Reduction] -> ArgsReductions
go !LiftingContext
lc [TyCoBinder]
binders Type
inner_ki [Role]
_ []
      = Reductions -> MCoercion -> ArgsReductions
ArgsReductions
          ([Coercion] -> [Type] -> Reductions
mkReductions [] [])
          MCoercion
kind_co
      where
        final_kind :: Type
final_kind = [TyCoBinder] -> Type -> Type
mkPiTys [TyCoBinder]
binders Type
inner_ki
        kind_co :: MCoercion
kind_co | Type -> Bool
noFreeVarsOfType Type
final_kind = MCoercion
MRefl
                | Bool
otherwise                   = Coercion -> MCoercion
MCo forall a b. (a -> b) -> a -> b
$ HasDebugCallStack => Role -> LiftingContext -> Type -> Coercion
liftCoSubst Role
Nominal LiftingContext
lc Type
final_kind

    go LiftingContext
lc (TyCoBinder
binder:[TyCoBinder]
binders) Type
inner_ki (Role
role:[Role]
roles) (Reduction
arg_redn:[Reduction]
arg_redns)
      =  let !kind_co :: Coercion
kind_co = HasDebugCallStack => Role -> LiftingContext -> Type -> Coercion
liftCoSubst Role
Nominal LiftingContext
lc (TyCoBinder -> Type
tyCoBinderType TyCoBinder
binder)
             !(Reduction Coercion
casted_co Type
casted_xi)
                      = Role -> Reduction -> Coercion -> Reduction
mkCoherenceRightRedn Role
role Reduction
arg_redn Coercion
kind_co
         -- now, extend the lifting context with the new binding
             !new_lc :: LiftingContext
new_lc | Just TyVar
tv <- TyCoBinder -> Maybe TyVar
tyCoBinderVar_maybe TyCoBinder
binder
                     = LiftingContext -> TyVar -> Coercion -> LiftingContext
extendLiftingContextAndInScope LiftingContext
lc TyVar
tv Coercion
casted_co
                     | Bool
otherwise
                     = LiftingContext
lc
             !(ArgsReductions (Reductions [Coercion]
cos [Type]
xis) MCoercion
final_kind_co)
               = LiftingContext
-> [TyCoBinder] -> Type -> [Role] -> [Reduction] -> ArgsReductions
go LiftingContext
new_lc [TyCoBinder]
binders Type
inner_ki [Role]
roles [Reduction]
arg_redns
         in Reductions -> MCoercion -> ArgsReductions
ArgsReductions
              ([Coercion] -> [Type] -> Reductions
Reductions (Coercion
casted_coforall a. a -> [a] -> [a]
:[Coercion]
cos) (Type
casted_xiforall a. a -> [a] -> [a]
:[Type]
xis))
              MCoercion
final_kind_co

    -- See Note [Last case in simplifyArgsWorker]
    go LiftingContext
lc [] Type
inner_ki [Role]
roles [Reduction]
arg_redns
      = let co1 :: Coercion
co1 = HasDebugCallStack => Role -> LiftingContext -> Type -> Coercion
liftCoSubst Role
Nominal LiftingContext
lc Type
inner_ki
            co1_kind :: Pair Type
co1_kind              = Coercion -> Pair Type
coercionKind Coercion
co1
            unrewritten_tys :: [Type]
unrewritten_tys       = forall a b. (a -> b) -> [a] -> [b]
map Reduction -> Type
reductionOriginalType [Reduction]
arg_redns
            ([Coercion]
arg_cos, Coercion
res_co)     = HasDebugCallStack =>
Coercion -> Pair Type -> [Type] -> ([Coercion], Coercion)
decomposePiCos Coercion
co1 Pair Type
co1_kind [Type]
unrewritten_tys
            casted_args :: [Reduction]
casted_args           = forall a b c d. (a -> b -> c -> d) -> [a] -> [b] -> [c] -> [d]
zipWith3 Role -> Reduction -> Coercion -> Reduction
mkCoherenceRightRedn [Role]
roles [Reduction]
arg_redns [Coercion]
arg_cos
            zapped_lc :: LiftingContext
zapped_lc             = LiftingContext -> LiftingContext
zapLiftingContext LiftingContext
lc
            Pair Type
rewritten_kind Type
_ = Pair Type
co1_kind
            ([TyCoBinder]
bndrs, Type
new_inner)    = Type -> ([TyCoBinder], Type)
splitPiTys Type
rewritten_kind

            ArgsReductions Reductions
redns_out MCoercion
res_co_out
              = LiftingContext
-> [TyCoBinder] -> Type -> [Role] -> [Reduction] -> ArgsReductions
go LiftingContext
zapped_lc [TyCoBinder]
bndrs Type
new_inner [Role]
roles [Reduction]
casted_args
        in
          Reductions -> MCoercion -> ArgsReductions
ArgsReductions Reductions
redns_out (Coercion
res_co Coercion -> MCoercion -> MCoercion
`mkTransMCoR` MCoercion
res_co_out)

    go LiftingContext
_ [TyCoBinder]
_ Type
_ [Role]
_ [Reduction]
_ = forall a. HasCallStack => String -> a
error String
"simplifyArgsWorker wandered into deeper water than usual"

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

-- | Get the reverse of an 'MCoercion'
mkSymMCo :: MCoercion -> MCoercion
mkSymMCo :: MCoercion -> MCoercion
mkSymMCo MCoercion
MRefl    = MCoercion
MRefl
mkSymMCo (MCo Coercion
co) = Coercion -> MCoercion
MCo (Coercion -> Coercion
mkSymCo Coercion
co)

mkGReflLeftMCo :: Role -> Type -> MCoercion -> Coercion
mkGReflLeftMCo :: Role -> Type -> MCoercion -> Coercion
mkGReflLeftMCo Role
r Type
ty MCoercion
MRefl    = Role -> Type -> Coercion
mkReflCo Role
r Type
ty
mkGReflLeftMCo Role
r Type
ty (MCo Coercion
co) = Role -> Type -> Coercion -> Coercion
mkGReflLeftCo Role
r Type
ty Coercion
co

mkGReflRightMCo :: Role -> Type -> MCoercion -> Coercion
mkGReflRightMCo :: Role -> Type -> MCoercion -> Coercion
mkGReflRightMCo Role
r Type
ty MCoercion
MRefl    = Role -> Type -> Coercion
mkReflCo Role
r Type
ty
mkGReflRightMCo Role
r Type
ty (MCo Coercion
co) = Role -> Type -> Coercion -> Coercion
mkGReflRightCo Role
r Type
ty Coercion
co

-- | Cast a type by an 'MCoercion'
mkCastTyMCo :: Type -> MCoercion -> Type
mkCastTyMCo :: Type -> MCoercion -> Type
mkCastTyMCo Type
ty MCoercion
MRefl    = Type
ty
mkCastTyMCo Type
ty (MCo Coercion
co) = Type
ty Type -> Coercion -> Type
`mkCastTy` Coercion
co

-- | Like 'mkCoherenceRightCo', but with an 'MCoercion'
mkCoherenceRightMCo :: Role -> Type -> MCoercion -> Coercion -> Coercion
mkCoherenceRightMCo :: Role -> Type -> MCoercion -> Coercion -> Coercion
mkCoherenceRightMCo Role
_ Type
_  MCoercion
MRefl    Coercion
co2 = Coercion
co2
mkCoherenceRightMCo Role
r Type
ty (MCo Coercion
co) Coercion
co2 = Role -> Type -> Coercion -> Coercion -> Coercion
mkCoherenceRightCo Role
r Type
ty Coercion
co Coercion
co2

mkTransMCoR :: Coercion -> MCoercion -> MCoercion
mkTransMCoR :: Coercion -> MCoercion -> MCoercion
mkTransMCoR Coercion
co1 MCoercion
MRefl     = Coercion -> MCoercion
coToMCo Coercion
co1
mkTransMCoR Coercion
co1 (MCo Coercion
co2) = Coercion -> MCoercion
MCo (Coercion -> Coercion -> Coercion
mkTransCo Coercion
co1 Coercion
co2)

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

#if !MIN_VERSION_ghc(9,0,0)

coercionLKind, coercionRKind :: Coercion -> Type
coercionLKind co = case coercionKind co of { Pair lco _ -> lco }
coercionRKind co = case coercionKind co of { Pair _ rco -> rco }

-- | Creates a new coercion with both of its types casted by different casts
-- @castCoercionKind2 g r t1 t2 h1 h2@, where @g :: t1 ~r t2@,
-- has type @(t1 |> h1) ~r (t2 |> h2)@.
-- @h1@ and @h2@ must be nominal.
castCoercionKind2 :: Coercion -> Role -> Type -> Type
                 -> CoercionN -> CoercionN -> Coercion
castCoercionKind2 g r t1 t2 h1 h2
  = mkCoherenceRightCo r t2 h2 (mkCoherenceLeftCo r t1 h1 g)

-- | @castCoercionKind1 g r t1 t2 h@ = @coercionKind g r t1 t2 h h@
-- That is, it's a specialised form of castCoercionKind, where the two
--          kind coercions are identical
-- @castCoercionKind1 g r t1 t2 h@, where @g :: t1 ~r t2@,
-- has type @(t1 |> h) ~r (t2 |> h)@.
-- @h@ must be nominal.
-- See Note [castCoercionKind1]
castCoercionKind1 :: Coercion -> Role -> Type -> Type
                  -> CoercionN -> Coercion
castCoercionKind1 g r t1 t2 h
  = case g of
      Refl {} -> mkNomReflCo (mkCastTy t2 h)
      GRefl _ _ mco -> case mco of
           MRefl       -> mkReflCo r (mkCastTy t2 h)
           MCo kind_co -> GRefl r (mkCastTy t1 h) $
                          MCo (mkSymCo h `mkTransCo` kind_co `mkTransCo` h)
      _ -> castCoercionKind2 g r t1 t2 h h
#endif

#if !MIN_VERSION_ghc(8,10,0)

coToMCo :: Coercion -> MCoercion
coToMCo co | isReflCo co = MRefl
           | otherwise   = MCo co

#endif