{-# LANGUAGE DeriveFunctor       #-}
{-# LANGUAGE FlexibleContexts    #-}
{-# LANGUAGE RankNTypes          #-}
{-# LANGUAGE ScopedTypeVariables #-}

{-
(c) The University of Glasgow 2006
-}

-- | Module for (a) type kinds and (b) type coercions,
-- as used in System FC. See 'GHC.Core.Expr' for
-- more on System FC and how coercions fit into it.
--
module GHC.Core.Coercion (
        -- * Main data type
        Coercion, CoercionN, CoercionR, CoercionP,
        MCoercion(..), MCoercionN, MCoercionR,
        CoSel(..), FunSel(..),
        UnivCoProvenance, CoercionHole(..),
        coHoleCoVar, setCoHoleCoVar,
        LeftOrRight(..),
        Var, CoVar, TyCoVar,
        Role(..), ltRole,

        -- ** Functions over coercions
        coVarRType, coVarLType, coVarTypes,
        coVarKind, coVarTypesRole, coVarRole,
        coercionType, mkCoercionType,
        coercionKind, coercionLKind, coercionRKind,coercionKinds,
        coercionRole, coercionKindRole,

        -- ** Constructing coercions
        mkGReflCo, mkReflCo, mkRepReflCo, mkNomReflCo,
        mkCoVarCo, mkCoVarCos,
        mkAxInstCo, mkUnbranchedAxInstCo,
        mkAxInstRHS, mkUnbranchedAxInstRHS,
        mkAxInstLHS, mkUnbranchedAxInstLHS,
        mkPiCo, mkPiCos, mkCoCast,
        mkSymCo, mkTransCo,
        mkSelCo, mkSelCoResRole, getNthFun, selectFromType, mkLRCo,
        mkInstCo, mkAppCo, mkAppCos, mkTyConAppCo,
        mkFunCo, mkFunCo2, mkFunCoNoFTF, mkFunResCo,
        mkNakedFunCo,
        mkNakedForAllCo, mkForAllCo, mkHomoForAllCos,
        mkPhantomCo,
        mkHoleCo, mkUnivCo, mkSubCo,
        mkProofIrrelCo,
        downgradeRole, mkAxiomCo,
        mkGReflRightCo, mkGReflLeftCo, mkCoherenceLeftCo, mkCoherenceRightCo,
        mkKindCo,
        castCoercionKind, castCoercionKind1, castCoercionKind2,

        mkPrimEqPred, mkReprPrimEqPred, mkPrimEqPredRole,
        mkNomPrimEqPred,

        -- ** Decomposition
        instNewTyCon_maybe,

        NormaliseStepper, NormaliseStepResult(..), composeSteppers, unwrapNewTypeStepper,
        topNormaliseNewType_maybe, topNormaliseTypeX,

        decomposeCo, decomposeFunCo, decomposePiCos, getCoVar_maybe,
        splitAppCo_maybe,
        splitFunCo_maybe,
        splitForAllCo_maybe,
        splitForAllCo_ty_maybe, splitForAllCo_co_maybe,

        tyConRole, tyConRolesX, tyConRolesRepresentational, setNominalRole_maybe,
        tyConRoleListX, tyConRoleListRepresentational, funRole,
        pickLR,

        isGReflCo, isReflCo, isReflCo_maybe, isGReflCo_maybe, isReflexiveCo, isReflexiveCo_maybe,
        isReflCoVar_maybe, isGReflMCo, mkGReflLeftMCo, mkGReflRightMCo,
        mkCoherenceRightMCo,

        coToMCo, mkTransMCo, mkTransMCoL, mkTransMCoR, mkCastTyMCo, mkSymMCo,
        mkFunResMCo, mkPiMCos,
        isReflMCo, checkReflexiveMCo,

        -- ** Coercion variables
        mkCoVar, isCoVar, coVarName, setCoVarName, setCoVarUnique,

        -- ** Free variables
        tyCoVarsOfCo, tyCoVarsOfCos, coVarsOfCo,
        tyCoFVsOfCo, tyCoFVsOfCos, tyCoVarsOfCoDSet,
        coercionSize, anyFreeVarsOfCo,

        -- ** Substitution
        CvSubstEnv, emptyCvSubstEnv,
        lookupCoVar,
        substCo, substCos, substCoVar, substCoVars, substCoWith,
        substCoVarBndr,
        extendTvSubstAndInScope, getCvSubstEnv,

        -- ** Lifting
        liftCoSubst, liftCoSubstTyVar, liftCoSubstWith, liftCoSubstWithEx,
        emptyLiftingContext, extendLiftingContext, extendLiftingContextAndInScope,
        liftCoSubstVarBndrUsing, isMappedByLC, extendLiftingContextCvSubst,

        mkSubstLiftingContext, liftingContextSubst, zapLiftingContext,
        substForAllCoBndrUsingLC, lcLookupCoVar, lcInScopeSet,

        LiftCoEnv, LiftingContext(..), liftEnvSubstLeft, liftEnvSubstRight,
        substRightCo, substLeftCo, swapLiftCoEnv, lcSubstLeft, lcSubstRight,

        -- ** Comparison
        eqCoercion, eqCoercionX,

        -- ** Forcing evaluation of coercions
        seqCo,

        -- * Pretty-printing
        pprCo, pprParendCo,
        pprCoAxiom, pprCoAxBranch, pprCoAxBranchLHS,
        pprCoAxBranchUser, tidyCoAxBndrsForUser,
        etaExpandCoAxBranch,

        -- * Tidying
        tidyCo, tidyCos,

        -- * Other
        promoteCoercion, buildCoercion,

        multToCo, mkRuntimeRepCo,

        hasCoercionHoleTy, hasCoercionHoleCo, hasThisCoercionHoleTy,

        setCoHoleType
       ) where

import {-# SOURCE #-} GHC.CoreToIface (toIfaceTyCon, tidyToIfaceTcArgs)

import GHC.Prelude

import GHC.Iface.Type
import GHC.Core.TyCo.Rep
import GHC.Core.TyCo.FVs
import GHC.Core.TyCo.Ppr
import GHC.Core.TyCo.Subst
import GHC.Core.TyCo.Tidy
import GHC.Core.TyCo.Compare
import GHC.Core.Type
import GHC.Core.TyCon
import GHC.Core.TyCon.RecWalk
import GHC.Core.Coercion.Axiom
import GHC.Types.Var
import GHC.Types.Var.Env
import GHC.Types.Var.Set
import GHC.Types.Name hiding ( varName )
import GHC.Types.Basic
import GHC.Types.Unique
import GHC.Data.FastString
import GHC.Data.Pair
import GHC.Types.SrcLoc
import GHC.Builtin.Names
import GHC.Builtin.Types.Prim
import GHC.Data.List.SetOps
import GHC.Data.Maybe
import GHC.Types.Unique.FM
import GHC.Data.List.Infinite (Infinite (..))
import qualified GHC.Data.List.Infinite as Inf

import GHC.Utils.Misc
import GHC.Utils.Outputable
import GHC.Utils.Panic

import Control.Monad (foldM, zipWithM)
import Data.Function ( on )
import Data.Char( isDigit )
import qualified Data.Monoid as Monoid
import Control.DeepSeq

{-
%************************************************************************
%*                                                                      *
     -- The coercion arguments always *precisely* saturate
     -- arity of (that branch of) the CoAxiom.  If there are
     -- any left over, we use AppCo.  See
     -- See [Coercion axioms applied to coercions] in GHC.Core.TyCo.Rep

\subsection{Coercion variables}
%*                                                                      *
%************************************************************************
-}

coVarName :: CoVar -> Name
coVarName :: CoVar -> Name
coVarName = CoVar -> Name
varName

setCoVarUnique :: CoVar -> Unique -> CoVar
setCoVarUnique :: CoVar -> Unique -> CoVar
setCoVarUnique = CoVar -> Unique -> CoVar
setVarUnique

setCoVarName :: CoVar -> Name -> CoVar
setCoVarName :: CoVar -> Name -> CoVar
setCoVarName   = CoVar -> Name -> CoVar
setVarName

{-
%************************************************************************
%*                                                                      *
                   Pretty-printing CoAxioms
%*                                                                      *
%************************************************************************

Defined here to avoid module loops. CoAxiom is loaded very early on.

-}

etaExpandCoAxBranch :: CoAxBranch -> ([TyVar], [Type], Type)
-- Return the (tvs,lhs,rhs) after eta-expanding,
-- to the way in which the axiom was originally written
-- See Note [Eta reduction for data families] in GHC.Core.Coercion.Axiom
etaExpandCoAxBranch :: CoAxBranch -> ([CoVar], [Type], Type)
etaExpandCoAxBranch (CoAxBranch { cab_tvs :: CoAxBranch -> [CoVar]
cab_tvs = [CoVar]
tvs
                                , cab_eta_tvs :: CoAxBranch -> [CoVar]
cab_eta_tvs = [CoVar]
eta_tvs
                                , cab_lhs :: CoAxBranch -> [Type]
cab_lhs = [Type]
lhs
                                , cab_rhs :: CoAxBranch -> Type
cab_rhs = Type
rhs })
  -- ToDo: what about eta_cvs?
  = ([CoVar]
tvs [CoVar] -> [CoVar] -> [CoVar]
forall a. [a] -> [a] -> [a]
++ [CoVar]
eta_tvs, [Type]
lhs [Type] -> [Type] -> [Type]
forall a. [a] -> [a] -> [a]
++ [Type]
eta_tys, Type -> [Type] -> Type
mkAppTys Type
rhs [Type]
eta_tys)
 where
    eta_tys :: [Type]
eta_tys = [CoVar] -> [Type]
mkTyVarTys [CoVar]
eta_tvs

pprCoAxiom :: CoAxiom br -> SDoc
-- Used in debug-printing only
pprCoAxiom :: forall (br :: BranchFlag). CoAxiom br -> SDoc
pprCoAxiom ax :: CoAxiom br
ax@(CoAxiom { co_ax_tc :: forall (br :: BranchFlag). CoAxiom br -> TyCon
co_ax_tc = TyCon
tc, co_ax_branches :: forall (br :: BranchFlag). CoAxiom br -> Branches br
co_ax_branches = Branches br
branches })
  = SDoc -> Arity -> SDoc -> SDoc
hang (String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"axiom" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> CoAxiom br -> SDoc
forall a. Outputable a => a -> SDoc
ppr CoAxiom br
ax)
       Arity
2 (SDoc -> SDoc
forall doc. IsLine doc => doc -> doc
braces (SDoc -> SDoc) -> SDoc -> SDoc
forall a b. (a -> b) -> a -> b
$ [SDoc] -> SDoc
forall doc. IsDoc doc => [doc] -> doc
vcat ((CoAxBranch -> SDoc) -> [CoAxBranch] -> [SDoc]
forall a b. (a -> b) -> [a] -> [b]
map (TyCon -> CoAxBranch -> SDoc
pprCoAxBranchUser TyCon
tc) (Branches br -> [CoAxBranch]
forall (br :: BranchFlag). Branches br -> [CoAxBranch]
fromBranches Branches br
branches)))

pprCoAxBranchUser :: TyCon -> CoAxBranch -> SDoc
-- Used when printing injectivity errors (FamInst.reportInjectivityErrors)
-- and inaccessible branches (GHC.Tc.Validity.inaccessibleCoAxBranch)
-- This happens in error messages: don't print the RHS of a data
--   family axiom, which is meaningless to a user
pprCoAxBranchUser :: TyCon -> CoAxBranch -> SDoc
pprCoAxBranchUser TyCon
tc CoAxBranch
br
  | TyCon -> Bool
isDataFamilyTyCon TyCon
tc = TyCon -> CoAxBranch -> SDoc
pprCoAxBranchLHS TyCon
tc CoAxBranch
br
  | Bool
otherwise            = TyCon -> CoAxBranch -> SDoc
pprCoAxBranch    TyCon
tc CoAxBranch
br

pprCoAxBranchLHS :: TyCon -> CoAxBranch -> SDoc
-- Print the family-instance equation when reporting
--   a conflict between equations (FamInst.conflictInstErr)
-- For type families the RHS is important; for data families not so.
--   Indeed for data families the RHS is a mysterious internal
--   type constructor, so we suppress it (#14179)
-- See FamInstEnv Note [Family instance overlap conflicts]
pprCoAxBranchLHS :: TyCon -> CoAxBranch -> SDoc
pprCoAxBranchLHS = (TidyEnv -> Type -> SDoc) -> TyCon -> CoAxBranch -> SDoc
ppr_co_ax_branch TidyEnv -> Type -> SDoc
forall {doc} {p} {p}. IsOutput doc => p -> p -> doc
pp_rhs
  where
    pp_rhs :: p -> p -> doc
pp_rhs p
_ p
_ = doc
forall doc. IsOutput doc => doc
empty

pprCoAxBranch :: TyCon -> CoAxBranch -> SDoc
pprCoAxBranch :: TyCon -> CoAxBranch -> SDoc
pprCoAxBranch = (TidyEnv -> Type -> SDoc) -> TyCon -> CoAxBranch -> SDoc
ppr_co_ax_branch TidyEnv -> Type -> SDoc
ppr_rhs
  where
    ppr_rhs :: TidyEnv -> Type -> SDoc
ppr_rhs TidyEnv
env Type
rhs = SDoc
forall doc. IsLine doc => doc
equals SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> TidyEnv -> PprPrec -> Type -> SDoc
pprPrecTypeX TidyEnv
env PprPrec
topPrec Type
rhs

ppr_co_ax_branch :: (TidyEnv -> Type -> SDoc)
                 -> TyCon -> CoAxBranch -> SDoc
ppr_co_ax_branch :: (TidyEnv -> Type -> SDoc) -> TyCon -> CoAxBranch -> SDoc
ppr_co_ax_branch TidyEnv -> Type -> SDoc
ppr_rhs TyCon
fam_tc CoAxBranch
branch
  = (SDoc -> SDoc -> SDoc) -> [SDoc] -> SDoc
forall a. (a -> a -> a) -> [a] -> a
forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
foldr1 ((SDoc -> Arity -> SDoc -> SDoc) -> Arity -> SDoc -> SDoc -> SDoc
forall a b c. (a -> b -> c) -> b -> a -> c
flip SDoc -> Arity -> SDoc -> SDoc
hangNotEmpty Arity
2)
    [ [ForAllTyBinder] -> SDoc
pprUserForAll (ForAllTyFlag -> [CoVar] -> [ForAllTyBinder]
forall vis. vis -> [CoVar] -> [VarBndr CoVar vis]
mkForAllTyBinders ForAllTyFlag
Inferred [CoVar]
bndrs')
         -- See Note [Printing foralls in type family instances] in GHC.Iface.Type
    , SDoc
pp_lhs SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> TidyEnv -> Type -> SDoc
ppr_rhs TidyEnv
tidy_env Type
ee_rhs
    , [SDoc] -> SDoc
forall doc. IsDoc doc => [doc] -> doc
vcat [ String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"-- Defined" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> SDoc
pp_loc
           , Bool -> SDoc -> SDoc
forall doc. IsOutput doc => Bool -> doc -> doc
ppUnless ([CoAxBranch] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [CoAxBranch]
incomps) (SDoc -> SDoc) -> SDoc -> SDoc
forall a b. (a -> b) -> a -> b
$ SDoc -> SDoc
forall doc. IsOutput doc => doc -> doc
whenPprDebug (SDoc -> SDoc) -> SDoc -> SDoc
forall a b. (a -> b) -> a -> b
$
             String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"-- Incomps:" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> [SDoc] -> SDoc
forall doc. IsDoc doc => [doc] -> doc
vcat ((CoAxBranch -> SDoc) -> [CoAxBranch] -> [SDoc]
forall a b. (a -> b) -> [a] -> [b]
map (TyCon -> CoAxBranch -> SDoc
pprCoAxBranch TyCon
fam_tc) [CoAxBranch]
incomps) ]
    ]
  where
    incomps :: [CoAxBranch]
incomps = CoAxBranch -> [CoAxBranch]
coAxBranchIncomps CoAxBranch
branch
    loc :: SrcSpan
loc = CoAxBranch -> SrcSpan
coAxBranchSpan CoAxBranch
branch
    pp_loc :: SDoc
pp_loc | SrcSpan -> Bool
isGoodSrcSpan SrcSpan
loc = String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"at" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> SrcLoc -> SDoc
forall a. Outputable a => a -> SDoc
ppr (SrcSpan -> SrcLoc
srcSpanStart SrcSpan
loc)
           | Bool
otherwise         = String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"in" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> SrcSpan -> SDoc
forall a. Outputable a => a -> SDoc
ppr SrcSpan
loc

    -- Eta-expand LHS and RHS types, because sometimes data family
    -- instances are eta-reduced.
    -- See Note [Eta reduction for data families] in GHC.Core.Coercion.Axiom.
    ([CoVar]
ee_tvs, [Type]
ee_lhs, Type
ee_rhs) = CoAxBranch -> ([CoVar], [Type], Type)
etaExpandCoAxBranch CoAxBranch
branch

    pp_lhs :: SDoc
pp_lhs = PprPrec -> IfaceTyCon -> IfaceAppArgs -> SDoc
pprIfaceTypeApp PprPrec
topPrec (TyCon -> IfaceTyCon
toIfaceTyCon TyCon
fam_tc)
                             (TidyEnv -> TyCon -> [Type] -> IfaceAppArgs
tidyToIfaceTcArgs TidyEnv
tidy_env TyCon
fam_tc [Type]
ee_lhs)

    (TidyEnv
tidy_env, [CoVar]
bndrs') = TidyEnv -> [CoVar] -> (TidyEnv, [CoVar])
tidyCoAxBndrsForUser TidyEnv
emptyTidyEnv [CoVar]
ee_tvs

tidyCoAxBndrsForUser :: TidyEnv -> [Var] -> (TidyEnv, [Var])
-- Tidy wildcards "_1", "_2" to "_", and do not return them
-- in the list of binders to be printed
-- This is so that in error messages we see
--     forall a. F _ [a] _ = ...
-- rather than
--     forall a _1 _2. F _1 [a] _2 = ...
--
-- This is a rather disgusting function
-- See Note [Wildcard names] in GHC.Tc.Gen.HsType
tidyCoAxBndrsForUser :: TidyEnv -> [CoVar] -> (TidyEnv, [CoVar])
tidyCoAxBndrsForUser TidyEnv
init_env [CoVar]
tcvs
  = (TidyEnv
tidy_env, [CoVar] -> [CoVar]
forall a. [a] -> [a]
reverse [CoVar]
tidy_bndrs)
  where
    (TidyEnv
tidy_env, [CoVar]
tidy_bndrs) = ((TidyEnv, [CoVar]) -> CoVar -> (TidyEnv, [CoVar]))
-> (TidyEnv, [CoVar]) -> [CoVar] -> (TidyEnv, [CoVar])
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl (TidyEnv, [CoVar]) -> CoVar -> (TidyEnv, [CoVar])
tidy_one (TidyEnv
init_env, []) [CoVar]
tcvs

    tidy_one :: (TidyEnv, [CoVar]) -> CoVar -> (TidyEnv, [CoVar])
tidy_one (env :: TidyEnv
env@(TidyOccEnv
occ_env, VarEnv CoVar
subst), [CoVar]
rev_bndrs') CoVar
bndr
      | CoVar -> Bool
is_wildcard CoVar
bndr = (TidyEnv
env_wild, [CoVar]
rev_bndrs')
      | Bool
otherwise        = (TidyEnv
env',     CoVar
bndr' CoVar -> [CoVar] -> [CoVar]
forall a. a -> [a] -> [a]
: [CoVar]
rev_bndrs')
      where
        (TidyEnv
env', CoVar
bndr') = TidyEnv -> CoVar -> (TidyEnv, CoVar)
tidyVarBndr TidyEnv
env CoVar
bndr
        env_wild :: TidyEnv
env_wild = (TidyOccEnv
occ_env, VarEnv CoVar -> CoVar -> CoVar -> VarEnv CoVar
forall a. VarEnv a -> CoVar -> a -> VarEnv a
extendVarEnv VarEnv CoVar
subst CoVar
bndr CoVar
wild_bndr)
        wild_bndr :: CoVar
wild_bndr = CoVar -> Name -> CoVar
setVarName CoVar
bndr (Name -> CoVar) -> Name -> CoVar
forall a b. (a -> b) -> a -> b
$
                    Name -> OccName -> Name
tidyNameOcc (CoVar -> Name
varName CoVar
bndr) (FastString -> OccName
mkTyVarOccFS (String -> FastString
fsLit String
"_"))
                    -- Tidy the binder to "_"

    is_wildcard :: Var -> Bool
    is_wildcard :: CoVar -> Bool
is_wildcard CoVar
tv = case OccName -> String
occNameString (CoVar -> OccName
forall a. NamedThing a => a -> OccName
getOccName CoVar
tv) of
                       (Char
'_' : String
rest) -> (Char -> Bool) -> String -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all Char -> Bool
isDigit String
rest
                       String
_            -> Bool
False


{- *********************************************************************
*                                                                      *
              MCoercion
*                                                                      *
********************************************************************* -}

coToMCo :: Coercion -> MCoercion
-- Convert a coercion to a MCoercion,
-- It's not clear whether or not isReflexiveCo would be better here
--    See #19815 for a bit of data and discussion on this point
coToMCo :: Coercion -> MCoercion
coToMCo Coercion
co | Coercion -> Bool
isReflCo Coercion
co = MCoercion
MRefl
           | Bool
otherwise   = Coercion -> MCoercion
MCo Coercion
co

checkReflexiveMCo :: MCoercion -> MCoercion
checkReflexiveMCo :: MCoercion -> MCoercion
checkReflexiveMCo MCoercion
MRefl                       = MCoercion
MRefl
checkReflexiveMCo (MCo Coercion
co) | Coercion -> Bool
isReflexiveCo Coercion
co = MCoercion
MRefl
                           | Bool
otherwise        = Coercion -> MCoercion
MCo Coercion
co

-- | Tests if this MCoercion is obviously generalized reflexive
-- Guaranteed to work very quickly.
isGReflMCo :: MCoercion -> Bool
isGReflMCo :: MCoercion -> Bool
isGReflMCo MCoercion
MRefl = Bool
True
isGReflMCo (MCo Coercion
co) | Coercion -> Bool
isGReflCo Coercion
co = Bool
True
isGReflMCo MCoercion
_ = Bool
False

-- | Make a generalized reflexive coercion
mkGReflCo :: Role -> Type -> MCoercionN -> Coercion
mkGReflCo :: Role -> Type -> MCoercion -> Coercion
mkGReflCo Role
r Type
ty MCoercion
mco
  | MCoercion -> Bool
isGReflMCo MCoercion
mco = if Role
r Role -> Role -> Bool
forall a. Eq a => a -> a -> Bool
== Role
Nominal then Type -> Coercion
Refl Type
ty
                     else Role -> Type -> MCoercion -> Coercion
GRefl Role
r Type
ty MCoercion
MRefl
  | Bool
otherwise    = Role -> Type -> MCoercion -> Coercion
GRefl Role
r Type
ty MCoercion
mco

-- | Compose two MCoercions via transitivity
mkTransMCo :: MCoercion -> MCoercion -> MCoercion
mkTransMCo :: MCoercion -> MCoercion -> MCoercion
mkTransMCo MCoercion
MRefl     MCoercion
co2       = MCoercion
co2
mkTransMCo MCoercion
co1       MCoercion
MRefl     = MCoercion
co1
mkTransMCo (MCo Coercion
co1) (MCo Coercion
co2) = Coercion -> MCoercion
MCo (Coercion -> Coercion -> Coercion
mkTransCo Coercion
co1 Coercion
co2)

mkTransMCoL :: MCoercion -> Coercion -> MCoercion
mkTransMCoL :: MCoercion -> Coercion -> MCoercion
mkTransMCoL MCoercion
MRefl     Coercion
co2 = Coercion -> MCoercion
coToMCo Coercion
co2
mkTransMCoL (MCo Coercion
co1) Coercion
co2 = Coercion -> MCoercion
MCo (Coercion -> Coercion -> Coercion
mkTransCo Coercion
co1 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)

-- | 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)

-- | 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

mkPiMCos :: [Var] -> MCoercion -> MCoercion
mkPiMCos :: [CoVar] -> MCoercion -> MCoercion
mkPiMCos [CoVar]
_ MCoercion
MRefl = MCoercion
MRefl
mkPiMCos [CoVar]
vs (MCo Coercion
co) = Coercion -> MCoercion
MCo (Role -> [CoVar] -> Coercion -> Coercion
mkPiCos Role
Representational [CoVar]
vs Coercion
co)

mkFunResMCo :: Id -> MCoercionR -> MCoercionR
mkFunResMCo :: CoVar -> MCoercion -> MCoercion
mkFunResMCo CoVar
_      MCoercion
MRefl    = MCoercion
MRefl
mkFunResMCo CoVar
arg_id (MCo Coercion
co) = Coercion -> MCoercion
MCo (Role -> CoVar -> Coercion -> Coercion
mkFunResCo Role
Representational CoVar
arg_id Coercion
co)

mkGReflLeftMCo :: Role -> Type -> MCoercionN -> 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 -> MCoercionN -> 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

-- | Like 'mkCoherenceRightCo', but with an 'MCoercion'
mkCoherenceRightMCo :: Role -> Type -> MCoercionN -> 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

isReflMCo :: MCoercion -> Bool
isReflMCo :: MCoercion -> Bool
isReflMCo MCoercion
MRefl = Bool
True
isReflMCo MCoercion
_     = Bool
False

{-
%************************************************************************
%*                                                                      *
        Destructing coercions
%*                                                                      *
%************************************************************************
-}

-- | This breaks a 'Coercion' with type @T A B C ~ T D E F@ into
-- a list of 'Coercion's of kinds @A ~ D@, @B ~ E@ and @E ~ F@. Hence:
--
-- > decomposeCo 3 c [r1, r2, r3] = [nth r1 0 c, nth r2 1 c, nth r3 2 c]
decomposeCo :: Arity -> Coercion
            -> Infinite Role  -- the roles of the output coercions
            -> [Coercion]
decomposeCo :: Arity -> Coercion -> Infinite Role -> [Coercion]
decomposeCo Arity
arity Coercion
co Infinite Role
rs
  = [HasDebugCallStack => CoSel -> Coercion -> Coercion
CoSel -> Coercion -> Coercion
mkSelCo (Arity -> Role -> CoSel
SelTyCon Arity
n Role
r) Coercion
co | (Arity
n,Role
r) <- [Arity
0..(Arity
arityArity -> Arity -> Arity
forall a. Num a => a -> a -> a
-Arity
1)] [Arity] -> [Role] -> [(Arity, Role)]
forall a b. [a] -> [b] -> [(a, b)]
`zip` Infinite Role -> [Role]
forall a. Infinite a -> [a]
Inf.toList Infinite Role
rs ]
     -- Remember, SelTyCon is zero-indexed

decomposeFunCo :: HasDebugCallStack
               => Coercion  -- Input coercion
               -> (CoercionN, Coercion, Coercion)
-- Expects co :: (s1 %m1-> t1) ~ (s2 %m2-> t2)
-- Returns (cow :: m1 ~N m2, co1 :: s1~s2, co2 :: t1~t2)
-- actually cow will be a Phantom coercion if the input is a Phantom coercion

decomposeFunCo :: HasDebugCallStack => Coercion -> (Coercion, Coercion, Coercion)
decomposeFunCo (FunCo { fco_mult :: Coercion -> Coercion
fco_mult = Coercion
w, fco_arg :: Coercion -> Coercion
fco_arg = Coercion
co1, fco_res :: Coercion -> Coercion
fco_res = Coercion
co2 })
  = (Coercion
w, Coercion
co1, Coercion
co2)
   -- Short-circuits the calls to mkSelCo

decomposeFunCo Coercion
co
  = Bool
-> SDoc
-> (Coercion, Coercion, Coercion)
-> (Coercion, Coercion, Coercion)
forall a. HasCallStack => Bool -> SDoc -> a -> a
assertPpr Bool
all_ok (Coercion -> SDoc
forall a. Outputable a => a -> SDoc
ppr Coercion
co) ((Coercion, Coercion, Coercion) -> (Coercion, Coercion, Coercion))
-> (Coercion, Coercion, Coercion) -> (Coercion, Coercion, Coercion)
forall a b. (a -> b) -> a -> b
$
    ( HasDebugCallStack => CoSel -> Coercion -> Coercion
CoSel -> Coercion -> Coercion
mkSelCo (FunSel -> CoSel
SelFun FunSel
SelMult) Coercion
co
    , HasDebugCallStack => CoSel -> Coercion -> Coercion
CoSel -> Coercion -> Coercion
mkSelCo (FunSel -> CoSel
SelFun FunSel
SelArg) Coercion
co
    , HasDebugCallStack => CoSel -> Coercion -> Coercion
CoSel -> Coercion -> Coercion
mkSelCo (FunSel -> CoSel
SelFun FunSel
SelRes) Coercion
co )
  where
    Pair Type
s1t1 Type
s2t2 = HasDebugCallStack => Coercion -> Pair Type
Coercion -> Pair Type
coercionKind Coercion
co
    all_ok :: Bool
all_ok = Type -> Bool
isFunTy Type
s1t1 Bool -> Bool -> Bool
&& Type -> Bool
isFunTy Type
s2t2

{- Note [Pushing a coercion into a pi-type]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Suppose we have this:
    (f |> co) t1 .. tn
Then we want to push the coercion into the arguments, so as to make
progress. For example of why you might want to do so, see Note
[Respecting definitional equality] in GHC.Core.TyCo.Rep.

This is done by decomposePiCos.  Specifically, if
    decomposePiCos co [t1,..,tn] = ([co1,...,cok], cor)
then
    (f |> co) t1 .. tn   =   (f (t1 |> co1) ... (tk |> cok)) |> cor) t(k+1) ... tn

Notes:

* k can be smaller than n! That is decomposePiCos can return *fewer*
  coercions than there are arguments (ie k < n), if the kind provided
  doesn't have enough binders.

* If there is a type error, we might see
       (f |> co) t1
  where co :: (forall a. ty) ~ (ty1 -> ty2)
  Here 'co' is insoluble, but we don't want to crash in decoposePiCos.
  So decomposePiCos carefully tests both sides of the coercion to check
  they are both foralls or both arrows.  Not doing this caused #15343.
-}

decomposePiCos :: HasDebugCallStack
               => CoercionN -> Pair Type  -- Coercion and its kind
               -> [Type]
               -> ([CoercionN], CoercionN)
-- See Note [Pushing a coercion into a pi-type]
decomposePiCos :: HasDebugCallStack =>
Coercion -> Pair Type -> [Type] -> ([Coercion], Coercion)
decomposePiCos Coercion
orig_co (Pair Type
orig_k1 Type
orig_k2) [Type]
orig_args
  = [Coercion]
-> (Subst, Type)
-> Coercion
-> (Subst, Type)
-> [Type]
-> ([Coercion], Coercion)
go [] (Subst
orig_subst,Type
orig_k1) Coercion
orig_co (Subst
orig_subst,Type
orig_k2) [Type]
orig_args
  where
    orig_subst :: Subst
orig_subst = InScopeSet -> Subst
mkEmptySubst (InScopeSet -> Subst) -> InScopeSet -> Subst
forall a b. (a -> b) -> a -> b
$ VarSet -> InScopeSet
mkInScopeSet (VarSet -> InScopeSet) -> VarSet -> InScopeSet
forall a b. (a -> b) -> a -> b
$
                 [Type] -> VarSet
tyCoVarsOfTypes [Type]
orig_args VarSet -> VarSet -> VarSet
`unionVarSet` Coercion -> VarSet
tyCoVarsOfCo Coercion
orig_co

    go :: [CoercionN]      -- accumulator for argument coercions, reversed
       -> (Subst,Kind)  -- Lhs kind of coercion
       -> CoercionN        -- coercion originally applied to the function
       -> (Subst,Kind)  -- Rhs kind of coercion
       -> [Type]           -- Arguments to that function
       -> ([CoercionN], Coercion)
    -- Invariant:  co :: subst1(k1) ~ subst2(k2)

    go :: [Coercion]
-> (Subst, Type)
-> Coercion
-> (Subst, Type)
-> [Type]
-> ([Coercion], Coercion)
go [Coercion]
acc_arg_cos (Subst
subst1,Type
k1) Coercion
co (Subst
subst2,Type
k2) (Type
ty:[Type]
tys)
      | Just (CoVar
a, Type
t1) <- Type -> Maybe (CoVar, Type)
splitForAllTyCoVar_maybe Type
k1
      , Just (CoVar
b, Type
t2) <- Type -> Maybe (CoVar, Type)
splitForAllTyCoVar_maybe Type
k2
        -- know     co :: (forall a:s1.t1) ~ (forall b:s2.t2)
        --    function :: forall a:s1.t1   (the function is not passed to decomposePiCos)
        --           a :: s1
        --           b :: s2
        --          ty :: s2
        -- need arg_co :: s2 ~ s1
        --      res_co :: t1[ty |> arg_co / a] ~ t2[ty / b]
      = let arg_co :: Coercion
arg_co  = HasDebugCallStack => CoSel -> Coercion -> Coercion
CoSel -> Coercion -> Coercion
mkSelCo CoSel
SelForAll (Coercion -> Coercion
mkSymCo Coercion
co)
            res_co :: Coercion
res_co  = Coercion -> Coercion -> Coercion
mkInstCo Coercion
co (Role -> Type -> Coercion -> Coercion
mkGReflLeftCo Role
Nominal Type
ty Coercion
arg_co)
            subst1' :: Subst
subst1' = Subst -> CoVar -> Type -> Subst
extendTCvSubst Subst
subst1 CoVar
a (Type
ty Type -> Coercion -> Type
`CastTy` Coercion
arg_co)
            subst2' :: Subst
subst2' = Subst -> CoVar -> Type -> Subst
extendTCvSubst Subst
subst2 CoVar
b Type
ty
        in
        [Coercion]
-> (Subst, Type)
-> Coercion
-> (Subst, Type)
-> [Type]
-> ([Coercion], Coercion)
go (Coercion
arg_co Coercion -> [Coercion] -> [Coercion]
forall a. a -> [a] -> [a]
: [Coercion]
acc_arg_cos) (Subst
subst1', Type
t1) Coercion
res_co (Subst
subst2', Type
t2) [Type]
tys

      | Just (FunTyFlag
af1, Type
_w1, Type
_s1, Type
t1) <- Type -> Maybe (FunTyFlag, Type, Type, Type)
splitFunTy_maybe Type
k1
      , Just (FunTyFlag
af2, Type
_w1, Type
_s2, Type
t2) <- Type -> Maybe (FunTyFlag, Type, Type, Type)
splitFunTy_maybe Type
k2
      , FunTyFlag
af1 FunTyFlag -> FunTyFlag -> Bool
forall a. Eq a => a -> a -> Bool
== FunTyFlag
af2  -- Same sort of arrow
        -- know     co :: (s1 -> t1) ~ (s2 -> t2)
        --    function :: s1 -> t1
        --          ty :: s2
        -- need arg_co :: s2 ~ s1
        --      res_co :: t1 ~ t2
      = let (Coercion
_, Coercion
sym_arg_co, Coercion
res_co) = HasDebugCallStack => Coercion -> (Coercion, Coercion, Coercion)
Coercion -> (Coercion, Coercion, Coercion)
decomposeFunCo Coercion
co
            -- It should be fine to ignore the multiplicity bit
            -- of the coercion for a Nominal coercion.
            arg_co :: Coercion
arg_co = Coercion -> Coercion
mkSymCo Coercion
sym_arg_co
        in
        [Coercion]
-> (Subst, Type)
-> Coercion
-> (Subst, Type)
-> [Type]
-> ([Coercion], Coercion)
go (Coercion
arg_co Coercion -> [Coercion] -> [Coercion]
forall a. a -> [a] -> [a]
: [Coercion]
acc_arg_cos) (Subst
subst1,Type
t1) Coercion
res_co (Subst
subst2,Type
t2) [Type]
tys

      | Bool -> Bool
not (Subst -> Bool
isEmptyTCvSubst Subst
subst1) Bool -> Bool -> Bool
|| Bool -> Bool
not (Subst -> Bool
isEmptyTCvSubst Subst
subst2)
      = [Coercion]
-> (Subst, Type)
-> Coercion
-> (Subst, Type)
-> [Type]
-> ([Coercion], Coercion)
go [Coercion]
acc_arg_cos (Subst -> Subst
zapSubst Subst
subst1, HasDebugCallStack => Subst -> Type -> Type
Subst -> Type -> Type
substTy Subst
subst1 Type
k1)
                       Coercion
co
                       (Subst -> Subst
zapSubst Subst
subst2, HasDebugCallStack => Subst -> Type -> Type
Subst -> Type -> Type
substTy Subst
subst1 Type
k2)
                       (Type
tyType -> [Type] -> [Type]
forall a. a -> [a] -> [a]
:[Type]
tys)

      -- tys might not be empty, if the left-hand type of the original coercion
      -- didn't have enough binders
    go [Coercion]
acc_arg_cos (Subst, Type)
_ki1 Coercion
co (Subst, Type)
_ki2 [Type]
_tys = ([Coercion] -> [Coercion]
forall a. [a] -> [a]
reverse [Coercion]
acc_arg_cos, Coercion
co)

-- | Extract a covar, if possible. This check is dirty. Be ashamed
-- of yourself. (It's dirty because it cares about the structure of
-- a coercion, which is morally reprehensible.)
getCoVar_maybe :: Coercion -> Maybe CoVar
getCoVar_maybe :: Coercion -> Maybe CoVar
getCoVar_maybe (CoVarCo CoVar
cv) = CoVar -> Maybe CoVar
forall a. a -> Maybe a
Just CoVar
cv
getCoVar_maybe Coercion
_            = Maybe CoVar
forall a. Maybe a
Nothing

multToCo :: Mult -> Coercion
multToCo :: Type -> Coercion
multToCo Type
r = Type -> Coercion
mkNomReflCo Type
r

-- first result has role equal to input; third result is Nominal
splitAppCo_maybe :: Coercion -> Maybe (Coercion, Coercion)
-- ^ Attempt to take a coercion application apart.
splitAppCo_maybe :: Coercion -> Maybe (Coercion, Coercion)
splitAppCo_maybe (AppCo Coercion
co Coercion
arg) = (Coercion, Coercion) -> Maybe (Coercion, Coercion)
forall a. a -> Maybe a
Just (Coercion
co, Coercion
arg)
splitAppCo_maybe (TyConAppCo Role
r TyCon
tc [Coercion]
args)
  | [Coercion]
args [Coercion] -> Arity -> Bool
forall a. [a] -> Arity -> Bool
`lengthExceeds` TyCon -> Arity
tyConArity TyCon
tc
  , Just ([Coercion]
args', Coercion
arg') <- [Coercion] -> Maybe ([Coercion], Coercion)
forall a. [a] -> Maybe ([a], a)
snocView [Coercion]
args
  = (Coercion, Coercion) -> Maybe (Coercion, Coercion)
forall a. a -> Maybe a
Just ( HasDebugCallStack => Role -> TyCon -> [Coercion] -> Coercion
Role -> TyCon -> [Coercion] -> Coercion
mkTyConAppCo Role
r TyCon
tc [Coercion]
args', Coercion
arg' )

  | Bool -> Bool
not (TyCon -> Bool
tyConMustBeSaturated TyCon
tc)
    -- Never create unsaturated type family apps!
  , Just ([Coercion]
args', Coercion
arg') <- [Coercion] -> Maybe ([Coercion], Coercion)
forall a. [a] -> Maybe ([a], a)
snocView [Coercion]
args
  , Just Coercion
arg'' <- Role -> Coercion -> Maybe Coercion
setNominalRole_maybe (Role -> TyCon -> Arity -> Role
tyConRole Role
r TyCon
tc ([Coercion] -> Arity
forall a. [a] -> Arity
forall (t :: * -> *) a. Foldable t => t a -> Arity
length [Coercion]
args')) Coercion
arg'
  = (Coercion, Coercion) -> Maybe (Coercion, Coercion)
forall a. a -> Maybe a
Just ( HasDebugCallStack => Role -> TyCon -> [Coercion] -> Coercion
Role -> TyCon -> [Coercion] -> Coercion
mkTyConAppCo Role
r TyCon
tc [Coercion]
args', Coercion
arg'' )
       -- Use mkTyConAppCo to preserve the invariant
       --  that identity coercions are always represented by Refl

splitAppCo_maybe Coercion
co
  | Just (Type
ty, Role
r) <- Coercion -> Maybe (Type, Role)
isReflCo_maybe Coercion
co
  , Just (Type
ty1, Type
ty2) <- Type -> Maybe (Type, Type)
splitAppTy_maybe Type
ty
  = (Coercion, Coercion) -> Maybe (Coercion, Coercion)
forall a. a -> Maybe a
Just (Role -> Type -> Coercion
mkReflCo Role
r Type
ty1, Type -> Coercion
mkNomReflCo Type
ty2)
splitAppCo_maybe Coercion
_ = Maybe (Coercion, Coercion)
forall a. Maybe a
Nothing

-- Only used in specialise/Rules
splitFunCo_maybe :: Coercion -> Maybe (Coercion, Coercion)
splitFunCo_maybe :: Coercion -> Maybe (Coercion, Coercion)
splitFunCo_maybe (FunCo { fco_arg :: Coercion -> Coercion
fco_arg = Coercion
arg, fco_res :: Coercion -> Coercion
fco_res = Coercion
res }) = (Coercion, Coercion) -> Maybe (Coercion, Coercion)
forall a. a -> Maybe a
Just (Coercion
arg, Coercion
res)
splitFunCo_maybe Coercion
_ = Maybe (Coercion, Coercion)
forall a. Maybe a
Nothing

splitForAllCo_maybe :: Coercion -> Maybe (TyCoVar, ForAllTyFlag, ForAllTyFlag, Coercion, Coercion)
splitForAllCo_maybe :: Coercion
-> Maybe (CoVar, ForAllTyFlag, ForAllTyFlag, Coercion, Coercion)
splitForAllCo_maybe (ForAllCo { fco_tcv :: Coercion -> CoVar
fco_tcv = CoVar
tv, fco_visL :: Coercion -> ForAllTyFlag
fco_visL = ForAllTyFlag
vL, fco_visR :: Coercion -> ForAllTyFlag
fco_visR = ForAllTyFlag
vR
                              , fco_kind :: Coercion -> Coercion
fco_kind = Coercion
k_co, fco_body :: Coercion -> Coercion
fco_body = Coercion
co })
  = (CoVar, ForAllTyFlag, ForAllTyFlag, Coercion, Coercion)
-> Maybe (CoVar, ForAllTyFlag, ForAllTyFlag, Coercion, Coercion)
forall a. a -> Maybe a
Just (CoVar
tv, ForAllTyFlag
vL, ForAllTyFlag
vR, Coercion
k_co, Coercion
co)
splitForAllCo_maybe Coercion
co
  | Just (Type
ty, Role
r)        <- Coercion -> Maybe (Type, Role)
isReflCo_maybe Coercion
co
  , Just (Bndr CoVar
tcv ForAllTyFlag
vis, Type
body_ty) <- Type -> Maybe (ForAllTyBinder, Type)
splitForAllForAllTyBinder_maybe Type
ty
  = (CoVar, ForAllTyFlag, ForAllTyFlag, Coercion, Coercion)
-> Maybe (CoVar, ForAllTyFlag, ForAllTyFlag, Coercion, Coercion)
forall a. a -> Maybe a
Just (CoVar
tcv, ForAllTyFlag
vis, ForAllTyFlag
vis, Type -> Coercion
mkNomReflCo (CoVar -> Type
varType CoVar
tcv), Role -> Type -> Coercion
mkReflCo Role
r Type
body_ty)
splitForAllCo_maybe Coercion
_ = Maybe (CoVar, ForAllTyFlag, ForAllTyFlag, Coercion, Coercion)
forall a. Maybe a
Nothing

-- | Like 'splitForAllCo_maybe', but only returns Just for tyvar binder
splitForAllCo_ty_maybe :: Coercion -> Maybe (TyVar, ForAllTyFlag, ForAllTyFlag, Coercion, Coercion)
splitForAllCo_ty_maybe :: Coercion
-> Maybe (CoVar, ForAllTyFlag, ForAllTyFlag, Coercion, Coercion)
splitForAllCo_ty_maybe Coercion
co
  | Just stuff :: (CoVar, ForAllTyFlag, ForAllTyFlag, Coercion, Coercion)
stuff@(CoVar
tv, ForAllTyFlag
_, ForAllTyFlag
_, Coercion
_, Coercion
_) <- Coercion
-> Maybe (CoVar, ForAllTyFlag, ForAllTyFlag, Coercion, Coercion)
splitForAllCo_maybe Coercion
co
  , CoVar -> Bool
isTyVar CoVar
tv
  = (CoVar, ForAllTyFlag, ForAllTyFlag, Coercion, Coercion)
-> Maybe (CoVar, ForAllTyFlag, ForAllTyFlag, Coercion, Coercion)
forall a. a -> Maybe a
Just (CoVar, ForAllTyFlag, ForAllTyFlag, Coercion, Coercion)
stuff
splitForAllCo_ty_maybe Coercion
_ = Maybe (CoVar, ForAllTyFlag, ForAllTyFlag, Coercion, Coercion)
forall a. Maybe a
Nothing

-- | Like 'splitForAllCo_maybe', but only returns Just for covar binder
splitForAllCo_co_maybe :: Coercion -> Maybe (CoVar, ForAllTyFlag, ForAllTyFlag, Coercion, Coercion)
splitForAllCo_co_maybe :: Coercion
-> Maybe (CoVar, ForAllTyFlag, ForAllTyFlag, Coercion, Coercion)
splitForAllCo_co_maybe Coercion
co
  | Just stuff :: (CoVar, ForAllTyFlag, ForAllTyFlag, Coercion, Coercion)
stuff@(CoVar
cv, ForAllTyFlag
_, ForAllTyFlag
_, Coercion
_, Coercion
_) <- Coercion
-> Maybe (CoVar, ForAllTyFlag, ForAllTyFlag, Coercion, Coercion)
splitForAllCo_maybe Coercion
co
  , CoVar -> Bool
isCoVar CoVar
cv
  = (CoVar, ForAllTyFlag, ForAllTyFlag, Coercion, Coercion)
-> Maybe (CoVar, ForAllTyFlag, ForAllTyFlag, Coercion, Coercion)
forall a. a -> Maybe a
Just (CoVar, ForAllTyFlag, ForAllTyFlag, Coercion, Coercion)
stuff
splitForAllCo_co_maybe Coercion
_ = Maybe (CoVar, ForAllTyFlag, ForAllTyFlag, Coercion, Coercion)
forall a. Maybe a
Nothing

-------------------------------------------------------
-- and some coercion kind stuff

coVarLType, coVarRType :: HasDebugCallStack => CoVar -> Type
coVarLType :: HasDebugCallStack => CoVar -> Type
coVarLType CoVar
cv | (Type
ty1, Type
_, Role
_) <- HasDebugCallStack => CoVar -> (Type, Type, Role)
CoVar -> (Type, Type, Role)
coVarTypesRole CoVar
cv = Type
ty1
coVarRType :: HasDebugCallStack => CoVar -> Type
coVarRType CoVar
cv | (Type
_, Type
ty2, Role
_) <- HasDebugCallStack => CoVar -> (Type, Type, Role)
CoVar -> (Type, Type, Role)
coVarTypesRole CoVar
cv = Type
ty2

coVarTypes :: HasDebugCallStack => CoVar -> Pair Type
coVarTypes :: HasDebugCallStack => CoVar -> Pair Type
coVarTypes CoVar
cv | (Type
ty1, Type
ty2, Role
_) <- HasDebugCallStack => CoVar -> (Type, Type, Role)
CoVar -> (Type, Type, Role)
coVarTypesRole CoVar
cv = Type -> Type -> Pair Type
forall a. a -> a -> Pair a
Pair Type
ty1 Type
ty2

coVarTypesRole :: HasDebugCallStack => CoVar -> (Type,Type,Role)
coVarTypesRole :: HasDebugCallStack => CoVar -> (Type, Type, Role)
coVarTypesRole CoVar
cv
 | Just (TyCon
tc, [Type
_,Type
_,Type
ty1,Type
ty2]) <- HasDebugCallStack => Type -> Maybe (TyCon, [Type])
Type -> Maybe (TyCon, [Type])
splitTyConApp_maybe (CoVar -> Type
varType CoVar
cv)
 = (Type
ty1, Type
ty2, TyCon -> Role
eqTyConRole TyCon
tc)
 | Bool
otherwise
 = String -> SDoc -> (Type, Type, Role)
forall a. HasCallStack => String -> SDoc -> a
pprPanic String
"coVarTypesRole, non coercion variable"
            (CoVar -> SDoc
forall a. Outputable a => a -> SDoc
ppr CoVar
cv SDoc -> SDoc -> SDoc
forall doc. IsDoc doc => doc -> doc -> doc
$$ Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr (CoVar -> Type
varType CoVar
cv))

coVarKind :: CoVar -> Type
coVarKind :: CoVar -> Type
coVarKind CoVar
cv
  = Bool -> (CoVar -> Type) -> CoVar -> Type
forall a. HasCallStack => Bool -> a -> a
assert (CoVar -> Bool
isCoVar CoVar
cv )
    CoVar -> Type
varType CoVar
cv

coVarRole :: CoVar -> Role
coVarRole :: CoVar -> Role
coVarRole CoVar
cv
  = TyCon -> Role
eqTyConRole (case Type -> Maybe TyCon
tyConAppTyCon_maybe (CoVar -> Type
varType CoVar
cv) of
                   Just TyCon
tc0 -> TyCon
tc0
                   Maybe TyCon
Nothing  -> String -> SDoc -> TyCon
forall a. HasCallStack => String -> SDoc -> a
pprPanic String
"coVarRole: not tyconapp" (CoVar -> SDoc
forall a. Outputable a => a -> SDoc
ppr CoVar
cv))

eqTyConRole :: TyCon -> Role
-- Given (~#) or (~R#) return the Nominal or Representational respectively
eqTyConRole :: TyCon -> Role
eqTyConRole TyCon
tc
  | TyCon
tc TyCon -> Unique -> Bool
forall a. Uniquable a => a -> Unique -> Bool
`hasKey` Unique
eqPrimTyConKey
  = Role
Nominal
  | TyCon
tc TyCon -> Unique -> Bool
forall a. Uniquable a => a -> Unique -> Bool
`hasKey` Unique
eqReprPrimTyConKey
  = Role
Representational
  | Bool
otherwise
  = String -> SDoc -> Role
forall a. HasCallStack => String -> SDoc -> a
pprPanic String
"eqTyConRole: unknown tycon" (TyCon -> SDoc
forall a. Outputable a => a -> SDoc
ppr TyCon
tc)

-- | Given a coercion `co :: (t1 :: TYPE r1) ~ (t2 :: TYPE r2)`
-- produce a coercion `rep_co :: r1 ~ r2`
-- But actually it is possible that
--     co :: (t1 :: CONSTRAINT r1) ~ (t2 :: CONSTRAINT r2)
-- or  co :: (t1 :: TYPE r1)       ~ (t2 :: CONSTRAINT r2)
-- or  co :: (t1 :: CONSTRAINT r1) ~ (t2 :: TYPE r2)
-- See Note [mkRuntimeRepCo]
mkRuntimeRepCo :: HasDebugCallStack => Coercion -> Coercion
mkRuntimeRepCo :: HasDebugCallStack => Coercion -> Coercion
mkRuntimeRepCo Coercion
co
  = Bool -> Coercion -> Coercion
forall a. HasCallStack => Bool -> a -> a
assert (Type -> Bool
isTYPEorCONSTRAINT Type
k1 Bool -> Bool -> Bool
&& Type -> Bool
isTYPEorCONSTRAINT Type
k2) (Coercion -> Coercion) -> Coercion -> Coercion
forall a b. (a -> b) -> a -> b
$
    HasDebugCallStack => CoSel -> Coercion -> Coercion
CoSel -> Coercion -> Coercion
mkSelCo (Arity -> Role -> CoSel
SelTyCon Arity
0 Role
Nominal) Coercion
kind_co
  where
    kind_co :: Coercion
kind_co = Coercion -> Coercion
mkKindCo Coercion
co  -- kind_co :: TYPE r1 ~ TYPE r2
    Pair Type
k1 Type
k2 = HasDebugCallStack => Coercion -> Pair Type
Coercion -> Pair Type
coercionKind Coercion
kind_co

{- Note [mkRuntimeRepCo]
~~~~~~~~~~~~~~~~~~~~~~~~
Given
   class C a where { op :: Maybe a }
we will get an axiom
   axC a :: (C a :: CONSTRAINT r1) ~ (Maybe a :: TYPE r2)
(See Note [Type and Constraint are not apart] in GHC.Builtin.Types.Prim.)

Then we may call mkRuntimeRepCo on (axC ty), and that will return
   mkSelCo (SelTyCon 0 Nominal) (Kind (axC ty)) :: r1 ~ r2

So mkSelCo needs to be happy with decomposing a coercion of kind
   CONSTRAINT r1 ~ TYPE r2

Hence the use of `tyConIsTYPEorCONSTRAINT` in the assertion `good_call`
in `mkSelCo`. See #23018 for a concrete example.  (In this context it's
important that TYPE and CONSTRAINT have the same arity and kind, not
merely that they are not-apart; otherwise SelCo would not make sense.)
-}

isReflCoVar_maybe :: Var -> Maybe Coercion
-- If cv :: t~t then isReflCoVar_maybe cv = Just (Refl t)
-- Works on all kinds of Vars, not just CoVars
isReflCoVar_maybe :: CoVar -> Maybe Coercion
isReflCoVar_maybe CoVar
cv
  | CoVar -> Bool
isCoVar CoVar
cv
  , Pair Type
ty1 Type
ty2 <- HasDebugCallStack => CoVar -> Pair Type
CoVar -> Pair Type
coVarTypes CoVar
cv
  , Type
ty1 HasCallStack => Type -> Type -> Bool
Type -> Type -> Bool
`eqType` Type
ty2
  = Coercion -> Maybe Coercion
forall a. a -> Maybe a
Just (Role -> Type -> Coercion
mkReflCo (CoVar -> Role
coVarRole CoVar
cv) Type
ty1)
  | Bool
otherwise
  = Maybe Coercion
forall a. Maybe a
Nothing

-- | Tests if this coercion is obviously a generalized reflexive coercion.
-- Guaranteed to work very quickly.
isGReflCo :: Coercion -> Bool
isGReflCo :: Coercion -> Bool
isGReflCo (GRefl{}) = Bool
True
isGReflCo (Refl{})  = Bool
True -- Refl ty == GRefl N ty MRefl
isGReflCo Coercion
_         = Bool
False

-- | Tests if this coercion is obviously reflexive. Guaranteed to work
-- very quickly. Sometimes a coercion can be reflexive, but not obviously
-- so. c.f. 'isReflexiveCo'
isReflCo :: Coercion -> Bool
isReflCo :: Coercion -> Bool
isReflCo (Refl{}) = Bool
True
isReflCo (GRefl Role
_ Type
_ MCoercion
mco) | MCoercion -> Bool
isGReflMCo MCoercion
mco = Bool
True
isReflCo Coercion
_ = Bool
False

-- | Returns the type coerced if this coercion is a generalized reflexive
-- coercion. Guaranteed to work very quickly.
isGReflCo_maybe :: Coercion -> Maybe (Type, Role)
isGReflCo_maybe :: Coercion -> Maybe (Type, Role)
isGReflCo_maybe (GRefl Role
r Type
ty MCoercion
_) = (Type, Role) -> Maybe (Type, Role)
forall a. a -> Maybe a
Just (Type
ty, Role
r)
isGReflCo_maybe (Refl Type
ty)      = (Type, Role) -> Maybe (Type, Role)
forall a. a -> Maybe a
Just (Type
ty, Role
Nominal)
isGReflCo_maybe Coercion
_ = Maybe (Type, Role)
forall a. Maybe a
Nothing

-- | Returns the type coerced if this coercion is reflexive. Guaranteed
-- to work very quickly. Sometimes a coercion can be reflexive, but not
-- obviously so. c.f. 'isReflexiveCo_maybe'
isReflCo_maybe :: Coercion -> Maybe (Type, Role)
isReflCo_maybe :: Coercion -> Maybe (Type, Role)
isReflCo_maybe (Refl Type
ty) = (Type, Role) -> Maybe (Type, Role)
forall a. a -> Maybe a
Just (Type
ty, Role
Nominal)
isReflCo_maybe (GRefl Role
r Type
ty MCoercion
mco) | MCoercion -> Bool
isGReflMCo MCoercion
mco = (Type, Role) -> Maybe (Type, Role)
forall a. a -> Maybe a
Just (Type
ty, Role
r)
isReflCo_maybe Coercion
_ = Maybe (Type, Role)
forall a. Maybe a
Nothing

-- | Slowly checks if the coercion is reflexive. Don't call this in a loop,
-- as it walks over the entire coercion.
isReflexiveCo :: Coercion -> Bool
isReflexiveCo :: Coercion -> Bool
isReflexiveCo = Maybe (Type, Role) -> Bool
forall a. Maybe a -> Bool
isJust (Maybe (Type, Role) -> Bool)
-> (Coercion -> Maybe (Type, Role)) -> Coercion -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Coercion -> Maybe (Type, Role)
isReflexiveCo_maybe

-- | Extracts the coerced type from a reflexive coercion. This potentially
-- walks over the entire coercion, so avoid doing this in a loop.
isReflexiveCo_maybe :: Coercion -> Maybe (Type, Role)
isReflexiveCo_maybe :: Coercion -> Maybe (Type, Role)
isReflexiveCo_maybe (Refl Type
ty) = (Type, Role) -> Maybe (Type, Role)
forall a. a -> Maybe a
Just (Type
ty, Role
Nominal)
isReflexiveCo_maybe (GRefl Role
r Type
ty MCoercion
mco) | MCoercion -> Bool
isGReflMCo MCoercion
mco = (Type, Role) -> Maybe (Type, Role)
forall a. a -> Maybe a
Just (Type
ty, Role
r)
isReflexiveCo_maybe Coercion
co
  | Type
ty1 HasCallStack => Type -> Type -> Bool
Type -> Type -> Bool
`eqType` Type
ty2
  = (Type, Role) -> Maybe (Type, Role)
forall a. a -> Maybe a
Just (Type
ty1, Role
r)
  | Bool
otherwise
  = Maybe (Type, Role)
forall a. Maybe a
Nothing
  where (Pair Type
ty1 Type
ty2, Role
r) = Coercion -> (Pair Type, Role)
coercionKindRole Coercion
co


{-
%************************************************************************
%*                                                                      *
            Building coercions
%*                                                                      *
%************************************************************************

These "smart constructors" maintain the invariants listed in the definition
of Coercion, and they perform very basic optimizations.

Note [Role twiddling functions]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
There are a plethora of functions for twiddling roles:

mkSubCo: Requires a nominal input coercion and always produces a
representational output. This is used when you (the programmer) are sure you
know exactly that role you have and what you want.

downgradeRole_maybe: This function takes both the input role and the output role
as parameters. (The *output* role comes first!) It can only *downgrade* a
role -- that is, change it from N to R or P, or from R to P. This one-way
behavior is why there is the "_maybe". If an upgrade is requested, this
function produces Nothing. This is used when you need to change the role of a
coercion, but you're not sure (as you're writing the code) of which roles are
involved.

This function could have been written using coercionRole to ascertain the role
of the input. But, that function is recursive, and the caller of downgradeRole_maybe
often knows the input role. So, this is more efficient.

downgradeRole: This is just like downgradeRole_maybe, but it panics if the
conversion isn't a downgrade.

setNominalRole_maybe: This is the only function that can *upgrade* a coercion.
The result (if it exists) is always Nominal. The input can be at any role. It
works on a "best effort" basis, as it should never be strictly necessary to
upgrade a coercion during compilation. It is currently only used within GHC in
splitAppCo_maybe. In order to be a proper inverse of mkAppCo, the second
coercion that splitAppCo_maybe returns must be nominal. But, it's conceivable
that splitAppCo_maybe is operating over a TyConAppCo that uses a
representational coercion. Hence the need for setNominalRole_maybe.
splitAppCo_maybe, in turn, is used only within coercion optimization -- thus,
it is not absolutely critical that setNominalRole_maybe be complete.

Note that setNominalRole_maybe will never upgrade a phantom UnivCo. Phantom
UnivCos are perfectly type-safe, whereas representational and nominal ones are
not. (Nominal ones are no worse than representational ones, so this function *will*
change a UnivCo Representational to a UnivCo Nominal.)

Conal Elliott also came across a need for this function while working with the
GHC API, as he was decomposing Core casts. The Core casts use representational
coercions, as they must, but his use case required nominal coercions (he was
building a GADT). So, that's why this function is exported from this module.

One might ask: shouldn't downgradeRole_maybe just use setNominalRole_maybe as
appropriate? I (Richard E.) have decided not to do this, because upgrading a
role is bizarre and a caller should have to ask for this behavior explicitly.

-}

-- | Make a reflexive coercion
mkReflCo :: Role -> Type -> Coercion
mkReflCo :: Role -> Type -> Coercion
mkReflCo Role
Nominal Type
ty = Type -> Coercion
Refl Type
ty
mkReflCo Role
r       Type
ty = Role -> Type -> MCoercion -> Coercion
GRefl Role
r Type
ty MCoercion
MRefl

-- | Make a representational reflexive coercion
mkRepReflCo :: Type -> Coercion
mkRepReflCo :: Type -> Coercion
mkRepReflCo Type
ty = Role -> Type -> MCoercion -> Coercion
GRefl Role
Representational Type
ty MCoercion
MRefl

-- | Make a nominal reflexive coercion
mkNomReflCo :: Type -> Coercion
mkNomReflCo :: Type -> Coercion
mkNomReflCo = Type -> Coercion
Refl

-- | Apply a type constructor to a list of coercions. It is the
-- caller's responsibility to get the roles correct on argument coercions.
mkTyConAppCo :: HasDebugCallStack => Role -> TyCon -> [Coercion] -> Coercion
mkTyConAppCo :: HasDebugCallStack => Role -> TyCon -> [Coercion] -> Coercion
mkTyConAppCo Role
r TyCon
tc [Coercion]
cos
  | Just Coercion
co <- HasDebugCallStack => Role -> TyCon -> [Coercion] -> Maybe Coercion
Role -> TyCon -> [Coercion] -> Maybe Coercion
tyConAppFunCo_maybe Role
r TyCon
tc [Coercion]
cos
  = Coercion
co

  -- Expand type synonyms
  | ExpandsSyn [(CoVar, Coercion)]
tv_co_prs Type
rhs_ty [Coercion]
leftover_cos <- TyCon -> [Coercion] -> ExpandSynResult Coercion
forall tyco. TyCon -> [tyco] -> ExpandSynResult tyco
expandSynTyCon_maybe TyCon
tc [Coercion]
cos
  = Coercion -> [Coercion] -> Coercion
mkAppCos (HasDebugCallStack => Role -> LiftingContext -> Type -> Coercion
Role -> LiftingContext -> Type -> Coercion
liftCoSubst Role
r ([(CoVar, Coercion)] -> LiftingContext
mkLiftingContext [(CoVar, Coercion)]
tv_co_prs) Type
rhs_ty) [Coercion]
leftover_cos

  | Just [(Type, Role)]
tys_roles <- (Coercion -> Maybe (Type, Role))
-> [Coercion] -> Maybe [(Type, Role)]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> [a] -> f [b]
traverse Coercion -> Maybe (Type, Role)
isReflCo_maybe [Coercion]
cos
  = Role -> Type -> Coercion
mkReflCo Role
r (TyCon -> [Type] -> Type
mkTyConApp TyCon
tc (((Type, Role) -> Type) -> [(Type, Role)] -> [Type]
forall a b. (a -> b) -> [a] -> [b]
map (Type, Role) -> Type
forall a b. (a, b) -> a
fst [(Type, Role)]
tys_roles))
  -- See Note [Refl invariant]

  | Bool
otherwise = Role -> TyCon -> [Coercion] -> Coercion
TyConAppCo Role
r TyCon
tc [Coercion]
cos

mkFunCoNoFTF :: HasDebugCallStack => Role -> CoercionN -> Coercion -> Coercion -> Coercion
-- This version of mkFunCo takes no FunTyFlags; it works them out
mkFunCoNoFTF :: HasDebugCallStack =>
Role -> Coercion -> Coercion -> Coercion -> Coercion
mkFunCoNoFTF Role
r Coercion
w Coercion
arg_co Coercion
res_co
  = Role
-> FunTyFlag
-> FunTyFlag
-> Coercion
-> Coercion
-> Coercion
-> Coercion
mkFunCo2 Role
r FunTyFlag
afl FunTyFlag
afr Coercion
w Coercion
arg_co Coercion
res_co
  where
    afl :: FunTyFlag
afl = HasDebugCallStack => Type -> Type -> FunTyFlag
Type -> Type -> FunTyFlag
chooseFunTyFlag Type
argl_ty Type
resl_ty
    afr :: FunTyFlag
afr = HasDebugCallStack => Type -> Type -> FunTyFlag
Type -> Type -> FunTyFlag
chooseFunTyFlag Type
argr_ty Type
resr_ty
    Pair Type
argl_ty Type
argr_ty = HasDebugCallStack => Coercion -> Pair Type
Coercion -> Pair Type
coercionKind Coercion
arg_co
    Pair Type
resl_ty Type
resr_ty = HasDebugCallStack => Coercion -> Pair Type
Coercion -> Pair Type
coercionKind Coercion
res_co

-- | Build a function 'Coercion' from two other 'Coercion's. That is,
-- given @co1 :: a ~ b@ and @co2 :: x ~ y@ produce @co :: (a -> x) ~ (b -> y)@
-- or @(a => x) ~ (b => y)@, depending on the kind of @a@/@b@.
-- This (most common) version takes a single FunTyFlag, which is used
--   for both fco_afl and ftf_afr of the FunCo
mkFunCo :: Role -> FunTyFlag -> CoercionN -> Coercion -> Coercion -> Coercion
mkFunCo :: Role -> FunTyFlag -> Coercion -> Coercion -> Coercion -> Coercion
mkFunCo Role
r FunTyFlag
af Coercion
w Coercion
arg_co Coercion
res_co
  = Role
-> FunTyFlag
-> FunTyFlag
-> Coercion
-> Coercion
-> Coercion
-> Coercion
mkFunCo2 Role
r FunTyFlag
af FunTyFlag
af Coercion
w Coercion
arg_co Coercion
res_co

mkNakedFunCo :: Role -> FunTyFlag -> CoercionN -> Coercion -> Coercion -> Coercion
-- This version of mkFunCo does not check FunCo invariants (checkFunCo)
-- It's a historical vestige; See Note [No assertion check on mkFunCo]
mkNakedFunCo :: Role -> FunTyFlag -> Coercion -> Coercion -> Coercion -> Coercion
mkNakedFunCo = Role -> FunTyFlag -> Coercion -> Coercion -> Coercion -> Coercion
mkFunCo

mkFunCo2 :: Role -> FunTyFlag -> FunTyFlag
         -> CoercionN -> Coercion -> Coercion -> Coercion
-- This is the smart constructor for FunCo; it checks invariants
mkFunCo2 :: Role
-> FunTyFlag
-> FunTyFlag
-> Coercion
-> Coercion
-> Coercion
-> Coercion
mkFunCo2 Role
r FunTyFlag
afl FunTyFlag
afr Coercion
w Coercion
arg_co Coercion
res_co
  -- See Note [No assertion check on mkFunCo]
  | Just (Type
ty1, Role
_) <- Coercion -> Maybe (Type, Role)
isReflCo_maybe Coercion
arg_co
  , Just (Type
ty2, Role
_) <- Coercion -> Maybe (Type, Role)
isReflCo_maybe Coercion
res_co
  , Just (Type
w, Role
_)   <- Coercion -> Maybe (Type, Role)
isReflCo_maybe Coercion
w
  = Role -> Type -> Coercion
mkReflCo Role
r (HasDebugCallStack => FunTyFlag -> Type -> Type -> Type -> Type
FunTyFlag -> Type -> Type -> Type -> Type
mkFunTy FunTyFlag
afl Type
w Type
ty1 Type
ty2)  -- See Note [Refl invariant]

  | Bool
otherwise
  = FunCo { fco_role :: Role
fco_role = Role
r, fco_afl :: FunTyFlag
fco_afl = FunTyFlag
afl, fco_afr :: FunTyFlag
fco_afr = FunTyFlag
afr
          , fco_mult :: Coercion
fco_mult = Coercion
w, fco_arg :: Coercion
fco_arg = Coercion
arg_co, fco_res :: Coercion
fco_res = Coercion
res_co }


{- Note [No assertion check on mkFunCo]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
We used to have a checkFunCo assertion on mkFunCo, but during typechecking
we can (legitimately) have not-full-zonked types or coercion variables, so
the assertion spuriously fails (test T11480b is a case in point).  Lint
checks all these things anyway.

We used to get around the problem by calling mkNakedFunCo from within the
typechecker, which dodged the assertion check.  But then mkAppCo calls
mkTyConAppCo, which calls tyConAppFunCo_maybe, which calls mkFunCo.
Duplicating this stack of calls with "naked" versions of each seems too much.

-- Commented out: see Note [No assertion check on mkFunCo]
checkFunCo :: Role -> FunTyFlag -> FunTyFlag
           -> CoercionN -> Coercion -> Coercion
           -> Maybe SDoc
-- Checks well-formed-ness for FunCo
-- Used only in assertions and Lint
{-# NOINLINE checkFunCo #-}
checkFunCo _r afl afr _w arg_co res_co
  | not (ok argl_ty && ok argr_ty && ok resl_ty && ok resr_ty)
  = Just (hang (text "Bad arg or res types") 2 pp_inputs)

  | afl == computed_afl
  , afr == computed_afr
  = Nothing
  | otherwise
  = Just (vcat [ text "afl (provided,computed):" <+> ppr afl <+> ppr computed_afl
               , text "afr (provided,computed):" <+> ppr afr <+> ppr computed_afr
               , pp_inputs ])
  where
    computed_afl = chooseFunTyFlag argl_ty resl_ty
    computed_afr = chooseFunTyFlag argr_ty resr_ty
    Pair argl_ty argr_ty = coercionKind arg_co
    Pair resl_ty resr_ty = coercionKind res_co

    pp_inputs = vcat [ pp_ty "argl" argl_ty, pp_ty "argr" argr_ty
                     , pp_ty "resl" resl_ty, pp_ty "resr" resr_ty
                     , text "arg_co:" <+> ppr arg_co
                     , text "res_co:" <+> ppr res_co ]

    ok ty = isTYPEorCONSTRAINT (typeKind ty)
    pp_ty str ty = text str <> colon <+> hang (ppr ty)
                                            2 (dcolon <+> ppr (typeKind ty))
-}

-- | Apply a 'Coercion' to another 'Coercion'.
-- The second coercion must be Nominal, unless the first is Phantom.
-- If the first is Phantom, then the second can be either Phantom or Nominal.
mkAppCo :: Coercion     -- ^ :: t1 ~r t2
        -> Coercion     -- ^ :: s1 ~N s2, where s1 :: k1, s2 :: k2
        -> Coercion     -- ^ :: t1 s1 ~r t2 s2
mkAppCo :: Coercion -> Coercion -> Coercion
mkAppCo Coercion
co Coercion
arg
  | Just (Type
ty1, Role
r) <- Coercion -> Maybe (Type, Role)
isReflCo_maybe Coercion
co
  , Just (Type
ty2, Role
_) <- Coercion -> Maybe (Type, Role)
isReflCo_maybe Coercion
arg
  = Role -> Type -> Coercion
mkReflCo Role
r (Type -> Type -> Type
mkAppTy Type
ty1 Type
ty2)

  | Just (Type
ty1, Role
r) <- Coercion -> Maybe (Type, Role)
isReflCo_maybe Coercion
co
  , Just (TyCon
tc, [Type]
tys) <- HasDebugCallStack => Type -> Maybe (TyCon, [Type])
Type -> Maybe (TyCon, [Type])
splitTyConApp_maybe Type
ty1
    -- Expand type synonyms; a TyConAppCo can't have a type synonym (#9102)
  = HasDebugCallStack => Role -> TyCon -> [Coercion] -> Coercion
Role -> TyCon -> [Coercion] -> Coercion
mkTyConAppCo Role
r TyCon
tc (Infinite Role -> [Type] -> [Coercion]
zip_roles (Role -> TyCon -> Infinite Role
tyConRolesX Role
r TyCon
tc) [Type]
tys)
  where
    zip_roles :: Infinite Role -> [Type] -> [Coercion]
zip_roles (Inf Role
r1 Infinite Role
_)  []            = [Role -> Role -> Coercion -> Coercion
downgradeRole Role
r1 Role
Nominal Coercion
arg]
    zip_roles (Inf Role
r1 Infinite Role
rs) (Type
ty1:[Type]
tys)     = Role -> Type -> Coercion
mkReflCo Role
r1 Type
ty1 Coercion -> [Coercion] -> [Coercion]
forall a. a -> [a] -> [a]
: Infinite Role -> [Type] -> [Coercion]
zip_roles Infinite Role
rs [Type]
tys

mkAppCo (TyConAppCo Role
r TyCon
tc [Coercion]
args) Coercion
arg
  = case Role
r of
      Role
Nominal          -> HasDebugCallStack => Role -> TyCon -> [Coercion] -> Coercion
Role -> TyCon -> [Coercion] -> Coercion
mkTyConAppCo Role
Nominal TyCon
tc ([Coercion]
args [Coercion] -> [Coercion] -> [Coercion]
forall a. [a] -> [a] -> [a]
++ [Coercion
arg])
      Role
Representational -> HasDebugCallStack => Role -> TyCon -> [Coercion] -> Coercion
Role -> TyCon -> [Coercion] -> Coercion
mkTyConAppCo Role
Representational TyCon
tc ([Coercion]
args [Coercion] -> [Coercion] -> [Coercion]
forall a. [a] -> [a] -> [a]
++ [Coercion
arg'])
        where new_role :: Role
new_role = TyCon -> Infinite Role
tyConRolesRepresentational TyCon
tc Infinite Role -> Arity -> Role
forall a. Infinite a -> Arity -> a
Inf.!! [Coercion] -> Arity
forall a. [a] -> Arity
forall (t :: * -> *) a. Foldable t => t a -> Arity
length [Coercion]
args
              arg' :: Coercion
arg'     = Role -> Role -> Coercion -> Coercion
downgradeRole Role
new_role Role
Nominal Coercion
arg
      Role
Phantom          -> HasDebugCallStack => Role -> TyCon -> [Coercion] -> Coercion
Role -> TyCon -> [Coercion] -> Coercion
mkTyConAppCo Role
Phantom TyCon
tc ([Coercion]
args [Coercion] -> [Coercion] -> [Coercion]
forall a. [a] -> [a] -> [a]
++ [Coercion -> Coercion
toPhantomCo Coercion
arg])
mkAppCo Coercion
co Coercion
arg = Coercion -> Coercion -> Coercion
AppCo Coercion
co  Coercion
arg
-- Note, mkAppCo is careful to maintain invariants regarding
-- where Refl constructors appear; see the comments in the definition
-- of Coercion and the Note [Refl invariant] in GHC.Core.TyCo.Rep.

-- | Applies multiple 'Coercion's to another 'Coercion', from left to right.
-- See also 'mkAppCo'.
mkAppCos :: Coercion
         -> [Coercion]
         -> Coercion
mkAppCos :: Coercion -> [Coercion] -> Coercion
mkAppCos Coercion
co1 [Coercion]
cos = (Coercion -> Coercion -> Coercion)
-> Coercion -> [Coercion] -> Coercion
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' Coercion -> Coercion -> Coercion
mkAppCo Coercion
co1 [Coercion]
cos


-- | Make a Coercion from a tycovar, a kind coercion, and a body coercion.
mkForAllCo :: HasDebugCallStack => TyCoVar -> ForAllTyFlag -> ForAllTyFlag -> CoercionN -> Coercion -> Coercion
mkForAllCo :: HasDebugCallStack =>
CoVar
-> ForAllTyFlag -> ForAllTyFlag -> Coercion -> Coercion -> Coercion
mkForAllCo CoVar
v ForAllTyFlag
visL ForAllTyFlag
visR Coercion
kind_co Coercion
co
  | Just (Type
ty, Role
r) <- Coercion -> Maybe (Type, Role)
isReflCo_maybe Coercion
co
  , Coercion -> Bool
isReflCo Coercion
kind_co
  , ForAllTyFlag
visL ForAllTyFlag -> ForAllTyFlag -> Bool
`eqForAllVis` ForAllTyFlag
visR
  = Role -> Type -> Coercion
mkReflCo Role
r (CoVar -> ForAllTyFlag -> Type -> Type
mkTyCoForAllTy CoVar
v ForAllTyFlag
visL Type
ty)

  | Bool
otherwise
  = CoVar
-> ForAllTyFlag -> ForAllTyFlag -> Coercion -> Coercion -> Coercion
mkForAllCo_NoRefl CoVar
v ForAllTyFlag
visL ForAllTyFlag
visR Coercion
kind_co Coercion
co

-- | Make a Coercion quantified over a type/coercion variable;
-- the variable has the same kind and visibility in both sides of the coercion
mkHomoForAllCos :: [ForAllTyBinder] -> Coercion -> Coercion
mkHomoForAllCos :: [ForAllTyBinder] -> Coercion -> Coercion
mkHomoForAllCos [ForAllTyBinder]
vs Coercion
orig_co
  | Just (Type
ty, Role
r) <- Coercion -> Maybe (Type, Role)
isReflCo_maybe Coercion
orig_co
  = Role -> Type -> Coercion
mkReflCo Role
r ([ForAllTyBinder] -> Type -> Type
mkTyCoForAllTys [ForAllTyBinder]
vs Type
ty)
  | Bool
otherwise
  = (ForAllTyBinder -> Coercion -> Coercion)
-> Coercion -> [ForAllTyBinder] -> Coercion
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr ForAllTyBinder -> Coercion -> Coercion
go Coercion
orig_co [ForAllTyBinder]
vs
  where
    go :: ForAllTyBinder -> Coercion -> Coercion
go (Bndr CoVar
var ForAllTyFlag
vis) Coercion
co
      = CoVar
-> ForAllTyFlag -> ForAllTyFlag -> Coercion -> Coercion -> Coercion
mkForAllCo_NoRefl CoVar
var ForAllTyFlag
vis ForAllTyFlag
vis (Type -> Coercion
mkNomReflCo (CoVar -> Type
varType CoVar
var)) Coercion
co

-- | Like 'mkForAllCo', but there is no need to check that the inner coercion isn't Refl;
--   the caller has done that. (For example, it is guaranteed in 'mkHomoForAllCos'.)
-- The kind of the tycovar should be the left-hand kind of the kind coercion.
mkForAllCo_NoRefl :: TyCoVar -> ForAllTyFlag -> ForAllTyFlag -> CoercionN -> Coercion -> Coercion
mkForAllCo_NoRefl :: CoVar
-> ForAllTyFlag -> ForAllTyFlag -> Coercion -> Coercion -> Coercion
mkForAllCo_NoRefl CoVar
tcv ForAllTyFlag
visL ForAllTyFlag
visR Coercion
kind_co Coercion
co
  = CoVar
-> ForAllTyFlag
-> ForAllTyFlag
-> Coercion
-> Coercion
-> Coercion
-> Coercion
forall a.
HasDebugCallStack =>
CoVar
-> ForAllTyFlag -> ForAllTyFlag -> Coercion -> Coercion -> a -> a
assertGoodForAllCo CoVar
tcv ForAllTyFlag
visL ForAllTyFlag
visR Coercion
kind_co Coercion
co (Coercion -> Coercion) -> Coercion -> Coercion
forall a b. (a -> b) -> a -> b
$
    Bool -> SDoc -> Coercion -> Coercion
forall a. HasCallStack => Bool -> SDoc -> a -> a
assertPpr (Bool -> Bool
not (Coercion -> Bool
isReflCo Coercion
co Bool -> Bool -> Bool
&& Coercion -> Bool
isReflCo Coercion
kind_co Bool -> Bool -> Bool
&& ForAllTyFlag
visL ForAllTyFlag -> ForAllTyFlag -> Bool
forall a. Eq a => a -> a -> Bool
== ForAllTyFlag
visR)) (Coercion -> SDoc
forall a. Outputable a => a -> SDoc
ppr Coercion
co) (Coercion -> Coercion) -> Coercion -> Coercion
forall a b. (a -> b) -> a -> b
$
    ForAllCo { fco_tcv :: CoVar
fco_tcv = CoVar
tcv, fco_visL :: ForAllTyFlag
fco_visL = ForAllTyFlag
visL, fco_visR :: ForAllTyFlag
fco_visR = ForAllTyFlag
visR
             , fco_kind :: Coercion
fco_kind = Coercion
kind_co, fco_body :: Coercion
fco_body = Coercion
co }

assertGoodForAllCo :: HasDebugCallStack
                   =>  TyCoVar -> ForAllTyFlag -> ForAllTyFlag
                   -> CoercionN -> Coercion -> a -> a
-- Check ForAllCo invariants; see Note [ForAllCo] in GHC.Core.TyCo.Rep
assertGoodForAllCo :: forall a.
HasDebugCallStack =>
CoVar
-> ForAllTyFlag -> ForAllTyFlag -> Coercion -> Coercion -> a -> a
assertGoodForAllCo CoVar
tcv ForAllTyFlag
visL ForAllTyFlag
visR Coercion
kind_co Coercion
co
  | CoVar -> Bool
isTyVar CoVar
tcv
  = Bool -> SDoc -> a -> a
forall a. HasCallStack => Bool -> SDoc -> a -> a
assertPpr (Type
tcv_type HasCallStack => Type -> Type -> Bool
Type -> Type -> Bool
`eqType` Type
kind_co_lkind) SDoc
doc

  | Bool
otherwise
  = Bool -> SDoc -> a -> a
forall a. HasCallStack => Bool -> SDoc -> a -> a
assertPpr (Type
tcv_type HasCallStack => Type -> Type -> Bool
Type -> Type -> Bool
`eqType` Type
kind_co_lkind) SDoc
doc
        -- The kind of the tycovar should be the left-hand kind of the kind coercion.
  (a -> a) -> (a -> a) -> a -> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Bool -> SDoc -> a -> a
forall a. HasCallStack => Bool -> SDoc -> a -> a
assertPpr (CoVar -> Coercion -> Bool
almostDevoidCoVarOfCo CoVar
tcv Coercion
co) SDoc
doc
        -- See (FC6) in Note [ForAllCo] in GHC.Core.TyCo.Rep
  (a -> a) -> (a -> a) -> a -> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Bool -> SDoc -> a -> a
forall a. HasCallStack => Bool -> SDoc -> a -> a
assertPpr (ForAllTyFlag
visL ForAllTyFlag -> ForAllTyFlag -> Bool
forall a. Eq a => a -> a -> Bool
== ForAllTyFlag
coreTyLamForAllTyFlag
            Bool -> Bool -> Bool
&& ForAllTyFlag
visR ForAllTyFlag -> ForAllTyFlag -> Bool
forall a. Eq a => a -> a -> Bool
== ForAllTyFlag
coreTyLamForAllTyFlag) SDoc
doc
        -- See (FC7) in Note [ForAllCo] in GHC.Core.TyCo.Rep
  where
    tcv_type :: Type
tcv_type      = CoVar -> Type
varType CoVar
tcv
    kind_co_lkind :: Type
kind_co_lkind = HasDebugCallStack => Coercion -> Type
Coercion -> Type
coercionLKind Coercion
kind_co

    doc :: SDoc
doc = [SDoc] -> SDoc
forall doc. IsDoc doc => [doc] -> doc
vcat [ String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"Var:" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> CoVar -> SDoc
forall a. Outputable a => a -> SDoc
ppr CoVar
tcv SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> SDoc
dcolon SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
tcv_type
               , String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"Vis:" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> ForAllTyFlag -> SDoc
forall a. Outputable a => a -> SDoc
ppr ForAllTyFlag
visL SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> ForAllTyFlag -> SDoc
forall a. Outputable a => a -> SDoc
ppr ForAllTyFlag
visR
               , String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"kind_co:" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> Coercion -> SDoc
forall a. Outputable a => a -> SDoc
ppr Coercion
kind_co
               , String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"kind_co_lkind" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
kind_co_lkind
               , String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"body_co" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> Coercion -> SDoc
forall a. Outputable a => a -> SDoc
ppr Coercion
co ]


mkNakedForAllCo :: TyVar    -- Never a CoVar
                -> ForAllTyFlag -> ForAllTyFlag
                -> CoercionN -> Coercion -> Coercion
-- This version lacks the assertion checks.
-- Used during type checking when the arguments may (legitimately) not be zonked
-- and so the assertions might (bogusly) fail
-- NB: since the coercions are un-zonked, we can't really deal with
--     (FC6) and (FC7) in Note [ForAllCo] in GHC.Core.TyCo.Rep.
--     Fortunately we don't have to: this function is needed only for /type/ variables.
mkNakedForAllCo :: CoVar
-> ForAllTyFlag -> ForAllTyFlag -> Coercion -> Coercion -> Coercion
mkNakedForAllCo CoVar
tv ForAllTyFlag
visL ForAllTyFlag
visR Coercion
kind_co Coercion
co
  | Bool -> SDoc -> Bool -> Bool
forall a. HasCallStack => Bool -> SDoc -> a -> a
assertPpr (CoVar -> Bool
isTyVar CoVar
tv) (CoVar -> SDoc
forall a. Outputable a => a -> SDoc
ppr CoVar
tv) Bool
True
  , Just (Type
ty, Role
r) <- Coercion -> Maybe (Type, Role)
isReflCo_maybe Coercion
co
  , Coercion -> Bool
isReflCo Coercion
kind_co
  , ForAllTyFlag
visL ForAllTyFlag -> ForAllTyFlag -> Bool
`eqForAllVis` ForAllTyFlag
visR
  = Role -> Type -> Coercion
mkReflCo Role
r (ForAllTyBinder -> Type -> Type
mkForAllTy (CoVar -> ForAllTyFlag -> ForAllTyBinder
forall var argf. var -> argf -> VarBndr var argf
Bndr CoVar
tv ForAllTyFlag
visL) Type
ty)
  | Bool
otherwise
  = ForAllCo { fco_tcv :: CoVar
fco_tcv = CoVar
tv, fco_visL :: ForAllTyFlag
fco_visL = ForAllTyFlag
visL, fco_visR :: ForAllTyFlag
fco_visR = ForAllTyFlag
visR
             , fco_kind :: Coercion
fco_kind = Coercion
kind_co, fco_body :: Coercion
fco_body = Coercion
co }


mkCoVarCo :: CoVar -> Coercion
-- cv :: s ~# t
-- See Note [mkCoVarCo]
mkCoVarCo :: CoVar -> Coercion
mkCoVarCo CoVar
cv = CoVar -> Coercion
CoVarCo CoVar
cv

mkCoVarCos :: [CoVar] -> [Coercion]
mkCoVarCos :: [CoVar] -> [Coercion]
mkCoVarCos = (CoVar -> Coercion) -> [CoVar] -> [Coercion]
forall a b. (a -> b) -> [a] -> [b]
map CoVar -> Coercion
mkCoVarCo

{- Note [mkCoVarCo]
~~~~~~~~~~~~~~~~~~~
In the past, mkCoVarCo optimised (c :: t~t) to (Refl t).  That is
valid (although see Note [Unbound RULE binders] in GHC.Core.Rules), but
it's a relatively expensive test and perhaps better done in
optCoercion.  Not a big deal either way.
-}

mkAxInstCo :: Role
           -> CoAxiomRule   -- Always BranchedAxiom or UnbranchedAxiom
           -> [Type] -> [Coercion]
           -> Coercion
-- mkAxInstCo can legitimately be called over-saturated;
-- i.e. with more type arguments than the coercion requires
-- Only called with BranchedAxiom or UnbranchedAxiom
mkAxInstCo :: Role -> CoAxiomRule -> [Type] -> [Coercion] -> Coercion
mkAxInstCo Role
role CoAxiomRule
axr [Type]
tys [Coercion]
cos
  | Arity
arity Arity -> Arity -> Bool
forall a. Eq a => a -> a -> Bool
== Arity
n_tys = Role -> Role -> Coercion -> Coercion
downgradeRole Role
role Role
ax_role (Coercion -> Coercion) -> Coercion -> Coercion
forall a b. (a -> b) -> a -> b
$
                     CoAxiomRule -> [Coercion] -> Coercion
AxiomCo CoAxiomRule
axr ([Coercion]
rtys [Coercion] -> [Coercion] -> [Coercion]
forall a. [a] -> [a] -> [a]
`chkAppend` [Coercion]
cos)
  | Bool
otherwise      = Bool -> Coercion -> Coercion
forall a. HasCallStack => Bool -> a -> a
assert (Arity
arity Arity -> Arity -> Bool
forall a. Ord a => a -> a -> Bool
< Arity
n_tys) (Coercion -> Coercion) -> Coercion -> Coercion
forall a b. (a -> b) -> a -> b
$
                     Role -> Role -> Coercion -> Coercion
downgradeRole Role
role Role
ax_role (Coercion -> Coercion) -> Coercion -> Coercion
forall a b. (a -> b) -> a -> b
$
                     Coercion -> [Coercion] -> Coercion
mkAppCos (CoAxiomRule -> [Coercion] -> Coercion
AxiomCo CoAxiomRule
axr ([Coercion]
ax_args [Coercion] -> [Coercion] -> [Coercion]
forall a. [a] -> [a] -> [a]
`chkAppend` [Coercion]
cos))
                              [Coercion]
leftover_args
  where
    (Role
ax_role, CoAxBranch
branch)        = case CoAxiomRule -> Maybe (TyCon, Role, CoAxBranch)
coAxiomRuleBranch_maybe CoAxiomRule
axr of
                                  Just (TyCon
_tc, Role
ax_role, CoAxBranch
branch) -> (Role
ax_role, CoAxBranch
branch)
                                  Maybe (TyCon, Role, CoAxBranch)
Nothing -> String -> SDoc -> (Role, CoAxBranch)
forall a. HasCallStack => String -> SDoc -> a
pprPanic String
"mkAxInstCo" (CoAxiomRule -> SDoc
forall a. Outputable a => a -> SDoc
ppr CoAxiomRule
axr)
    n_tys :: Arity
n_tys                    = [Type] -> Arity
forall a. [a] -> Arity
forall (t :: * -> *) a. Foldable t => t a -> Arity
length [Type]
tys
    arity :: Arity
arity                    = [CoVar] -> Arity
forall a. [a] -> Arity
forall (t :: * -> *) a. Foldable t => t a -> Arity
length (CoAxBranch -> [CoVar]
coAxBranchTyVars CoAxBranch
branch)
    arg_roles :: [Role]
arg_roles                = CoAxBranch -> [Role]
coAxBranchRoles CoAxBranch
branch
    rtys :: [Coercion]
rtys                     = (Role -> Type -> Coercion) -> [Role] -> [Type] -> [Coercion]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith Role -> Type -> Coercion
mkReflCo ([Role]
arg_roles [Role] -> [Role] -> [Role]
forall a. [a] -> [a] -> [a]
++ Role -> [Role]
forall a. a -> [a]
repeat Role
Nominal) [Type]
tys
    ([Coercion]
ax_args, [Coercion]
leftover_args) = Arity -> [Coercion] -> ([Coercion], [Coercion])
forall a. Arity -> [a] -> ([a], [a])
splitAt Arity
arity [Coercion]
rtys

-- worker function
mkAxiomCo :: CoAxiomRule -> [Coercion] -> Coercion
mkAxiomCo :: CoAxiomRule -> [Coercion] -> Coercion
mkAxiomCo = CoAxiomRule -> [Coercion] -> Coercion
AxiomCo

-- to be used only with unbranched axioms
mkUnbranchedAxInstCo :: Role -> CoAxiom Unbranched
                     -> [Type] -> [Coercion] -> Coercion
mkUnbranchedAxInstCo :: Role -> CoAxiom Unbranched -> [Type] -> [Coercion] -> Coercion
mkUnbranchedAxInstCo Role
role CoAxiom Unbranched
ax [Type]
tys [Coercion]
cos
  = Role -> CoAxiomRule -> [Type] -> [Coercion] -> Coercion
mkAxInstCo Role
role (CoAxiom Unbranched -> CoAxiomRule
UnbranchedAxiom CoAxiom Unbranched
ax) [Type]
tys [Coercion]
cos

mkAxInstRHS :: CoAxiom br -> BranchIndex -> [Type] -> [Coercion] -> Type
-- Instantiate the axiom with specified types,
-- returning the instantiated RHS
-- A companion to mkAxInstCo:
--    mkAxInstRhs ax index tys = snd (coercionKind (mkAxInstCo ax index tys))
mkAxInstRHS :: forall (br :: BranchFlag).
CoAxiom br -> Arity -> [Type] -> [Coercion] -> Type
mkAxInstRHS CoAxiom br
ax Arity
index [Type]
tys [Coercion]
cos
  = Bool -> Type -> Type
forall a. HasCallStack => Bool -> a -> a
assert ([CoVar]
tvs [CoVar] -> [Type] -> Bool
forall a b. [a] -> [b] -> Bool
`equalLength` [Type]
tys1) (Type -> Type) -> Type -> Type
forall a b. (a -> b) -> a -> b
$
    Type -> [Type] -> Type
mkAppTys Type
rhs' [Type]
tys2
  where
    branch :: CoAxBranch
branch       = CoAxiom br -> Arity -> CoAxBranch
forall (br :: BranchFlag). CoAxiom br -> Arity -> CoAxBranch
coAxiomNthBranch CoAxiom br
ax Arity
index
    tvs :: [CoVar]
tvs          = CoAxBranch -> [CoVar]
coAxBranchTyVars CoAxBranch
branch
    cvs :: [CoVar]
cvs          = CoAxBranch -> [CoVar]
coAxBranchCoVars CoAxBranch
branch
    ([Type]
tys1, [Type]
tys2) = [CoVar] -> [Type] -> ([Type], [Type])
forall b a. [b] -> [a] -> ([a], [a])
splitAtList [CoVar]
tvs [Type]
tys
    rhs' :: Type
rhs'         = [CoVar] -> [Type] -> Type -> Type
HasDebugCallStack => [CoVar] -> [Type] -> Type -> Type
substTyWith [CoVar]
tvs [Type]
tys1 (Type -> Type) -> Type -> Type
forall a b. (a -> b) -> a -> b
$
                   [CoVar] -> [Coercion] -> Type -> Type
substTyWithCoVars [CoVar]
cvs [Coercion]
cos (Type -> Type) -> Type -> Type
forall a b. (a -> b) -> a -> b
$
                   CoAxBranch -> Type
coAxBranchRHS CoAxBranch
branch

mkUnbranchedAxInstRHS :: CoAxiom Unbranched -> [Type] -> [Coercion] -> Type
mkUnbranchedAxInstRHS :: CoAxiom Unbranched -> [Type] -> [Coercion] -> Type
mkUnbranchedAxInstRHS CoAxiom Unbranched
ax = CoAxiom Unbranched -> Arity -> [Type] -> [Coercion] -> Type
forall (br :: BranchFlag).
CoAxiom br -> Arity -> [Type] -> [Coercion] -> Type
mkAxInstRHS CoAxiom Unbranched
ax Arity
0

-- | Return the left-hand type of the axiom, when the axiom is instantiated
-- at the types given.
mkAxInstLHS :: CoAxiom br -> BranchIndex -> [Type] -> [Coercion] -> Type
mkAxInstLHS :: forall (br :: BranchFlag).
CoAxiom br -> Arity -> [Type] -> [Coercion] -> Type
mkAxInstLHS CoAxiom br
ax Arity
index [Type]
tys [Coercion]
cos
  = Bool -> Type -> Type
forall a. HasCallStack => Bool -> a -> a
assert ([CoVar]
tvs [CoVar] -> [Type] -> Bool
forall a b. [a] -> [b] -> Bool
`equalLength` [Type]
tys1) (Type -> Type) -> Type -> Type
forall a b. (a -> b) -> a -> b
$
    TyCon -> [Type] -> Type
mkTyConApp TyCon
fam_tc ([Type]
lhs_tys [Type] -> [Type] -> [Type]
forall a. [a] -> [a] -> [a]
`chkAppend` [Type]
tys2)
  where
    branch :: CoAxBranch
branch       = CoAxiom br -> Arity -> CoAxBranch
forall (br :: BranchFlag). CoAxiom br -> Arity -> CoAxBranch
coAxiomNthBranch CoAxiom br
ax Arity
index
    tvs :: [CoVar]
tvs          = CoAxBranch -> [CoVar]
coAxBranchTyVars CoAxBranch
branch
    cvs :: [CoVar]
cvs          = CoAxBranch -> [CoVar]
coAxBranchCoVars CoAxBranch
branch
    ([Type]
tys1, [Type]
tys2) = [CoVar] -> [Type] -> ([Type], [Type])
forall b a. [b] -> [a] -> ([a], [a])
splitAtList [CoVar]
tvs [Type]
tys
    lhs_tys :: [Type]
lhs_tys      = [CoVar] -> [Type] -> [Type] -> [Type]
HasDebugCallStack => [CoVar] -> [Type] -> [Type] -> [Type]
substTysWith [CoVar]
tvs [Type]
tys1 ([Type] -> [Type]) -> [Type] -> [Type]
forall a b. (a -> b) -> a -> b
$
                   [CoVar] -> [Coercion] -> [Type] -> [Type]
HasDebugCallStack => [CoVar] -> [Coercion] -> [Type] -> [Type]
substTysWithCoVars [CoVar]
cvs [Coercion]
cos ([Type] -> [Type]) -> [Type] -> [Type]
forall a b. (a -> b) -> a -> b
$
                   CoAxBranch -> [Type]
coAxBranchLHS CoAxBranch
branch
    fam_tc :: TyCon
fam_tc       = CoAxiom br -> TyCon
forall (br :: BranchFlag). CoAxiom br -> TyCon
coAxiomTyCon CoAxiom br
ax

-- | Instantiate the left-hand side of an unbranched axiom
mkUnbranchedAxInstLHS :: CoAxiom Unbranched -> [Type] -> [Coercion] -> Type
mkUnbranchedAxInstLHS :: CoAxiom Unbranched -> [Type] -> [Coercion] -> Type
mkUnbranchedAxInstLHS CoAxiom Unbranched
ax = CoAxiom Unbranched -> Arity -> [Type] -> [Coercion] -> Type
forall (br :: BranchFlag).
CoAxiom br -> Arity -> [Type] -> [Coercion] -> Type
mkAxInstLHS CoAxiom Unbranched
ax Arity
0

-- | Make a coercion from a coercion hole
mkHoleCo :: CoercionHole -> Coercion
mkHoleCo :: CoercionHole -> Coercion
mkHoleCo CoercionHole
h = CoercionHole -> Coercion
HoleCo CoercionHole
h

-- | Make a universal coercion between two arbitrary types.
mkUnivCo :: UnivCoProvenance
         -> [Coercion] -- ^ Coercions on which this depends
         -> Role       -- ^ role of the built coercion, "r"
         -> Type       -- ^ t1 :: k1
         -> Type       -- ^ t2 :: k2
         -> Coercion   -- ^ :: t1 ~r t2
mkUnivCo :: UnivCoProvenance -> [Coercion] -> Role -> Type -> Type -> Coercion
mkUnivCo UnivCoProvenance
prov [Coercion]
deps Role
role Type
ty1 Type
ty2
  | Type
ty1 HasCallStack => Type -> Type -> Bool
Type -> Type -> Bool
`eqType` Type
ty2 = Role -> Type -> Coercion
mkReflCo Role
role Type
ty1
  | Bool
otherwise        = UnivCo { uco_prov :: UnivCoProvenance
uco_prov = UnivCoProvenance
prov, uco_role :: Role
uco_role = Role
role
                              , uco_lty :: Type
uco_lty = Type
ty1, uco_rty :: Type
uco_rty = Type
ty2
                              , uco_deps :: [Coercion]
uco_deps = [Coercion]
deps }

-- | Create a symmetric version of the given 'Coercion' that asserts
--   equality between the same types but in the other "direction", so
--   a kind of @t1 ~ t2@ becomes the kind @t2 ~ t1@.
mkSymCo :: Coercion -> Coercion

-- Do a few simple optimizations, mainly to expose the underlying
-- constructors to other 'mk' functions.  E.g.
--   mkInstCo (mkSymCo (ForAllCo ...)) ty
-- We want to push the SymCo inside the ForallCo, so that we can instantiate
-- This can make a big difference.  E.g without coercion optimisation, GHC.Read
-- totally explodes; but when we push Sym inside ForAll, it's fine.
mkSymCo :: Coercion -> Coercion
mkSymCo Coercion
co | Coercion -> Bool
isReflCo Coercion
co   = Coercion
co
mkSymCo (SymCo Coercion
co)         = Coercion
co
mkSymCo (SubCo (SymCo Coercion
co)) = Coercion -> Coercion
SubCo Coercion
co
mkSymCo co :: Coercion
co@(ForAllCo { fco_kind :: Coercion -> Coercion
fco_kind = Coercion
kco, fco_body :: Coercion -> Coercion
fco_body = Coercion
body_co })
  | Coercion -> Bool
isReflCo Coercion
kco           = Coercion
co { fco_body = mkSymCo body_co }
mkSymCo Coercion
co                 = Coercion -> Coercion
SymCo Coercion
co

-- | Create a new 'Coercion' by composing the two given 'Coercion's transitively.
--   (co1 ; co2)
mkTransCo :: Coercion -> Coercion -> Coercion
mkTransCo :: Coercion -> Coercion -> Coercion
mkTransCo Coercion
co1 Coercion
co2 | Coercion -> Bool
isReflCo Coercion
co1 = Coercion
co2
                  | Coercion -> Bool
isReflCo Coercion
co2 = Coercion
co1
mkTransCo (GRefl Role
r Type
t1 (MCo Coercion
co1)) (GRefl Role
_ Type
_ (MCo Coercion
co2))
  = Role -> Type -> MCoercion -> Coercion
GRefl Role
r Type
t1 (Coercion -> MCoercion
MCo (Coercion -> MCoercion) -> Coercion -> MCoercion
forall a b. (a -> b) -> a -> b
$ Coercion -> Coercion -> Coercion
mkTransCo Coercion
co1 Coercion
co2)
mkTransCo Coercion
co1 Coercion
co2                = Coercion -> Coercion -> Coercion
TransCo Coercion
co1 Coercion
co2

--------------------
{- Note [mkSelCo precondition]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
To satisfy the Purely Kinded Type Invariant (PKTI), we require that
  in any call (mkSelCo cs co)
  * selectFromType cs (coercionLKind co) works
  * selectFromType cs (coercionRKind co) works
  * and hence coercionKind (SelCo cs co) works (PKTI)
-}

mkSelCo :: HasDebugCallStack
        => CoSel
        -> Coercion
        -> Coercion
-- See Note [mkSelCo precondition]
mkSelCo :: HasDebugCallStack => CoSel -> Coercion -> Coercion
mkSelCo CoSel
n Coercion
co = HasDebugCallStack => CoSel -> Coercion -> Maybe Coercion
CoSel -> Coercion -> Maybe Coercion
mkSelCo_maybe CoSel
n Coercion
co Maybe Coercion -> Coercion -> Coercion
forall a. Maybe a -> a -> a
`orElse` CoSel -> Coercion -> Coercion
SelCo CoSel
n Coercion
co

mkSelCo_maybe :: HasDebugCallStack
        => CoSel
        -> Coercion
        -> Maybe Coercion
-- Note [mkSelCo precondition]
mkSelCo_maybe :: HasDebugCallStack => CoSel -> Coercion -> Maybe Coercion
mkSelCo_maybe CoSel
cs Coercion
co
  = Bool -> SDoc -> Maybe Coercion -> Maybe Coercion
forall a. HasCallStack => Bool -> SDoc -> a -> a
assertPpr (CoSel -> Bool
good_call CoSel
cs) SDoc
bad_call_msg (Maybe Coercion -> Maybe Coercion)
-> Maybe Coercion -> Maybe Coercion
forall a b. (a -> b) -> a -> b
$
    CoSel -> Coercion -> Maybe Coercion
go CoSel
cs Coercion
co
  where

    go :: CoSel -> Coercion -> Maybe Coercion
go CoSel
SelForAll (ForAllCo { fco_kind :: Coercion -> Coercion
fco_kind = Coercion
kind_co })
      = Coercion -> Maybe Coercion
forall a. a -> Maybe a
Just Coercion
kind_co
      -- If co :: (forall a1:k1. t1) ~ (forall a2:k2. t2)
      -- then (nth SelForAll co :: k1 ~N k2)
      -- If co :: (forall a1:t1 ~ t2. t1) ~ (forall a2:t3 ~ t4. t2)
      -- then (nth SelForAll co :: (t1 ~ t2) ~N (t3 ~ t4))

    go (SelFun FunSel
fs) (FunCo Role
_ FunTyFlag
_ FunTyFlag
_ Coercion
w Coercion
arg Coercion
res)
      = Coercion -> Maybe Coercion
forall a. a -> Maybe a
Just (FunSel -> Coercion -> Coercion -> Coercion -> Coercion
forall a. FunSel -> a -> a -> a -> a
getNthFun FunSel
fs Coercion
w Coercion
arg Coercion
res)

    go (SelTyCon Arity
i Role
r) (TyConAppCo Role
r0 TyCon
tc [Coercion]
arg_cos)
      = Bool -> SDoc -> Maybe Coercion -> Maybe Coercion
forall a. HasCallStack => Bool -> SDoc -> a -> a
assertPpr (Role
r Role -> Role -> Bool
forall a. Eq a => a -> a -> Bool
== Role -> TyCon -> Arity -> Role
tyConRole Role
r0 TyCon
tc Arity
i)
                  ([SDoc] -> SDoc
forall doc. IsDoc doc => [doc] -> doc
vcat [ TyCon -> SDoc
forall a. Outputable a => a -> SDoc
ppr TyCon
tc, [Coercion] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [Coercion]
arg_cos, Role -> SDoc
forall a. Outputable a => a -> SDoc
ppr Role
r0, Arity -> SDoc
forall a. Outputable a => a -> SDoc
ppr Arity
i, Role -> SDoc
forall a. Outputable a => a -> SDoc
ppr Role
r ]) (Maybe Coercion -> Maybe Coercion)
-> Maybe Coercion -> Maybe Coercion
forall a b. (a -> b) -> a -> b
$
        Coercion -> Maybe Coercion
forall a. a -> Maybe a
Just ([Coercion]
arg_cos [Coercion] -> Arity -> Coercion
forall a. Outputable a => [a] -> Arity -> a
`getNth` Arity
i)

    go CoSel
cs (SymCo Coercion
co)  -- Recurse, hoping to get to a TyConAppCo or FunCo
      = do { co' <- CoSel -> Coercion -> Maybe Coercion
go CoSel
cs Coercion
co; return (mkSymCo co') }

    go CoSel
cs Coercion
co
      | Just (Type
ty, Role
co_role) <- Coercion -> Maybe (Type, Role)
isReflCo_maybe Coercion
co
      = Coercion -> Maybe Coercion
forall a. a -> Maybe a
Just (Role -> Type -> Coercion
mkReflCo (CoSel -> Role -> Role
mkSelCoResRole CoSel
cs Role
co_role) (HasDebugCallStack => CoSel -> Type -> Type
CoSel -> Type -> Type
selectFromType CoSel
cs Type
ty))
        -- mkSelCoreResRole: The role of the result may not be
        -- be equal to co_role, the role of co, per Note [SelCo].
        -- This was revealed by #23938.

      | Pair Type
ty1 Type
ty2 <- HasDebugCallStack => Coercion -> Pair Type
Coercion -> Pair Type
coercionKind Coercion
co
      , let sty1 :: Type
sty1    = HasDebugCallStack => CoSel -> Type -> Type
CoSel -> Type -> Type
selectFromType CoSel
cs Type
ty1
            sty2 :: Type
sty2    = HasDebugCallStack => CoSel -> Type -> Type
CoSel -> Type -> Type
selectFromType CoSel
cs Type
ty2
            co_role :: Role
co_role = Coercion -> Role
coercionRole Coercion
co
      , Type
sty1 HasCallStack => Type -> Type -> Bool
Type -> Type -> Bool
`eqType` Type
sty2
      = Coercion -> Maybe Coercion
forall a. a -> Maybe a
Just (Role -> Type -> Coercion
mkReflCo (CoSel -> Role -> Role
mkSelCoResRole CoSel
cs Role
co_role) Type
sty1)
            -- Checking for fully reflexive-ness (by seeing if sty1=sty2)
            -- is worthwhile, because a non-Refl coercion `co` may well have a
            -- reflexive (SelCo cs co).
            -- E.g. co :: Either a b ~ Either a c
            --      Then (SubCo (SelTyCon 0) co) is reflexive

      | Bool
otherwise = Maybe Coercion
forall a. Maybe a
Nothing

    ----------- Assertion checking --------------
    -- NB: using coercionKind requires Note [mkSelCo precondition]
    Pair Type
ty1 Type
ty2 = HasDebugCallStack => Coercion -> Pair Type
Coercion -> Pair Type
coercionKind Coercion
co
    bad_call_msg :: SDoc
bad_call_msg = [SDoc] -> SDoc
forall doc. IsDoc doc => [doc] -> doc
vcat [ String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"Coercion =" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> Coercion -> SDoc
forall a. Outputable a => a -> SDoc
ppr Coercion
co
                        , String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"LHS ty =" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
ty1
                        , String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"RHS ty =" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
ty2
                        , String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"cs =" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> CoSel -> SDoc
forall a. Outputable a => a -> SDoc
ppr CoSel
cs
                        , String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"coercion role =" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> Role -> SDoc
forall a. Outputable a => a -> SDoc
ppr (Coercion -> Role
coercionRole Coercion
co) ]

    -- good_call checks the typing rules given in Note [SelCo]
    good_call :: CoSel -> Bool
good_call CoSel
SelForAll
      | Just (CoVar
_tv1, Type
_) <- Type -> Maybe (CoVar, Type)
splitForAllTyCoVar_maybe Type
ty1
      , Just (CoVar
_tv2, Type
_) <- Type -> Maybe (CoVar, Type)
splitForAllTyCoVar_maybe Type
ty2
      =  Bool
True

    good_call (SelFun {})
       = Type -> Bool
isFunTy Type
ty1 Bool -> Bool -> Bool
&& Type -> Bool
isFunTy Type
ty2

    good_call (SelTyCon Arity
n Role
r)
       | Just (TyCon
tc1, [Type]
tys1) <- HasDebugCallStack => Type -> Maybe (TyCon, [Type])
Type -> Maybe (TyCon, [Type])
splitTyConApp_maybe Type
ty1
       , Just (TyCon
tc2, [Type]
tys2) <- HasDebugCallStack => Type -> Maybe (TyCon, [Type])
Type -> Maybe (TyCon, [Type])
splitTyConApp_maybe Type
ty2
       , let { len1 :: Arity
len1 = [Type] -> Arity
forall a. [a] -> Arity
forall (t :: * -> *) a. Foldable t => t a -> Arity
length [Type]
tys1
             ; len2 :: Arity
len2 = [Type] -> Arity
forall a. [a] -> Arity
forall (t :: * -> *) a. Foldable t => t a -> Arity
length [Type]
tys2 }
       =  (TyCon
tc1 TyCon -> TyCon -> Bool
forall a. Eq a => a -> a -> Bool
== TyCon
tc2 Bool -> Bool -> Bool
|| (TyCon -> Bool
tyConIsTYPEorCONSTRAINT TyCon
tc1 Bool -> Bool -> Bool
&& TyCon -> Bool
tyConIsTYPEorCONSTRAINT TyCon
tc2))
                      -- tyConIsTYPEorCONSTRAINT: see Note [mkRuntimeRepCo]
       Bool -> Bool -> Bool
&& Arity
len1 Arity -> Arity -> Bool
forall a. Eq a => a -> a -> Bool
== Arity
len2
       Bool -> Bool -> Bool
&& Arity
n Arity -> Arity -> Bool
forall a. Ord a => a -> a -> Bool
< Arity
len1
       Bool -> Bool -> Bool
&& Role
r Role -> Role -> Bool
forall a. Eq a => a -> a -> Bool
== Role -> TyCon -> Arity -> Role
tyConRole (Coercion -> Role
coercionRole Coercion
co) TyCon
tc1 Arity
n

    good_call CoSel
_ = Bool
False

mkSelCoResRole :: CoSel -> Role -> Role
-- What is the role of (SelCo cs co), if co has role 'r'?
-- It is not just 'r'!
-- c.f. the SelCo case of coercionRole
mkSelCoResRole :: CoSel -> Role -> Role
mkSelCoResRole CoSel
SelForAll       Role
_ = Role
Nominal
mkSelCoResRole (SelTyCon Arity
_ Role
r') Role
_ = Role
r'
mkSelCoResRole (SelFun FunSel
fs)     Role
r = Role -> FunSel -> Role
funRole Role
r FunSel
fs

-- | Extract the nth field of a FunCo
getNthFun :: FunSel
          -> a    -- ^ multiplicity
          -> a    -- ^ argument
          -> a    -- ^ result
          -> a    -- ^ One of the above three
getNthFun :: forall a. FunSel -> a -> a -> a -> a
getNthFun FunSel
SelMult a
mult a
_   a
_   = a
mult
getNthFun FunSel
SelArg a
_     a
arg a
_   = a
arg
getNthFun FunSel
SelRes a
_     a
_   a
res = a
res

selectFromType :: HasDebugCallStack => CoSel -> Type -> Type
selectFromType :: HasDebugCallStack => CoSel -> Type -> Type
selectFromType (SelFun FunSel
fs) Type
ty
  | Just (FunTyFlag
_af, Type
mult, Type
arg, Type
res) <- Type -> Maybe (FunTyFlag, Type, Type, Type)
splitFunTy_maybe Type
ty
  = FunSel -> Type -> Type -> Type -> Type
forall a. FunSel -> a -> a -> a -> a
getNthFun FunSel
fs Type
mult Type
arg Type
res

selectFromType (SelTyCon Arity
n Role
_) Type
ty
  | Just [Type]
args <- Type -> Maybe [Type]
tyConAppArgs_maybe Type
ty
  = Bool -> SDoc -> Type -> Type
forall a. HasCallStack => Bool -> SDoc -> a -> a
assertPpr ([Type]
args [Type] -> Arity -> Bool
forall a. [a] -> Arity -> Bool
`lengthExceeds` Arity
n) (Arity -> SDoc
forall a. Outputable a => a -> SDoc
ppr Arity
n SDoc -> SDoc -> SDoc
forall doc. IsDoc doc => doc -> doc -> doc
$$ Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
ty) (Type -> Type) -> Type -> Type
forall a b. (a -> b) -> a -> b
$
    [Type]
args [Type] -> Arity -> Type
forall a. Outputable a => [a] -> Arity -> a
`getNth` Arity
n

selectFromType CoSel
SelForAll Type
ty       -- Works for both tyvar and covar
  | Just (CoVar
tv,Type
_) <- Type -> Maybe (CoVar, Type)
splitForAllTyCoVar_maybe Type
ty
  = CoVar -> Type
tyVarKind CoVar
tv

selectFromType CoSel
cs Type
ty
  = String -> SDoc -> Type
forall a. HasCallStack => String -> SDoc -> a
pprPanic String
"selectFromType" (CoSel -> SDoc
forall a. Outputable a => a -> SDoc
ppr CoSel
cs SDoc -> SDoc -> SDoc
forall doc. IsDoc doc => doc -> doc -> doc
$$ Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
ty)

--------------------
mkLRCo :: LeftOrRight -> Coercion -> Coercion
mkLRCo :: LeftOrRight -> Coercion -> Coercion
mkLRCo LeftOrRight
lr Coercion
co
  | Just (Type
ty, Role
eq) <- Coercion -> Maybe (Type, Role)
isReflCo_maybe Coercion
co
  = Role -> Type -> Coercion
mkReflCo Role
eq (LeftOrRight -> (Type, Type) -> Type
forall a. LeftOrRight -> (a, a) -> a
pickLR LeftOrRight
lr (Type -> (Type, Type)
splitAppTy Type
ty))
  | Bool
otherwise
  = LeftOrRight -> Coercion -> Coercion
LRCo LeftOrRight
lr Coercion
co

-- | Instantiates a 'Coercion'.
-- Works for both tyvar and covar
mkInstCo :: Coercion -> CoercionN -> Coercion
mkInstCo :: Coercion -> Coercion -> Coercion
mkInstCo Coercion
co_fun Coercion
co_arg
  | Just (CoVar
tcv, ForAllTyFlag
_, ForAllTyFlag
_, Coercion
kind_co, Coercion
body_co) <- Coercion
-> Maybe (CoVar, ForAllTyFlag, ForAllTyFlag, Coercion, Coercion)
splitForAllCo_maybe Coercion
co_fun
  , Just (Type
arg, Role
_) <- Coercion -> Maybe (Type, Role)
isReflCo_maybe Coercion
co_arg
  = Bool -> SDoc -> Coercion -> Coercion
forall a. HasCallStack => Bool -> SDoc -> a -> a
assertPpr (Coercion -> Bool
isReflexiveCo Coercion
kind_co) (Coercion -> SDoc
forall a. Outputable a => a -> SDoc
ppr Coercion
co_fun SDoc -> SDoc -> SDoc
forall doc. IsDoc doc => doc -> doc -> doc
$$ Coercion -> SDoc
forall a. Outputable a => a -> SDoc
ppr Coercion
co_arg) (Coercion -> Coercion) -> Coercion -> Coercion
forall a b. (a -> b) -> a -> b
$
       -- If the arg is Refl, then kind_co must be reflexive too
    Subst -> Coercion -> Coercion
substCoUnchecked ([CoVar] -> [Type] -> Subst
HasDebugCallStack => [CoVar] -> [Type] -> Subst
zipTCvSubst [CoVar
tcv] [Type
arg]) Coercion
body_co
mkInstCo Coercion
co Coercion
arg = Coercion -> Coercion -> Coercion
InstCo Coercion
co Coercion
arg

-- | Given @ty :: k1@, @co :: k1 ~ k2@,
-- produces @co' :: ty ~r (ty |> co)@
mkGReflRightCo :: Role -> Type -> CoercionN -> Coercion
mkGReflRightCo :: Role -> Type -> Coercion -> Coercion
mkGReflRightCo Role
r Type
ty Coercion
co
  | Coercion -> Bool
isGReflCo Coercion
co = Role -> Type -> Coercion
mkReflCo Role
r Type
ty
    -- the kinds of @k1@ and @k2@ are the same, thus @isGReflCo@
    -- instead of @isReflCo@
  | Bool
otherwise = Role -> Type -> MCoercion -> Coercion
GRefl Role
r Type
ty (Coercion -> MCoercion
MCo Coercion
co)

-- | Given @r@, @ty :: k1@, and @co :: k1 ~N k2@,
-- produces @co' :: (ty |> co) ~r ty@
mkGReflLeftCo :: Role -> Type -> CoercionN -> Coercion
mkGReflLeftCo :: Role -> Type -> Coercion -> Coercion
mkGReflLeftCo Role
r Type
ty Coercion
co
  | Coercion -> Bool
isGReflCo Coercion
co = Role -> Type -> Coercion
mkReflCo Role
r Type
ty
    -- the kinds of @k1@ and @k2@ are the same, thus @isGReflCo@
    -- instead of @isReflCo@
  | Bool
otherwise    = Coercion -> Coercion
mkSymCo (Coercion -> Coercion) -> Coercion -> Coercion
forall a b. (a -> b) -> a -> b
$ Role -> Type -> MCoercion -> Coercion
GRefl Role
r Type
ty (Coercion -> MCoercion
MCo Coercion
co)

-- | Given @ty :: k1@, @co :: k1 ~ k2@, @co2:: ty ~r ty'@,
-- produces @co' :: (ty |> co) ~r ty'
-- It is not only a utility function, but it saves allocation when co
-- is a GRefl coercion.
mkCoherenceLeftCo :: Role -> Type -> CoercionN -> Coercion -> Coercion
mkCoherenceLeftCo :: Role -> Type -> Coercion -> Coercion -> Coercion
mkCoherenceLeftCo Role
r Type
ty Coercion
co Coercion
co2
  | Coercion -> Bool
isGReflCo Coercion
co = Coercion
co2
  | Bool
otherwise    = (Coercion -> Coercion
mkSymCo (Coercion -> Coercion) -> Coercion -> Coercion
forall a b. (a -> b) -> a -> b
$ Role -> Type -> MCoercion -> Coercion
GRefl Role
r Type
ty (Coercion -> MCoercion
MCo Coercion
co)) Coercion -> Coercion -> Coercion
`mkTransCo` Coercion
co2

-- | Given @ty :: k1@, @co :: k1 ~ k2@, @co2:: ty' ~r ty@,
-- produces @co' :: ty' ~r (ty |> co)
-- It is not only a utility function, but it saves allocation when co
-- is a GRefl coercion.
mkCoherenceRightCo :: Role -> Type -> CoercionN -> Coercion -> Coercion
mkCoherenceRightCo :: Role -> Type -> Coercion -> Coercion -> Coercion
mkCoherenceRightCo Role
r Type
ty Coercion
co Coercion
co2
  | Coercion -> Bool
isGReflCo Coercion
co = Coercion
co2
  | Bool
otherwise    = Coercion
co2 Coercion -> Coercion -> Coercion
`mkTransCo` Role -> Type -> MCoercion -> Coercion
GRefl Role
r Type
ty (Coercion -> MCoercion
MCo Coercion
co)

-- | Given @co :: (a :: k) ~ (b :: k')@ produce @co' :: k ~ k'@.
mkKindCo :: Coercion -> Coercion
mkKindCo :: Coercion -> Coercion
mkKindCo Coercion
co | Just (Type
ty, Role
_) <- Coercion -> Maybe (Type, Role)
isReflCo_maybe Coercion
co = Type -> Coercion
Refl (HasDebugCallStack => Type -> Type
Type -> Type
typeKind Type
ty)
mkKindCo (GRefl Role
_ Type
_ (MCo Coercion
co)) = Coercion
co
mkKindCo Coercion
co
  | Pair Type
ty1 Type
ty2 <- HasDebugCallStack => Coercion -> Pair Type
Coercion -> Pair Type
coercionKind Coercion
co
       -- Generally, calling coercionKind during coercion creation is a bad idea,
       -- as it can lead to exponential behavior. But, we don't have nested mkKindCos,
       -- so it's OK here.
  , let tk1 :: Type
tk1 = HasDebugCallStack => Type -> Type
Type -> Type
typeKind Type
ty1
        tk2 :: Type
tk2 = HasDebugCallStack => Type -> Type
Type -> Type
typeKind Type
ty2
  , Type
tk1 HasCallStack => Type -> Type -> Bool
Type -> Type -> Bool
`eqType` Type
tk2
  = Type -> Coercion
Refl Type
tk1
  | Bool
otherwise
  = Coercion -> Coercion
KindCo Coercion
co

mkSubCo :: HasDebugCallStack => Coercion -> Coercion
-- Input coercion is Nominal, result is Representational
-- see also Note [Role twiddling functions]
mkSubCo :: HasDebugCallStack => Coercion -> Coercion
mkSubCo (Refl Type
ty) = Role -> Type -> MCoercion -> Coercion
GRefl Role
Representational Type
ty MCoercion
MRefl
mkSubCo (GRefl Role
Nominal Type
ty MCoercion
co) = Role -> Type -> MCoercion -> Coercion
GRefl Role
Representational Type
ty MCoercion
co
mkSubCo (TyConAppCo Role
Nominal TyCon
tc [Coercion]
cos)
  = Role -> TyCon -> [Coercion] -> Coercion
TyConAppCo Role
Representational TyCon
tc (TyCon -> [Coercion] -> [Coercion]
applyRoles TyCon
tc [Coercion]
cos)
mkSubCo co :: Coercion
co@(FunCo { fco_role :: Coercion -> Role
fco_role = Role
Nominal, fco_arg :: Coercion -> Coercion
fco_arg = Coercion
arg, fco_res :: Coercion -> Coercion
fco_res = Coercion
res })
  = Coercion
co { fco_role = Representational
       , fco_arg = downgradeRole Representational Nominal arg
       , fco_res = downgradeRole Representational Nominal res }
mkSubCo Coercion
co = Bool -> SDoc -> Coercion -> Coercion
forall a. HasCallStack => Bool -> SDoc -> a -> a
assertPpr (Coercion -> Role
coercionRole Coercion
co Role -> Role -> Bool
forall a. Eq a => a -> a -> Bool
== Role
Nominal) (Coercion -> SDoc
forall a. Outputable a => a -> SDoc
ppr Coercion
co SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> Role -> SDoc
forall a. Outputable a => a -> SDoc
ppr (Coercion -> Role
coercionRole Coercion
co)) (Coercion -> Coercion) -> Coercion -> Coercion
forall a b. (a -> b) -> a -> b
$
             Coercion -> Coercion
SubCo Coercion
co

-- | Changes a role, but only a downgrade. See Note [Role twiddling functions]
downgradeRole_maybe :: Role   -- ^ desired role
                    -> Role   -- ^ current role
                    -> Coercion -> Maybe Coercion
-- In (downgradeRole_maybe dr cr co) it's a precondition that
--                                   cr = coercionRole co

downgradeRole_maybe :: Role -> Role -> Coercion -> Maybe Coercion
downgradeRole_maybe Role
Nominal          Role
Nominal          Coercion
co = Coercion -> Maybe Coercion
forall a. a -> Maybe a
Just Coercion
co
downgradeRole_maybe Role
Nominal          Role
_                Coercion
_  = Maybe Coercion
forall a. Maybe a
Nothing

downgradeRole_maybe Role
Representational Role
Nominal          Coercion
co = Coercion -> Maybe Coercion
forall a. a -> Maybe a
Just (HasDebugCallStack => Coercion -> Coercion
Coercion -> Coercion
mkSubCo Coercion
co)
downgradeRole_maybe Role
Representational Role
Representational Coercion
co = Coercion -> Maybe Coercion
forall a. a -> Maybe a
Just Coercion
co
downgradeRole_maybe Role
Representational Role
Phantom          Coercion
_  = Maybe Coercion
forall a. Maybe a
Nothing

downgradeRole_maybe Role
Phantom          Role
Phantom          Coercion
co = Coercion -> Maybe Coercion
forall a. a -> Maybe a
Just Coercion
co
downgradeRole_maybe Role
Phantom          Role
_                Coercion
co = Coercion -> Maybe Coercion
forall a. a -> Maybe a
Just (Coercion -> Coercion
toPhantomCo Coercion
co)

-- | Like 'downgradeRole_maybe', but panics if the change isn't a downgrade.
-- See Note [Role twiddling functions]
downgradeRole :: Role  -- desired role
              -> Role  -- current role
              -> Coercion -> Coercion
downgradeRole :: Role -> Role -> Coercion -> Coercion
downgradeRole Role
r1 Role
r2 Coercion
co
  = case Role -> Role -> Coercion -> Maybe Coercion
downgradeRole_maybe Role
r1 Role
r2 Coercion
co of
      Just Coercion
co' -> Coercion
co'
      Maybe Coercion
Nothing  -> String -> SDoc -> Coercion
forall a. HasCallStack => String -> SDoc -> a
pprPanic String
"downgradeRole" (Coercion -> SDoc
forall a. Outputable a => a -> SDoc
ppr Coercion
co)

-- | Make a "coercion between coercions".
mkProofIrrelCo :: Role       -- ^ role of the created coercion, "r"
               -> CoercionN  -- ^ :: phi1 ~N phi2
               -> Coercion   -- ^ g1 :: phi1
               -> Coercion   -- ^ g2 :: phi2
               -> Coercion   -- ^ :: g1 ~r g2

-- if the two coercion prove the same fact, I just don't care what
-- the individual coercions are.
mkProofIrrelCo :: Role -> Coercion -> Coercion -> Coercion -> Coercion
mkProofIrrelCo Role
r Coercion
co Coercion
g  Coercion
_ | Coercion -> Bool
isGReflCo Coercion
co  = Role -> Type -> Coercion
mkReflCo Role
r (Coercion -> Type
mkCoercionTy Coercion
g)
  -- kco is a kind coercion, thus @isGReflCo@ rather than @isReflCo@
mkProofIrrelCo Role
r Coercion
kco Coercion
g1 Coercion
g2 = UnivCoProvenance -> [Coercion] -> Role -> Type -> Type -> Coercion
mkUnivCo UnivCoProvenance
ProofIrrelProv [Coercion
kco] Role
r
                                      (Coercion -> Type
mkCoercionTy Coercion
g1) (Coercion -> Type
mkCoercionTy Coercion
g2)

{-
%************************************************************************
%*                                                                      *
   Roles
%*                                                                      *
%************************************************************************
-}

-- | Converts a coercion to be nominal, if possible.
-- See Note [Role twiddling functions]
setNominalRole_maybe :: Role -- of input coercion
                     -> Coercion -> Maybe CoercionN
setNominalRole_maybe :: Role -> Coercion -> Maybe Coercion
setNominalRole_maybe Role
r Coercion
co
  | Role
r Role -> Role -> Bool
forall a. Eq a => a -> a -> Bool
== Role
Nominal = Coercion -> Maybe Coercion
forall a. a -> Maybe a
Just Coercion
co
  | Bool
otherwise = Coercion -> Maybe Coercion
setNominalRole_maybe_helper Coercion
co
  where
    setNominalRole_maybe_helper :: Coercion -> Maybe Coercion
setNominalRole_maybe_helper (SubCo Coercion
co)  = Coercion -> Maybe Coercion
forall a. a -> Maybe a
Just Coercion
co
    setNominalRole_maybe_helper co :: Coercion
co@(Refl Type
_) = Coercion -> Maybe Coercion
forall a. a -> Maybe a
Just Coercion
co
    setNominalRole_maybe_helper (GRefl Role
_ Type
ty MCoercion
co) = Coercion -> Maybe Coercion
forall a. a -> Maybe a
Just (Coercion -> Maybe Coercion) -> Coercion -> Maybe Coercion
forall a b. (a -> b) -> a -> b
$ Role -> Type -> MCoercion -> Coercion
GRefl Role
Nominal Type
ty MCoercion
co
    setNominalRole_maybe_helper (TyConAppCo Role
Representational TyCon
tc [Coercion]
cos)
      = do { cos' <- (Role -> Coercion -> Maybe Coercion)
-> [Role] -> [Coercion] -> Maybe [Coercion]
forall (m :: * -> *) a b c.
Applicative m =>
(a -> b -> m c) -> [a] -> [b] -> m [c]
zipWithM Role -> Coercion -> Maybe Coercion
setNominalRole_maybe (Role -> TyCon -> [Role]
tyConRoleListX Role
Representational TyCon
tc) [Coercion]
cos
           ; return $ TyConAppCo Nominal tc cos' }
    setNominalRole_maybe_helper co :: Coercion
co@(FunCo { fco_role :: Coercion -> Role
fco_role = Role
Representational
                                          , fco_arg :: Coercion -> Coercion
fco_arg = Coercion
co1, fco_res :: Coercion -> Coercion
fco_res = Coercion
co2 })
      = do { co1' <- Role -> Coercion -> Maybe Coercion
setNominalRole_maybe Role
Representational Coercion
co1
           ; co2' <- setNominalRole_maybe Representational co2
           ; return $ co { fco_role = Nominal, fco_arg = co1', fco_res = co2' }
           }
    setNominalRole_maybe_helper (SymCo Coercion
co)
      = Coercion -> Coercion
SymCo (Coercion -> Coercion) -> Maybe Coercion -> Maybe Coercion
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Coercion -> Maybe Coercion
setNominalRole_maybe_helper Coercion
co
    setNominalRole_maybe_helper (TransCo Coercion
co1 Coercion
co2)
      = Coercion -> Coercion -> Coercion
TransCo (Coercion -> Coercion -> Coercion)
-> Maybe Coercion -> Maybe (Coercion -> Coercion)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Coercion -> Maybe Coercion
setNominalRole_maybe_helper Coercion
co1 Maybe (Coercion -> Coercion) -> Maybe Coercion -> Maybe Coercion
forall a b. Maybe (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Coercion -> Maybe Coercion
setNominalRole_maybe_helper Coercion
co2
    setNominalRole_maybe_helper (AppCo Coercion
co1 Coercion
co2)
      = Coercion -> Coercion -> Coercion
AppCo (Coercion -> Coercion -> Coercion)
-> Maybe Coercion -> Maybe (Coercion -> Coercion)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Coercion -> Maybe Coercion
setNominalRole_maybe_helper Coercion
co1 Maybe (Coercion -> Coercion) -> Maybe Coercion -> Maybe Coercion
forall a b. Maybe (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Coercion -> Maybe Coercion
forall a. a -> Maybe a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Coercion
co2
    setNominalRole_maybe_helper co :: Coercion
co@(ForAllCo { fco_visL :: Coercion -> ForAllTyFlag
fco_visL = ForAllTyFlag
visL, fco_visR :: Coercion -> ForAllTyFlag
fco_visR = ForAllTyFlag
visR, fco_body :: Coercion -> Coercion
fco_body = Coercion
body_co })
      | ForAllTyFlag
visL ForAllTyFlag -> ForAllTyFlag -> Bool
`eqForAllVis` ForAllTyFlag
visR -- See (FC3) in Note [ForAllCo] in GHC.Core.TyCo.Rep
      = do { body_co' <- Coercion -> Maybe Coercion
setNominalRole_maybe_helper Coercion
body_co
           ; return (co { fco_body = body_co' }) }
    setNominalRole_maybe_helper (SelCo CoSel
cs Coercion
co) =
      -- NB, this case recurses via setNominalRole_maybe, not
      -- setNominalRole_maybe_helper!
      case CoSel
cs of
        SelTyCon Arity
n Role
_r ->
          -- Remember to update the role in SelTyCon to nominal;
          -- not doing this caused #23362.
          -- See the typing rule in Note [SelCo] in GHC.Core.TyCo.Rep.
          CoSel -> Coercion -> Coercion
SelCo (Arity -> Role -> CoSel
SelTyCon Arity
n Role
Nominal) (Coercion -> Coercion) -> Maybe Coercion -> Maybe Coercion
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Role -> Coercion -> Maybe Coercion
setNominalRole_maybe (Coercion -> Role
coercionRole Coercion
co) Coercion
co
        SelFun FunSel
fs ->
          CoSel -> Coercion -> Coercion
SelCo (FunSel -> CoSel
SelFun FunSel
fs) (Coercion -> Coercion) -> Maybe Coercion -> Maybe Coercion
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Role -> Coercion -> Maybe Coercion
setNominalRole_maybe (Coercion -> Role
coercionRole Coercion
co) Coercion
co
        CoSel
SelForAll ->
          String -> SDoc -> Maybe Coercion
forall a. HasCallStack => String -> SDoc -> a
pprPanic String
"setNominalRole_maybe: the coercion should already be nominal" (Coercion -> SDoc
forall a. Outputable a => a -> SDoc
ppr Coercion
co)
    setNominalRole_maybe_helper (InstCo Coercion
co Coercion
arg)
      = Coercion -> Coercion -> Coercion
InstCo (Coercion -> Coercion -> Coercion)
-> Maybe Coercion -> Maybe (Coercion -> Coercion)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Coercion -> Maybe Coercion
setNominalRole_maybe_helper Coercion
co Maybe (Coercion -> Coercion) -> Maybe Coercion -> Maybe Coercion
forall a b. Maybe (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Coercion -> Maybe Coercion
forall a. a -> Maybe a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Coercion
arg
    setNominalRole_maybe_helper co :: Coercion
co@(UnivCo { uco_prov :: Coercion -> UnivCoProvenance
uco_prov = UnivCoProvenance
prov })
      | case UnivCoProvenance
prov of PhantomProv {}    -> Bool
False  -- should always be phantom
                     ProofIrrelProv {} -> Bool
True   -- it's always safe
                     PluginProv {}     -> Bool
False  -- who knows? This choice is conservative.
      = Coercion -> Maybe Coercion
forall a. a -> Maybe a
Just (Coercion -> Maybe Coercion) -> Coercion -> Maybe Coercion
forall a b. (a -> b) -> a -> b
$ Coercion
co { uco_role = Nominal }
    setNominalRole_maybe_helper Coercion
_ = Maybe Coercion
forall a. Maybe a
Nothing

-- | Make a phantom coercion between two types. The coercion passed
-- in must be a nominal coercion between the kinds of the
-- types.
mkPhantomCo :: Coercion -> Type -> Type -> Coercion
mkPhantomCo :: Coercion -> Type -> Type -> Coercion
mkPhantomCo Coercion
h Type
t1 Type
t2
  = UnivCoProvenance -> [Coercion] -> Role -> Type -> Type -> Coercion
mkUnivCo UnivCoProvenance
PhantomProv [Coercion
h] Role
Phantom Type
t1 Type
t2

-- takes any coercion and turns it into a Phantom coercion
toPhantomCo :: Coercion -> Coercion
toPhantomCo :: Coercion -> Coercion
toPhantomCo Coercion
co
  = Coercion -> Type -> Type -> Coercion
mkPhantomCo (Coercion -> Coercion
mkKindCo Coercion
co) Type
ty1 Type
ty2
  where Pair Type
ty1 Type
ty2 = HasDebugCallStack => Coercion -> Pair Type
Coercion -> Pair Type
coercionKind Coercion
co

-- Convert args to a TyConAppCo Nominal to the same TyConAppCo Representational
applyRoles :: TyCon -> [Coercion] -> [Coercion]
applyRoles :: TyCon -> [Coercion] -> [Coercion]
applyRoles = (Role -> Coercion -> Coercion)
-> [Role] -> [Coercion] -> [Coercion]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (Role -> Role -> Coercion -> Coercion
`downgradeRole` Role
Nominal) ([Role] -> [Coercion] -> [Coercion])
-> (TyCon -> [Role]) -> TyCon -> [Coercion] -> [Coercion]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TyCon -> [Role]
tyConRoleListRepresentational

-- The Role parameter is the Role of the TyConAppCo
-- defined here because this is intimately concerned with the implementation
-- of TyConAppCo
-- Always returns an infinite list (with a infinite tail of Nominal)
tyConRolesX :: Role -> TyCon -> Infinite Role
tyConRolesX :: Role -> TyCon -> Infinite Role
tyConRolesX Role
Representational TyCon
tc = TyCon -> Infinite Role
tyConRolesRepresentational TyCon
tc
tyConRolesX Role
role             TyCon
_  = Role -> Infinite Role
forall a. a -> Infinite a
Inf.repeat Role
role

tyConRoleListX :: Role -> TyCon -> [Role]
tyConRoleListX :: Role -> TyCon -> [Role]
tyConRoleListX Role
role = Infinite Role -> [Role]
forall a. Infinite a -> [a]
Inf.toList (Infinite Role -> [Role])
-> (TyCon -> Infinite Role) -> TyCon -> [Role]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Role -> TyCon -> Infinite Role
tyConRolesX Role
role

-- Returns the roles of the parameters of a tycon, with an infinite tail
-- of Nominal
tyConRolesRepresentational :: TyCon -> Infinite Role
tyConRolesRepresentational :: TyCon -> Infinite Role
tyConRolesRepresentational TyCon
tc = TyCon -> [Role]
tyConRoles TyCon
tc [Role] -> Infinite Role -> Infinite Role
forall (f :: * -> *) a.
Foldable f =>
f a -> Infinite a -> Infinite a
Inf.++ Role -> Infinite Role
forall a. a -> Infinite a
Inf.repeat Role
Nominal

-- Returns the roles of the parameters of a tycon, with an infinite tail
-- of Nominal
tyConRoleListRepresentational :: TyCon -> [Role]
tyConRoleListRepresentational :: TyCon -> [Role]
tyConRoleListRepresentational = Infinite Role -> [Role]
forall a. Infinite a -> [a]
Inf.toList (Infinite Role -> [Role])
-> (TyCon -> Infinite Role) -> TyCon -> [Role]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TyCon -> Infinite Role
tyConRolesRepresentational

tyConRole :: Role -> TyCon -> Int -> Role
tyConRole :: Role -> TyCon -> Arity -> Role
tyConRole Role
Nominal          TyCon
_  Arity
_ = Role
Nominal
tyConRole Role
Phantom          TyCon
_  Arity
_ = Role
Phantom
tyConRole Role
Representational TyCon
tc Arity
n = TyCon -> Infinite Role
tyConRolesRepresentational TyCon
tc Infinite Role -> Arity -> Role
forall a. Infinite a -> Arity -> a
Inf.!! Arity
n

funRole :: Role -> FunSel -> Role
funRole :: Role -> FunSel -> Role
funRole Role
Nominal          FunSel
_  = Role
Nominal
funRole Role
Phantom          FunSel
_  = Role
Phantom
funRole Role
Representational FunSel
fs = FunSel -> Role
funRoleRepresentational FunSel
fs

funRoleRepresentational :: FunSel -> Role
funRoleRepresentational :: FunSel -> Role
funRoleRepresentational FunSel
SelMult = Role
Nominal
funRoleRepresentational FunSel
SelArg  = Role
Representational
funRoleRepresentational FunSel
SelRes  = Role
Representational

ltRole :: Role -> Role -> Bool
-- Is one role "less" than another?
--     Nominal < Representational < Phantom
ltRole :: Role -> Role -> Bool
ltRole Role
Phantom          Role
_       = Bool
False
ltRole Role
Representational Role
Phantom = Bool
True
ltRole Role
Representational Role
_       = Bool
False
ltRole Role
Nominal          Role
Nominal = Bool
False
ltRole Role
Nominal          Role
_       = Bool
True

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

-- | like mkKindCo, but aggressively & recursively optimizes to avoid using
-- a KindCo constructor. The output role is nominal.
promoteCoercion :: HasDebugCallStack => Coercion -> CoercionN

-- First cases handles anything that should yield refl.
promoteCoercion :: HasDebugCallStack => Coercion -> Coercion
promoteCoercion Coercion
co = case Coercion
co of

    Refl Type
_ -> Type -> Coercion
mkNomReflCo Type
ki1

    GRefl Role
_ Type
_ MCoercion
MRefl -> Type -> Coercion
mkNomReflCo Type
ki1

    GRefl Role
_ Type
_ (MCo Coercion
co) -> Coercion
co

    Coercion
_ | Type
ki1 HasCallStack => Type -> Type -> Bool
Type -> Type -> Bool
`eqType` Type
ki2
      -> Type -> Coercion
mkNomReflCo (HasDebugCallStack => Type -> Type
Type -> Type
typeKind Type
ty1)
     -- No later branch should return refl
     -- The assert (False )s throughout
     -- are these cases explicitly, but they should never fire.

    TyConAppCo Role
_ TyCon
tc [Coercion]
args
      | Just Coercion
co' <- Coercion -> [Coercion] -> Maybe Coercion
instCoercions (Type -> Coercion
mkNomReflCo (TyCon -> Type
tyConKind TyCon
tc)) [Coercion]
args
      -> Coercion
co'
      | Bool
otherwise
      -> Coercion -> Coercion
mkKindCo Coercion
co

    AppCo Coercion
co1 Coercion
arg
      | Just Coercion
co' <- Pair Type -> Coercion -> Coercion -> Maybe Coercion
instCoercion (HasDebugCallStack => Coercion -> Pair Type
Coercion -> Pair Type
coercionKind (Coercion -> Coercion
mkKindCo Coercion
co1))
                                 (HasDebugCallStack => Coercion -> Coercion
Coercion -> Coercion
promoteCoercion Coercion
co1) Coercion
arg
      -> Coercion
co'
      | Bool
otherwise
      -> Coercion -> Coercion
mkKindCo Coercion
co

    ForAllCo { fco_tcv :: Coercion -> CoVar
fco_tcv = CoVar
tv, fco_body :: Coercion -> Coercion
fco_body = Coercion
g }
      | CoVar -> Bool
isTyVar CoVar
tv
      -> HasDebugCallStack => Coercion -> Coercion
Coercion -> Coercion
promoteCoercion Coercion
g

    ForAllCo {}
      -> Bool -> Coercion -> Coercion
forall a. HasCallStack => Bool -> a -> a
assert Bool
False (Coercion -> Coercion) -> Coercion -> Coercion
forall a b. (a -> b) -> a -> b
$
            -- (ForAllCo {} :: (forall cv.t1) ~ (forall cv.t2)
            -- The tyvar case is handled above, so the bound var is a
            -- a coercion variable. So both sides have kind Type
            -- (Note [Weird typing rule for ForAllTy] in GHC.Core.TyCo.Rep).
            -- So the result is Refl, and that should have been caught by
            -- the first equation above.  Hence `assert False`
         Type -> Coercion
mkNomReflCo Type
liftedTypeKind

    FunCo {} -> Coercion -> Coercion
mkKindCo Coercion
co
       -- We can get Type~Constraint or Constraint~Type
       -- from FunCo {} :: (a -> (b::Type)) ~ (a -=> (b'::Constraint))

    CoVarCo {} -> Coercion -> Coercion
mkKindCo Coercion
co
    HoleCo {}  -> Coercion -> Coercion
mkKindCo Coercion
co
    AxiomCo {} -> Coercion -> Coercion
mkKindCo Coercion
co
    UnivCo {}  -> Coercion -> Coercion
mkKindCo Coercion
co  -- We could instead return the (single) `uco_deps` coercion in
                               -- the `ProofIrrelProv` and `PhantomProv` cases, but it doesn't
                               -- quite seem worth doing.

    SymCo Coercion
g
      -> Coercion -> Coercion
mkSymCo (HasDebugCallStack => Coercion -> Coercion
Coercion -> Coercion
promoteCoercion Coercion
g)

    TransCo Coercion
co1 Coercion
co2
      -> Coercion -> Coercion -> Coercion
mkTransCo (HasDebugCallStack => Coercion -> Coercion
Coercion -> Coercion
promoteCoercion Coercion
co1) (HasDebugCallStack => Coercion -> Coercion
Coercion -> Coercion
promoteCoercion Coercion
co2)

    SelCo CoSel
n Coercion
co1
      | Just Coercion
co' <- HasDebugCallStack => CoSel -> Coercion -> Maybe Coercion
CoSel -> Coercion -> Maybe Coercion
mkSelCo_maybe CoSel
n Coercion
co1
      -> HasDebugCallStack => Coercion -> Coercion
Coercion -> Coercion
promoteCoercion Coercion
co'

      | Bool
otherwise
      -> Coercion -> Coercion
mkKindCo Coercion
co

    LRCo LeftOrRight
lr Coercion
co1
      | Just (Coercion
lco, Coercion
rco) <- Coercion -> Maybe (Coercion, Coercion)
splitAppCo_maybe Coercion
co1
      -> case LeftOrRight
lr of
           LeftOrRight
CLeft  -> HasDebugCallStack => Coercion -> Coercion
Coercion -> Coercion
promoteCoercion Coercion
lco
           LeftOrRight
CRight -> HasDebugCallStack => Coercion -> Coercion
Coercion -> Coercion
promoteCoercion Coercion
rco

      | Bool
otherwise
      -> Coercion -> Coercion
mkKindCo Coercion
co

    InstCo Coercion
g Coercion
_
      | Type -> Bool
isForAllTy_ty Type
ty1
      -> Bool -> Coercion -> Coercion
forall a. HasCallStack => Bool -> a -> a
assert (Type -> Bool
isForAllTy_ty Type
ty2) (Coercion -> Coercion) -> Coercion -> Coercion
forall a b. (a -> b) -> a -> b
$
         HasDebugCallStack => Coercion -> Coercion
Coercion -> Coercion
promoteCoercion Coercion
g
      | Bool
otherwise
      -> Bool -> Coercion -> Coercion
forall a. HasCallStack => Bool -> a -> a
assert Bool
False (Coercion -> Coercion) -> Coercion -> Coercion
forall a b. (a -> b) -> a -> b
$
         Type -> Coercion
mkNomReflCo Type
liftedTypeKind
           -- See Note [Weird typing rule for ForAllTy] in GHC.Core.TyCo.Rep

    KindCo Coercion
_
      -> Bool -> Coercion -> Coercion
forall a. HasCallStack => Bool -> a -> a
assert Bool
False (Coercion -> Coercion) -> Coercion -> Coercion
forall a b. (a -> b) -> a -> b
$ -- See the first equation above
         Type -> Coercion
mkNomReflCo Type
liftedTypeKind

    SubCo Coercion
g
      -> HasDebugCallStack => Coercion -> Coercion
Coercion -> Coercion
promoteCoercion Coercion
g

  where
    Pair Type
ty1 Type
ty2 = HasDebugCallStack => Coercion -> Pair Type
Coercion -> Pair Type
coercionKind Coercion
co
    ki1 :: Type
ki1 = HasDebugCallStack => Type -> Type
Type -> Type
typeKind Type
ty1
    ki2 :: Type
ki2 = HasDebugCallStack => Type -> Type
Type -> Type
typeKind Type
ty2

-- | say @g = promoteCoercion h@. Then, @instCoercion g w@ yields @Just g'@,
-- where @g' = promoteCoercion (h w)@.
-- fails if this is not possible, if @g@ coerces between a forall and an ->
-- or if second parameter has a representational role and can't be used
-- with an InstCo.
instCoercion :: Pair Type -- g :: lty ~ rty
             -> CoercionN  -- ^  must be nominal
             -> Coercion
             -> Maybe CoercionN
instCoercion :: Pair Type -> Coercion -> Coercion -> Maybe Coercion
instCoercion (Pair Type
lty Type
rty) Coercion
g Coercion
w
  | (Type -> Bool
isForAllTy_ty Type
lty Bool -> Bool -> Bool
&& Type -> Bool
isForAllTy_ty Type
rty)
  Bool -> Bool -> Bool
|| (Type -> Bool
isForAllTy_co Type
lty Bool -> Bool -> Bool
&& Type -> Bool
isForAllTy_co Type
rty)
  , Just Coercion
w' <- Role -> Coercion -> Maybe Coercion
setNominalRole_maybe (Coercion -> Role
coercionRole Coercion
w) Coercion
w
    -- g :: (forall t1. t2) ~ (forall t1. t3)
    -- w :: s1 ~ s2
    -- returns mkInstCo g w' :: t2 [t1 |-> s1 ] ~ t3 [t1 |-> s2]
  = Coercion -> Maybe Coercion
forall a. a -> Maybe a
Just (Coercion -> Maybe Coercion) -> Coercion -> Maybe Coercion
forall a b. (a -> b) -> a -> b
$ Coercion -> Coercion -> Coercion
mkInstCo Coercion
g Coercion
w'

  | Type -> Bool
isFunTy Type
lty Bool -> Bool -> Bool
&& Type -> Bool
isFunTy Type
rty
    -- g :: (t1 -> t2) ~ (t3 -> t4)
    -- returns t2 ~ t4
  = Coercion -> Maybe Coercion
forall a. a -> Maybe a
Just (Coercion -> Maybe Coercion) -> Coercion -> Maybe Coercion
forall a b. (a -> b) -> a -> b
$ HasDebugCallStack => CoSel -> Coercion -> Coercion
CoSel -> Coercion -> Coercion
mkSelCo (FunSel -> CoSel
SelFun FunSel
SelRes) Coercion
g -- extract result type

  | Bool
otherwise -- one forall, one funty...
  = Maybe Coercion
forall a. Maybe a
Nothing

-- | Repeated use of 'instCoercion'
instCoercions :: CoercionN -> [Coercion] -> Maybe CoercionN
instCoercions :: Coercion -> [Coercion] -> Maybe Coercion
instCoercions Coercion
g [Coercion]
ws
  = let arg_ty_pairs :: [Pair Type]
arg_ty_pairs = (Coercion -> Pair Type) -> [Coercion] -> [Pair Type]
forall a b. (a -> b) -> [a] -> [b]
map HasDebugCallStack => Coercion -> Pair Type
Coercion -> Pair Type
coercionKind [Coercion]
ws in
    (Pair Type, Coercion) -> Coercion
forall a b. (a, b) -> b
snd ((Pair Type, Coercion) -> Coercion)
-> Maybe (Pair Type, Coercion) -> Maybe Coercion
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ((Pair Type, Coercion)
 -> (Pair Type, Coercion) -> Maybe (Pair Type, Coercion))
-> (Pair Type, Coercion)
-> [(Pair Type, Coercion)]
-> Maybe (Pair Type, Coercion)
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM (Pair Type, Coercion)
-> (Pair Type, Coercion) -> Maybe (Pair Type, Coercion)
go (HasDebugCallStack => Coercion -> Pair Type
Coercion -> Pair Type
coercionKind Coercion
g, Coercion
g) ([Pair Type] -> [Coercion] -> [(Pair Type, Coercion)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Pair Type]
arg_ty_pairs [Coercion]
ws)
  where
    go :: (Pair Type, Coercion) -> (Pair Type, Coercion)
       -> Maybe (Pair Type, Coercion)
    go :: (Pair Type, Coercion)
-> (Pair Type, Coercion) -> Maybe (Pair Type, Coercion)
go (Pair Type
g_tys, Coercion
g) (Pair Type
w_tys, Coercion
w)
      = do { g' <- Pair Type -> Coercion -> Coercion -> Maybe Coercion
instCoercion Pair Type
g_tys Coercion
g Coercion
w
           ; return (piResultTy <$> g_tys <*> w_tys, g') }

-- | 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 :: Coercion
-> Role -> Type -> Type -> Coercion -> Coercion -> Coercion
castCoercionKind2 Coercion
g Role
r Type
t1 Type
t2 Coercion
h1 Coercion
h2
  = Role -> Type -> Coercion -> Coercion -> Coercion
mkCoherenceRightCo Role
r Type
t2 Coercion
h2 (Role -> Type -> Coercion -> Coercion -> Coercion
mkCoherenceLeftCo Role
r Type
t1 Coercion
h1 Coercion
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 :: Coercion -> Role -> Type -> Type -> Coercion -> Coercion
castCoercionKind1 Coercion
g Role
r Type
t1 Type
t2 Coercion
h
  = case Coercion
g of
      Refl {} -> Bool -> Coercion -> Coercion
forall a. HasCallStack => Bool -> a -> a
assert (Role
r Role -> Role -> Bool
forall a. Eq a => a -> a -> Bool
== Role
Nominal) (Coercion -> Coercion) -> Coercion -> Coercion
forall a b. (a -> b) -> a -> b
$ -- Refl is always Nominal
                 Type -> Coercion
mkNomReflCo (Type -> Coercion -> Type
mkCastTy Type
t2 Coercion
h)
      GRefl Role
_ Type
_ MCoercion
mco -> case MCoercion
mco of
           MCoercion
MRefl       -> Role -> Type -> Coercion
mkReflCo Role
r (Type -> Coercion -> Type
mkCastTy Type
t2 Coercion
h)
           MCo Coercion
kind_co -> Role -> Type -> MCoercion -> Coercion
GRefl Role
r (Type -> Coercion -> Type
mkCastTy Type
t1 Coercion
h) (MCoercion -> Coercion) -> MCoercion -> Coercion
forall a b. (a -> b) -> a -> b
$
                          Coercion -> MCoercion
MCo (Coercion -> Coercion
mkSymCo Coercion
h Coercion -> Coercion -> Coercion
`mkTransCo` Coercion
kind_co Coercion -> Coercion -> Coercion
`mkTransCo` Coercion
h)
      Coercion
_ -> Coercion
-> Role -> Type -> Type -> Coercion -> Coercion -> Coercion
castCoercionKind2 Coercion
g Role
r Type
t1 Type
t2 Coercion
h Coercion
h

-- | Creates a new coercion with both of its types casted by different casts
-- @castCoercionKind g h1 h2@, where @g :: t1 ~r t2@,
-- has type @(t1 |> h1) ~r (t2 |> h2)@.
-- @h1@ and @h2@ must be nominal.
-- It calls @coercionKindRole@, so it's quite inefficient (which 'I' stands for)
-- Use @castCoercionKind2@ instead if @t1@, @t2@, and @r@ are known beforehand.
castCoercionKind :: Coercion -> CoercionN -> CoercionN -> Coercion
castCoercionKind :: Coercion -> Coercion -> Coercion -> Coercion
castCoercionKind Coercion
g Coercion
h1 Coercion
h2
  = Coercion
-> Role -> Type -> Type -> Coercion -> Coercion -> Coercion
castCoercionKind2 Coercion
g Role
r Type
t1 Type
t2 Coercion
h1 Coercion
h2
  where
    (Pair Type
t1 Type
t2, Role
r) = Coercion -> (Pair Type, Role)
coercionKindRole Coercion
g

mkPiCos :: Role -> [Var] -> Coercion -> Coercion
mkPiCos :: Role -> [CoVar] -> Coercion -> Coercion
mkPiCos Role
r [CoVar]
vs Coercion
co = (CoVar -> Coercion -> Coercion) -> Coercion -> [CoVar] -> Coercion
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (Role -> CoVar -> Coercion -> Coercion
mkPiCo Role
r) Coercion
co [CoVar]
vs

-- | Make a forall 'Coercion', where both types related by the coercion
-- are quantified over the same variable.
mkPiCo  :: Role -> Var -> Coercion -> Coercion
mkPiCo :: Role -> CoVar -> Coercion -> Coercion
mkPiCo Role
r CoVar
v Coercion
co | CoVar -> Bool
isTyVar CoVar
v = [ForAllTyBinder] -> Coercion -> Coercion
mkHomoForAllCos [CoVar -> ForAllTyFlag -> ForAllTyBinder
forall var argf. var -> argf -> VarBndr var argf
Bndr CoVar
v ForAllTyFlag
coreTyLamForAllTyFlag] Coercion
co
              | CoVar -> Bool
isCoVar CoVar
v = Bool -> Coercion -> Coercion
forall a. HasCallStack => Bool -> a -> a
assert (Bool -> Bool
not (CoVar
v CoVar -> VarSet -> Bool
`elemVarSet` Coercion -> VarSet
tyCoVarsOfCo Coercion
co)) (Coercion -> Coercion) -> Coercion -> Coercion
forall a b. (a -> b) -> a -> b
$
                  -- We didn't call mkForAllCo here because if v does not appear
                  -- in co, the argument coercion will be nominal. But here we
                  -- want it to be r. It is only called in 'mkPiCos', which is
                  -- only used in GHC.Core.Opt.Simplify.Utils, where we are sure for
                  -- now (Aug 2018) v won't occur in co.
                            Role -> CoVar -> Coercion -> Coercion
mkFunResCo Role
r CoVar
v Coercion
co
              | Bool
otherwise = Role -> CoVar -> Coercion -> Coercion
mkFunResCo Role
r CoVar
v Coercion
co

mkFunResCo :: Role -> Id -> Coercion -> Coercion
-- Given res_co :: res1 ~ res2,
--   mkFunResCo r m arg res_co :: (arg -> res1) ~r (arg -> res2)
-- Reflexive in the multiplicity argument
mkFunResCo :: Role -> CoVar -> Coercion -> Coercion
mkFunResCo Role
role CoVar
id Coercion
res_co
  = HasDebugCallStack =>
Role -> Coercion -> Coercion -> Coercion -> Coercion
Role -> Coercion -> Coercion -> Coercion -> Coercion
mkFunCoNoFTF Role
role Coercion
mult Coercion
arg_co Coercion
res_co
  where
    arg_co :: Coercion
arg_co = Role -> Type -> Coercion
mkReflCo Role
role (CoVar -> Type
varType CoVar
id)
    mult :: Coercion
mult   = Type -> Coercion
multToCo (CoVar -> Type
varMult CoVar
id)

-- mkCoCast (c :: s1 ~?r t1) (g :: (s1 ~?r t1) ~#R (s2 ~?r t2)) :: s2 ~?r t2
-- The first coercion might be lifted or unlifted; thus the ~? above
-- Lifted and unlifted equalities take different numbers of arguments,
-- so we have to make sure to supply the right parameter to decomposeCo.
-- Also, note that the role of the first coercion is the same as the role of
-- the equalities related by the second coercion. The second coercion is
-- itself always representational.
mkCoCast :: Coercion -> CoercionR -> Coercion
mkCoCast :: Coercion -> Coercion -> Coercion
mkCoCast Coercion
c Coercion
g
  | (Coercion
g2:Coercion
g1:[Coercion]
_) <- [Coercion] -> [Coercion]
forall a. [a] -> [a]
reverse [Coercion]
co_list
  = Coercion -> Coercion
mkSymCo Coercion
g1 Coercion -> Coercion -> Coercion
`mkTransCo` Coercion
c Coercion -> Coercion -> Coercion
`mkTransCo` Coercion
g2

  | Bool
otherwise
  = String -> SDoc -> Coercion
forall a. HasCallStack => String -> SDoc -> a
pprPanic String
"mkCoCast" (Coercion -> SDoc
forall a. Outputable a => a -> SDoc
ppr Coercion
g SDoc -> SDoc -> SDoc
forall doc. IsDoc doc => doc -> doc -> doc
$$ Pair Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr (HasDebugCallStack => Coercion -> Pair Type
Coercion -> Pair Type
coercionKind Coercion
g))
  where
    -- g  :: (s1 ~# t1) ~# (s2 ~# t2)
    -- g1 :: s1 ~# s2
    -- g2 :: t1 ~# t2
    (TyCon
tc, [Type]
_) = Type -> (TyCon, [Type])
splitTyConApp (HasDebugCallStack => Coercion -> Type
Coercion -> Type
coercionLKind Coercion
g)
    co_list :: [Coercion]
co_list = Arity -> Coercion -> Infinite Role -> [Coercion]
decomposeCo (TyCon -> Arity
tyConArity TyCon
tc) Coercion
g (TyCon -> Infinite Role
tyConRolesRepresentational TyCon
tc)

{- Note [castCoercionKind1]
~~~~~~~~~~~~~~~~~~~~~~~~~~~
castCoercionKind1 deals with the very important special case of castCoercionKind2
where the two kind coercions are identical.  In that case we can exploit the
situation where the main coercion is reflexive, via the special cases for Refl
and GRefl.

This is important when rewriting  (ty |> co). We rewrite ty, yielding
   fco :: ty ~ ty'
and now we want a coercion xco between
   xco :: (ty |> co) ~ (ty' |> co)
That's exactly what castCoercionKind1 does.  And it's very very common for
fco to be Refl.  In that case we do NOT want to get some terrible composition
of mkLeftCoherenceCo and mkRightCoherenceCo, which is what castCoercionKind2
has to do in its full generality.  See #18413.
-}

{-
%************************************************************************
%*                                                                      *
            Newtypes
%*                                                                      *
%************************************************************************
-}

-- | If `instNewTyCon_maybe T ts = Just (rep_ty, co)`
--   then `co :: T ts ~R# rep_ty`
--
-- Checks for a newtype, and for being saturated
instNewTyCon_maybe :: TyCon -> [Type] -> Maybe (Type, Coercion)
instNewTyCon_maybe :: TyCon -> [Type] -> Maybe (Type, Coercion)
instNewTyCon_maybe TyCon
tc [Type]
tys
  | Just ([CoVar]
tvs, Type
ty, CoAxiom Unbranched
co_tc) <- TyCon -> Maybe ([CoVar], Type, CoAxiom Unbranched)
unwrapNewTyConEtad_maybe TyCon
tc  -- Check for newtype
  , [CoVar]
tvs [CoVar] -> [Type] -> Bool
forall a b. [a] -> [b] -> Bool
`leLength` [Type]
tys                                    -- Check saturated enough
  = (Type, Coercion) -> Maybe (Type, Coercion)
forall a. a -> Maybe a
Just ([CoVar] -> Type -> [Type] -> Type
HasDebugCallStack => [CoVar] -> Type -> [Type] -> Type
applyTysX [CoVar]
tvs Type
ty [Type]
tys, Role -> CoAxiom Unbranched -> [Type] -> [Coercion] -> Coercion
mkUnbranchedAxInstCo Role
Representational CoAxiom Unbranched
co_tc [Type]
tys [])
  | Bool
otherwise
  = Maybe (Type, Coercion)
forall a. Maybe a
Nothing

{-
************************************************************************
*                                                                      *
         Type normalisation
*                                                                      *
************************************************************************
-}

-- | A function to check if we can reduce a type by one step. Used
-- with 'topNormaliseTypeX'.
type NormaliseStepper ev = RecTcChecker
                         -> TyCon     -- tc
                         -> [Type]    -- tys
                         -> NormaliseStepResult ev

-- | The result of stepping in a normalisation function.
-- See 'topNormaliseTypeX'.
data NormaliseStepResult ev
  = NS_Done   -- ^ Nothing more to do
  | NS_Abort  -- ^ Utter failure. The outer function should fail too.
  | NS_Step RecTcChecker Type ev    -- ^ We stepped, yielding new bits;
                                    -- ^ ev is evidence;
                                    -- Usually a co :: old type ~ new type
  deriving ((forall a b.
 (a -> b) -> NormaliseStepResult a -> NormaliseStepResult b)
-> (forall a b.
    a -> NormaliseStepResult b -> NormaliseStepResult a)
-> Functor NormaliseStepResult
forall a b. a -> NormaliseStepResult b -> NormaliseStepResult a
forall a b.
(a -> b) -> NormaliseStepResult a -> NormaliseStepResult b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
$cfmap :: forall a b.
(a -> b) -> NormaliseStepResult a -> NormaliseStepResult b
fmap :: forall a b.
(a -> b) -> NormaliseStepResult a -> NormaliseStepResult b
$c<$ :: forall a b. a -> NormaliseStepResult b -> NormaliseStepResult a
<$ :: forall a b. a -> NormaliseStepResult b -> NormaliseStepResult a
Functor)

instance Outputable ev => Outputable (NormaliseStepResult ev) where
  ppr :: NormaliseStepResult ev -> SDoc
ppr NormaliseStepResult ev
NS_Done           = String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"NS_Done"
  ppr NormaliseStepResult ev
NS_Abort          = String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"NS_Abort"
  ppr (NS_Step RecTcChecker
_ Type
ty ev
ev) = [SDoc] -> SDoc
forall doc. IsLine doc => [doc] -> doc
sep [String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"NS_Step", Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
ty, ev -> SDoc
forall a. Outputable a => a -> SDoc
ppr ev
ev]

-- | Try one stepper and then try the next, if the first doesn't make
-- progress.
-- So if it returns NS_Done, it means that both steppers are satisfied
composeSteppers :: NormaliseStepper ev -> NormaliseStepper ev
                -> NormaliseStepper ev
composeSteppers :: forall ev.
NormaliseStepper ev -> NormaliseStepper ev -> NormaliseStepper ev
composeSteppers NormaliseStepper ev
step1 NormaliseStepper ev
step2 RecTcChecker
rec_nts TyCon
tc [Type]
tys
  = case NormaliseStepper ev
step1 RecTcChecker
rec_nts TyCon
tc [Type]
tys of
      success :: NormaliseStepResult ev
success@(NS_Step {}) -> NormaliseStepResult ev
success
      NormaliseStepResult ev
NS_Done              -> NormaliseStepper ev
step2 RecTcChecker
rec_nts TyCon
tc [Type]
tys
      NormaliseStepResult ev
NS_Abort             -> NormaliseStepResult ev
forall ev. NormaliseStepResult ev
NS_Abort

-- | A 'NormaliseStepper' that unwraps newtypes, careful not to fall into
-- a loop. If it would fall into a loop, it produces 'NS_Abort'.
unwrapNewTypeStepper :: NormaliseStepper Coercion
unwrapNewTypeStepper :: NormaliseStepper Coercion
unwrapNewTypeStepper RecTcChecker
rec_nts TyCon
tc [Type]
tys
  | Just (Type
ty', Coercion
co) <- TyCon -> [Type] -> Maybe (Type, Coercion)
instNewTyCon_maybe TyCon
tc [Type]
tys
  = -- pprTrace "unNS" (ppr tc <+> ppr (getUnique tc) <+> ppr tys $$ ppr ty' $$ ppr rec_nts) $
    case RecTcChecker -> TyCon -> Maybe RecTcChecker
checkRecTc RecTcChecker
rec_nts TyCon
tc of
      Just RecTcChecker
rec_nts' -> RecTcChecker -> Type -> Coercion -> NormaliseStepResult Coercion
forall ev. RecTcChecker -> Type -> ev -> NormaliseStepResult ev
NS_Step RecTcChecker
rec_nts' Type
ty' Coercion
co
      Maybe RecTcChecker
Nothing       -> NormaliseStepResult Coercion
forall ev. NormaliseStepResult ev
NS_Abort

  | Bool
otherwise
  = NormaliseStepResult Coercion
forall ev. NormaliseStepResult ev
NS_Done

-- | A general function for normalising the top-level of a type. It continues
-- to use the provided 'NormaliseStepper' until that function fails, and then
-- this function returns. The roles of the coercions produced by the
-- 'NormaliseStepper' must all be the same, which is the role returned from
-- the call to 'topNormaliseTypeX'.
--
-- Typically ev is Coercion.
--
-- If topNormaliseTypeX step plus ty = Just (ev, ty')
-- then ty ~ev1~ t1 ~ev2~ t2 ... ~evn~ ty'
-- and ev = ev1 `plus` ev2 `plus` ... `plus` evn
-- If it returns Nothing then no newtype unwrapping could happen
topNormaliseTypeX :: NormaliseStepper ev
                  -> (ev -> ev -> ev)
                  -> Type -> Maybe (ev, Type)
topNormaliseTypeX :: forall ev.
NormaliseStepper ev -> (ev -> ev -> ev) -> Type -> Maybe (ev, Type)
topNormaliseTypeX NormaliseStepper ev
stepper ev -> ev -> ev
plus Type
ty
 | Just (TyCon
tc, [Type]
tys) <- HasDebugCallStack => Type -> Maybe (TyCon, [Type])
Type -> Maybe (TyCon, [Type])
splitTyConApp_maybe Type
ty
 -- SPJ: The default threshold for initRecTc is 100 which is extremely dangerous
 --      for certain type synonyms, we should think about reducing it (see #20990)
 , NS_Step RecTcChecker
rec_nts Type
ty' ev
ev <- NormaliseStepper ev
stepper RecTcChecker
initRecTc TyCon
tc [Type]
tys
 = RecTcChecker -> ev -> Type -> Maybe (ev, Type)
go RecTcChecker
rec_nts ev
ev Type
ty'
 | Bool
otherwise
 = Maybe (ev, Type)
forall a. Maybe a
Nothing
 where
    go :: RecTcChecker -> ev -> Type -> Maybe (ev, Type)
go RecTcChecker
rec_nts ev
ev Type
ty
      | Just (TyCon
tc, [Type]
tys) <- HasDebugCallStack => Type -> Maybe (TyCon, [Type])
Type -> Maybe (TyCon, [Type])
splitTyConApp_maybe Type
ty
      = case NormaliseStepper ev
stepper RecTcChecker
rec_nts TyCon
tc [Type]
tys of
          NS_Step RecTcChecker
rec_nts' Type
ty' ev
ev' -> RecTcChecker -> ev -> Type -> Maybe (ev, Type)
go RecTcChecker
rec_nts' (ev
ev ev -> ev -> ev
`plus` ev
ev') Type
ty'
          NormaliseStepResult ev
NS_Done  -> (ev, Type) -> Maybe (ev, Type)
forall a. a -> Maybe a
Just (ev
ev, Type
ty)
          NormaliseStepResult ev
NS_Abort -> Maybe (ev, Type)
forall a. Maybe a
Nothing

      | Bool
otherwise
      = (ev, Type) -> Maybe (ev, Type)
forall a. a -> Maybe a
Just (ev
ev, Type
ty)

topNormaliseNewType_maybe :: Type -> Maybe (Coercion, Type)
-- ^ Sometimes we want to look through a @newtype@ and get its associated coercion.
-- This function strips off @newtype@ layers enough to reveal something that isn't
-- a @newtype@.  Specifically, here's the invariant:
--
-- > topNormaliseNewType_maybe rec_nts ty = Just (co, ty')
--
-- then (a)  @co : ty ~R ty'@.
--      (b)  ty' is not a newtype.
--
-- The function returns @Nothing@ for non-@newtypes@,
-- or unsaturated applications
--
-- This function does *not* look through type families, because it has no access to
-- the type family environment. If you do have that at hand, consider to use
-- topNormaliseType_maybe, which should be a drop-in replacement for
-- topNormaliseNewType_maybe
-- If topNormliseNewType_maybe ty = Just (co, ty'), then co : ty ~R ty'
topNormaliseNewType_maybe :: Type -> Maybe (Coercion, Type)
topNormaliseNewType_maybe Type
ty
  = NormaliseStepper Coercion
-> (Coercion -> Coercion -> Coercion)
-> Type
-> Maybe (Coercion, Type)
forall ev.
NormaliseStepper ev -> (ev -> ev -> ev) -> Type -> Maybe (ev, Type)
topNormaliseTypeX NormaliseStepper Coercion
unwrapNewTypeStepper Coercion -> Coercion -> Coercion
mkTransCo Type
ty

{-
%************************************************************************
%*                                                                      *
                   Comparison of coercions
%*                                                                      *
%************************************************************************
-}

-- | Syntactic equality of coercions
eqCoercion :: Coercion -> Coercion -> Bool
eqCoercion :: Coercion -> Coercion -> Bool
eqCoercion = HasCallStack => Type -> Type -> Bool
Type -> Type -> Bool
eqType (Type -> Type -> Bool)
-> (Coercion -> Type) -> Coercion -> Coercion -> Bool
forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` Coercion -> Type
coercionType

-- | Compare two 'Coercion's, with respect to an RnEnv2
eqCoercionX :: RnEnv2 -> Coercion -> Coercion -> Bool
eqCoercionX :: RnEnv2 -> Coercion -> Coercion -> Bool
eqCoercionX RnEnv2
env = HasCallStack => RnEnv2 -> Type -> Type -> Bool
RnEnv2 -> Type -> Type -> Bool
eqTypeX RnEnv2
env (Type -> Type -> Bool)
-> (Coercion -> Type) -> Coercion -> Coercion -> Bool
forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` Coercion -> Type
coercionType

{-
%************************************************************************
%*                                                                      *
                   "Lifting" substitution
           [(TyCoVar,Coercion)] -> Type -> Coercion
%*                                                                      *
%************************************************************************

Note [Lifting coercions over types: liftCoSubst]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
The KPUSH rule deals with this situation
   data T a = K (a -> Maybe a)
   g :: T t1 ~ T t2
   x :: t1 -> Maybe t1

   case (K @t1 x) |> g of
     K (y:t2 -> Maybe t2) -> rhs

We want to push the coercion inside the constructor application.
So we do this

   g' :: t1~t2  =  SelCo (SelTyCon 0) g

   case K @t2 (x |> g' -> Maybe g') of
     K (y:t2 -> Maybe t2) -> rhs

The crucial operation is that we
  * take the type of K's argument: a -> Maybe a
  * and substitute g' for a
thus giving *coercion*.  This is what liftCoSubst does.

In the presence of kind coercions, this is a bit
of a hairy operation. So, we refer you to the paper introducing kind coercions,
available at www.cis.upenn.edu/~sweirich/papers/fckinds-extended.pdf

Note [extendLiftingContextEx]
~~~~~~~~~~~~~~~~~~~~~~~~~~~
Consider we have datatype
  K :: /\k. /\a::k. P -> T k  -- P be some type
  g :: T k1 ~ T k2

  case (K @k1 @t1 x) |> g of
    K y -> rhs

We want to push the coercion inside the constructor application.
We first get the coercion mapped by the universal type variable k:
   lc = k |-> SelCo (SelTyCon 0) g :: k1~k2

Here, the important point is that the kind of a is coerced, and P might be
dependent on the existential type variable a.
Thus we first get the coercion of a's kind
   g2 = liftCoSubst lc k :: k1 ~ k2

Then we store a new mapping into the lifting context
   lc2 = a |-> (t1 ~ t1 |> g2), lc

So later when we can correctly deal with the argument type P
   liftCoSubst lc2 P :: P [k|->k1][a|->t1] ~ P[k|->k2][a |-> (t1|>g2)]

This is exactly what extendLiftingContextEx does.
* For each (tyvar:k, ty) pair, we product the mapping
    tyvar |-> (ty ~ ty |> (liftCoSubst lc k))
* For each (covar:s1~s2, ty) pair, we produce the mapping
    covar |-> (co ~ co')
    co' = Sym (liftCoSubst lc s1) ;; covar ;; liftCoSubst lc s2 :: s1'~s2'

This follows the lifting context extension definition in the
"FC with Explicit Kind Equality" paper.
-}

-- ----------------------------------------------------
-- See Note [Lifting coercions over types: liftCoSubst]
-- ----------------------------------------------------

data LiftingContext = LC Subst LiftCoEnv
  -- in optCoercion, we need to lift when optimizing InstCo.
  -- See Note [Optimising InstCo] in GHC.Core.Coercion.Opt
  -- We thus propagate the substitution from GHC.Core.Coercion.Opt here.

instance Outputable LiftingContext where
  ppr :: LiftingContext -> SDoc
ppr (LC Subst
_ LiftCoEnv
env) = SDoc -> Arity -> SDoc -> SDoc
hang (String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"LiftingContext:") Arity
2 (LiftCoEnv -> SDoc
forall a. Outputable a => a -> SDoc
ppr LiftCoEnv
env)

type LiftCoEnv = VarEnv Coercion
     -- Maps *type variables* to *coercions*.
     -- That's the whole point of this function!
     -- Also maps coercion variables to ProofIrrelCos.

-- like liftCoSubstWith, but allows for existentially-bound types as well
liftCoSubstWithEx :: Role          -- desired role for output coercion
                  -> [TyVar]       -- universally quantified tyvars
                  -> [Coercion]    -- coercions to substitute for those
                  -> [TyCoVar]     -- existentially quantified tycovars
                  -> [Type]        -- types and coercions to be bound to ex vars
                  -> (Type -> Coercion, [Type]) -- (lifting function, converted ex args)
liftCoSubstWithEx :: Role
-> [CoVar]
-> [Coercion]
-> [CoVar]
-> [Type]
-> (Type -> Coercion, [Type])
liftCoSubstWithEx Role
role [CoVar]
univs [Coercion]
omegas [CoVar]
exs [Type]
rhos
  = let theta :: LiftingContext
theta = [(CoVar, Coercion)] -> LiftingContext
mkLiftingContext (String -> [CoVar] -> [Coercion] -> [(CoVar, Coercion)]
forall a b. HasDebugCallStack => String -> [a] -> [b] -> [(a, b)]
zipEqual String
"liftCoSubstWithExU" [CoVar]
univs [Coercion]
omegas)
        psi :: LiftingContext
psi   = LiftingContext -> [(CoVar, Type)] -> LiftingContext
extendLiftingContextEx LiftingContext
theta (String -> [CoVar] -> [Type] -> [(CoVar, Type)]
forall a b. HasDebugCallStack => String -> [a] -> [b] -> [(a, b)]
zipEqual String
"liftCoSubstWithExX" [CoVar]
exs [Type]
rhos)
    in (LiftingContext -> Role -> Type -> Coercion
ty_co_subst LiftingContext
psi Role
role, HasDebugCallStack => Subst -> [Type] -> [Type]
Subst -> [Type] -> [Type]
substTys (LiftingContext -> Subst
lcSubstRight LiftingContext
psi) ([CoVar] -> [Type]
mkTyCoVarTys [CoVar]
exs))

liftCoSubstWith :: Role -> [TyCoVar] -> [Coercion] -> Type -> Coercion
liftCoSubstWith :: Role -> [CoVar] -> [Coercion] -> Type -> Coercion
liftCoSubstWith Role
r [CoVar]
tvs [Coercion]
cos Type
ty
  = HasDebugCallStack => Role -> LiftingContext -> Type -> Coercion
Role -> LiftingContext -> Type -> Coercion
liftCoSubst Role
r ([(CoVar, Coercion)] -> LiftingContext
mkLiftingContext ([(CoVar, Coercion)] -> LiftingContext)
-> [(CoVar, Coercion)] -> LiftingContext
forall a b. (a -> b) -> a -> b
$ String -> [CoVar] -> [Coercion] -> [(CoVar, Coercion)]
forall a b. HasDebugCallStack => String -> [a] -> [b] -> [(a, b)]
zipEqual String
"liftCoSubstWith" [CoVar]
tvs [Coercion]
cos) Type
ty

-- | @liftCoSubst role lc ty@ produces a coercion (at role @role@)
-- that coerces between @lc_left(ty)@ and @lc_right(ty)@, where
-- @lc_left@ is a substitution mapping type variables to the left-hand
-- types of the mapped coercions in @lc@, and similar for @lc_right@.
liftCoSubst :: HasDebugCallStack => Role -> LiftingContext -> Type -> Coercion
{-# INLINE liftCoSubst #-}
-- Inlining this function is worth 2% of allocation in T9872d,
liftCoSubst :: HasDebugCallStack => Role -> LiftingContext -> Type -> Coercion
liftCoSubst Role
r lc :: LiftingContext
lc@(LC Subst
subst LiftCoEnv
env) Type
ty
  | LiftCoEnv -> Bool
forall a. VarEnv a -> Bool
isEmptyVarEnv LiftCoEnv
env = Role -> Type -> Coercion
mkReflCo Role
r (HasDebugCallStack => Subst -> Type -> Type
Subst -> Type -> Type
substTy Subst
subst Type
ty)
  | Bool
otherwise         = LiftingContext -> Role -> Type -> Coercion
ty_co_subst LiftingContext
lc Role
r Type
ty

emptyLiftingContext :: InScopeSet -> LiftingContext
emptyLiftingContext :: InScopeSet -> LiftingContext
emptyLiftingContext InScopeSet
in_scope = Subst -> LiftCoEnv -> LiftingContext
LC (InScopeSet -> Subst
mkEmptySubst InScopeSet
in_scope) LiftCoEnv
forall a. VarEnv a
emptyVarEnv

mkLiftingContext :: [(TyCoVar,Coercion)] -> LiftingContext
mkLiftingContext :: [(CoVar, Coercion)] -> LiftingContext
mkLiftingContext [(CoVar, Coercion)]
pairs
  = Subst -> LiftCoEnv -> LiftingContext
LC (InScopeSet -> Subst
mkEmptySubst (InScopeSet -> Subst) -> InScopeSet -> Subst
forall a b. (a -> b) -> a -> b
$ VarSet -> InScopeSet
mkInScopeSet (VarSet -> InScopeSet) -> VarSet -> InScopeSet
forall a b. (a -> b) -> a -> b
$ [Coercion] -> VarSet
tyCoVarsOfCos (((CoVar, Coercion) -> Coercion)
-> [(CoVar, Coercion)] -> [Coercion]
forall a b. (a -> b) -> [a] -> [b]
map (CoVar, Coercion) -> Coercion
forall a b. (a, b) -> b
snd [(CoVar, Coercion)]
pairs))
       ([(CoVar, Coercion)] -> LiftCoEnv
forall a. [(CoVar, a)] -> VarEnv a
mkVarEnv [(CoVar, Coercion)]
pairs)

mkSubstLiftingContext :: Subst -> LiftingContext
mkSubstLiftingContext :: Subst -> LiftingContext
mkSubstLiftingContext Subst
subst = Subst -> LiftCoEnv -> LiftingContext
LC Subst
subst LiftCoEnv
forall a. VarEnv a
emptyVarEnv

liftingContextSubst :: LiftingContext -> Subst
liftingContextSubst :: LiftingContext -> Subst
liftingContextSubst (LC Subst
subst LiftCoEnv
_) = Subst
subst

-- | Extend a lifting context with a new mapping.
extendLiftingContext :: LiftingContext  -- ^ original LC
                     -> TyCoVar         -- ^ new variable to map...
                     -> Coercion        -- ^ ...to this lifted version
                     -> LiftingContext
    -- mappings to reflexive coercions are just substitutions
extendLiftingContext :: LiftingContext -> CoVar -> Coercion -> LiftingContext
extendLiftingContext (LC Subst
subst LiftCoEnv
env) CoVar
tv Coercion
arg
  | Just (Type
ty, Role
_) <- Coercion -> Maybe (Type, Role)
isReflCo_maybe Coercion
arg
  = Subst -> LiftCoEnv -> LiftingContext
LC (Subst -> CoVar -> Type -> Subst
extendTCvSubst Subst
subst CoVar
tv Type
ty) LiftCoEnv
env
  | Bool
otherwise
  = Subst -> LiftCoEnv -> LiftingContext
LC Subst
subst (LiftCoEnv -> CoVar -> Coercion -> LiftCoEnv
forall a. VarEnv a -> CoVar -> a -> VarEnv a
extendVarEnv LiftCoEnv
env CoVar
tv Coercion
arg)

-- | Extend the substitution component of a lifting context with
-- a new binding for a coercion variable. Used during coercion optimisation.
extendLiftingContextCvSubst :: LiftingContext
                            -> CoVar
                            -> Coercion
                            -> LiftingContext
extendLiftingContextCvSubst :: LiftingContext -> CoVar -> Coercion -> LiftingContext
extendLiftingContextCvSubst (LC Subst
subst LiftCoEnv
env) CoVar
cv Coercion
co
  = Subst -> LiftCoEnv -> LiftingContext
LC (Subst -> CoVar -> Coercion -> Subst
extendCvSubst Subst
subst CoVar
cv Coercion
co) LiftCoEnv
env

-- | Extend a lifting context with a new mapping, and extend the in-scope set
extendLiftingContextAndInScope :: LiftingContext  -- ^ Original LC
                               -> TyCoVar         -- ^ new variable to map...
                               -> Coercion        -- ^ to this coercion
                               -> LiftingContext
extendLiftingContextAndInScope :: LiftingContext -> CoVar -> Coercion -> LiftingContext
extendLiftingContextAndInScope (LC Subst
subst LiftCoEnv
env) CoVar
tv Coercion
co
  = LiftingContext -> CoVar -> Coercion -> LiftingContext
extendLiftingContext (Subst -> LiftCoEnv -> LiftingContext
LC (Subst -> VarSet -> Subst
extendSubstInScopeSet Subst
subst (Coercion -> VarSet
tyCoVarsOfCo Coercion
co)) LiftCoEnv
env) CoVar
tv Coercion
co

-- | Extend a lifting context with existential-variable bindings.
-- See Note [extendLiftingContextEx]
extendLiftingContextEx :: LiftingContext    -- ^ original lifting context
                       -> [(TyCoVar,Type)]  -- ^ ex. var / value pairs
                       -> LiftingContext
-- Note that this is more involved than extendLiftingContext. That function
-- takes a coercion to extend with, so it's assumed that the caller has taken
-- into account any of the kind-changing stuff worried about here.
extendLiftingContextEx :: LiftingContext -> [(CoVar, Type)] -> LiftingContext
extendLiftingContextEx LiftingContext
lc [] = LiftingContext
lc
extendLiftingContextEx lc :: LiftingContext
lc@(LC Subst
subst LiftCoEnv
env) ((CoVar
v,Type
ty):[(CoVar, Type)]
rest)
-- This function adds bindings for *Nominal* coercions. Why? Because it
-- works with existentially bound variables, which are considered to have
-- nominal roles.
  | CoVar -> Bool
isTyVar CoVar
v
  = let lc' :: LiftingContext
lc' = Subst -> LiftCoEnv -> LiftingContext
LC (Subst
subst Subst -> VarSet -> Subst
`extendSubstInScopeSet` Type -> VarSet
tyCoVarsOfType Type
ty)
                 (LiftCoEnv -> CoVar -> Coercion -> LiftCoEnv
forall a. VarEnv a -> CoVar -> a -> VarEnv a
extendVarEnv LiftCoEnv
env CoVar
v (Coercion -> LiftCoEnv) -> Coercion -> LiftCoEnv
forall a b. (a -> b) -> a -> b
$
                  Role -> Type -> Coercion -> Coercion
mkGReflRightCo Role
Nominal
                                 Type
ty
                                 (LiftingContext -> Role -> Type -> Coercion
ty_co_subst LiftingContext
lc Role
Nominal (CoVar -> Type
tyVarKind CoVar
v)))
    in LiftingContext -> [(CoVar, Type)] -> LiftingContext
extendLiftingContextEx LiftingContext
lc' [(CoVar, Type)]
rest
  | CoercionTy Coercion
co <- Type
ty
  = -- co      :: s1 ~r s2
    -- lift_s1 :: s1 ~r s1'
    -- lift_s2 :: s2 ~r s2'
    -- kco     :: (s1 ~r s2) ~N (s1' ~r s2')
    Bool -> LiftingContext -> LiftingContext
forall a. HasCallStack => Bool -> a -> a
assert (CoVar -> Bool
isCoVar CoVar
v) (LiftingContext -> LiftingContext)
-> LiftingContext -> LiftingContext
forall a b. (a -> b) -> a -> b
$
    let (Type
s1, Type
s2, Role
r) = HasDebugCallStack => CoVar -> (Type, Type, Role)
CoVar -> (Type, Type, Role)
coVarTypesRole CoVar
v
        lift_s1 :: Coercion
lift_s1 = LiftingContext -> Role -> Type -> Coercion
ty_co_subst LiftingContext
lc Role
r Type
s1
        lift_s2 :: Coercion
lift_s2 = LiftingContext -> Role -> Type -> Coercion
ty_co_subst LiftingContext
lc Role
r Type
s2
        kco :: Coercion
kco     = HasDebugCallStack => Role -> TyCon -> [Coercion] -> Coercion
Role -> TyCon -> [Coercion] -> Coercion
mkTyConAppCo Role
Nominal (Role -> TyCon
equalityTyCon Role
r)
                               [ Coercion -> Coercion
mkKindCo Coercion
lift_s1, Coercion -> Coercion
mkKindCo Coercion
lift_s2
                               , Coercion
lift_s1         , Coercion
lift_s2          ]
        lc' :: LiftingContext
lc'     = Subst -> LiftCoEnv -> LiftingContext
LC (Subst
subst Subst -> VarSet -> Subst
`extendSubstInScopeSet` Coercion -> VarSet
tyCoVarsOfCo Coercion
co)
                     (LiftCoEnv -> CoVar -> Coercion -> LiftCoEnv
forall a. VarEnv a -> CoVar -> a -> VarEnv a
extendVarEnv LiftCoEnv
env CoVar
v
                        (Role -> Coercion -> Coercion -> Coercion -> Coercion
mkProofIrrelCo Role
Nominal Coercion
kco Coercion
co (Coercion -> Coercion) -> Coercion -> Coercion
forall a b. (a -> b) -> a -> b
$
                          (Coercion -> Coercion
mkSymCo Coercion
lift_s1) Coercion -> Coercion -> Coercion
`mkTransCo` Coercion
co Coercion -> Coercion -> Coercion
`mkTransCo` Coercion
lift_s2))
    in LiftingContext -> [(CoVar, Type)] -> LiftingContext
extendLiftingContextEx LiftingContext
lc' [(CoVar, Type)]
rest
  | Bool
otherwise
  = String -> SDoc -> LiftingContext
forall a. HasCallStack => String -> SDoc -> a
pprPanic String
"extendLiftingContextEx" (CoVar -> SDoc
forall a. Outputable a => a -> SDoc
ppr CoVar
v SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"|->" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
ty)


-- | Erase the environments in a lifting context
zapLiftingContext :: LiftingContext -> LiftingContext
zapLiftingContext :: LiftingContext -> LiftingContext
zapLiftingContext (LC Subst
subst LiftCoEnv
_) = Subst -> LiftCoEnv -> LiftingContext
LC (Subst -> Subst
zapSubst Subst
subst) LiftCoEnv
forall a. VarEnv a
emptyVarEnv

-- | Like 'substForAllCoBndr', but works on a lifting context
substForAllCoBndrUsingLC :: Bool
                            -> (Coercion -> Coercion)
                            -> LiftingContext -> TyCoVar -> Coercion
                            -> (LiftingContext, TyCoVar, Coercion)
substForAllCoBndrUsingLC :: Bool
-> (Coercion -> Coercion)
-> LiftingContext
-> CoVar
-> Coercion
-> (LiftingContext, CoVar, Coercion)
substForAllCoBndrUsingLC Bool
sym Coercion -> Coercion
sco (LC Subst
subst LiftCoEnv
lc_env) CoVar
tv Coercion
co
  = (Subst -> LiftCoEnv -> LiftingContext
LC Subst
subst' LiftCoEnv
lc_env, CoVar
tv', Coercion
co')
  where
    (Subst
subst', CoVar
tv', Coercion
co') = Bool
-> (Coercion -> Coercion)
-> Subst
-> CoVar
-> Coercion
-> (Subst, CoVar, Coercion)
substForAllCoBndrUsing Bool
sym Coercion -> Coercion
sco Subst
subst CoVar
tv Coercion
co

-- | The \"lifting\" operation which substitutes coercions for type
--   variables in a type to produce a coercion.
--
--   For the inverse operation, see 'liftCoMatch'
ty_co_subst :: LiftingContext -> Role -> Type -> Coercion
ty_co_subst :: LiftingContext -> Role -> Type -> Coercion
ty_co_subst !LiftingContext
lc Role
role Type
ty
    -- !lc: making this function strict in lc allows callers to
    -- pass its two components separately, rather than boxing them.
    -- Unfortunately, Boxity Analysis concludes that we need lc boxed
    -- because it's used that way in liftCoSubstTyVarBndrUsing.
  = Role -> Type -> Coercion
go Role
role Type
ty
  where
    go :: Role -> Type -> Coercion
    go :: Role -> Type -> Coercion
go Role
r Type
ty                 | Just Type
ty' <- Type -> Maybe Type
coreView Type
ty
                            = Role -> Type -> Coercion
go Role
r Type
ty'
    go Role
Phantom Type
ty           = Type -> Coercion
lift_phantom Type
ty
    go Role
r (TyVarTy CoVar
tv)       = String -> Maybe Coercion -> Coercion
forall a. HasDebugCallStack => String -> Maybe a -> a
expectJust String
"ty_co_subst bad roles" (Maybe Coercion -> Coercion) -> Maybe Coercion -> Coercion
forall a b. (a -> b) -> a -> b
$
                              LiftingContext -> Role -> CoVar -> Maybe Coercion
liftCoSubstTyVar LiftingContext
lc Role
r CoVar
tv
    go Role
r (AppTy Type
ty1 Type
ty2)    = Coercion -> Coercion -> Coercion
mkAppCo (Role -> Type -> Coercion
go Role
r Type
ty1) (Role -> Type -> Coercion
go Role
Nominal Type
ty2)
    go Role
r (TyConApp TyCon
tc [Type]
tys)  = HasDebugCallStack => Role -> TyCon -> [Coercion] -> Coercion
Role -> TyCon -> [Coercion] -> Coercion
mkTyConAppCo Role
r TyCon
tc ((Role -> Type -> Coercion) -> [Role] -> [Type] -> [Coercion]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith Role -> Type -> Coercion
go (Role -> TyCon -> [Role]
tyConRoleListX Role
r TyCon
tc) [Type]
tys)
    go Role
r (FunTy FunTyFlag
af Type
w Type
t1 Type
t2) = Role -> FunTyFlag -> Coercion -> Coercion -> Coercion -> Coercion
mkFunCo Role
r FunTyFlag
af (Role -> Type -> Coercion
go Role
Nominal Type
w) (Role -> Type -> Coercion
go Role
r Type
t1) (Role -> Type -> Coercion
go Role
r Type
t2)
    go Role
r t :: Type
t@(ForAllTy (Bndr CoVar
v ForAllTyFlag
vis) Type
ty)
       = let (LiftingContext
lc', CoVar
v', Coercion
h) = LiftingContext -> CoVar -> (LiftingContext, CoVar, Coercion)
liftCoSubstVarBndr LiftingContext
lc CoVar
v
             body_co :: Coercion
body_co = LiftingContext -> Role -> Type -> Coercion
ty_co_subst LiftingContext
lc' Role
r Type
ty in
         if CoVar -> Bool
isTyVar CoVar
v' Bool -> Bool -> Bool
|| CoVar -> Coercion -> Bool
almostDevoidCoVarOfCo CoVar
v' Coercion
body_co
           -- Lifting a ForAllTy over a coercion variable could fail as ForAllCo
           -- imposes an extra restriction on where a covar can appear. See
           -- (FC6) of Note [ForAllCo] in GHC.Tc.TyCo.Rep
            -- We specifically check for this and panic because we know that
           -- there's a hole in the type system here (see (FC6), and we'd rather
           -- panic than fall into it.
         then HasDebugCallStack =>
CoVar
-> ForAllTyFlag -> ForAllTyFlag -> Coercion -> Coercion -> Coercion
CoVar
-> ForAllTyFlag -> ForAllTyFlag -> Coercion -> Coercion -> Coercion
mkForAllCo CoVar
v' ForAllTyFlag
vis ForAllTyFlag
vis Coercion
h Coercion
body_co
         else String -> SDoc -> Coercion
forall a. HasCallStack => String -> SDoc -> a
pprPanic String
"ty_co_subst: covar is not almost devoid" (Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
t)
    go Role
r ty :: Type
ty@(LitTy {})     = Bool -> Coercion -> Coercion
forall a. HasCallStack => Bool -> a -> a
assert (Role
r Role -> Role -> Bool
forall a. Eq a => a -> a -> Bool
== Role
Nominal) (Coercion -> Coercion) -> Coercion -> Coercion
forall a b. (a -> b) -> a -> b
$
                             Type -> Coercion
mkNomReflCo Type
ty
    go Role
r (CastTy Type
ty Coercion
co)    = Coercion -> Coercion -> Coercion -> Coercion
castCoercionKind (Role -> Type -> Coercion
go Role
r Type
ty) (LiftingContext -> Coercion -> Coercion
substLeftCo LiftingContext
lc Coercion
co)
                                                        (LiftingContext -> Coercion -> Coercion
substRightCo LiftingContext
lc Coercion
co)
    go Role
r (CoercionTy Coercion
co)   = Role -> Coercion -> Coercion -> Coercion -> Coercion
mkProofIrrelCo Role
r Coercion
kco (LiftingContext -> Coercion -> Coercion
substLeftCo LiftingContext
lc Coercion
co)
                                                  (LiftingContext -> Coercion -> Coercion
substRightCo LiftingContext
lc Coercion
co)
      where kco :: Coercion
kco = Role -> Type -> Coercion
go Role
Nominal (Coercion -> Type
coercionType Coercion
co)

    lift_phantom :: Type -> Coercion
lift_phantom Type
ty = Coercion -> Type -> Type -> Coercion
mkPhantomCo (Role -> Type -> Coercion
go Role
Nominal (HasDebugCallStack => Type -> Type
Type -> Type
typeKind Type
ty))
                                  (HasDebugCallStack => Subst -> Type -> Type
Subst -> Type -> Type
substTy (LiftingContext -> Subst
lcSubstLeft  LiftingContext
lc) Type
ty)
                                  (HasDebugCallStack => Subst -> Type -> Type
Subst -> Type -> Type
substTy (LiftingContext -> Subst
lcSubstRight LiftingContext
lc) Type
ty)

{-
Note [liftCoSubstTyVar]
~~~~~~~~~~~~~~~~~~~~~~~~~
This function can fail if a coercion in the environment is of too low a role.

liftCoSubstTyVar is called from two places: in liftCoSubst (naturally), and
also in matchAxiom in GHC.Core.Coercion.Opt. From liftCoSubst, the so-called lifting
lemma guarantees that the roles work out. If we fail in this
case, we really should panic -- something is deeply wrong. But, in matchAxiom,
failing is fine. matchAxiom is trying to find a set of coercions
that match, but it may fail, and this is healthy behavior.
-}

-- See Note [liftCoSubstTyVar]
liftCoSubstTyVar :: LiftingContext -> Role -> TyVar -> Maybe Coercion
liftCoSubstTyVar :: LiftingContext -> Role -> CoVar -> Maybe Coercion
liftCoSubstTyVar (LC Subst
subst LiftCoEnv
env) Role
r CoVar
v
  | Just Coercion
co_arg <- LiftCoEnv -> CoVar -> Maybe Coercion
forall a. VarEnv a -> CoVar -> Maybe a
lookupVarEnv LiftCoEnv
env CoVar
v
  = Role -> Role -> Coercion -> Maybe Coercion
downgradeRole_maybe Role
r (Coercion -> Role
coercionRole Coercion
co_arg) Coercion
co_arg

  | Bool
otherwise
  = Coercion -> Maybe Coercion
forall a. a -> Maybe a
Just (Coercion -> Maybe Coercion) -> Coercion -> Maybe Coercion
forall a b. (a -> b) -> a -> b
$ Role -> Type -> Coercion
mkReflCo Role
r (Subst -> CoVar -> Type
substTyVar Subst
subst CoVar
v)

{- Note [liftCoSubstVarBndr]
   ~~~~~~~~~~~~~~~~~~~~~~~~~
callback:
  'liftCoSubstVarBndrUsing' needs to be general enough to work in two
  situations:

    - in this module, which manipulates 'Coercion's, and
    - in GHC.Core.FamInstEnv, where we work with 'Reduction's, which contain
      a coercion as well as a type.

  To achieve this, we require that the return type of the 'callback' function
  contain a coercion within it. This is witnessed by the first argument
  to 'liftCoSubstVarBndrUsing': a getter, which allows us to retrieve
  the coercion inside the return type. Thus:

    - in this module, we simply pass 'id' as the getter,
    - in GHC.Core.FamInstEnv, we pass 'reductionCoercion' as the getter.

liftCoSubstTyVarBndrUsing:
  Given
    forall tv:k. t
  We want to get
    forall (tv:k1) (kind_co :: k1 ~ k2) body_co

  We lift the kind k to get the kind_co
    kind_co = ty_co_subst k :: k1 ~ k2

  Now in the LiftingContext, we add the new mapping
    tv |-> (tv :: k1) ~ ((tv |> kind_co) :: k2)

liftCoSubstCoVarBndrUsing:
  Given
    forall cv:(s1 ~ s2). t
  We want to get
    forall (cv:s1'~s2') (kind_co :: (s1'~s2') ~ (t1 ~ t2)) body_co

  We lift s1 and s2 respectively to get
    eta1 :: s1' ~ t1
    eta2 :: s2' ~ t2
  And
    kind_co = TyConAppCo Nominal (~#) eta1 eta2

  Now in the liftingContext, we add the new mapping
    cv |-> (cv :: s1' ~ s2') ~ ((sym eta1;cv;eta2) :: t1 ~ t2)
-}

-- See Note [liftCoSubstVarBndr]
liftCoSubstVarBndr :: LiftingContext -> TyCoVar
                   -> (LiftingContext, TyCoVar, Coercion)
liftCoSubstVarBndr :: LiftingContext -> CoVar -> (LiftingContext, CoVar, Coercion)
liftCoSubstVarBndr LiftingContext
lc CoVar
tv
  = (Coercion -> Coercion)
-> (LiftingContext -> Type -> Coercion)
-> LiftingContext
-> CoVar
-> (LiftingContext, CoVar, Coercion)
forall r.
(r -> Coercion)
-> (LiftingContext -> Type -> r)
-> LiftingContext
-> CoVar
-> (LiftingContext, CoVar, r)
liftCoSubstVarBndrUsing Coercion -> Coercion
forall a. a -> a
id LiftingContext -> Type -> Coercion
callback LiftingContext
lc CoVar
tv
  where
    callback :: LiftingContext -> Type -> Coercion
callback LiftingContext
lc' Type
ty' = LiftingContext -> Role -> Type -> Coercion
ty_co_subst LiftingContext
lc' Role
Nominal Type
ty'

-- the callback must produce a nominal coercion
liftCoSubstVarBndrUsing :: (r -> CoercionN)              -- ^ coercion getter
                        -> (LiftingContext -> Type -> r) -- ^ callback
                        -> LiftingContext -> TyCoVar
                        -> (LiftingContext, TyCoVar, r)
liftCoSubstVarBndrUsing :: forall r.
(r -> Coercion)
-> (LiftingContext -> Type -> r)
-> LiftingContext
-> CoVar
-> (LiftingContext, CoVar, r)
liftCoSubstVarBndrUsing r -> Coercion
view_co LiftingContext -> Type -> r
fun LiftingContext
lc CoVar
old_var
  | CoVar -> Bool
isTyVar CoVar
old_var
  = (r -> Coercion)
-> (LiftingContext -> Type -> r)
-> LiftingContext
-> CoVar
-> (LiftingContext, CoVar, r)
forall r.
(r -> Coercion)
-> (LiftingContext -> Type -> r)
-> LiftingContext
-> CoVar
-> (LiftingContext, CoVar, r)
liftCoSubstTyVarBndrUsing r -> Coercion
view_co LiftingContext -> Type -> r
fun LiftingContext
lc CoVar
old_var
  | Bool
otherwise
  = (r -> Coercion)
-> (LiftingContext -> Type -> r)
-> LiftingContext
-> CoVar
-> (LiftingContext, CoVar, r)
forall r.
(r -> Coercion)
-> (LiftingContext -> Type -> r)
-> LiftingContext
-> CoVar
-> (LiftingContext, CoVar, r)
liftCoSubstCoVarBndrUsing r -> Coercion
view_co LiftingContext -> Type -> r
fun LiftingContext
lc CoVar
old_var

-- Works for tyvar binder
liftCoSubstTyVarBndrUsing :: (r -> CoercionN)              -- ^ coercion getter
                          -> (LiftingContext -> Type -> r) -- ^ callback
                          -> LiftingContext -> TyVar
                          -> (LiftingContext, TyVar, r)
liftCoSubstTyVarBndrUsing :: forall r.
(r -> Coercion)
-> (LiftingContext -> Type -> r)
-> LiftingContext
-> CoVar
-> (LiftingContext, CoVar, r)
liftCoSubstTyVarBndrUsing r -> Coercion
view_co LiftingContext -> Type -> r
fun lc :: LiftingContext
lc@(LC Subst
subst LiftCoEnv
cenv) CoVar
old_var
  = Bool -> (LiftingContext, CoVar, r) -> (LiftingContext, CoVar, r)
forall a. HasCallStack => Bool -> a -> a
assert (CoVar -> Bool
isTyVar CoVar
old_var) ((LiftingContext, CoVar, r) -> (LiftingContext, CoVar, r))
-> (LiftingContext, CoVar, r) -> (LiftingContext, CoVar, r)
forall a b. (a -> b) -> a -> b
$
    ( Subst -> LiftCoEnv -> LiftingContext
LC (Subst
subst Subst -> CoVar -> Subst
`extendSubstInScope` CoVar
new_var) LiftCoEnv
new_cenv
    , CoVar
new_var, r
stuff )
  where
    old_kind :: Type
old_kind = CoVar -> Type
tyVarKind CoVar
old_var
    stuff :: r
stuff    = LiftingContext -> Type -> r
fun LiftingContext
lc Type
old_kind
    eta :: Coercion
eta      = r -> Coercion
view_co r
stuff
    k1 :: Type
k1       = HasDebugCallStack => Coercion -> Type
Coercion -> Type
coercionLKind Coercion
eta
    new_var :: CoVar
new_var  = InScopeSet -> CoVar -> CoVar
uniqAway (Subst -> InScopeSet
getSubstInScope Subst
subst) (CoVar -> Type -> CoVar
setVarType CoVar
old_var Type
k1)

    lifted :: Coercion
lifted   = Role -> Type -> Coercion -> Coercion
mkGReflRightCo Role
Nominal (CoVar -> Type
TyVarTy CoVar
new_var) Coercion
eta
               -- :: new_var ~ new_var |> eta
    new_cenv :: LiftCoEnv
new_cenv = LiftCoEnv -> CoVar -> Coercion -> LiftCoEnv
forall a. VarEnv a -> CoVar -> a -> VarEnv a
extendVarEnv LiftCoEnv
cenv CoVar
old_var Coercion
lifted

-- Works for covar binder
liftCoSubstCoVarBndrUsing :: (r -> CoercionN)              -- ^ coercion getter
                          -> (LiftingContext -> Type -> r) -- ^ callback
                          -> LiftingContext -> CoVar
                          -> (LiftingContext, CoVar, r)
liftCoSubstCoVarBndrUsing :: forall r.
(r -> Coercion)
-> (LiftingContext -> Type -> r)
-> LiftingContext
-> CoVar
-> (LiftingContext, CoVar, r)
liftCoSubstCoVarBndrUsing r -> Coercion
view_co LiftingContext -> Type -> r
fun lc :: LiftingContext
lc@(LC Subst
subst LiftCoEnv
cenv) CoVar
old_var
  = Bool -> (LiftingContext, CoVar, r) -> (LiftingContext, CoVar, r)
forall a. HasCallStack => Bool -> a -> a
assert (CoVar -> Bool
isCoVar CoVar
old_var) ((LiftingContext, CoVar, r) -> (LiftingContext, CoVar, r))
-> (LiftingContext, CoVar, r) -> (LiftingContext, CoVar, r)
forall a b. (a -> b) -> a -> b
$
    ( Subst -> LiftCoEnv -> LiftingContext
LC (Subst
subst Subst -> CoVar -> Subst
`extendSubstInScope` CoVar
new_var) LiftCoEnv
new_cenv
    , CoVar
new_var, r
stuff )
  where
    old_kind :: Type
old_kind = CoVar -> Type
coVarKind CoVar
old_var
    stuff :: r
stuff    = LiftingContext -> Type -> r
fun LiftingContext
lc Type
old_kind
    eta :: Coercion
eta      = r -> Coercion
view_co r
stuff
    k1 :: Type
k1       = HasDebugCallStack => Coercion -> Type
Coercion -> Type
coercionLKind Coercion
eta
    new_var :: CoVar
new_var  = InScopeSet -> CoVar -> CoVar
uniqAway (Subst -> InScopeSet
getSubstInScope Subst
subst) (CoVar -> Type -> CoVar
setVarType CoVar
old_var Type
k1)

    -- old_var :: s1  ~r s2
    -- eta     :: (s1' ~r s2') ~N (t1 ~r t2)
    -- eta1    :: s1' ~r t1
    -- eta2    :: s2' ~r t2
    -- co1     :: s1' ~r s2'
    -- co2     :: t1  ~r t2
    -- lifted  :: co1 ~N co2

    role :: Role
role   = CoVar -> Role
coVarRole CoVar
old_var
    eta' :: Coercion
eta'   = Role -> Role -> Coercion -> Coercion
downgradeRole Role
role Role
Nominal Coercion
eta
    eta1 :: Coercion
eta1   = HasDebugCallStack => CoSel -> Coercion -> Coercion
CoSel -> Coercion -> Coercion
mkSelCo (Arity -> Role -> CoSel
SelTyCon Arity
2 Role
role) Coercion
eta'
    eta2 :: Coercion
eta2   = HasDebugCallStack => CoSel -> Coercion -> Coercion
CoSel -> Coercion -> Coercion
mkSelCo (Arity -> Role -> CoSel
SelTyCon Arity
3 Role
role) Coercion
eta'

    co1 :: Coercion
co1     = CoVar -> Coercion
mkCoVarCo CoVar
new_var
    co2 :: Coercion
co2     = Coercion -> Coercion
mkSymCo Coercion
eta1 Coercion -> Coercion -> Coercion
`mkTransCo` Coercion
co1 Coercion -> Coercion -> Coercion
`mkTransCo` Coercion
eta2
    lifted :: Coercion
lifted  = Role -> Coercion -> Coercion -> Coercion -> Coercion
mkProofIrrelCo Role
Nominal Coercion
eta Coercion
co1 Coercion
co2

    new_cenv :: LiftCoEnv
new_cenv = LiftCoEnv -> CoVar -> Coercion -> LiftCoEnv
forall a. VarEnv a -> CoVar -> a -> VarEnv a
extendVarEnv LiftCoEnv
cenv CoVar
old_var Coercion
lifted

-- | Is a var in the domain of a lifting context?
isMappedByLC :: TyCoVar -> LiftingContext -> Bool
isMappedByLC :: CoVar -> LiftingContext -> Bool
isMappedByLC CoVar
tv (LC Subst
_ LiftCoEnv
env) = CoVar
tv CoVar -> LiftCoEnv -> Bool
forall a. CoVar -> VarEnv a -> Bool
`elemVarEnv` LiftCoEnv
env

-- If [a |-> g] is in the substitution and g :: t1 ~ t2, substitute a for t1
-- If [a |-> (g1, g2)] is in the substitution, substitute a for g1
substLeftCo :: LiftingContext -> Coercion -> Coercion
substLeftCo :: LiftingContext -> Coercion -> Coercion
substLeftCo LiftingContext
lc Coercion
co
  = HasDebugCallStack => Subst -> Coercion -> Coercion
Subst -> Coercion -> Coercion
substCo (LiftingContext -> Subst
lcSubstLeft LiftingContext
lc) Coercion
co

-- Ditto, but for t2 and g2
substRightCo :: LiftingContext -> Coercion -> Coercion
substRightCo :: LiftingContext -> Coercion -> Coercion
substRightCo LiftingContext
lc Coercion
co
  = HasDebugCallStack => Subst -> Coercion -> Coercion
Subst -> Coercion -> Coercion
substCo (LiftingContext -> Subst
lcSubstRight LiftingContext
lc) Coercion
co

-- | Apply "sym" to all coercions in a 'LiftCoEnv'
swapLiftCoEnv :: LiftCoEnv -> LiftCoEnv
swapLiftCoEnv :: LiftCoEnv -> LiftCoEnv
swapLiftCoEnv = (Coercion -> Coercion) -> LiftCoEnv -> LiftCoEnv
forall a b. (a -> b) -> VarEnv a -> VarEnv b
mapVarEnv Coercion -> Coercion
mkSymCo

lcSubstLeft :: LiftingContext -> Subst
lcSubstLeft :: LiftingContext -> Subst
lcSubstLeft (LC Subst
subst LiftCoEnv
lc_env) = Subst -> LiftCoEnv -> Subst
liftEnvSubstLeft Subst
subst LiftCoEnv
lc_env

lcSubstRight :: LiftingContext -> Subst
lcSubstRight :: LiftingContext -> Subst
lcSubstRight (LC Subst
subst LiftCoEnv
lc_env) = Subst -> LiftCoEnv -> Subst
liftEnvSubstRight Subst
subst LiftCoEnv
lc_env

liftEnvSubstLeft :: Subst -> LiftCoEnv -> Subst
liftEnvSubstLeft :: Subst -> LiftCoEnv -> Subst
liftEnvSubstLeft = (forall a. Pair a -> a) -> Subst -> LiftCoEnv -> Subst
liftEnvSubst Pair a -> a
forall a. Pair a -> a
pFst

liftEnvSubstRight :: Subst -> LiftCoEnv -> Subst
liftEnvSubstRight :: Subst -> LiftCoEnv -> Subst
liftEnvSubstRight = (forall a. Pair a -> a) -> Subst -> LiftCoEnv -> Subst
liftEnvSubst Pair a -> a
forall a. Pair a -> a
pSnd

liftEnvSubst :: (forall a. Pair a -> a) -> Subst -> LiftCoEnv -> Subst
liftEnvSubst :: (forall a. Pair a -> a) -> Subst -> LiftCoEnv -> Subst
liftEnvSubst forall a. Pair a -> a
selector Subst
subst LiftCoEnv
lc_env
  = Subst -> Subst -> Subst
composeTCvSubst (InScopeSet -> IdSubstEnv -> TvSubstEnv -> LiftCoEnv -> Subst
Subst InScopeSet
in_scope IdSubstEnv
emptyIdSubstEnv TvSubstEnv
tenv LiftCoEnv
cenv) Subst
subst
  where
    pairs :: [(Unique, Coercion)]
pairs            = LiftCoEnv -> [(Unique, Coercion)]
forall {k} (key :: k) elt. UniqFM key elt -> [(Unique, elt)]
nonDetUFMToList LiftCoEnv
lc_env
                       -- It's OK to use nonDetUFMToList here because we
                       -- immediately forget the ordering by creating
                       -- a VarEnv
    ([(Unique, Type)]
tpairs, [(Unique, Coercion)]
cpairs) = ((Unique, Coercion) -> Either (Unique, Type) (Unique, Coercion))
-> [(Unique, Coercion)] -> ([(Unique, Type)], [(Unique, Coercion)])
forall a b c. (a -> Either b c) -> [a] -> ([b], [c])
partitionWith (Unique, Coercion) -> Either (Unique, Type) (Unique, Coercion)
ty_or_co [(Unique, Coercion)]
pairs
    -- Make sure the in-scope set is wide enough to cover the range of the
    -- substitution (#22235).
    in_scope :: InScopeSet
in_scope         = VarSet -> InScopeSet
mkInScopeSet (VarSet -> InScopeSet) -> VarSet -> InScopeSet
forall a b. (a -> b) -> a -> b
$
                       [Type] -> VarSet
tyCoVarsOfTypes (((Unique, Type) -> Type) -> [(Unique, Type)] -> [Type]
forall a b. (a -> b) -> [a] -> [b]
map (Unique, Type) -> Type
forall a b. (a, b) -> b
snd [(Unique, Type)]
tpairs) VarSet -> VarSet -> VarSet
`unionVarSet`
                       [Coercion] -> VarSet
tyCoVarsOfCos (((Unique, Coercion) -> Coercion)
-> [(Unique, Coercion)] -> [Coercion]
forall a b. (a -> b) -> [a] -> [b]
map (Unique, Coercion) -> Coercion
forall a b. (a, b) -> b
snd [(Unique, Coercion)]
cpairs)
    tenv :: TvSubstEnv
tenv             = [(Unique, Type)] -> TvSubstEnv
forall a. [(Unique, a)] -> VarEnv a
mkVarEnv_Directly [(Unique, Type)]
tpairs
    cenv :: LiftCoEnv
cenv             = [(Unique, Coercion)] -> LiftCoEnv
forall a. [(Unique, a)] -> VarEnv a
mkVarEnv_Directly [(Unique, Coercion)]
cpairs

    ty_or_co :: (Unique, Coercion) -> Either (Unique, Type) (Unique, Coercion)
    ty_or_co :: (Unique, Coercion) -> Either (Unique, Type) (Unique, Coercion)
ty_or_co (Unique
u, Coercion
co)
      | Just Coercion
equality_co <- Type -> Maybe Coercion
isCoercionTy_maybe Type
equality_ty
      = (Unique, Coercion) -> Either (Unique, Type) (Unique, Coercion)
forall a b. b -> Either a b
Right (Unique
u, Coercion
equality_co)
      | Bool
otherwise
      = (Unique, Type) -> Either (Unique, Type) (Unique, Coercion)
forall a b. a -> Either a b
Left (Unique
u, Type
equality_ty)
      where
        equality_ty :: Type
equality_ty = Pair Type -> Type
forall a. Pair a -> a
selector (HasDebugCallStack => Coercion -> Pair Type
Coercion -> Pair Type
coercionKind Coercion
co)

-- | Lookup a 'CoVar' in the substitution in a 'LiftingContext'
lcLookupCoVar :: LiftingContext -> CoVar -> Maybe Coercion
lcLookupCoVar :: LiftingContext -> CoVar -> Maybe Coercion
lcLookupCoVar (LC Subst
subst LiftCoEnv
_) CoVar
cv = Subst -> CoVar -> Maybe Coercion
lookupCoVar Subst
subst CoVar
cv

-- | Get the 'InScopeSet' from a 'LiftingContext'
lcInScopeSet :: LiftingContext -> InScopeSet
lcInScopeSet :: LiftingContext -> InScopeSet
lcInScopeSet (LC Subst
subst LiftCoEnv
_) = Subst -> InScopeSet
getSubstInScope Subst
subst

{-
%************************************************************************
%*                                                                      *
            Sequencing on coercions
%*                                                                      *
%************************************************************************
-}

seqMCo :: MCoercion -> ()
seqMCo :: MCoercion -> ()
seqMCo MCoercion
MRefl    = ()
seqMCo (MCo Coercion
co) = Coercion -> ()
seqCo Coercion
co

seqCo :: Coercion -> ()
seqCo :: Coercion -> ()
seqCo (Refl Type
ty)             = Type -> ()
seqType Type
ty
seqCo (GRefl Role
r Type
ty MCoercion
mco)      = Role
r Role -> () -> ()
forall a b. a -> b -> b
`seq` Type -> ()
seqType Type
ty () -> () -> ()
forall a b. a -> b -> b
`seq` MCoercion -> ()
seqMCo MCoercion
mco
seqCo (TyConAppCo Role
r TyCon
tc [Coercion]
cos) = Role
r Role -> () -> ()
forall a b. a -> b -> b
`seq` TyCon
tc TyCon -> () -> ()
forall a b. a -> b -> b
`seq` [Coercion] -> ()
seqCos [Coercion]
cos
seqCo (AppCo Coercion
co1 Coercion
co2)       = Coercion -> ()
seqCo Coercion
co1 () -> () -> ()
forall a b. a -> b -> b
`seq` Coercion -> ()
seqCo Coercion
co2
seqCo (CoVarCo CoVar
cv)          = CoVar
cv CoVar -> () -> ()
forall a b. a -> b -> b
`seq` ()
seqCo (HoleCo CoercionHole
h)            = CoercionHole -> CoVar
coHoleCoVar CoercionHole
h CoVar -> () -> ()
forall a b. a -> b -> b
`seq` ()
seqCo (SymCo Coercion
co)            = Coercion -> ()
seqCo Coercion
co
seqCo (TransCo Coercion
co1 Coercion
co2)     = Coercion -> ()
seqCo Coercion
co1 () -> () -> ()
forall a b. a -> b -> b
`seq` Coercion -> ()
seqCo Coercion
co2
seqCo (SelCo CoSel
n Coercion
co)          = CoSel
n CoSel -> () -> ()
forall a b. a -> b -> b
`seq` Coercion -> ()
seqCo Coercion
co
seqCo (LRCo LeftOrRight
lr Coercion
co)          = LeftOrRight
lr LeftOrRight -> () -> ()
forall a b. a -> b -> b
`seq` Coercion -> ()
seqCo Coercion
co
seqCo (InstCo Coercion
co Coercion
arg)       = Coercion -> ()
seqCo Coercion
co () -> () -> ()
forall a b. a -> b -> b
`seq` Coercion -> ()
seqCo Coercion
arg
seqCo (KindCo Coercion
co)           = Coercion -> ()
seqCo Coercion
co
seqCo (SubCo Coercion
co)            = Coercion -> ()
seqCo Coercion
co
seqCo (AxiomCo CoAxiomRule
_ [Coercion]
cs)        = [Coercion] -> ()
seqCos [Coercion]
cs
seqCo (ForAllCo CoVar
tv ForAllTyFlag
visL ForAllTyFlag
visR Coercion
k Coercion
co)
  = Type -> ()
seqType (CoVar -> Type
varType CoVar
tv) () -> () -> ()
forall a b. a -> b -> b
`seq` ForAllTyFlag -> ()
forall a. NFData a => a -> ()
rnf ForAllTyFlag
visL () -> () -> ()
forall a b. a -> b -> b
`seq` ForAllTyFlag -> ()
forall a. NFData a => a -> ()
rnf ForAllTyFlag
visR () -> () -> ()
forall a b. a -> b -> b
`seq`
    Coercion -> ()
seqCo Coercion
k () -> () -> ()
forall a b. a -> b -> b
`seq` Coercion -> ()
seqCo Coercion
co
seqCo (FunCo Role
r FunTyFlag
af1 FunTyFlag
af2 Coercion
w Coercion
co1 Coercion
co2)
  = Role
r Role -> () -> ()
forall a b. a -> b -> b
`seq` FunTyFlag
af1 FunTyFlag -> () -> ()
forall a b. a -> b -> b
`seq` FunTyFlag
af2 FunTyFlag -> () -> ()
forall a b. a -> b -> b
`seq` Coercion -> ()
seqCo Coercion
w () -> () -> ()
forall a b. a -> b -> b
`seq` Coercion -> ()
seqCo Coercion
co1 () -> () -> ()
forall a b. a -> b -> b
`seq` Coercion -> ()
seqCo Coercion
co2
seqCo (UnivCo { uco_prov :: Coercion -> UnivCoProvenance
uco_prov = UnivCoProvenance
p, uco_role :: Coercion -> Role
uco_role = Role
r
              , uco_lty :: Coercion -> Type
uco_lty = Type
t1, uco_rty :: Coercion -> Type
uco_rty = Type
t2, uco_deps :: Coercion -> [Coercion]
uco_deps = [Coercion]
deps })
  = UnivCoProvenance
p UnivCoProvenance -> () -> ()
forall a b. a -> b -> b
`seq` Role
r Role -> () -> ()
forall a b. a -> b -> b
`seq` Type -> ()
seqType Type
t1 () -> () -> ()
forall a b. a -> b -> b
`seq` Type -> ()
seqType Type
t2 () -> () -> ()
forall a b. a -> b -> b
`seq` [Coercion] -> ()
seqCos [Coercion]
deps

seqCos :: [Coercion] -> ()
seqCos :: [Coercion] -> ()
seqCos []       = ()
seqCos (Coercion
co:[Coercion]
cos) = Coercion -> ()
seqCo Coercion
co () -> () -> ()
forall a b. a -> b -> b
`seq` [Coercion] -> ()
seqCos [Coercion]
cos

{-
%************************************************************************
%*                                                                      *
             The kind of a type, and of a coercion
%*                                                                      *
%************************************************************************
-}

{- Note [coercionKind performance]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
coercionKind, coercionLKind, and coercionRKind are very "hot" functions; in some
coercion-heavy programs they can have a material effect on compile time/allocation.

Hence
* Rather than making one function which returns a pair (lots of allocation and
  de-allocation) we have two functions, coercionLKind and coercionRKind, which
  return the left and right kind respectively.

* Both are defined by a single worker function `coercion_lr_kind`, which takes a
  flag of type `LeftOrRight`.  This worker function is marked INLINE, and inlined
  at its precisely-two call-sites in coercionLKind and coercionRKind.

Take care when making changes here... it's easy to accidentally add allocation!
-}

-- | Apply 'coercionKind' to multiple 'Coercion's
coercionKinds :: [Coercion] -> Pair [Type]
coercionKinds :: [Coercion] -> Pair [Type]
coercionKinds [Coercion]
tys = [Pair Type] -> Pair [Type]
forall (t :: * -> *) (f :: * -> *) a.
(Traversable t, Applicative f) =>
t (f a) -> f (t a)
forall (f :: * -> *) a. Applicative f => [f a] -> f [a]
sequenceA ([Pair Type] -> Pair [Type]) -> [Pair Type] -> Pair [Type]
forall a b. (a -> b) -> a -> b
$ (Coercion -> Pair Type) -> [Coercion] -> [Pair Type]
forall a b. (a -> b) -> [a] -> [b]
map HasDebugCallStack => Coercion -> Pair Type
Coercion -> Pair Type
coercionKind [Coercion]
tys

-- | Get a coercion's kind and role.
coercionKindRole :: Coercion -> (Pair Type, Role)
coercionKindRole :: Coercion -> (Pair Type, Role)
coercionKindRole Coercion
co = (HasDebugCallStack => Coercion -> Pair Type
Coercion -> Pair Type
coercionKind Coercion
co, Coercion -> Role
coercionRole Coercion
co)

coercionType :: Coercion -> Type
coercionType :: Coercion -> Type
coercionType Coercion
co = case Coercion -> (Pair Type, Role)
coercionKindRole Coercion
co of
  (Pair Type
ty1 Type
ty2, Role
r) -> Role -> Type -> Type -> Type
mkCoercionType Role
r Type
ty1 Type
ty2

------------------
-- | If it is the case that
--
-- > c :: (t1 ~ t2)
--
-- i.e. the kind of @c@ relates @t1@ and @t2@, then @coercionKind c = Pair t1 t2@.

coercionKind :: HasDebugCallStack => Coercion -> Pair Type
-- See Note [coercionKind performance]
coercionKind :: HasDebugCallStack => Coercion -> Pair Type
coercionKind Coercion
co = Type -> Type -> Pair Type
forall a. a -> a -> Pair a
Pair (HasDebugCallStack => Coercion -> Type
Coercion -> Type
coercionLKind Coercion
co) (HasDebugCallStack => Coercion -> Type
Coercion -> Type
coercionRKind Coercion
co)

coercionLKind, coercionRKind :: HasDebugCallStack => Coercion -> Type
-- See Note [coercionKind performance]
coercionLKind :: HasDebugCallStack => Coercion -> Type
coercionLKind Coercion
co = HasDebugCallStack => LeftOrRight -> Coercion -> Type
LeftOrRight -> Coercion -> Type
coercion_lr_kind LeftOrRight
CLeft  Coercion
co
coercionRKind :: HasDebugCallStack => Coercion -> Type
coercionRKind Coercion
co = HasDebugCallStack => LeftOrRight -> Coercion -> Type
LeftOrRight -> Coercion -> Type
coercion_lr_kind LeftOrRight
CRight Coercion
co

coercion_lr_kind :: HasDebugCallStack => LeftOrRight -> Coercion -> Type
{-# INLINE coercion_lr_kind #-}
-- See Note [coercionKind performance]
coercion_lr_kind :: HasDebugCallStack => LeftOrRight -> Coercion -> Type
coercion_lr_kind LeftOrRight
which Coercion
orig_co
  = Coercion -> Type
go Coercion
orig_co
  where
    go :: Coercion -> Type
go (Refl Type
ty)              = Type
ty
    go (GRefl Role
_ Type
ty MCoercion
MRefl)     = Type
ty
    go (GRefl Role
_ Type
ty (MCo Coercion
co1)) = LeftOrRight -> (Type, Type) -> Type
forall a. LeftOrRight -> (a, a) -> a
pickLR LeftOrRight
which (Type
ty, Type -> Coercion -> Type
mkCastTy Type
ty Coercion
co1)
    go (TyConAppCo Role
_ TyCon
tc [Coercion]
cos)  = TyCon -> [Type] -> Type
mkTyConApp TyCon
tc ((Coercion -> Type) -> [Coercion] -> [Type]
forall a b. (a -> b) -> [a] -> [b]
map Coercion -> Type
go [Coercion]
cos)
    go (AppCo Coercion
co1 Coercion
co2)        = Type -> Type -> Type
mkAppTy (Coercion -> Type
go Coercion
co1) (Coercion -> Type
go Coercion
co2)
    go (CoVarCo CoVar
cv)           = CoVar -> Type
go_covar CoVar
cv
    go (HoleCo CoercionHole
h)             = CoVar -> Type
go_covar (CoercionHole -> CoVar
coHoleCoVar CoercionHole
h)
    go (SymCo Coercion
co)             = LeftOrRight -> (Type, Type) -> Type
forall a. LeftOrRight -> (a, a) -> a
pickLR LeftOrRight
which (HasDebugCallStack => Coercion -> Type
Coercion -> Type
coercionRKind Coercion
co, HasDebugCallStack => Coercion -> Type
Coercion -> Type
coercionLKind Coercion
co)
    go (TransCo Coercion
co1 Coercion
co2)      = LeftOrRight -> (Type, Type) -> Type
forall a. LeftOrRight -> (a, a) -> a
pickLR LeftOrRight
which (Coercion -> Type
go Coercion
co1,           Coercion -> Type
go Coercion
co2)
    go (LRCo LeftOrRight
lr Coercion
co)           = LeftOrRight -> (Type, Type) -> Type
forall a. LeftOrRight -> (a, a) -> a
pickLR LeftOrRight
lr (Type -> (Type, Type)
splitAppTy (Coercion -> Type
go Coercion
co))
    go (InstCo Coercion
aco Coercion
arg)       = Coercion -> [Type] -> Type
go_app Coercion
aco [Coercion -> Type
go Coercion
arg]
    go (KindCo Coercion
co)            = HasDebugCallStack => Type -> Type
Type -> Type
typeKind (Coercion -> Type
go Coercion
co)
    go (SubCo Coercion
co)             = Coercion -> Type
go Coercion
co
    go (SelCo CoSel
d Coercion
co)           = HasDebugCallStack => CoSel -> Type -> Type
CoSel -> Type -> Type
selectFromType CoSel
d (Coercion -> Type
go Coercion
co)
    go (AxiomCo CoAxiomRule
ax [Coercion]
cos)       = CoAxiomRule -> [Coercion] -> Type
go_ax CoAxiomRule
ax [Coercion]
cos

    go (UnivCo { uco_lty :: Coercion -> Type
uco_lty = Type
lty, uco_rty :: Coercion -> Type
uco_rty = Type
rty})
      = LeftOrRight -> (Type, Type) -> Type
forall a. LeftOrRight -> (a, a) -> a
pickLR LeftOrRight
which (Type
lty, Type
rty)
    go (FunCo { fco_afl :: Coercion -> FunTyFlag
fco_afl = FunTyFlag
afl, fco_afr :: Coercion -> FunTyFlag
fco_afr = FunTyFlag
afr, fco_mult :: Coercion -> Coercion
fco_mult = Coercion
mult
              , fco_arg :: Coercion -> Coercion
fco_arg = Coercion
arg, fco_res :: Coercion -> Coercion
fco_res = Coercion
res})
      = -- See Note [FunCo]
        FunTy { ft_af :: FunTyFlag
ft_af = LeftOrRight -> (FunTyFlag, FunTyFlag) -> FunTyFlag
forall a. LeftOrRight -> (a, a) -> a
pickLR LeftOrRight
which (FunTyFlag
afl, FunTyFlag
afr), ft_mult :: Type
ft_mult = Coercion -> Type
go Coercion
mult
              , ft_arg :: Type
ft_arg = Coercion -> Type
go Coercion
arg, ft_res :: Type
ft_res = Coercion -> Type
go Coercion
res }

    go co :: Coercion
co@(ForAllCo { fco_tcv :: Coercion -> CoVar
fco_tcv = CoVar
tv1, fco_visL :: Coercion -> ForAllTyFlag
fco_visL = ForAllTyFlag
visL, fco_visR :: Coercion -> ForAllTyFlag
fco_visR = ForAllTyFlag
visR
                    , fco_kind :: Coercion -> Coercion
fco_kind = Coercion
k_co, fco_body :: Coercion -> Coercion
fco_body = Coercion
co1 })
      = case LeftOrRight
which of
          LeftOrRight
CLeft  -> CoVar -> ForAllTyFlag -> Type -> Type
mkTyCoForAllTy CoVar
tv1 ForAllTyFlag
visL (Coercion -> Type
go Coercion
co1)
          LeftOrRight
CRight | Coercion -> Bool
isGReflCo Coercion
k_co  -- kind_co always has kind `Type`, thus `isGReflCo`
                 -> CoVar -> ForAllTyFlag -> Type -> Type
mkTyCoForAllTy CoVar
tv1 ForAllTyFlag
visR (Coercion -> Type
go Coercion
co1)
                 | Bool
otherwise
                 -> Subst -> Coercion -> Type
go_forall_right Subst
empty_subst Coercion
co
      where
         empty_subst :: Subst
empty_subst = InScopeSet -> Subst
mkEmptySubst (VarSet -> InScopeSet
mkInScopeSet (VarSet -> InScopeSet) -> VarSet -> InScopeSet
forall a b. (a -> b) -> a -> b
$ Coercion -> VarSet
tyCoVarsOfCo Coercion
co)

    -------------
    go_covar :: CoVar -> Type
go_covar CoVar
cv = LeftOrRight -> (Type, Type) -> Type
forall a. LeftOrRight -> (a, a) -> a
pickLR LeftOrRight
which (HasDebugCallStack => CoVar -> Type
CoVar -> Type
coVarLType CoVar
cv, HasDebugCallStack => CoVar -> Type
CoVar -> Type
coVarRType CoVar
cv)

    -------------
    go_app :: Coercion -> [Type] -> Type
    -- Collect up all the arguments and apply all at once
    -- See Note [Nested InstCos]
    go_app :: Coercion -> [Type] -> Type
go_app (InstCo Coercion
co Coercion
arg) [Type]
args = Coercion -> [Type] -> Type
go_app Coercion
co (Coercion -> Type
go Coercion
argType -> [Type] -> [Type]
forall a. a -> [a] -> [a]
:[Type]
args)
    go_app Coercion
co              [Type]
args = HasDebugCallStack => Type -> [Type] -> Type
Type -> [Type] -> Type
piResultTys (Coercion -> Type
go Coercion
co) [Type]
args

    -------------
    go_ax :: CoAxiomRule -> [Coercion] -> Type
go_ax axr :: CoAxiomRule
axr@(BuiltInFamRew  BuiltInFamRewrite
bif) [Coercion]
cos  = CoAxiomRule -> Maybe (Pair Type) -> Type
check_bif_res CoAxiomRule
axr (BuiltInFamRewrite -> [Pair Type] -> Maybe (Pair Type)
bifrw_proves  BuiltInFamRewrite
bif ((Coercion -> Pair Type) -> [Coercion] -> [Pair Type]
forall a b. (a -> b) -> [a] -> [b]
map HasDebugCallStack => Coercion -> Pair Type
Coercion -> Pair Type
coercionKind [Coercion]
cos))
    go_ax axr :: CoAxiomRule
axr@(BuiltInFamInj BuiltInFamInjectivity
bif) [Coercion
co]  = CoAxiomRule -> Maybe (Pair Type) -> Type
check_bif_res CoAxiomRule
axr (BuiltInFamInjectivity -> Pair Type -> Maybe (Pair Type)
bifinj_proves BuiltInFamInjectivity
bif (HasDebugCallStack => Coercion -> Pair Type
Coercion -> Pair Type
coercionKind Coercion
co))
    go_ax axr :: CoAxiomRule
axr@(BuiltInFamInj {})  [Coercion]
_     = CoAxiomRule -> Type
crash CoAxiomRule
axr
    go_ax     (UnbranchedAxiom CoAxiom Unbranched
ax) [Coercion]
cos  = CoAxiom Unbranched -> CoAxBranch -> [Coercion] -> Type
forall (br :: BranchFlag).
CoAxiom br -> CoAxBranch -> [Coercion] -> Type
go_branch CoAxiom Unbranched
ax (CoAxiom Unbranched -> CoAxBranch
coAxiomSingleBranch CoAxiom Unbranched
ax) [Coercion]
cos
    go_ax     (BranchedAxiom CoAxiom Branched
ax Arity
i) [Coercion]
cos  = CoAxiom Branched -> CoAxBranch -> [Coercion] -> Type
forall (br :: BranchFlag).
CoAxiom br -> CoAxBranch -> [Coercion] -> Type
go_branch CoAxiom Branched
ax (CoAxiom Branched -> Arity -> CoAxBranch
forall (br :: BranchFlag). CoAxiom br -> Arity -> CoAxBranch
coAxiomNthBranch CoAxiom Branched
ax Arity
i)  [Coercion]
cos

    -------------
    check_bif_res :: CoAxiomRule -> Maybe (Pair Type) -> Type
check_bif_res CoAxiomRule
_   (Just (Pair Type
lhs Type
rhs)) = LeftOrRight -> (Type, Type) -> Type
forall a. LeftOrRight -> (a, a) -> a
pickLR LeftOrRight
which (Type
lhs,Type
rhs)
    check_bif_res CoAxiomRule
axr Maybe (Pair Type)
Nothing               = CoAxiomRule -> Type
crash CoAxiomRule
axr

    crash :: CoAxiomRule -> Type
    crash :: CoAxiomRule -> Type
crash CoAxiomRule
axr = String -> SDoc -> Type
forall a. HasCallStack => String -> SDoc -> a
pprPanic String
"coercionKind" (CoAxiomRule -> SDoc
forall a. Outputable a => a -> SDoc
ppr CoAxiomRule
axr)

    -------------
    go_branch :: CoAxiom br -> CoAxBranch -> [Coercion] -> Type
    go_branch :: forall (br :: BranchFlag).
CoAxiom br -> CoAxBranch -> [Coercion] -> Type
go_branch CoAxiom br
ax (CoAxBranch { cab_tvs :: CoAxBranch -> [CoVar]
cab_tvs = [CoVar]
tvs, cab_cvs :: CoAxBranch -> [CoVar]
cab_cvs = [CoVar]
cvs
                             , cab_lhs :: CoAxBranch -> [Type]
cab_lhs = [Type]
lhs_tys, cab_rhs :: CoAxBranch -> Type
cab_rhs = Type
rhs_ty }) [Coercion]
cos
      = Bool -> Type -> Type
forall a. HasCallStack => Bool -> a -> a
assert ([Coercion]
cos [Coercion] -> [CoVar] -> Bool
forall a b. [a] -> [b] -> Bool
`equalLength` [CoVar]
tcvs) (Type -> Type) -> Type -> Type
forall a b. (a -> b) -> a -> b
$
                  -- Invariant of AxiomRuleCo: cos should
                  -- exactly saturate the axiom branch
        let ([Type]
tys1, [Type]
cotys1) = [CoVar] -> [Type] -> ([Type], [Type])
forall b a. [b] -> [a] -> ([a], [a])
splitAtList [CoVar]
tvs [Type]
tys
            cos1 :: [Coercion]
cos1           = (Type -> Coercion) -> [Type] -> [Coercion]
forall a b. (a -> b) -> [a] -> [b]
map Type -> Coercion
stripCoercionTy [Type]
cotys1
        in
        -- You might think to use
        --        substTy (zipTCvSubst tcvs ltys) (pickLR ...)
        -- but #25066 makes it much less efficient than the silly calls below
        [CoVar] -> [Type] -> Type -> Type
HasDebugCallStack => [CoVar] -> [Type] -> Type -> Type
substTyWith [CoVar]
tvs [Type]
tys1       (Type -> Type) -> Type -> Type
forall a b. (a -> b) -> a -> b
$
        [CoVar] -> [Coercion] -> Type -> Type
substTyWithCoVars [CoVar]
cvs [Coercion]
cos1 (Type -> Type) -> Type -> Type
forall a b. (a -> b) -> a -> b
$
        LeftOrRight -> (Type, Type) -> Type
forall a. LeftOrRight -> (a, a) -> a
pickLR LeftOrRight
which (TyCon -> [Type] -> Type
mkTyConApp TyCon
tc [Type]
lhs_tys, Type
rhs_ty)
     where
       tc :: TyCon
tc   = CoAxiom br -> TyCon
forall (br :: BranchFlag). CoAxiom br -> TyCon
coAxiomTyCon CoAxiom br
ax
       tcvs :: [CoVar]
tcvs | [CoVar] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [CoVar]
cvs  = [CoVar]
tvs  -- Very common case (currently always!)
            | Bool
otherwise = [CoVar]
tvs [CoVar] -> [CoVar] -> [CoVar]
forall a. [a] -> [a] -> [a]
++ [CoVar]
cvs
       tys :: [Type]
tys = (Coercion -> Type) -> [Coercion] -> [Type]
forall a b. (a -> b) -> [a] -> [b]
map Coercion -> Type
go [Coercion]
cos

    -------------
    go_forall_right :: Subst -> Coercion -> Type
go_forall_right Subst
subst (ForAllCo { fco_tcv :: Coercion -> CoVar
fco_tcv = CoVar
tv1, fco_visR :: Coercion -> ForAllTyFlag
fco_visR = ForAllTyFlag
visR
                                    , fco_kind :: Coercion -> Coercion
fco_kind = Coercion
k_co, fco_body :: Coercion -> Coercion
fco_body = Coercion
co })
      -- See Note [Nested ForAllCos]
      | CoVar -> Bool
isTyVar CoVar
tv1
      = ForAllTyBinder -> Type -> Type
mkForAllTy (CoVar -> ForAllTyFlag -> ForAllTyBinder
forall var argf. var -> argf -> VarBndr var argf
Bndr CoVar
tv2 ForAllTyFlag
visR) (Subst -> Coercion -> Type
go_forall_right Subst
subst' Coercion
co)
      where
        k2 :: Type
k2  = HasDebugCallStack => Coercion -> Type
Coercion -> Type
coercionRKind Coercion
k_co
        tv2 :: CoVar
tv2 = CoVar -> Type -> CoVar
setTyVarKind CoVar
tv1 (HasDebugCallStack => Subst -> Type -> Type
Subst -> Type -> Type
substTy Subst
subst Type
k2)
        subst' :: Subst
subst' | Coercion -> Bool
isGReflCo Coercion
k_co = Subst -> CoVar -> Subst
extendSubstInScope Subst
subst CoVar
tv1
                 -- kind_co always has kind @Type@, thus @isGReflCo@
               | Bool
otherwise      = Subst -> CoVar -> Type -> Subst
extendTvSubst (Subst -> CoVar -> Subst
extendSubstInScope Subst
subst CoVar
tv2) CoVar
tv1 (Type -> Subst) -> Type -> Subst
forall a b. (a -> b) -> a -> b
$
                                  CoVar -> Type
TyVarTy CoVar
tv2 Type -> Coercion -> Type
`mkCastTy` Coercion -> Coercion
mkSymCo Coercion
k_co

    go_forall_right Subst
subst (ForAllCo { fco_tcv :: Coercion -> CoVar
fco_tcv = CoVar
cv1, fco_visR :: Coercion -> ForAllTyFlag
fco_visR = ForAllTyFlag
visR
                                    , fco_kind :: Coercion -> Coercion
fco_kind = Coercion
k_co, fco_body :: Coercion -> Coercion
fco_body = Coercion
co })
      | CoVar -> Bool
isCoVar CoVar
cv1
      = CoVar -> ForAllTyFlag -> Type -> Type
mkTyCoForAllTy CoVar
cv2 ForAllTyFlag
visR (Subst -> Coercion -> Type
go_forall_right Subst
subst' Coercion
co)
      where
        k2 :: Type
k2    = HasDebugCallStack => Coercion -> Type
Coercion -> Type
coercionRKind Coercion
k_co
        r :: Role
r     = CoVar -> Role
coVarRole CoVar
cv1
        k_co' :: Coercion
k_co' = Role -> Role -> Coercion -> Coercion
downgradeRole Role
r Role
Nominal Coercion
k_co
        eta1 :: Coercion
eta1  = HasDebugCallStack => CoSel -> Coercion -> Coercion
CoSel -> Coercion -> Coercion
mkSelCo (Arity -> Role -> CoSel
SelTyCon Arity
2 Role
r) Coercion
k_co'
        eta2 :: Coercion
eta2  = HasDebugCallStack => CoSel -> Coercion -> Coercion
CoSel -> Coercion -> Coercion
mkSelCo (Arity -> Role -> CoSel
SelTyCon Arity
3 Role
r) Coercion
k_co'

        -- k_co :: (t1 ~r t2) ~N (s1 ~r s2)
        -- k1    = t1 ~r t2
        -- k2    = s1 ~r s2
        -- cv1  :: t1 ~r t2
        -- cv2  :: s1 ~r s2
        -- eta1 :: t1 ~r s1
        -- eta2 :: t2 ~r s2
        -- n_subst  = (eta1 ; cv2 ; sym eta2) :: t1 ~r t2

        cv2 :: CoVar
cv2     = CoVar -> Type -> CoVar
setVarType CoVar
cv1 (HasDebugCallStack => Subst -> Type -> Type
Subst -> Type -> Type
substTy Subst
subst Type
k2)
        n_subst :: Coercion
n_subst = Coercion
eta1 Coercion -> Coercion -> Coercion
`mkTransCo` (CoVar -> Coercion
mkCoVarCo CoVar
cv2) Coercion -> Coercion -> Coercion
`mkTransCo` (Coercion -> Coercion
mkSymCo Coercion
eta2)
        subst' :: Subst
subst'  | Coercion -> Bool
isReflCo Coercion
k_co = Subst -> CoVar -> Subst
extendSubstInScope Subst
subst CoVar
cv1
                | Bool
otherwise     = Subst -> CoVar -> Coercion -> Subst
extendCvSubst (Subst -> CoVar -> Subst
extendSubstInScope Subst
subst CoVar
cv2)
                                                CoVar
cv1 Coercion
n_subst

    go_forall_right Subst
subst Coercion
other_co
      -- when other_co is not a ForAllCo
      = HasDebugCallStack => Subst -> Type -> Type
Subst -> Type -> Type
substTy Subst
subst (Coercion -> Type
go Coercion
other_co)

{- Note [Nested ForAllCos]
~~~~~~~~~~~~~~~~~~~~~~~~~~
Suppose we need `coercionKind (ForAllCo a1 (ForAllCo a2 ... (ForAllCo an co)...) )`.
We do not want to perform `n` single-type-variable substitutions over the kind
of `co`; rather we want to do one substitution which substitutes for all of
`a1`, `a2` ... simultaneously.  If we do one at a time we get the performance
hole reported in #11735.

Solution: gather up the type variables for nested `ForAllCos`, and
substitute for them all at once.  Remarkably, for #11735 this single
change reduces /total/ compile time by a factor of more than ten.

Note [Nested InstCos]
~~~~~~~~~~~~~~~~~~~~~
In #5631 we found that 70% of the entire compilation time was
being spent in coercionKind!  The reason was that we had
   (g @ ty1 @ ty2 .. @ ty100)    -- The "@s" are InstCos
where
   g :: forall a1 a2 .. a100. phi
If we deal with the InstCos one at a time, we'll do this:
   1.  Find the kind of (g @ ty1 .. @ ty99) : forall a100. phi'
   2.  Substitute phi'[ ty100/a100 ], a single tyvar->type subst
But this is a *quadratic* algorithm, and the blew up #5631.
So it's very important to do the substitution simultaneously;
cf Type.piResultTys (which in fact we call here).
-}

-- | Retrieve the role from a coercion.
coercionRole :: Coercion -> Role
coercionRole :: Coercion -> Role
coercionRole = Coercion -> Role
go
  where
    go :: Coercion -> Role
go (Refl Type
_)                     = Role
Nominal
    go (GRefl Role
r Type
_ MCoercion
_)                = Role
r
    go (TyConAppCo Role
r TyCon
_ [Coercion]
_)           = Role
r
    go (AppCo Coercion
co1 Coercion
_)                = Coercion -> Role
go Coercion
co1
    go (ForAllCo { fco_body :: Coercion -> Coercion
fco_body = Coercion
co }) = Coercion -> Role
go Coercion
co
    go (FunCo { fco_role :: Coercion -> Role
fco_role = Role
r })     = Role
r
    go (CoVarCo CoVar
cv)                 = CoVar -> Role
coVarRole CoVar
cv
    go (HoleCo CoercionHole
h)                   = CoVar -> Role
coVarRole (CoercionHole -> CoVar
coHoleCoVar CoercionHole
h)
    go (UnivCo { uco_role :: Coercion -> Role
uco_role = Role
r })    = Role
r
    go (SymCo Coercion
co)                   = Coercion -> Role
go Coercion
co
    go (TransCo Coercion
co1 Coercion
_co2)           = Coercion -> Role
go Coercion
co1
    go (SelCo CoSel
cs Coercion
co)                = CoSel -> Role -> Role
mkSelCoResRole CoSel
cs (Coercion -> Role
coercionRole Coercion
co)
    go (LRCo {})                    = Role
Nominal
    go (InstCo Coercion
co Coercion
_)                = Coercion -> Role
go Coercion
co
    go (KindCo {})                  = Role
Nominal
    go (SubCo Coercion
_)                    = Role
Representational
    go (AxiomCo CoAxiomRule
ax [Coercion]
_)               = CoAxiomRule -> Role
coAxiomRuleRole CoAxiomRule
ax

-- | Makes a coercion type from two types: the types whose equality
-- is proven by the relevant 'Coercion'
mkCoercionType :: Role -> Type -> Type -> Type
mkCoercionType :: Role -> Type -> Type -> Type
mkCoercionType Role
Nominal          = Type -> Type -> Type
mkPrimEqPred
mkCoercionType Role
Representational = Type -> Type -> Type
mkReprPrimEqPred
mkCoercionType Role
Phantom          = \Type
ty1 Type
ty2 ->
  let ki1 :: Type
ki1 = HasDebugCallStack => Type -> Type
Type -> Type
typeKind Type
ty1
      ki2 :: Type
ki2 = HasDebugCallStack => Type -> Type
Type -> Type
typeKind Type
ty2
  in
  TyCon -> [Type] -> Type
TyConApp TyCon
eqPhantPrimTyCon [Type
ki1, Type
ki2, Type
ty1, Type
ty2]

-- | Creates a primitive nominal type equality predicate.
--      t1 ~# t2
-- Invariant: the types are not Coercions
mkPrimEqPred :: Type -> Type -> Type
mkPrimEqPred :: Type -> Type -> Type
mkPrimEqPred Type
ty1 Type
ty2
  = TyCon -> [Type] -> Type
mkTyConApp TyCon
eqPrimTyCon [Type
k1, Type
k2, Type
ty1, Type
ty2]
  where
    k1 :: Type
k1 = HasDebugCallStack => Type -> Type
Type -> Type
typeKind Type
ty1
    k2 :: Type
k2 = HasDebugCallStack => Type -> Type
Type -> Type
typeKind Type
ty2

-- | Creates a primitive representational type equality predicate.
--      t1 ~R# t2
-- Invariant: the types are not Coercions
mkReprPrimEqPred :: Type -> Type -> Type
mkReprPrimEqPred :: Type -> Type -> Type
mkReprPrimEqPred Type
ty1  Type
ty2
  = TyCon -> [Type] -> Type
mkTyConApp TyCon
eqReprPrimTyCon [Type
k1, Type
k2, Type
ty1, Type
ty2]
  where
    k1 :: Type
k1 = HasDebugCallStack => Type -> Type
Type -> Type
typeKind Type
ty1
    k2 :: Type
k2 = HasDebugCallStack => Type -> Type
Type -> Type
typeKind Type
ty2

-- | Makes a lifted equality predicate at the given role
mkPrimEqPredRole :: Role -> Type -> Type -> PredType
mkPrimEqPredRole :: Role -> Type -> Type -> Type
mkPrimEqPredRole Role
Nominal          = Type -> Type -> Type
mkPrimEqPred
mkPrimEqPredRole Role
Representational = Type -> Type -> Type
mkReprPrimEqPred
mkPrimEqPredRole Role
Phantom          = String -> Type -> Type -> Type
forall a. HasCallStack => String -> a
panic String
"mkPrimEqPredRole phantom"

-- | Creates a primitive nominal type equality predicate with an explicit
--   (but homogeneous) kind: (~#) k k ty1 ty2
mkNomPrimEqPred :: Kind -> Type -> Type -> Type
mkNomPrimEqPred :: Type -> Type -> Type -> Type
mkNomPrimEqPred Type
k Type
ty1 Type
ty2 = TyCon -> [Type] -> Type
mkTyConApp TyCon
eqPrimTyCon [Type
k, Type
k, Type
ty1, Type
ty2]

-- | Assuming that two types are the same, ignoring coercions, find
-- a nominal coercion between the types. This is useful when optimizing
-- transitivity over coercion applications, where splitting two
-- AppCos might yield different kinds. See Note [EtaAppCo] in
-- "GHC.Core.Coercion.Opt".
buildCoercion :: Type -> Type -> CoercionN
buildCoercion :: Type -> Type -> Coercion
buildCoercion Type
orig_ty1 Type
orig_ty2 = Type -> Type -> Coercion
go Type
orig_ty1 Type
orig_ty2
  where
    go :: Type -> Type -> Coercion
go Type
ty1 Type
ty2 | Just Type
ty1' <- Type -> Maybe Type
coreView Type
ty1 = Type -> Type -> Coercion
go Type
ty1' Type
ty2
               | Just Type
ty2' <- Type -> Maybe Type
coreView Type
ty2 = Type -> Type -> Coercion
go Type
ty1 Type
ty2'

    go (CastTy Type
ty1 Coercion
co) Type
ty2
      = let co' :: Coercion
co' = Type -> Type -> Coercion
go Type
ty1 Type
ty2
            r :: Role
r = Coercion -> Role
coercionRole Coercion
co'
        in  Role -> Type -> Coercion -> Coercion -> Coercion
mkCoherenceLeftCo Role
r Type
ty1 Coercion
co Coercion
co'

    go Type
ty1 (CastTy Type
ty2 Coercion
co)
      = let co' :: Coercion
co' = Type -> Type -> Coercion
go Type
ty1 Type
ty2
            r :: Role
r = Coercion -> Role
coercionRole Coercion
co'
        in  Role -> Type -> Coercion -> Coercion -> Coercion
mkCoherenceRightCo Role
r Type
ty2 Coercion
co Coercion
co'

    go ty1 :: Type
ty1@(TyVarTy CoVar
tv1) Type
_tyvarty
      = Bool -> Coercion -> Coercion
forall a. HasCallStack => Bool -> a -> a
assert (case Type
_tyvarty of
                  { TyVarTy CoVar
tv2 -> CoVar
tv1 CoVar -> CoVar -> Bool
forall a. Eq a => a -> a -> Bool
== CoVar
tv2
                  ; Type
_           -> Bool
False      }) (Coercion -> Coercion) -> Coercion -> Coercion
forall a b. (a -> b) -> a -> b
$
        Type -> Coercion
mkNomReflCo Type
ty1

    go (FunTy { ft_af :: Type -> FunTyFlag
ft_af = FunTyFlag
af1, ft_mult :: Type -> Type
ft_mult = Type
w1, ft_arg :: Type -> Type
ft_arg = Type
arg1, ft_res :: Type -> Type
ft_res = Type
res1 })
       (FunTy { ft_af :: Type -> FunTyFlag
ft_af = FunTyFlag
af2, ft_mult :: Type -> Type
ft_mult = Type
w2, ft_arg :: Type -> Type
ft_arg = Type
arg2, ft_res :: Type -> Type
ft_res = Type
res2 })
      = Bool -> Coercion -> Coercion
forall a. HasCallStack => Bool -> a -> a
assert (FunTyFlag
af1 FunTyFlag -> FunTyFlag -> Bool
forall a. Eq a => a -> a -> Bool
== FunTyFlag
af2) (Coercion -> Coercion) -> Coercion -> Coercion
forall a b. (a -> b) -> a -> b
$
        Role -> FunTyFlag -> Coercion -> Coercion -> Coercion -> Coercion
mkFunCo Role
Nominal FunTyFlag
af1 (Type -> Type -> Coercion
go Type
w1 Type
w2) (Type -> Type -> Coercion
go Type
arg1 Type
arg2) (Type -> Type -> Coercion
go Type
res1 Type
res2)

    go (TyConApp TyCon
tc1 [Type]
args1) (TyConApp TyCon
tc2 [Type]
args2)
      = Bool -> Coercion -> Coercion
forall a. HasCallStack => Bool -> a -> a
assert (TyCon
tc1 TyCon -> TyCon -> Bool
forall a. Eq a => a -> a -> Bool
== TyCon
tc2) (Coercion -> Coercion) -> Coercion -> Coercion
forall a b. (a -> b) -> a -> b
$
        HasDebugCallStack => Role -> TyCon -> [Coercion] -> Coercion
Role -> TyCon -> [Coercion] -> Coercion
mkTyConAppCo Role
Nominal TyCon
tc1 ((Type -> Type -> Coercion) -> [Type] -> [Type] -> [Coercion]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith Type -> Type -> Coercion
go [Type]
args1 [Type]
args2)

    go (AppTy Type
ty1a Type
ty1b) Type
ty2
      | Just (Type
ty2a, Type
ty2b) <- HasDebugCallStack => Type -> Maybe (Type, Type)
Type -> Maybe (Type, Type)
splitAppTyNoView_maybe Type
ty2
      = Coercion -> Coercion -> Coercion
mkAppCo (Type -> Type -> Coercion
go Type
ty1a Type
ty2a) (Type -> Type -> Coercion
go Type
ty1b Type
ty2b)

    go Type
ty1 (AppTy Type
ty2a Type
ty2b)
      | Just (Type
ty1a, Type
ty1b) <- HasDebugCallStack => Type -> Maybe (Type, Type)
Type -> Maybe (Type, Type)
splitAppTyNoView_maybe Type
ty1
      = Coercion -> Coercion -> Coercion
mkAppCo (Type -> Type -> Coercion
go Type
ty1a Type
ty2a) (Type -> Type -> Coercion
go Type
ty1b Type
ty2b)

    go (ForAllTy (Bndr CoVar
tv1 ForAllTyFlag
flag1) Type
ty1) (ForAllTy (Bndr CoVar
tv2 ForAllTyFlag
flag2) Type
ty2)
      | CoVar -> Bool
isTyVar CoVar
tv1
      = Bool -> Coercion -> Coercion
forall a. HasCallStack => Bool -> a -> a
assert (CoVar -> Bool
isTyVar CoVar
tv2) (Coercion -> Coercion) -> Coercion -> Coercion
forall a b. (a -> b) -> a -> b
$
        HasDebugCallStack =>
CoVar
-> ForAllTyFlag -> ForAllTyFlag -> Coercion -> Coercion -> Coercion
CoVar
-> ForAllTyFlag -> ForAllTyFlag -> Coercion -> Coercion -> Coercion
mkForAllCo CoVar
tv1 ForAllTyFlag
flag1 ForAllTyFlag
flag2 Coercion
kind_co (Type -> Type -> Coercion
go Type
ty1 Type
ty2')
      where kind_co :: Coercion
kind_co  = Type -> Type -> Coercion
go (CoVar -> Type
tyVarKind CoVar
tv1) (CoVar -> Type
tyVarKind CoVar
tv2)
            in_scope :: InScopeSet
in_scope = VarSet -> InScopeSet
mkInScopeSet (VarSet -> InScopeSet) -> VarSet -> InScopeSet
forall a b. (a -> b) -> a -> b
$ Type -> VarSet
tyCoVarsOfType Type
ty2 VarSet -> VarSet -> VarSet
`unionVarSet` Coercion -> VarSet
tyCoVarsOfCo Coercion
kind_co
            ty2' :: Type
ty2'     = HasDebugCallStack =>
InScopeSet -> [CoVar] -> [Type] -> Type -> Type
InScopeSet -> [CoVar] -> [Type] -> Type -> Type
substTyWithInScope InScopeSet
in_scope [CoVar
tv2]
                         [CoVar -> Type
mkTyVarTy CoVar
tv1 Type -> Coercion -> Type
`mkCastTy` Coercion
kind_co]
                         Type
ty2

    go (ForAllTy (Bndr CoVar
cv1 ForAllTyFlag
flag1) Type
ty1) (ForAllTy (Bndr CoVar
cv2 ForAllTyFlag
flag2) Type
ty2)
      = Bool -> Coercion -> Coercion
forall a. HasCallStack => Bool -> a -> a
assert (CoVar -> Bool
isCoVar CoVar
cv1 Bool -> Bool -> Bool
&& CoVar -> Bool
isCoVar CoVar
cv2) (Coercion -> Coercion) -> Coercion -> Coercion
forall a b. (a -> b) -> a -> b
$
        HasDebugCallStack =>
CoVar
-> ForAllTyFlag -> ForAllTyFlag -> Coercion -> Coercion -> Coercion
CoVar
-> ForAllTyFlag -> ForAllTyFlag -> Coercion -> Coercion -> Coercion
mkForAllCo CoVar
cv1 ForAllTyFlag
flag1 ForAllTyFlag
flag2 Coercion
kind_co (Type -> Type -> Coercion
go Type
ty1 Type
ty2')
      where s1 :: Type
s1 = CoVar -> Type
varType CoVar
cv1
            s2 :: Type
s2 = CoVar -> Type
varType CoVar
cv2
            kind_co :: Coercion
kind_co = Type -> Type -> Coercion
go Type
s1 Type
s2

            -- s1 = t1 ~r t2
            -- s2 = t3 ~r t4
            -- kind_co :: (t1 ~r t2) ~N (t3 ~r t4)
            -- eta1 :: t1 ~r t3
            -- eta2 :: t2 ~r t4

            r :: Role
r    = CoVar -> Role
coVarRole CoVar
cv1
            kind_co' :: Coercion
kind_co' = Role -> Role -> Coercion -> Coercion
downgradeRole Role
r Role
Nominal Coercion
kind_co
            eta1 :: Coercion
eta1 = HasDebugCallStack => CoSel -> Coercion -> Coercion
CoSel -> Coercion -> Coercion
mkSelCo (Arity -> Role -> CoSel
SelTyCon Arity
2 Role
r) Coercion
kind_co'
            eta2 :: Coercion
eta2 = HasDebugCallStack => CoSel -> Coercion -> Coercion
CoSel -> Coercion -> Coercion
mkSelCo (Arity -> Role -> CoSel
SelTyCon Arity
3 Role
r) Coercion
kind_co'

            subst :: Subst
subst = InScopeSet -> Subst
mkEmptySubst (InScopeSet -> Subst) -> InScopeSet -> Subst
forall a b. (a -> b) -> a -> b
$ VarSet -> InScopeSet
mkInScopeSet (VarSet -> InScopeSet) -> VarSet -> InScopeSet
forall a b. (a -> b) -> a -> b
$
                      Type -> VarSet
tyCoVarsOfType Type
ty2 VarSet -> VarSet -> VarSet
`unionVarSet` Coercion -> VarSet
tyCoVarsOfCo Coercion
kind_co
            ty2' :: Type
ty2'  = HasDebugCallStack => Subst -> Type -> Type
Subst -> Type -> Type
substTy (Subst -> CoVar -> Coercion -> Subst
extendCvSubst Subst
subst CoVar
cv2 (Coercion -> Subst) -> Coercion -> Subst
forall a b. (a -> b) -> a -> b
$ Coercion -> Coercion
mkSymCo Coercion
eta1 Coercion -> Coercion -> Coercion
`mkTransCo`
                                                       CoVar -> Coercion
mkCoVarCo CoVar
cv1 Coercion -> Coercion -> Coercion
`mkTransCo`
                                                       Coercion
eta2)
                            Type
ty2

    go ty1 :: Type
ty1@(LitTy TyLit
lit1) Type
_lit2
      = Bool -> Coercion -> Coercion
forall a. HasCallStack => Bool -> a -> a
assert (case Type
_lit2 of
                  { LitTy TyLit
lit2 -> TyLit
lit1 TyLit -> TyLit -> Bool
forall a. Eq a => a -> a -> Bool
== TyLit
lit2
                  ; Type
_          -> Bool
False        }) (Coercion -> Coercion) -> Coercion -> Coercion
forall a b. (a -> b) -> a -> b
$
        Type -> Coercion
mkNomReflCo Type
ty1

    go (CoercionTy Coercion
co1) (CoercionTy Coercion
co2)
      = Role -> Coercion -> Coercion -> Coercion -> Coercion
mkProofIrrelCo Role
Nominal Coercion
kind_co Coercion
co1 Coercion
co2
      where
        kind_co :: Coercion
kind_co = Type -> Type -> Coercion
go (Coercion -> Type
coercionType Coercion
co1) (Coercion -> Type
coercionType Coercion
co2)

    go Type
ty1 Type
ty2
      = String -> SDoc -> Coercion
forall a. HasCallStack => String -> SDoc -> a
pprPanic String
"buildKindCoercion" ([SDoc] -> SDoc
forall doc. IsDoc doc => [doc] -> doc
vcat [ Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
orig_ty1, Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
orig_ty2
                                           , Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
ty1, Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
ty2 ])


{-
%************************************************************************
%*                                                                      *
       Coercion holes
%*                                                                      *
%************************************************************************
-}

has_co_hole_ty :: Type -> Monoid.Any
has_co_hole_co :: Coercion -> Monoid.Any
(Type -> Any
has_co_hole_ty, [Type] -> Any
_, Coercion -> Any
has_co_hole_co, [Coercion] -> Any
_)
  = TyCoFolder () Any
-> ()
-> (Type -> Any, [Type] -> Any, Coercion -> Any, [Coercion] -> Any)
forall a env.
Monoid a =>
TyCoFolder env a
-> env -> (Type -> a, [Type] -> a, Coercion -> a, [Coercion] -> a)
foldTyCo TyCoFolder () Any
forall {env}. TyCoFolder env Any
folder ()
  where
    folder :: TyCoFolder env Any
folder = TyCoFolder { tcf_view :: Type -> Maybe Type
tcf_view  = Type -> Maybe Type
noView
                        , tcf_tyvar :: env -> CoVar -> Any
tcf_tyvar = Any -> env -> CoVar -> Any
forall a b c. a -> b -> c -> a
const2 (Bool -> Any
Monoid.Any Bool
False)
                        , tcf_covar :: env -> CoVar -> Any
tcf_covar = Any -> env -> CoVar -> Any
forall a b c. a -> b -> c -> a
const2 (Bool -> Any
Monoid.Any Bool
False)
                        , tcf_hole :: env -> CoercionHole -> Any
tcf_hole  = \env
_ CoercionHole
hole -> Bool -> Any
Monoid.Any (CoercionHole -> Bool
isHeteroKindCoHole CoercionHole
hole)
                        , tcf_tycobinder :: env -> CoVar -> ForAllTyFlag -> env
tcf_tycobinder = env -> CoVar -> ForAllTyFlag -> env
forall a b c. a -> b -> c -> a
const2
                        }

-- | Is there a hetero-kind coercion hole in this type?
--   (That is, a coercion hole with ch_hetero_kind=True.)
-- See wrinkle (EIK2) of Note [Equalities with incompatible kinds] in GHC.Tc.Solver.Equality
hasCoercionHoleTy :: Type -> Bool
hasCoercionHoleTy :: Type -> Bool
hasCoercionHoleTy = Any -> Bool
Monoid.getAny (Any -> Bool) -> (Type -> Any) -> Type -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Type -> Any
has_co_hole_ty

-- | Is there a hetero-kind coercion hole in this coercion?
hasCoercionHoleCo :: Coercion -> Bool
hasCoercionHoleCo :: Coercion -> Bool
hasCoercionHoleCo = Any -> Bool
Monoid.getAny (Any -> Bool) -> (Coercion -> Any) -> Coercion -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Coercion -> Any
has_co_hole_co

hasThisCoercionHoleTy :: Type -> CoercionHole -> Bool
hasThisCoercionHoleTy :: Type -> CoercionHole -> Bool
hasThisCoercionHoleTy Type
ty CoercionHole
hole = Any -> Bool
Monoid.getAny (Type -> Any
f Type
ty)
  where
    (Type -> Any
f, [Type] -> Any
_, Coercion -> Any
_, [Coercion] -> Any
_) = TyCoFolder () Any
-> ()
-> (Type -> Any, [Type] -> Any, Coercion -> Any, [Coercion] -> Any)
forall a env.
Monoid a =>
TyCoFolder env a
-> env -> (Type -> a, [Type] -> a, Coercion -> a, [Coercion] -> a)
foldTyCo TyCoFolder () Any
folder ()

    folder :: TyCoFolder () Any
folder = TyCoFolder { tcf_view :: Type -> Maybe Type
tcf_view  = Type -> Maybe Type
noView
                        , tcf_tyvar :: () -> CoVar -> Any
tcf_tyvar = Any -> () -> CoVar -> Any
forall a b c. a -> b -> c -> a
const2 (Bool -> Any
Monoid.Any Bool
False)
                        , tcf_covar :: () -> CoVar -> Any
tcf_covar = Any -> () -> CoVar -> Any
forall a b c. a -> b -> c -> a
const2 (Bool -> Any
Monoid.Any Bool
False)
                        , tcf_hole :: () -> CoercionHole -> Any
tcf_hole  = \ ()
_ CoercionHole
h -> Bool -> Any
Monoid.Any (CoercionHole -> Unique
forall a. Uniquable a => a -> Unique
getUnique CoercionHole
h Unique -> Unique -> Bool
forall a. Eq a => a -> a -> Bool
== CoercionHole -> Unique
forall a. Uniquable a => a -> Unique
getUnique CoercionHole
hole)
                        , tcf_tycobinder :: () -> CoVar -> ForAllTyFlag -> ()
tcf_tycobinder = () -> CoVar -> ForAllTyFlag -> ()
forall a b c. a -> b -> c -> a
const2
                        }

-- | Set the type of a 'CoercionHole'
setCoHoleType :: CoercionHole -> Type -> CoercionHole
setCoHoleType :: CoercionHole -> Type -> CoercionHole
setCoHoleType CoercionHole
h Type
t = CoercionHole -> CoVar -> CoercionHole
setCoHoleCoVar CoercionHole
h (CoVar -> Type -> CoVar
setVarType (CoercionHole -> CoVar
coHoleCoVar CoercionHole
h) Type
t)