{-# OPTIONS_HADDOCK not-home #-}
{-# LANGUAGE CPP, DeriveDataTypeable, MultiWayIf #-}
module TyCoRep (
TyThing(..), tyThingCategory, pprTyThingCategory, pprShortTyThing,
Type(..),
TyLit(..),
KindOrType, Kind,
KnotTied,
PredType, ThetaType,
ArgFlag(..),
Coercion(..),
UnivCoProvenance(..),
CoercionHole(..), coHoleCoVar, setCoHoleCoVar,
CoercionN, CoercionR, CoercionP, KindCoercion,
MCoercion(..), MCoercionR, MCoercionN,
mkTyConTy, mkTyVarTy, mkTyVarTys,
mkTyCoVarTy, mkTyCoVarTys,
mkFunTy, mkFunTys, mkTyCoForAllTy, mkForAllTys,
mkForAllTy,
mkTyCoPiTy, mkTyCoPiTys,
mkPiTys,
kindRep_maybe, kindRep,
isLiftedTypeKind, isUnliftedTypeKind,
isLiftedRuntimeRep, isUnliftedRuntimeRep,
isRuntimeRepTy, isRuntimeRepVar,
sameVis,
TyCoBinder(..), TyCoVarBinder, TyBinder,
binderVar, binderVars, binderType, binderArgFlag,
delBinderVar,
isInvisibleArgFlag, isVisibleArgFlag,
isInvisibleBinder, isVisibleBinder,
isTyBinder, isNamedBinder,
tyCoBinderArgFlag,
pickLR,
pprType, pprParendType, pprPrecType, pprPrecTypeX,
pprTypeApp, pprTCvBndr, pprTCvBndrs,
pprSigmaType,
pprTheta, pprParendTheta, pprForAll, pprUserForAll,
pprTyVar, pprTyVars,
pprThetaArrowTy, pprClassPred,
pprKind, pprParendKind, pprTyLit,
PprPrec(..), topPrec, sigPrec, opPrec, funPrec, appPrec, maybeParen,
pprDataCons, pprWithExplicitKindsWhen,
pprCo, pprParendCo,
debugPprType,
tyCoVarsOfType, tyCoVarsOfTypeDSet, tyCoVarsOfTypes, tyCoVarsOfTypesDSet,
tyCoFVsBndr, tyCoFVsVarBndr, tyCoFVsVarBndrs,
tyCoFVsOfType, tyCoVarsOfTypeList,
tyCoFVsOfTypes, tyCoVarsOfTypesList,
coVarsOfType, coVarsOfTypes,
coVarsOfCo, coVarsOfCos,
tyCoVarsOfCo, tyCoVarsOfCos,
tyCoVarsOfCoDSet,
tyCoFVsOfCo, tyCoFVsOfCos,
tyCoVarsOfCoList, tyCoVarsOfProv,
almostDevoidCoVarOfCo,
injectiveVarsOfType, tyConAppNeedsKindSig,
noFreeVarsOfType, noFreeVarsOfCo,
TCvSubst(..), TvSubstEnv, CvSubstEnv,
emptyTvSubstEnv, emptyCvSubstEnv, composeTCvSubstEnv, composeTCvSubst,
emptyTCvSubst, mkEmptyTCvSubst, isEmptyTCvSubst,
mkTCvSubst, mkTvSubst, mkCvSubst,
getTvSubstEnv,
getCvSubstEnv, getTCvInScope, getTCvSubstRangeFVs,
isInScope, notElemTCvSubst,
setTvSubstEnv, setCvSubstEnv, zapTCvSubst,
extendTCvInScope, extendTCvInScopeList, extendTCvInScopeSet,
extendTCvSubst, extendTCvSubstWithClone,
extendCvSubst, extendCvSubstWithClone,
extendTvSubst, extendTvSubstBinderAndInScope, extendTvSubstWithClone,
extendTvSubstList, extendTvSubstAndInScope,
extendTCvSubstList,
unionTCvSubst, zipTyEnv, zipCoEnv, mkTyCoInScopeSet,
zipTvSubst, zipCvSubst,
zipTCvSubst,
mkTvSubstPrs,
substTyWith, substTyWithCoVars, substTysWith, substTysWithCoVars,
substCoWith,
substTy, substTyAddInScope,
substTyUnchecked, substTysUnchecked, substThetaUnchecked,
substTyWithUnchecked,
substCoUnchecked, substCoWithUnchecked,
substTyWithInScope,
substTys, substTheta,
lookupTyVar,
substCo, substCos, substCoVar, substCoVars, lookupCoVar,
cloneTyVarBndr, cloneTyVarBndrs,
substVarBndr, substVarBndrs,
substTyVarBndr, substTyVarBndrs,
substCoVarBndr,
substTyVar, substTyVars, substTyCoVars,
substForAllCoBndr,
substVarBndrUsing, substForAllCoBndrUsing,
checkValidSubst, isValidTCvSubst,
tidyType, tidyTypes,
tidyOpenType, tidyOpenTypes,
tidyOpenKind,
tidyVarBndr, tidyVarBndrs, tidyFreeTyCoVars, avoidNameClashes,
tidyOpenTyCoVar, tidyOpenTyCoVars,
tidyTyCoVarOcc,
tidyTopType,
tidyKind,
tidyCo, tidyCos,
tidyTyCoVarBinder, tidyTyCoVarBinders,
typeSize, coercionSize, provSize
) where
#include "HsVersions.h"
import GhcPrelude
import {-# SOURCE #-} DataCon( dataConFullSig
, dataConUserTyVarBinders
, DataCon )
import {-# SOURCE #-} Type( isPredTy, isCoercionTy, mkAppTy, mkCastTy
, tyCoVarsOfTypeWellScoped
, tyCoVarsOfTypesWellScoped
, scopedSort
, coreView )
import {-# SOURCE #-} Coercion
import {-# SOURCE #-} ConLike ( ConLike(..), conLikeName )
import {-# SOURCE #-} ToIface( toIfaceTypeX, toIfaceTyLit, toIfaceForAllBndr
, toIfaceTyCon, toIfaceTcArgs, toIfaceCoercionX )
import IfaceType
import Var
import VarEnv
import VarSet
import Name hiding ( varName )
import TyCon
import Class
import CoAxiom
import FV
import BasicTypes ( LeftOrRight(..), PprPrec(..), topPrec, sigPrec, opPrec
, funPrec, appPrec, maybeParen, pickLR )
import PrelNames
import Outputable
import DynFlags
import FastString
import Pair
import UniqSupply
import Util
import UniqFM
import UniqSet
import qualified Data.Data as Data hiding ( TyCon )
import Data.List
import Data.IORef ( IORef )
data TyThing
= AnId Id
| AConLike ConLike
| ATyCon TyCon
| ACoAxiom (CoAxiom Branched)
instance Outputable TyThing where
ppr :: TyThing -> SDoc
ppr = TyThing -> SDoc
pprShortTyThing
instance NamedThing TyThing where
getName :: TyThing -> Name
getName (AnId id :: Id
id) = Id -> Name
forall a. NamedThing a => a -> Name
getName Id
id
getName (ATyCon tc :: TyCon
tc) = TyCon -> Name
forall a. NamedThing a => a -> Name
getName TyCon
tc
getName (ACoAxiom cc :: CoAxiom Branched
cc) = CoAxiom Branched -> Name
forall a. NamedThing a => a -> Name
getName CoAxiom Branched
cc
getName (AConLike cl :: ConLike
cl) = ConLike -> Name
conLikeName ConLike
cl
pprShortTyThing :: TyThing -> SDoc
pprShortTyThing :: TyThing -> SDoc
pprShortTyThing thing :: TyThing
thing
= TyThing -> SDoc
pprTyThingCategory TyThing
thing SDoc -> SDoc -> SDoc
<+> SDoc -> SDoc
quotes (Name -> SDoc
forall a. Outputable a => a -> SDoc
ppr (TyThing -> Name
forall a. NamedThing a => a -> Name
getName TyThing
thing))
pprTyThingCategory :: TyThing -> SDoc
pprTyThingCategory :: TyThing -> SDoc
pprTyThingCategory = String -> SDoc
text (String -> SDoc) -> (TyThing -> String) -> TyThing -> SDoc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> String
capitalise (String -> String) -> (TyThing -> String) -> TyThing -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TyThing -> String
tyThingCategory
tyThingCategory :: TyThing -> String
tyThingCategory :: TyThing -> String
tyThingCategory (ATyCon tc :: TyCon
tc)
| TyCon -> Bool
isClassTyCon TyCon
tc = "class"
| Bool
otherwise = "type constructor"
tyThingCategory (ACoAxiom _) = "coercion axiom"
tyThingCategory (AnId _) = "identifier"
tyThingCategory (AConLike (RealDataCon _)) = "data constructor"
tyThingCategory (AConLike (PatSynCon _)) = "pattern synonym"
type KindOrType = Type
type Kind = Type
data Type
= TyVarTy Var
| AppTy
Type
Type
| TyConApp
TyCon
[KindOrType]
| ForAllTy
{-# UNPACK #-} !TyCoVarBinder
Type
| FunTy Type Type
| LitTy TyLit
| CastTy
Type
KindCoercion
| CoercionTy
Coercion
deriving Typeable Type
DataType
Constr
Typeable Type =>
(forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Type -> c Type)
-> (forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Type)
-> (Type -> Constr)
-> (Type -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Type))
-> (forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Type))
-> ((forall b. Data b => b -> b) -> Type -> Type)
-> (forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Type -> r)
-> (forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Type -> r)
-> (forall u. (forall d. Data d => d -> u) -> Type -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> Type -> u)
-> (forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Type -> m Type)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Type -> m Type)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Type -> m Type)
-> Data Type
Type -> DataType
Type -> Constr
(forall b. Data b => b -> b) -> Type -> Type
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Type -> c Type
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Type
forall a.
Typeable a =>
(forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u. Int -> (forall d. Data d => d -> u) -> Type -> u
forall u. (forall d. Data d => d -> u) -> Type -> [u]
forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Type -> r
forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Type -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Type -> m Type
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Type -> m Type
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Type
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Type -> c Type
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Type)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Type)
$cCoercionTy :: Constr
$cCastTy :: Constr
$cLitTy :: Constr
$cFunTy :: Constr
$cForAllTy :: Constr
$cTyConApp :: Constr
$cAppTy :: Constr
$cTyVarTy :: Constr
$tType :: DataType
gmapMo :: (forall d. Data d => d -> m d) -> Type -> m Type
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Type -> m Type
gmapMp :: (forall d. Data d => d -> m d) -> Type -> m Type
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Type -> m Type
gmapM :: (forall d. Data d => d -> m d) -> Type -> m Type
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Type -> m Type
gmapQi :: Int -> (forall d. Data d => d -> u) -> Type -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Type -> u
gmapQ :: (forall d. Data d => d -> u) -> Type -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> Type -> [u]
gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Type -> r
$cgmapQr :: forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Type -> r
gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Type -> r
$cgmapQl :: forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Type -> r
gmapT :: (forall b. Data b => b -> b) -> Type -> Type
$cgmapT :: (forall b. Data b => b -> b) -> Type -> Type
dataCast2 :: (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Type)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Type)
dataCast1 :: (forall d. Data d => c (t d)) -> Maybe (c Type)
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Type)
dataTypeOf :: Type -> DataType
$cdataTypeOf :: Type -> DataType
toConstr :: Type -> Constr
$ctoConstr :: Type -> Constr
gunfold :: (forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Type
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Type
gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Type -> c Type
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Type -> c Type
$cp1Data :: Typeable Type
Data.Data
data TyLit
= NumTyLit Integer
| StrTyLit FastString
deriving (TyLit -> TyLit -> Bool
(TyLit -> TyLit -> Bool) -> (TyLit -> TyLit -> Bool) -> Eq TyLit
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: TyLit -> TyLit -> Bool
$c/= :: TyLit -> TyLit -> Bool
== :: TyLit -> TyLit -> Bool
$c== :: TyLit -> TyLit -> Bool
Eq, Eq TyLit
Eq TyLit =>
(TyLit -> TyLit -> Ordering)
-> (TyLit -> TyLit -> Bool)
-> (TyLit -> TyLit -> Bool)
-> (TyLit -> TyLit -> Bool)
-> (TyLit -> TyLit -> Bool)
-> (TyLit -> TyLit -> TyLit)
-> (TyLit -> TyLit -> TyLit)
-> Ord TyLit
TyLit -> TyLit -> Bool
TyLit -> TyLit -> Ordering
TyLit -> TyLit -> TyLit
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: TyLit -> TyLit -> TyLit
$cmin :: TyLit -> TyLit -> TyLit
max :: TyLit -> TyLit -> TyLit
$cmax :: TyLit -> TyLit -> TyLit
>= :: TyLit -> TyLit -> Bool
$c>= :: TyLit -> TyLit -> Bool
> :: TyLit -> TyLit -> Bool
$c> :: TyLit -> TyLit -> Bool
<= :: TyLit -> TyLit -> Bool
$c<= :: TyLit -> TyLit -> Bool
< :: TyLit -> TyLit -> Bool
$c< :: TyLit -> TyLit -> Bool
compare :: TyLit -> TyLit -> Ordering
$ccompare :: TyLit -> TyLit -> Ordering
$cp1Ord :: Eq TyLit
Ord, Typeable TyLit
DataType
Constr
Typeable TyLit =>
(forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> TyLit -> c TyLit)
-> (forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c TyLit)
-> (TyLit -> Constr)
-> (TyLit -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c TyLit))
-> (forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c TyLit))
-> ((forall b. Data b => b -> b) -> TyLit -> TyLit)
-> (forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> TyLit -> r)
-> (forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> TyLit -> r)
-> (forall u. (forall d. Data d => d -> u) -> TyLit -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> TyLit -> u)
-> (forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> TyLit -> m TyLit)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> TyLit -> m TyLit)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> TyLit -> m TyLit)
-> Data TyLit
TyLit -> DataType
TyLit -> Constr
(forall b. Data b => b -> b) -> TyLit -> TyLit
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> TyLit -> c TyLit
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c TyLit
forall a.
Typeable a =>
(forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u. Int -> (forall d. Data d => d -> u) -> TyLit -> u
forall u. (forall d. Data d => d -> u) -> TyLit -> [u]
forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> TyLit -> r
forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> TyLit -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> TyLit -> m TyLit
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> TyLit -> m TyLit
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c TyLit
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> TyLit -> c TyLit
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c TyLit)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c TyLit)
$cStrTyLit :: Constr
$cNumTyLit :: Constr
$tTyLit :: DataType
gmapMo :: (forall d. Data d => d -> m d) -> TyLit -> m TyLit
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> TyLit -> m TyLit
gmapMp :: (forall d. Data d => d -> m d) -> TyLit -> m TyLit
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> TyLit -> m TyLit
gmapM :: (forall d. Data d => d -> m d) -> TyLit -> m TyLit
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> TyLit -> m TyLit
gmapQi :: Int -> (forall d. Data d => d -> u) -> TyLit -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> TyLit -> u
gmapQ :: (forall d. Data d => d -> u) -> TyLit -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> TyLit -> [u]
gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> TyLit -> r
$cgmapQr :: forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> TyLit -> r
gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> TyLit -> r
$cgmapQl :: forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> TyLit -> r
gmapT :: (forall b. Data b => b -> b) -> TyLit -> TyLit
$cgmapT :: (forall b. Data b => b -> b) -> TyLit -> TyLit
dataCast2 :: (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c TyLit)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c TyLit)
dataCast1 :: (forall d. Data d => c (t d)) -> Maybe (c TyLit)
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c TyLit)
dataTypeOf :: TyLit -> DataType
$cdataTypeOf :: TyLit -> DataType
toConstr :: TyLit -> Constr
$ctoConstr :: TyLit -> Constr
gunfold :: (forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c TyLit
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c TyLit
gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> TyLit -> c TyLit
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> TyLit -> c TyLit
$cp1Data :: Typeable TyLit
Data.Data)
type KnotTied ty = ty
data TyCoBinder
= Named TyCoVarBinder
| Anon Type
deriving Typeable TyCoBinder
DataType
Constr
Typeable TyCoBinder =>
(forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> TyCoBinder -> c TyCoBinder)
-> (forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c TyCoBinder)
-> (TyCoBinder -> Constr)
-> (TyCoBinder -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c TyCoBinder))
-> (forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c TyCoBinder))
-> ((forall b. Data b => b -> b) -> TyCoBinder -> TyCoBinder)
-> (forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> TyCoBinder -> r)
-> (forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> TyCoBinder -> r)
-> (forall u. (forall d. Data d => d -> u) -> TyCoBinder -> [u])
-> (forall u.
Int -> (forall d. Data d => d -> u) -> TyCoBinder -> u)
-> (forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> TyCoBinder -> m TyCoBinder)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> TyCoBinder -> m TyCoBinder)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> TyCoBinder -> m TyCoBinder)
-> Data TyCoBinder
TyCoBinder -> DataType
TyCoBinder -> Constr
(forall b. Data b => b -> b) -> TyCoBinder -> TyCoBinder
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> TyCoBinder -> c TyCoBinder
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c TyCoBinder
forall a.
Typeable a =>
(forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u. Int -> (forall d. Data d => d -> u) -> TyCoBinder -> u
forall u. (forall d. Data d => d -> u) -> TyCoBinder -> [u]
forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> TyCoBinder -> r
forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> TyCoBinder -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> TyCoBinder -> m TyCoBinder
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> TyCoBinder -> m TyCoBinder
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c TyCoBinder
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> TyCoBinder -> c TyCoBinder
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c TyCoBinder)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c TyCoBinder)
$cAnon :: Constr
$cNamed :: Constr
$tTyCoBinder :: DataType
gmapMo :: (forall d. Data d => d -> m d) -> TyCoBinder -> m TyCoBinder
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> TyCoBinder -> m TyCoBinder
gmapMp :: (forall d. Data d => d -> m d) -> TyCoBinder -> m TyCoBinder
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> TyCoBinder -> m TyCoBinder
gmapM :: (forall d. Data d => d -> m d) -> TyCoBinder -> m TyCoBinder
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> TyCoBinder -> m TyCoBinder
gmapQi :: Int -> (forall d. Data d => d -> u) -> TyCoBinder -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> TyCoBinder -> u
gmapQ :: (forall d. Data d => d -> u) -> TyCoBinder -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> TyCoBinder -> [u]
gmapQr :: (r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> TyCoBinder -> r
$cgmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> TyCoBinder -> r
gmapQl :: (r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> TyCoBinder -> r
$cgmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> TyCoBinder -> r
gmapT :: (forall b. Data b => b -> b) -> TyCoBinder -> TyCoBinder
$cgmapT :: (forall b. Data b => b -> b) -> TyCoBinder -> TyCoBinder
dataCast2 :: (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c TyCoBinder)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c TyCoBinder)
dataCast1 :: (forall d. Data d => c (t d)) -> Maybe (c TyCoBinder)
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c TyCoBinder)
dataTypeOf :: TyCoBinder -> DataType
$cdataTypeOf :: TyCoBinder -> DataType
toConstr :: TyCoBinder -> Constr
$ctoConstr :: TyCoBinder -> Constr
gunfold :: (forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c TyCoBinder
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c TyCoBinder
gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> TyCoBinder -> c TyCoBinder
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> TyCoBinder -> c TyCoBinder
$cp1Data :: Typeable TyCoBinder
Data.Data
type TyBinder = TyCoBinder
delBinderVar :: VarSet -> TyCoVarBinder -> VarSet
delBinderVar :: VarSet -> TyCoVarBinder -> VarSet
delBinderVar vars :: VarSet
vars (Bndr tv :: Id
tv _) = VarSet
vars VarSet -> Id -> VarSet
`delVarSet` Id
tv
isInvisibleBinder :: TyCoBinder -> Bool
isInvisibleBinder :: TyCoBinder -> Bool
isInvisibleBinder (Named (Bndr _ vis :: ArgFlag
vis)) = ArgFlag -> Bool
isInvisibleArgFlag ArgFlag
vis
isInvisibleBinder (Anon ty :: Type
ty) = Type -> Bool
isPredTy Type
ty
isVisibleBinder :: TyCoBinder -> Bool
isVisibleBinder :: TyCoBinder -> Bool
isVisibleBinder = Bool -> Bool
not (Bool -> Bool) -> (TyCoBinder -> Bool) -> TyCoBinder -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TyCoBinder -> Bool
isInvisibleBinder
isNamedBinder :: TyCoBinder -> Bool
isNamedBinder :: TyCoBinder -> Bool
isNamedBinder (Named {}) = Bool
True
isNamedBinder (Anon {}) = Bool
False
isTyBinder :: TyCoBinder -> Bool
isTyBinder :: TyCoBinder -> Bool
isTyBinder (Named bnd :: TyCoVarBinder
bnd) = TyCoVarBinder -> Bool
isTyVarBinder TyCoVarBinder
bnd
isTyBinder _ = Bool
True
tyCoBinderArgFlag :: TyCoBinder -> ArgFlag
tyCoBinderArgFlag :: TyCoBinder -> ArgFlag
tyCoBinderArgFlag (Named (Bndr _ flag :: ArgFlag
flag)) = ArgFlag
flag
tyCoBinderArgFlag (Anon ty :: Type
ty)
| Type -> Bool
isPredTy Type
ty = ArgFlag
Inferred
| Bool
otherwise = ArgFlag
Required
type PredType = Type
type ThetaType = [PredType]
mkTyVarTy :: TyVar -> Type
mkTyVarTy :: Id -> Type
mkTyVarTy v :: Id
v = ASSERT2( isTyVar v, ppr v <+> dcolon <+> ppr (tyVarKind v) )
Id -> Type
TyVarTy Id
v
mkTyVarTys :: [TyVar] -> [Type]
mkTyVarTys :: [Id] -> [Type]
mkTyVarTys = (Id -> Type) -> [Id] -> [Type]
forall a b. (a -> b) -> [a] -> [b]
map Id -> Type
mkTyVarTy
mkTyCoVarTy :: TyCoVar -> Type
mkTyCoVarTy :: Id -> Type
mkTyCoVarTy v :: Id
v
| Id -> Bool
isTyVar Id
v
= Id -> Type
TyVarTy Id
v
| Bool
otherwise
= Coercion -> Type
CoercionTy (Id -> Coercion
CoVarCo Id
v)
mkTyCoVarTys :: [TyCoVar] -> [Type]
mkTyCoVarTys :: [Id] -> [Type]
mkTyCoVarTys = (Id -> Type) -> [Id] -> [Type]
forall a b. (a -> b) -> [a] -> [b]
map Id -> Type
mkTyCoVarTy
infixr 3 `mkFunTy`
mkFunTy :: Type -> Type -> Type
mkFunTy :: Type -> Type -> Type
mkFunTy arg :: Type
arg res :: Type
res = Type -> Type -> Type
FunTy Type
arg Type
res
mkFunTys :: [Type] -> Type -> Type
mkFunTys :: [Type] -> Type -> Type
mkFunTys tys :: [Type]
tys ty :: Type
ty = (Type -> Type -> Type) -> Type -> [Type] -> Type
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr Type -> Type -> Type
mkFunTy Type
ty [Type]
tys
mkTyCoForAllTy :: TyCoVar -> ArgFlag -> Type -> Type
mkTyCoForAllTy :: Id -> ArgFlag -> Type -> Type
mkTyCoForAllTy tv :: Id
tv vis :: ArgFlag
vis ty :: Type
ty
| Id -> Bool
isCoVar Id
tv
, Bool -> Bool
not (Id
tv Id -> VarSet -> Bool
`elemVarSet` Type -> VarSet
tyCoVarsOfType Type
ty)
= ASSERT( vis == Inferred )
Type -> Type -> Type
mkFunTy (Id -> Type
varType Id
tv) Type
ty
| Bool
otherwise
= TyCoVarBinder -> Type -> Type
ForAllTy (Id -> ArgFlag -> TyCoVarBinder
forall var argf. var -> argf -> VarBndr var argf
Bndr Id
tv ArgFlag
vis) Type
ty
mkForAllTy :: TyCoVar -> ArgFlag -> Type -> Type
mkForAllTy :: Id -> ArgFlag -> Type -> Type
mkForAllTy tv :: Id
tv vis :: ArgFlag
vis ty :: Type
ty = TyCoVarBinder -> Type -> Type
ForAllTy (Id -> ArgFlag -> TyCoVarBinder
forall var argf. var -> argf -> VarBndr var argf
Bndr Id
tv ArgFlag
vis) Type
ty
mkForAllTys :: [TyCoVarBinder] -> Type -> Type
mkForAllTys :: [TyCoVarBinder] -> Type -> Type
mkForAllTys tyvars :: [TyCoVarBinder]
tyvars ty :: Type
ty = (TyCoVarBinder -> Type -> Type) -> Type -> [TyCoVarBinder] -> Type
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr TyCoVarBinder -> Type -> Type
ForAllTy Type
ty [TyCoVarBinder]
tyvars
mkTyCoPiTy :: TyCoBinder -> Type -> Type
mkTyCoPiTy :: TyCoBinder -> Type -> Type
mkTyCoPiTy (Anon ty1 :: Type
ty1) ty2 :: Type
ty2 = Type -> Type -> Type
FunTy Type
ty1 Type
ty2
mkTyCoPiTy (Named (Bndr tv :: Id
tv vis :: ArgFlag
vis)) ty :: Type
ty = Id -> ArgFlag -> Type -> Type
mkTyCoForAllTy Id
tv ArgFlag
vis Type
ty
mkPiTy:: TyCoBinder -> Type -> Type
mkPiTy :: TyCoBinder -> Type -> Type
mkPiTy (Anon ty1 :: Type
ty1) ty2 :: Type
ty2 = Type -> Type -> Type
FunTy Type
ty1 Type
ty2
mkPiTy (Named (Bndr tv :: Id
tv vis :: ArgFlag
vis)) ty :: Type
ty = Id -> ArgFlag -> Type -> Type
mkForAllTy Id
tv ArgFlag
vis Type
ty
mkTyCoPiTys :: [TyCoBinder] -> Type -> Type
mkTyCoPiTys :: [TyCoBinder] -> Type -> Type
mkTyCoPiTys tbs :: [TyCoBinder]
tbs ty :: Type
ty = (TyCoBinder -> Type -> Type) -> Type -> [TyCoBinder] -> Type
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr TyCoBinder -> Type -> Type
mkTyCoPiTy Type
ty [TyCoBinder]
tbs
mkPiTys :: [TyCoBinder] -> Type -> Type
mkPiTys :: [TyCoBinder] -> Type -> Type
mkPiTys tbs :: [TyCoBinder]
tbs ty :: Type
ty = (TyCoBinder -> Type -> Type) -> Type -> [TyCoBinder] -> Type
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr TyCoBinder -> Type -> Type
mkPiTy Type
ty [TyCoBinder]
tbs
mkTyConTy :: TyCon -> Type
mkTyConTy :: TyCon -> Type
mkTyConTy tycon :: TyCon
tycon = TyCon -> [Type] -> Type
TyConApp TyCon
tycon []
kindRep :: HasDebugCallStack => Kind -> Type
kindRep :: Type -> Type
kindRep k :: Type
k = case HasDebugCallStack => Type -> Maybe Type
Type -> Maybe Type
kindRep_maybe Type
k of
Just r :: Type
r -> Type
r
Nothing -> String -> SDoc -> Type
forall a. HasCallStack => String -> SDoc -> a
pprPanic "kindRep" (Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
k)
kindRep_maybe :: HasDebugCallStack => Kind -> Maybe Type
kindRep_maybe :: Type -> Maybe Type
kindRep_maybe kind :: Type
kind
| Just kind' :: Type
kind' <- Type -> Maybe Type
coreView Type
kind = HasDebugCallStack => Type -> Maybe Type
Type -> Maybe Type
kindRep_maybe Type
kind'
| TyConApp tc :: TyCon
tc [arg :: Type
arg] <- Type
kind
, TyCon
tc TyCon -> Unique -> Bool
forall a. Uniquable a => a -> Unique -> Bool
`hasKey` Unique
tYPETyConKey = Type -> Maybe Type
forall a. a -> Maybe a
Just Type
arg
| Bool
otherwise = Maybe Type
forall a. Maybe a
Nothing
isLiftedTypeKind :: Kind -> Bool
isLiftedTypeKind :: Type -> Bool
isLiftedTypeKind kind :: Type
kind
= case HasDebugCallStack => Type -> Maybe Type
Type -> Maybe Type
kindRep_maybe Type
kind of
Just rep :: Type
rep -> Type -> Bool
isLiftedRuntimeRep Type
rep
Nothing -> Bool
False
isUnliftedTypeKind :: Kind -> Bool
isUnliftedTypeKind :: Type -> Bool
isUnliftedTypeKind kind :: Type
kind
= case HasDebugCallStack => Type -> Maybe Type
Type -> Maybe Type
kindRep_maybe Type
kind of
Just rep :: Type
rep -> Type -> Bool
isUnliftedRuntimeRep Type
rep
Nothing -> Bool
False
isLiftedRuntimeRep, isUnliftedRuntimeRep :: Type -> Bool
isLiftedRuntimeRep :: Type -> Bool
isLiftedRuntimeRep rep :: Type
rep
| Just rep' :: Type
rep' <- Type -> Maybe Type
coreView Type
rep = Type -> Bool
isLiftedRuntimeRep Type
rep'
| TyConApp rr_tc :: TyCon
rr_tc args :: [Type]
args <- Type
rep
, TyCon
rr_tc TyCon -> Unique -> Bool
forall a. Uniquable a => a -> Unique -> Bool
`hasKey` Unique
liftedRepDataConKey = ASSERT( null args ) True
| Bool
otherwise = Bool
False
isUnliftedRuntimeRep :: Type -> Bool
isUnliftedRuntimeRep rep :: Type
rep
| Just rep' :: Type
rep' <- Type -> Maybe Type
coreView Type
rep = Type -> Bool
isUnliftedRuntimeRep Type
rep'
| TyConApp rr_tc :: TyCon
rr_tc args :: [Type]
args <- Type
rep
, TyCon -> Bool
isUnliftedRuntimeRepTyCon TyCon
rr_tc = ASSERT( null args ) True
| Bool
otherwise = Bool
False
isUnliftedRuntimeRepTyCon :: TyCon -> Bool
isUnliftedRuntimeRepTyCon :: TyCon -> Bool
isUnliftedRuntimeRepTyCon rr_tc :: TyCon
rr_tc
= Unique -> [Unique] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
elem (TyCon -> Unique
forall a. Uniquable a => a -> Unique
getUnique TyCon
rr_tc) [Unique]
unliftedRepDataConKeys
isRuntimeRepTy :: Type -> Bool
isRuntimeRepTy :: Type -> Bool
isRuntimeRepTy ty :: Type
ty | Just ty' :: Type
ty' <- Type -> Maybe Type
coreView Type
ty = Type -> Bool
isRuntimeRepTy Type
ty'
isRuntimeRepTy (TyConApp tc :: TyCon
tc []) = TyCon
tc TyCon -> Unique -> Bool
forall a. Uniquable a => a -> Unique -> Bool
`hasKey` Unique
runtimeRepTyConKey
isRuntimeRepTy _ = Bool
False
isRuntimeRepVar :: TyVar -> Bool
isRuntimeRepVar :: Id -> Bool
isRuntimeRepVar = Type -> Bool
isRuntimeRepTy (Type -> Bool) -> (Id -> Type) -> Id -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Id -> Type
tyVarKind
data Coercion
=
Refl Type
| GRefl Role Type MCoercionN
| TyConAppCo Role TyCon [Coercion]
| AppCo Coercion CoercionN
| ForAllCo TyCoVar KindCoercion Coercion
| FunCo Role Coercion Coercion
| CoVarCo CoVar
| AxiomInstCo (CoAxiom Branched) BranchIndex [Coercion]
| AxiomRuleCo CoAxiomRule [Coercion]
| UnivCo UnivCoProvenance Role Type Type
| SymCo Coercion
| TransCo Coercion Coercion
| NthCo Role Int Coercion
| LRCo LeftOrRight CoercionN
| InstCo Coercion CoercionN
| KindCo Coercion
| SubCo CoercionN
| HoleCo CoercionHole
deriving Typeable Coercion
DataType
Constr
Typeable Coercion =>
(forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Coercion -> c Coercion)
-> (forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Coercion)
-> (Coercion -> Constr)
-> (Coercion -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Coercion))
-> (forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Coercion))
-> ((forall b. Data b => b -> b) -> Coercion -> Coercion)
-> (forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> Coercion -> r)
-> (forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> Coercion -> r)
-> (forall u. (forall d. Data d => d -> u) -> Coercion -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> Coercion -> u)
-> (forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Coercion -> m Coercion)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Coercion -> m Coercion)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Coercion -> m Coercion)
-> Data Coercion
Coercion -> DataType
Coercion -> Constr
(forall b. Data b => b -> b) -> Coercion -> Coercion
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Coercion -> c Coercion
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Coercion
forall a.
Typeable a =>
(forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u. Int -> (forall d. Data d => d -> u) -> Coercion -> u
forall u. (forall d. Data d => d -> u) -> Coercion -> [u]
forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> Coercion -> r
forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> Coercion -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Coercion -> m Coercion
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Coercion -> m Coercion
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Coercion
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Coercion -> c Coercion
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Coercion)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Coercion)
$cHoleCo :: Constr
$cSubCo :: Constr
$cKindCo :: Constr
$cInstCo :: Constr
$cLRCo :: Constr
$cNthCo :: Constr
$cTransCo :: Constr
$cSymCo :: Constr
$cUnivCo :: Constr
$cAxiomRuleCo :: Constr
$cAxiomInstCo :: Constr
$cCoVarCo :: Constr
$cFunCo :: Constr
$cForAllCo :: Constr
$cAppCo :: Constr
$cTyConAppCo :: Constr
$cGRefl :: Constr
$cRefl :: Constr
$tCoercion :: DataType
gmapMo :: (forall d. Data d => d -> m d) -> Coercion -> m Coercion
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Coercion -> m Coercion
gmapMp :: (forall d. Data d => d -> m d) -> Coercion -> m Coercion
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Coercion -> m Coercion
gmapM :: (forall d. Data d => d -> m d) -> Coercion -> m Coercion
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Coercion -> m Coercion
gmapQi :: Int -> (forall d. Data d => d -> u) -> Coercion -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Coercion -> u
gmapQ :: (forall d. Data d => d -> u) -> Coercion -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> Coercion -> [u]
gmapQr :: (r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> Coercion -> r
$cgmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> Coercion -> r
gmapQl :: (r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> Coercion -> r
$cgmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> Coercion -> r
gmapT :: (forall b. Data b => b -> b) -> Coercion -> Coercion
$cgmapT :: (forall b. Data b => b -> b) -> Coercion -> Coercion
dataCast2 :: (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Coercion)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Coercion)
dataCast1 :: (forall d. Data d => c (t d)) -> Maybe (c Coercion)
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Coercion)
dataTypeOf :: Coercion -> DataType
$cdataTypeOf :: Coercion -> DataType
toConstr :: Coercion -> Constr
$ctoConstr :: Coercion -> Constr
gunfold :: (forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Coercion
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Coercion
gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Coercion -> c Coercion
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Coercion -> c Coercion
$cp1Data :: Typeable Coercion
Data.Data
type CoercionN = Coercion
type CoercionR = Coercion
type CoercionP = Coercion
type KindCoercion = CoercionN
data MCoercion
= MRefl
| MCo Coercion
deriving Typeable MCoercion
DataType
Constr
Typeable MCoercion =>
(forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> MCoercion -> c MCoercion)
-> (forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c MCoercion)
-> (MCoercion -> Constr)
-> (MCoercion -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c MCoercion))
-> (forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c MCoercion))
-> ((forall b. Data b => b -> b) -> MCoercion -> MCoercion)
-> (forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> MCoercion -> r)
-> (forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> MCoercion -> r)
-> (forall u. (forall d. Data d => d -> u) -> MCoercion -> [u])
-> (forall u.
Int -> (forall d. Data d => d -> u) -> MCoercion -> u)
-> (forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> MCoercion -> m MCoercion)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> MCoercion -> m MCoercion)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> MCoercion -> m MCoercion)
-> Data MCoercion
MCoercion -> DataType
MCoercion -> Constr
(forall b. Data b => b -> b) -> MCoercion -> MCoercion
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> MCoercion -> c MCoercion
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c MCoercion
forall a.
Typeable a =>
(forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u. Int -> (forall d. Data d => d -> u) -> MCoercion -> u
forall u. (forall d. Data d => d -> u) -> MCoercion -> [u]
forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> MCoercion -> r
forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> MCoercion -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> MCoercion -> m MCoercion
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> MCoercion -> m MCoercion
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c MCoercion
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> MCoercion -> c MCoercion
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c MCoercion)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c MCoercion)
$cMCo :: Constr
$cMRefl :: Constr
$tMCoercion :: DataType
gmapMo :: (forall d. Data d => d -> m d) -> MCoercion -> m MCoercion
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> MCoercion -> m MCoercion
gmapMp :: (forall d. Data d => d -> m d) -> MCoercion -> m MCoercion
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> MCoercion -> m MCoercion
gmapM :: (forall d. Data d => d -> m d) -> MCoercion -> m MCoercion
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> MCoercion -> m MCoercion
gmapQi :: Int -> (forall d. Data d => d -> u) -> MCoercion -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> MCoercion -> u
gmapQ :: (forall d. Data d => d -> u) -> MCoercion -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> MCoercion -> [u]
gmapQr :: (r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> MCoercion -> r
$cgmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> MCoercion -> r
gmapQl :: (r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> MCoercion -> r
$cgmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> MCoercion -> r
gmapT :: (forall b. Data b => b -> b) -> MCoercion -> MCoercion
$cgmapT :: (forall b. Data b => b -> b) -> MCoercion -> MCoercion
dataCast2 :: (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c MCoercion)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c MCoercion)
dataCast1 :: (forall d. Data d => c (t d)) -> Maybe (c MCoercion)
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c MCoercion)
dataTypeOf :: MCoercion -> DataType
$cdataTypeOf :: MCoercion -> DataType
toConstr :: MCoercion -> Constr
$ctoConstr :: MCoercion -> Constr
gunfold :: (forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c MCoercion
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c MCoercion
gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> MCoercion -> c MCoercion
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> MCoercion -> c MCoercion
$cp1Data :: Typeable MCoercion
Data.Data
type MCoercionR = MCoercion
type MCoercionN = MCoercion
instance Outputable MCoercion where
ppr :: MCoercion -> SDoc
ppr MRefl = String -> SDoc
text "MRefl"
ppr (MCo co :: Coercion
co) = String -> SDoc
text "MCo" SDoc -> SDoc -> SDoc
<+> Coercion -> SDoc
forall a. Outputable a => a -> SDoc
ppr Coercion
co
data UnivCoProvenance
= UnsafeCoerceProv
| PhantomProv KindCoercion
| ProofIrrelProv KindCoercion
| PluginProv String
deriving Typeable UnivCoProvenance
DataType
Constr
Typeable UnivCoProvenance =>
(forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> UnivCoProvenance -> c UnivCoProvenance)
-> (forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c UnivCoProvenance)
-> (UnivCoProvenance -> Constr)
-> (UnivCoProvenance -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c UnivCoProvenance))
-> (forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c UnivCoProvenance))
-> ((forall b. Data b => b -> b)
-> UnivCoProvenance -> UnivCoProvenance)
-> (forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> UnivCoProvenance -> r)
-> (forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> UnivCoProvenance -> r)
-> (forall u.
(forall d. Data d => d -> u) -> UnivCoProvenance -> [u])
-> (forall u.
Int -> (forall d. Data d => d -> u) -> UnivCoProvenance -> u)
-> (forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d)
-> UnivCoProvenance -> m UnivCoProvenance)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d)
-> UnivCoProvenance -> m UnivCoProvenance)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d)
-> UnivCoProvenance -> m UnivCoProvenance)
-> Data UnivCoProvenance
UnivCoProvenance -> DataType
UnivCoProvenance -> Constr
(forall b. Data b => b -> b)
-> UnivCoProvenance -> UnivCoProvenance
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> UnivCoProvenance -> c UnivCoProvenance
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c UnivCoProvenance
forall a.
Typeable a =>
(forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u.
Int -> (forall d. Data d => d -> u) -> UnivCoProvenance -> u
forall u. (forall d. Data d => d -> u) -> UnivCoProvenance -> [u]
forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> UnivCoProvenance -> r
forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> UnivCoProvenance -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d)
-> UnivCoProvenance -> m UnivCoProvenance
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d)
-> UnivCoProvenance -> m UnivCoProvenance
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c UnivCoProvenance
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> UnivCoProvenance -> c UnivCoProvenance
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c UnivCoProvenance)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c UnivCoProvenance)
$cPluginProv :: Constr
$cProofIrrelProv :: Constr
$cPhantomProv :: Constr
$cUnsafeCoerceProv :: Constr
$tUnivCoProvenance :: DataType
gmapMo :: (forall d. Data d => d -> m d)
-> UnivCoProvenance -> m UnivCoProvenance
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d)
-> UnivCoProvenance -> m UnivCoProvenance
gmapMp :: (forall d. Data d => d -> m d)
-> UnivCoProvenance -> m UnivCoProvenance
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d)
-> UnivCoProvenance -> m UnivCoProvenance
gmapM :: (forall d. Data d => d -> m d)
-> UnivCoProvenance -> m UnivCoProvenance
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d)
-> UnivCoProvenance -> m UnivCoProvenance
gmapQi :: Int -> (forall d. Data d => d -> u) -> UnivCoProvenance -> u
$cgmapQi :: forall u.
Int -> (forall d. Data d => d -> u) -> UnivCoProvenance -> u
gmapQ :: (forall d. Data d => d -> u) -> UnivCoProvenance -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> UnivCoProvenance -> [u]
gmapQr :: (r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> UnivCoProvenance -> r
$cgmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> UnivCoProvenance -> r
gmapQl :: (r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> UnivCoProvenance -> r
$cgmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> UnivCoProvenance -> r
gmapT :: (forall b. Data b => b -> b)
-> UnivCoProvenance -> UnivCoProvenance
$cgmapT :: (forall b. Data b => b -> b)
-> UnivCoProvenance -> UnivCoProvenance
dataCast2 :: (forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c UnivCoProvenance)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c UnivCoProvenance)
dataCast1 :: (forall d. Data d => c (t d)) -> Maybe (c UnivCoProvenance)
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c UnivCoProvenance)
dataTypeOf :: UnivCoProvenance -> DataType
$cdataTypeOf :: UnivCoProvenance -> DataType
toConstr :: UnivCoProvenance -> Constr
$ctoConstr :: UnivCoProvenance -> Constr
gunfold :: (forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c UnivCoProvenance
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c UnivCoProvenance
gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> UnivCoProvenance -> c UnivCoProvenance
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> UnivCoProvenance -> c UnivCoProvenance
$cp1Data :: Typeable UnivCoProvenance
Data.Data
instance Outputable UnivCoProvenance where
ppr :: UnivCoProvenance -> SDoc
ppr UnsafeCoerceProv = String -> SDoc
text "(unsafeCoerce#)"
ppr (PhantomProv _) = String -> SDoc
text "(phantom)"
ppr (ProofIrrelProv _) = String -> SDoc
text "(proof irrel.)"
ppr (PluginProv str :: String
str) = SDoc -> SDoc
parens (String -> SDoc
text "plugin" SDoc -> SDoc -> SDoc
<+> SDoc -> SDoc
brackets (String -> SDoc
text String
str))
data CoercionHole
= CoercionHole { CoercionHole -> Id
ch_co_var :: CoVar
, CoercionHole -> IORef (Maybe Coercion)
ch_ref :: IORef (Maybe Coercion)
}
coHoleCoVar :: CoercionHole -> CoVar
coHoleCoVar :: CoercionHole -> Id
coHoleCoVar = CoercionHole -> Id
ch_co_var
setCoHoleCoVar :: CoercionHole -> CoVar -> CoercionHole
setCoHoleCoVar :: CoercionHole -> Id -> CoercionHole
setCoHoleCoVar h :: CoercionHole
h cv :: Id
cv = CoercionHole
h { ch_co_var :: Id
ch_co_var = Id
cv }
instance Data.Data CoercionHole where
toConstr :: CoercionHole -> Constr
toConstr _ = String -> Constr
abstractConstr "CoercionHole"
gunfold :: (forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c CoercionHole
gunfold _ _ = String -> Constr -> c CoercionHole
forall a. HasCallStack => String -> a
error "gunfold"
dataTypeOf :: CoercionHole -> DataType
dataTypeOf _ = String -> DataType
mkNoRepType "CoercionHole"
instance Outputable CoercionHole where
ppr :: CoercionHole -> SDoc
ppr (CoercionHole { ch_co_var :: CoercionHole -> Id
ch_co_var = Id
cv }) = SDoc -> SDoc
braces (Id -> SDoc
forall a. Outputable a => a -> SDoc
ppr Id
cv)
tyCoVarsOfType :: Type -> TyCoVarSet
tyCoVarsOfType :: Type -> VarSet
tyCoVarsOfType ty :: Type
ty = Type -> VarSet -> VarSet -> VarSet
ty_co_vars_of_type Type
ty VarSet
emptyVarSet VarSet
emptyVarSet
tyCoVarsOfTypes :: [Type] -> TyCoVarSet
tyCoVarsOfTypes :: [Type] -> VarSet
tyCoVarsOfTypes tys :: [Type]
tys = [Type] -> VarSet -> VarSet -> VarSet
ty_co_vars_of_types [Type]
tys VarSet
emptyVarSet VarSet
emptyVarSet
ty_co_vars_of_type :: Type -> TyCoVarSet -> TyCoVarSet -> TyCoVarSet
ty_co_vars_of_type :: Type -> VarSet -> VarSet -> VarSet
ty_co_vars_of_type (TyVarTy v :: Id
v) is :: VarSet
is acc :: VarSet
acc
| Id
v Id -> VarSet -> Bool
`elemVarSet` VarSet
is = VarSet
acc
| Id
v Id -> VarSet -> Bool
`elemVarSet` VarSet
acc = VarSet
acc
| Bool
otherwise = Type -> VarSet -> VarSet -> VarSet
ty_co_vars_of_type (Id -> Type
tyVarKind Id
v)
VarSet
emptyVarSet
(VarSet -> Id -> VarSet
extendVarSet VarSet
acc Id
v)
ty_co_vars_of_type (TyConApp _ tys :: [Type]
tys) is :: VarSet
is acc :: VarSet
acc = [Type] -> VarSet -> VarSet -> VarSet
ty_co_vars_of_types [Type]
tys VarSet
is VarSet
acc
ty_co_vars_of_type (LitTy {}) _ acc :: VarSet
acc = VarSet
acc
ty_co_vars_of_type (AppTy fun :: Type
fun arg :: Type
arg) is :: VarSet
is acc :: VarSet
acc = Type -> VarSet -> VarSet -> VarSet
ty_co_vars_of_type Type
fun VarSet
is (Type -> VarSet -> VarSet -> VarSet
ty_co_vars_of_type Type
arg VarSet
is VarSet
acc)
ty_co_vars_of_type (FunTy arg :: Type
arg res :: Type
res) is :: VarSet
is acc :: VarSet
acc = Type -> VarSet -> VarSet -> VarSet
ty_co_vars_of_type Type
arg VarSet
is (Type -> VarSet -> VarSet -> VarSet
ty_co_vars_of_type Type
res VarSet
is VarSet
acc)
ty_co_vars_of_type (ForAllTy (Bndr tv :: Id
tv _) ty :: Type
ty) is :: VarSet
is acc :: VarSet
acc = Type -> VarSet -> VarSet -> VarSet
ty_co_vars_of_type (Id -> Type
varType Id
tv) VarSet
is (VarSet -> VarSet) -> VarSet -> VarSet
forall a b. (a -> b) -> a -> b
$
Type -> VarSet -> VarSet -> VarSet
ty_co_vars_of_type Type
ty (VarSet -> Id -> VarSet
extendVarSet VarSet
is Id
tv) VarSet
acc
ty_co_vars_of_type (CastTy ty :: Type
ty co :: Coercion
co) is :: VarSet
is acc :: VarSet
acc = Type -> VarSet -> VarSet -> VarSet
ty_co_vars_of_type Type
ty VarSet
is (Coercion -> VarSet -> VarSet -> VarSet
ty_co_vars_of_co Coercion
co VarSet
is VarSet
acc)
ty_co_vars_of_type (CoercionTy co :: Coercion
co) is :: VarSet
is acc :: VarSet
acc = Coercion -> VarSet -> VarSet -> VarSet
ty_co_vars_of_co Coercion
co VarSet
is VarSet
acc
ty_co_vars_of_types :: [Type] -> TyCoVarSet -> TyCoVarSet -> TyCoVarSet
ty_co_vars_of_types :: [Type] -> VarSet -> VarSet -> VarSet
ty_co_vars_of_types [] _ acc :: VarSet
acc = VarSet
acc
ty_co_vars_of_types (ty :: Type
ty:tys :: [Type]
tys) is :: VarSet
is acc :: VarSet
acc = Type -> VarSet -> VarSet -> VarSet
ty_co_vars_of_type Type
ty VarSet
is ([Type] -> VarSet -> VarSet -> VarSet
ty_co_vars_of_types [Type]
tys VarSet
is VarSet
acc)
tyCoVarsOfCo :: Coercion -> TyCoVarSet
tyCoVarsOfCo :: Coercion -> VarSet
tyCoVarsOfCo co :: Coercion
co = Coercion -> VarSet -> VarSet -> VarSet
ty_co_vars_of_co Coercion
co VarSet
emptyVarSet VarSet
emptyVarSet
tyCoVarsOfCos :: [Coercion] -> TyCoVarSet
tyCoVarsOfCos :: [Coercion] -> VarSet
tyCoVarsOfCos cos :: [Coercion]
cos = [Coercion] -> VarSet -> VarSet -> VarSet
ty_co_vars_of_cos [Coercion]
cos VarSet
emptyVarSet VarSet
emptyVarSet
ty_co_vars_of_co :: Coercion -> TyCoVarSet -> TyCoVarSet -> TyCoVarSet
ty_co_vars_of_co :: Coercion -> VarSet -> VarSet -> VarSet
ty_co_vars_of_co (Refl ty :: Type
ty) is :: VarSet
is acc :: VarSet
acc = Type -> VarSet -> VarSet -> VarSet
ty_co_vars_of_type Type
ty VarSet
is VarSet
acc
ty_co_vars_of_co (GRefl _ ty :: Type
ty mco :: MCoercion
mco) is :: VarSet
is acc :: VarSet
acc = Type -> VarSet -> VarSet -> VarSet
ty_co_vars_of_type Type
ty VarSet
is (VarSet -> VarSet) -> VarSet -> VarSet
forall a b. (a -> b) -> a -> b
$
MCoercion -> VarSet -> VarSet -> VarSet
ty_co_vars_of_mco MCoercion
mco VarSet
is VarSet
acc
ty_co_vars_of_co (TyConAppCo _ _ cos :: [Coercion]
cos) is :: VarSet
is acc :: VarSet
acc = [Coercion] -> VarSet -> VarSet -> VarSet
ty_co_vars_of_cos [Coercion]
cos VarSet
is VarSet
acc
ty_co_vars_of_co (AppCo co :: Coercion
co arg :: Coercion
arg) is :: VarSet
is acc :: VarSet
acc = Coercion -> VarSet -> VarSet -> VarSet
ty_co_vars_of_co Coercion
co VarSet
is (VarSet -> VarSet) -> VarSet -> VarSet
forall a b. (a -> b) -> a -> b
$
Coercion -> VarSet -> VarSet -> VarSet
ty_co_vars_of_co Coercion
arg VarSet
is VarSet
acc
ty_co_vars_of_co (ForAllCo tv :: Id
tv kind_co :: Coercion
kind_co co :: Coercion
co) is :: VarSet
is acc :: VarSet
acc = Coercion -> VarSet -> VarSet -> VarSet
ty_co_vars_of_co Coercion
kind_co VarSet
is (VarSet -> VarSet) -> VarSet -> VarSet
forall a b. (a -> b) -> a -> b
$
Coercion -> VarSet -> VarSet -> VarSet
ty_co_vars_of_co Coercion
co (VarSet -> Id -> VarSet
extendVarSet VarSet
is Id
tv) VarSet
acc
ty_co_vars_of_co (FunCo _ co1 :: Coercion
co1 co2 :: Coercion
co2) is :: VarSet
is acc :: VarSet
acc = Coercion -> VarSet -> VarSet -> VarSet
ty_co_vars_of_co Coercion
co1 VarSet
is (VarSet -> VarSet) -> VarSet -> VarSet
forall a b. (a -> b) -> a -> b
$
Coercion -> VarSet -> VarSet -> VarSet
ty_co_vars_of_co Coercion
co2 VarSet
is VarSet
acc
ty_co_vars_of_co (CoVarCo v :: Id
v) is :: VarSet
is acc :: VarSet
acc = Id -> VarSet -> VarSet -> VarSet
ty_co_vars_of_co_var Id
v VarSet
is VarSet
acc
ty_co_vars_of_co (HoleCo h :: CoercionHole
h) is :: VarSet
is acc :: VarSet
acc = Id -> VarSet -> VarSet -> VarSet
ty_co_vars_of_co_var (CoercionHole -> Id
coHoleCoVar CoercionHole
h) VarSet
is VarSet
acc
ty_co_vars_of_co (AxiomInstCo _ _ cos :: [Coercion]
cos) is :: VarSet
is acc :: VarSet
acc = [Coercion] -> VarSet -> VarSet -> VarSet
ty_co_vars_of_cos [Coercion]
cos VarSet
is VarSet
acc
ty_co_vars_of_co (UnivCo p :: UnivCoProvenance
p _ t1 :: Type
t1 t2 :: Type
t2) is :: VarSet
is acc :: VarSet
acc = UnivCoProvenance -> VarSet -> VarSet -> VarSet
ty_co_vars_of_prov UnivCoProvenance
p VarSet
is (VarSet -> VarSet) -> VarSet -> VarSet
forall a b. (a -> b) -> a -> b
$
Type -> VarSet -> VarSet -> VarSet
ty_co_vars_of_type Type
t1 VarSet
is (VarSet -> VarSet) -> VarSet -> VarSet
forall a b. (a -> b) -> a -> b
$
Type -> VarSet -> VarSet -> VarSet
ty_co_vars_of_type Type
t2 VarSet
is VarSet
acc
ty_co_vars_of_co (SymCo co :: Coercion
co) is :: VarSet
is acc :: VarSet
acc = Coercion -> VarSet -> VarSet -> VarSet
ty_co_vars_of_co Coercion
co VarSet
is VarSet
acc
ty_co_vars_of_co (TransCo co1 :: Coercion
co1 co2 :: Coercion
co2) is :: VarSet
is acc :: VarSet
acc = Coercion -> VarSet -> VarSet -> VarSet
ty_co_vars_of_co Coercion
co1 VarSet
is (VarSet -> VarSet) -> VarSet -> VarSet
forall a b. (a -> b) -> a -> b
$
Coercion -> VarSet -> VarSet -> VarSet
ty_co_vars_of_co Coercion
co2 VarSet
is VarSet
acc
ty_co_vars_of_co (NthCo _ _ co :: Coercion
co) is :: VarSet
is acc :: VarSet
acc = Coercion -> VarSet -> VarSet -> VarSet
ty_co_vars_of_co Coercion
co VarSet
is VarSet
acc
ty_co_vars_of_co (LRCo _ co :: Coercion
co) is :: VarSet
is acc :: VarSet
acc = Coercion -> VarSet -> VarSet -> VarSet
ty_co_vars_of_co Coercion
co VarSet
is VarSet
acc
ty_co_vars_of_co (InstCo co :: Coercion
co arg :: Coercion
arg) is :: VarSet
is acc :: VarSet
acc = Coercion -> VarSet -> VarSet -> VarSet
ty_co_vars_of_co Coercion
co VarSet
is (VarSet -> VarSet) -> VarSet -> VarSet
forall a b. (a -> b) -> a -> b
$
Coercion -> VarSet -> VarSet -> VarSet
ty_co_vars_of_co Coercion
arg VarSet
is VarSet
acc
ty_co_vars_of_co (KindCo co :: Coercion
co) is :: VarSet
is acc :: VarSet
acc = Coercion -> VarSet -> VarSet -> VarSet
ty_co_vars_of_co Coercion
co VarSet
is VarSet
acc
ty_co_vars_of_co (SubCo co :: Coercion
co) is :: VarSet
is acc :: VarSet
acc = Coercion -> VarSet -> VarSet -> VarSet
ty_co_vars_of_co Coercion
co VarSet
is VarSet
acc
ty_co_vars_of_co (AxiomRuleCo _ cs :: [Coercion]
cs) is :: VarSet
is acc :: VarSet
acc = [Coercion] -> VarSet -> VarSet -> VarSet
ty_co_vars_of_cos [Coercion]
cs VarSet
is VarSet
acc
ty_co_vars_of_mco :: MCoercion -> TyCoVarSet -> TyCoVarSet -> TyCoVarSet
ty_co_vars_of_mco :: MCoercion -> VarSet -> VarSet -> VarSet
ty_co_vars_of_mco MRefl _is :: VarSet
_is acc :: VarSet
acc = VarSet
acc
ty_co_vars_of_mco (MCo co :: Coercion
co) is :: VarSet
is acc :: VarSet
acc = Coercion -> VarSet -> VarSet -> VarSet
ty_co_vars_of_co Coercion
co VarSet
is VarSet
acc
ty_co_vars_of_co_var :: CoVar -> TyCoVarSet -> TyCoVarSet -> TyCoVarSet
ty_co_vars_of_co_var :: Id -> VarSet -> VarSet -> VarSet
ty_co_vars_of_co_var v :: Id
v is :: VarSet
is acc :: VarSet
acc
| Id
v Id -> VarSet -> Bool
`elemVarSet` VarSet
is = VarSet
acc
| Id
v Id -> VarSet -> Bool
`elemVarSet` VarSet
acc = VarSet
acc
| Bool
otherwise = Type -> VarSet -> VarSet -> VarSet
ty_co_vars_of_type (Id -> Type
varType Id
v)
VarSet
emptyVarSet
(VarSet -> Id -> VarSet
extendVarSet VarSet
acc Id
v)
ty_co_vars_of_cos :: [Coercion] -> TyCoVarSet -> TyCoVarSet -> TyCoVarSet
ty_co_vars_of_cos :: [Coercion] -> VarSet -> VarSet -> VarSet
ty_co_vars_of_cos [] _ acc :: VarSet
acc = VarSet
acc
ty_co_vars_of_cos (co :: Coercion
co:cos :: [Coercion]
cos) is :: VarSet
is acc :: VarSet
acc = Coercion -> VarSet -> VarSet -> VarSet
ty_co_vars_of_co Coercion
co VarSet
is ([Coercion] -> VarSet -> VarSet -> VarSet
ty_co_vars_of_cos [Coercion]
cos VarSet
is VarSet
acc)
tyCoVarsOfProv :: UnivCoProvenance -> TyCoVarSet
tyCoVarsOfProv :: UnivCoProvenance -> VarSet
tyCoVarsOfProv prov :: UnivCoProvenance
prov = UnivCoProvenance -> VarSet -> VarSet -> VarSet
ty_co_vars_of_prov UnivCoProvenance
prov VarSet
emptyVarSet VarSet
emptyVarSet
ty_co_vars_of_prov :: UnivCoProvenance -> TyCoVarSet -> TyCoVarSet -> TyCoVarSet
ty_co_vars_of_prov :: UnivCoProvenance -> VarSet -> VarSet -> VarSet
ty_co_vars_of_prov (PhantomProv co :: Coercion
co) is :: VarSet
is acc :: VarSet
acc = Coercion -> VarSet -> VarSet -> VarSet
ty_co_vars_of_co Coercion
co VarSet
is VarSet
acc
ty_co_vars_of_prov (ProofIrrelProv co :: Coercion
co) is :: VarSet
is acc :: VarSet
acc = Coercion -> VarSet -> VarSet -> VarSet
ty_co_vars_of_co Coercion
co VarSet
is VarSet
acc
ty_co_vars_of_prov UnsafeCoerceProv _ acc :: VarSet
acc = VarSet
acc
ty_co_vars_of_prov (PluginProv _) _ acc :: VarSet
acc = VarSet
acc
mkTyCoInScopeSet :: [Type] -> [Coercion] -> InScopeSet
mkTyCoInScopeSet :: [Type] -> [Coercion] -> InScopeSet
mkTyCoInScopeSet tys :: [Type]
tys cos :: [Coercion]
cos
= VarSet -> InScopeSet
mkInScopeSet ([Type] -> VarSet -> VarSet -> VarSet
ty_co_vars_of_types [Type]
tys VarSet
emptyVarSet (VarSet -> VarSet) -> VarSet -> VarSet
forall a b. (a -> b) -> a -> b
$
[Coercion] -> VarSet -> VarSet -> VarSet
ty_co_vars_of_cos [Coercion]
cos VarSet
emptyVarSet VarSet
emptyVarSet)
tyCoVarsOfTypeDSet :: Type -> DTyCoVarSet
tyCoVarsOfTypeDSet :: Type -> DTyCoVarSet
tyCoVarsOfTypeDSet ty :: Type
ty = FV -> DTyCoVarSet
fvDVarSet (FV -> DTyCoVarSet) -> FV -> DTyCoVarSet
forall a b. (a -> b) -> a -> b
$ Type -> FV
tyCoFVsOfType Type
ty
tyCoVarsOfTypeList :: Type -> [TyCoVar]
tyCoVarsOfTypeList :: Type -> [Id]
tyCoVarsOfTypeList ty :: Type
ty = FV -> [Id]
fvVarList (FV -> [Id]) -> FV -> [Id]
forall a b. (a -> b) -> a -> b
$ Type -> FV
tyCoFVsOfType Type
ty
tyCoVarsOfTypesSet :: TyVarEnv Type -> TyCoVarSet
tyCoVarsOfTypesSet :: TyVarEnv Type -> VarSet
tyCoVarsOfTypesSet tys :: TyVarEnv Type
tys = [Type] -> VarSet
tyCoVarsOfTypes ([Type] -> VarSet) -> [Type] -> VarSet
forall a b. (a -> b) -> a -> b
$ TyVarEnv Type -> [Type]
forall elt. UniqFM elt -> [elt]
nonDetEltsUFM TyVarEnv Type
tys
tyCoVarsOfTypesDSet :: [Type] -> DTyCoVarSet
tyCoVarsOfTypesDSet :: [Type] -> DTyCoVarSet
tyCoVarsOfTypesDSet tys :: [Type]
tys = FV -> DTyCoVarSet
fvDVarSet (FV -> DTyCoVarSet) -> FV -> DTyCoVarSet
forall a b. (a -> b) -> a -> b
$ [Type] -> FV
tyCoFVsOfTypes [Type]
tys
tyCoVarsOfTypesList :: [Type] -> [TyCoVar]
tyCoVarsOfTypesList :: [Type] -> [Id]
tyCoVarsOfTypesList tys :: [Type]
tys = FV -> [Id]
fvVarList (FV -> [Id]) -> FV -> [Id]
forall a b. (a -> b) -> a -> b
$ [Type] -> FV
tyCoFVsOfTypes [Type]
tys
tyCoFVsOfType :: Type -> FV
tyCoFVsOfType :: Type -> FV
tyCoFVsOfType (TyVarTy v :: Id
v) f :: Id -> Bool
f bound_vars :: VarSet
bound_vars (acc_list :: [Id]
acc_list, acc_set :: VarSet
acc_set)
| Bool -> Bool
not (Id -> Bool
f Id
v) = ([Id]
acc_list, VarSet
acc_set)
| Id
v Id -> VarSet -> Bool
`elemVarSet` VarSet
bound_vars = ([Id]
acc_list, VarSet
acc_set)
| Id
v Id -> VarSet -> Bool
`elemVarSet` VarSet
acc_set = ([Id]
acc_list, VarSet
acc_set)
| Bool
otherwise = Type -> FV
tyCoFVsOfType (Id -> Type
tyVarKind Id
v) Id -> Bool
f
VarSet
emptyVarSet
(Id
vId -> [Id] -> [Id]
forall a. a -> [a] -> [a]
:[Id]
acc_list, VarSet -> Id -> VarSet
extendVarSet VarSet
acc_set Id
v)
tyCoFVsOfType (TyConApp _ tys :: [Type]
tys) f :: Id -> Bool
f bound_vars :: VarSet
bound_vars acc :: ([Id], VarSet)
acc = [Type] -> FV
tyCoFVsOfTypes [Type]
tys Id -> Bool
f VarSet
bound_vars ([Id], VarSet)
acc
tyCoFVsOfType (LitTy {}) f :: Id -> Bool
f bound_vars :: VarSet
bound_vars acc :: ([Id], VarSet)
acc = FV
emptyFV Id -> Bool
f VarSet
bound_vars ([Id], VarSet)
acc
tyCoFVsOfType (AppTy fun :: Type
fun arg :: Type
arg) f :: Id -> Bool
f bound_vars :: VarSet
bound_vars acc :: ([Id], VarSet)
acc = (Type -> FV
tyCoFVsOfType Type
fun FV -> FV -> FV
`unionFV` Type -> FV
tyCoFVsOfType Type
arg) Id -> Bool
f VarSet
bound_vars ([Id], VarSet)
acc
tyCoFVsOfType (FunTy arg :: Type
arg res :: Type
res) f :: Id -> Bool
f bound_vars :: VarSet
bound_vars acc :: ([Id], VarSet)
acc = (Type -> FV
tyCoFVsOfType Type
arg FV -> FV -> FV
`unionFV` Type -> FV
tyCoFVsOfType Type
res) Id -> Bool
f VarSet
bound_vars ([Id], VarSet)
acc
tyCoFVsOfType (ForAllTy bndr :: TyCoVarBinder
bndr ty :: Type
ty) f :: Id -> Bool
f bound_vars :: VarSet
bound_vars acc :: ([Id], VarSet)
acc = TyCoVarBinder -> FV -> FV
tyCoFVsBndr TyCoVarBinder
bndr (Type -> FV
tyCoFVsOfType Type
ty) Id -> Bool
f VarSet
bound_vars ([Id], VarSet)
acc
tyCoFVsOfType (CastTy ty :: Type
ty co :: Coercion
co) f :: Id -> Bool
f bound_vars :: VarSet
bound_vars acc :: ([Id], VarSet)
acc = (Type -> FV
tyCoFVsOfType Type
ty FV -> FV -> FV
`unionFV` Coercion -> FV
tyCoFVsOfCo Coercion
co) Id -> Bool
f VarSet
bound_vars ([Id], VarSet)
acc
tyCoFVsOfType (CoercionTy co :: Coercion
co) f :: Id -> Bool
f bound_vars :: VarSet
bound_vars acc :: ([Id], VarSet)
acc = Coercion -> FV
tyCoFVsOfCo Coercion
co Id -> Bool
f VarSet
bound_vars ([Id], VarSet)
acc
tyCoFVsBndr :: TyCoVarBinder -> FV -> FV
tyCoFVsBndr :: TyCoVarBinder -> FV -> FV
tyCoFVsBndr (Bndr tv :: Id
tv _) fvs :: FV
fvs = Id -> FV -> FV
tyCoFVsVarBndr Id
tv FV
fvs
tyCoFVsVarBndrs :: [Var] -> FV -> FV
tyCoFVsVarBndrs :: [Id] -> FV -> FV
tyCoFVsVarBndrs vars :: [Id]
vars fvs :: FV
fvs = (Id -> FV -> FV) -> FV -> [Id] -> FV
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr Id -> FV -> FV
tyCoFVsVarBndr FV
fvs [Id]
vars
tyCoFVsVarBndr :: Var -> FV -> FV
tyCoFVsVarBndr :: Id -> FV -> FV
tyCoFVsVarBndr var :: Id
var fvs :: FV
fvs
= Type -> FV
tyCoFVsOfType (Id -> Type
varType Id
var)
FV -> FV -> FV
`unionFV` Id -> FV -> FV
delFV Id
var FV
fvs
tyCoFVsOfTypes :: [Type] -> FV
tyCoFVsOfTypes :: [Type] -> FV
tyCoFVsOfTypes (ty :: Type
ty:tys :: [Type]
tys) fv_cand :: Id -> Bool
fv_cand in_scope :: VarSet
in_scope acc :: ([Id], VarSet)
acc = (Type -> FV
tyCoFVsOfType Type
ty FV -> FV -> FV
`unionFV` [Type] -> FV
tyCoFVsOfTypes [Type]
tys) Id -> Bool
fv_cand VarSet
in_scope ([Id], VarSet)
acc
tyCoFVsOfTypes [] fv_cand :: Id -> Bool
fv_cand in_scope :: VarSet
in_scope acc :: ([Id], VarSet)
acc = FV
emptyFV Id -> Bool
fv_cand VarSet
in_scope ([Id], VarSet)
acc
tyCoVarsOfCoDSet :: Coercion -> DTyCoVarSet
tyCoVarsOfCoDSet :: Coercion -> DTyCoVarSet
tyCoVarsOfCoDSet co :: Coercion
co = FV -> DTyCoVarSet
fvDVarSet (FV -> DTyCoVarSet) -> FV -> DTyCoVarSet
forall a b. (a -> b) -> a -> b
$ Coercion -> FV
tyCoFVsOfCo Coercion
co
tyCoVarsOfCoList :: Coercion -> [TyCoVar]
tyCoVarsOfCoList :: Coercion -> [Id]
tyCoVarsOfCoList co :: Coercion
co = FV -> [Id]
fvVarList (FV -> [Id]) -> FV -> [Id]
forall a b. (a -> b) -> a -> b
$ Coercion -> FV
tyCoFVsOfCo Coercion
co
tyCoFVsOfMCo :: MCoercion -> FV
tyCoFVsOfMCo :: MCoercion -> FV
tyCoFVsOfMCo MRefl = FV
emptyFV
tyCoFVsOfMCo (MCo co :: Coercion
co) = Coercion -> FV
tyCoFVsOfCo Coercion
co
tyCoVarsOfCosSet :: CoVarEnv Coercion -> TyCoVarSet
tyCoVarsOfCosSet :: CoVarEnv Coercion -> VarSet
tyCoVarsOfCosSet cos :: CoVarEnv Coercion
cos = [Coercion] -> VarSet
tyCoVarsOfCos ([Coercion] -> VarSet) -> [Coercion] -> VarSet
forall a b. (a -> b) -> a -> b
$ CoVarEnv Coercion -> [Coercion]
forall elt. UniqFM elt -> [elt]
nonDetEltsUFM CoVarEnv Coercion
cos
tyCoFVsOfCo :: Coercion -> FV
tyCoFVsOfCo :: Coercion -> FV
tyCoFVsOfCo (Refl ty :: Type
ty) fv_cand :: Id -> Bool
fv_cand in_scope :: VarSet
in_scope acc :: ([Id], VarSet)
acc
= Type -> FV
tyCoFVsOfType Type
ty Id -> Bool
fv_cand VarSet
in_scope ([Id], VarSet)
acc
tyCoFVsOfCo (GRefl _ ty :: Type
ty mco :: MCoercion
mco) fv_cand :: Id -> Bool
fv_cand in_scope :: VarSet
in_scope acc :: ([Id], VarSet)
acc
= (Type -> FV
tyCoFVsOfType Type
ty FV -> FV -> FV
`unionFV` MCoercion -> FV
tyCoFVsOfMCo MCoercion
mco) Id -> Bool
fv_cand VarSet
in_scope ([Id], VarSet)
acc
tyCoFVsOfCo (TyConAppCo _ _ cos :: [Coercion]
cos) fv_cand :: Id -> Bool
fv_cand in_scope :: VarSet
in_scope acc :: ([Id], VarSet)
acc = [Coercion] -> FV
tyCoFVsOfCos [Coercion]
cos Id -> Bool
fv_cand VarSet
in_scope ([Id], VarSet)
acc
tyCoFVsOfCo (AppCo co :: Coercion
co arg :: Coercion
arg) fv_cand :: Id -> Bool
fv_cand in_scope :: VarSet
in_scope acc :: ([Id], VarSet)
acc
= (Coercion -> FV
tyCoFVsOfCo Coercion
co FV -> FV -> FV
`unionFV` Coercion -> FV
tyCoFVsOfCo Coercion
arg) Id -> Bool
fv_cand VarSet
in_scope ([Id], VarSet)
acc
tyCoFVsOfCo (ForAllCo tv :: Id
tv kind_co :: Coercion
kind_co co :: Coercion
co) fv_cand :: Id -> Bool
fv_cand in_scope :: VarSet
in_scope acc :: ([Id], VarSet)
acc
= (Id -> FV -> FV
tyCoFVsVarBndr Id
tv (Coercion -> FV
tyCoFVsOfCo Coercion
co) FV -> FV -> FV
`unionFV` Coercion -> FV
tyCoFVsOfCo Coercion
kind_co) Id -> Bool
fv_cand VarSet
in_scope ([Id], VarSet)
acc
tyCoFVsOfCo (FunCo _ co1 :: Coercion
co1 co2 :: Coercion
co2) fv_cand :: Id -> Bool
fv_cand in_scope :: VarSet
in_scope acc :: ([Id], VarSet)
acc
= (Coercion -> FV
tyCoFVsOfCo Coercion
co1 FV -> FV -> FV
`unionFV` Coercion -> FV
tyCoFVsOfCo Coercion
co2) Id -> Bool
fv_cand VarSet
in_scope ([Id], VarSet)
acc
tyCoFVsOfCo (CoVarCo v :: Id
v) fv_cand :: Id -> Bool
fv_cand in_scope :: VarSet
in_scope acc :: ([Id], VarSet)
acc
= Id -> FV
tyCoFVsOfCoVar Id
v Id -> Bool
fv_cand VarSet
in_scope ([Id], VarSet)
acc
tyCoFVsOfCo (HoleCo h :: CoercionHole
h) fv_cand :: Id -> Bool
fv_cand in_scope :: VarSet
in_scope acc :: ([Id], VarSet)
acc
= Id -> FV
tyCoFVsOfCoVar (CoercionHole -> Id
coHoleCoVar CoercionHole
h) Id -> Bool
fv_cand VarSet
in_scope ([Id], VarSet)
acc
tyCoFVsOfCo (AxiomInstCo _ _ cos :: [Coercion]
cos) fv_cand :: Id -> Bool
fv_cand in_scope :: VarSet
in_scope acc :: ([Id], VarSet)
acc = [Coercion] -> FV
tyCoFVsOfCos [Coercion]
cos Id -> Bool
fv_cand VarSet
in_scope ([Id], VarSet)
acc
tyCoFVsOfCo (UnivCo p :: UnivCoProvenance
p _ t1 :: Type
t1 t2 :: Type
t2) fv_cand :: Id -> Bool
fv_cand in_scope :: VarSet
in_scope acc :: ([Id], VarSet)
acc
= (UnivCoProvenance -> FV
tyCoFVsOfProv UnivCoProvenance
p FV -> FV -> FV
`unionFV` Type -> FV
tyCoFVsOfType Type
t1
FV -> FV -> FV
`unionFV` Type -> FV
tyCoFVsOfType Type
t2) Id -> Bool
fv_cand VarSet
in_scope ([Id], VarSet)
acc
tyCoFVsOfCo (SymCo co :: Coercion
co) fv_cand :: Id -> Bool
fv_cand in_scope :: VarSet
in_scope acc :: ([Id], VarSet)
acc = Coercion -> FV
tyCoFVsOfCo Coercion
co Id -> Bool
fv_cand VarSet
in_scope ([Id], VarSet)
acc
tyCoFVsOfCo (TransCo co1 :: Coercion
co1 co2 :: Coercion
co2) fv_cand :: Id -> Bool
fv_cand in_scope :: VarSet
in_scope acc :: ([Id], VarSet)
acc = (Coercion -> FV
tyCoFVsOfCo Coercion
co1 FV -> FV -> FV
`unionFV` Coercion -> FV
tyCoFVsOfCo Coercion
co2) Id -> Bool
fv_cand VarSet
in_scope ([Id], VarSet)
acc
tyCoFVsOfCo (NthCo _ _ co :: Coercion
co) fv_cand :: Id -> Bool
fv_cand in_scope :: VarSet
in_scope acc :: ([Id], VarSet)
acc = Coercion -> FV
tyCoFVsOfCo Coercion
co Id -> Bool
fv_cand VarSet
in_scope ([Id], VarSet)
acc
tyCoFVsOfCo (LRCo _ co :: Coercion
co) fv_cand :: Id -> Bool
fv_cand in_scope :: VarSet
in_scope acc :: ([Id], VarSet)
acc = Coercion -> FV
tyCoFVsOfCo Coercion
co Id -> Bool
fv_cand VarSet
in_scope ([Id], VarSet)
acc
tyCoFVsOfCo (InstCo co :: Coercion
co arg :: Coercion
arg) fv_cand :: Id -> Bool
fv_cand in_scope :: VarSet
in_scope acc :: ([Id], VarSet)
acc = (Coercion -> FV
tyCoFVsOfCo Coercion
co FV -> FV -> FV
`unionFV` Coercion -> FV
tyCoFVsOfCo Coercion
arg) Id -> Bool
fv_cand VarSet
in_scope ([Id], VarSet)
acc
tyCoFVsOfCo (KindCo co :: Coercion
co) fv_cand :: Id -> Bool
fv_cand in_scope :: VarSet
in_scope acc :: ([Id], VarSet)
acc = Coercion -> FV
tyCoFVsOfCo Coercion
co Id -> Bool
fv_cand VarSet
in_scope ([Id], VarSet)
acc
tyCoFVsOfCo (SubCo co :: Coercion
co) fv_cand :: Id -> Bool
fv_cand in_scope :: VarSet
in_scope acc :: ([Id], VarSet)
acc = Coercion -> FV
tyCoFVsOfCo Coercion
co Id -> Bool
fv_cand VarSet
in_scope ([Id], VarSet)
acc
tyCoFVsOfCo (AxiomRuleCo _ cs :: [Coercion]
cs) fv_cand :: Id -> Bool
fv_cand in_scope :: VarSet
in_scope acc :: ([Id], VarSet)
acc = [Coercion] -> FV
tyCoFVsOfCos [Coercion]
cs Id -> Bool
fv_cand VarSet
in_scope ([Id], VarSet)
acc
tyCoFVsOfCoVar :: CoVar -> FV
tyCoFVsOfCoVar :: Id -> FV
tyCoFVsOfCoVar v :: Id
v fv_cand :: Id -> Bool
fv_cand in_scope :: VarSet
in_scope acc :: ([Id], VarSet)
acc
= (Id -> FV
unitFV Id
v FV -> FV -> FV
`unionFV` Type -> FV
tyCoFVsOfType (Id -> Type
varType Id
v)) Id -> Bool
fv_cand VarSet
in_scope ([Id], VarSet)
acc
tyCoFVsOfProv :: UnivCoProvenance -> FV
tyCoFVsOfProv :: UnivCoProvenance -> FV
tyCoFVsOfProv UnsafeCoerceProv fv_cand :: Id -> Bool
fv_cand in_scope :: VarSet
in_scope acc :: ([Id], VarSet)
acc = FV
emptyFV Id -> Bool
fv_cand VarSet
in_scope ([Id], VarSet)
acc
tyCoFVsOfProv (PhantomProv co :: Coercion
co) fv_cand :: Id -> Bool
fv_cand in_scope :: VarSet
in_scope acc :: ([Id], VarSet)
acc = Coercion -> FV
tyCoFVsOfCo Coercion
co Id -> Bool
fv_cand VarSet
in_scope ([Id], VarSet)
acc
tyCoFVsOfProv (ProofIrrelProv co :: Coercion
co) fv_cand :: Id -> Bool
fv_cand in_scope :: VarSet
in_scope acc :: ([Id], VarSet)
acc = Coercion -> FV
tyCoFVsOfCo Coercion
co Id -> Bool
fv_cand VarSet
in_scope ([Id], VarSet)
acc
tyCoFVsOfProv (PluginProv _) fv_cand :: Id -> Bool
fv_cand in_scope :: VarSet
in_scope acc :: ([Id], VarSet)
acc = FV
emptyFV Id -> Bool
fv_cand VarSet
in_scope ([Id], VarSet)
acc
tyCoFVsOfCos :: [Coercion] -> FV
tyCoFVsOfCos :: [Coercion] -> FV
tyCoFVsOfCos [] fv_cand :: Id -> Bool
fv_cand in_scope :: VarSet
in_scope acc :: ([Id], VarSet)
acc = FV
emptyFV Id -> Bool
fv_cand VarSet
in_scope ([Id], VarSet)
acc
tyCoFVsOfCos (co :: Coercion
co:cos :: [Coercion]
cos) fv_cand :: Id -> Bool
fv_cand in_scope :: VarSet
in_scope acc :: ([Id], VarSet)
acc = (Coercion -> FV
tyCoFVsOfCo Coercion
co FV -> FV -> FV
`unionFV` [Coercion] -> FV
tyCoFVsOfCos [Coercion]
cos) Id -> Bool
fv_cand VarSet
in_scope ([Id], VarSet)
acc
getCoVarSet :: FV -> CoVarSet
getCoVarSet :: FV -> VarSet
getCoVarSet fv :: FV
fv = ([Id], VarSet) -> VarSet
forall a b. (a, b) -> b
snd (FV
fv Id -> Bool
isCoVar VarSet
emptyVarSet ([], VarSet
emptyVarSet))
coVarsOfType :: Type -> CoVarSet
coVarsOfType :: Type -> VarSet
coVarsOfType ty :: Type
ty = FV -> VarSet
getCoVarSet (Type -> FV
tyCoFVsOfType Type
ty)
coVarsOfTypes :: [Type] -> TyCoVarSet
coVarsOfTypes :: [Type] -> VarSet
coVarsOfTypes tys :: [Type]
tys = FV -> VarSet
getCoVarSet ([Type] -> FV
tyCoFVsOfTypes [Type]
tys)
coVarsOfCo :: Coercion -> CoVarSet
coVarsOfCo :: Coercion -> VarSet
coVarsOfCo co :: Coercion
co = FV -> VarSet
getCoVarSet (Coercion -> FV
tyCoFVsOfCo Coercion
co)
coVarsOfCos :: [Coercion] -> CoVarSet
coVarsOfCos :: [Coercion] -> VarSet
coVarsOfCos cos :: [Coercion]
cos = FV -> VarSet
getCoVarSet ([Coercion] -> FV
tyCoFVsOfCos [Coercion]
cos)
almostDevoidCoVarOfCo :: CoVar -> Coercion -> Bool
almostDevoidCoVarOfCo :: Id -> Coercion -> Bool
almostDevoidCoVarOfCo cv :: Id
cv co :: Coercion
co =
Coercion -> Id -> Bool
almost_devoid_co_var_of_co Coercion
co Id
cv
almost_devoid_co_var_of_co :: Coercion -> CoVar -> Bool
almost_devoid_co_var_of_co :: Coercion -> Id -> Bool
almost_devoid_co_var_of_co (Refl {}) _ = Bool
True
almost_devoid_co_var_of_co (GRefl {}) _ = Bool
True
almost_devoid_co_var_of_co (TyConAppCo _ _ cos :: [Coercion]
cos) cv :: Id
cv
= [Coercion] -> Id -> Bool
almost_devoid_co_var_of_cos [Coercion]
cos Id
cv
almost_devoid_co_var_of_co (AppCo co :: Coercion
co arg :: Coercion
arg) cv :: Id
cv
= Coercion -> Id -> Bool
almost_devoid_co_var_of_co Coercion
co Id
cv
Bool -> Bool -> Bool
&& Coercion -> Id -> Bool
almost_devoid_co_var_of_co Coercion
arg Id
cv
almost_devoid_co_var_of_co (ForAllCo v :: Id
v kind_co :: Coercion
kind_co co :: Coercion
co) cv :: Id
cv
= Coercion -> Id -> Bool
almost_devoid_co_var_of_co Coercion
kind_co Id
cv
Bool -> Bool -> Bool
&& (Id
v Id -> Id -> Bool
forall a. Eq a => a -> a -> Bool
== Id
cv Bool -> Bool -> Bool
|| Coercion -> Id -> Bool
almost_devoid_co_var_of_co Coercion
co Id
cv)
almost_devoid_co_var_of_co (FunCo _ co1 :: Coercion
co1 co2 :: Coercion
co2) cv :: Id
cv
= Coercion -> Id -> Bool
almost_devoid_co_var_of_co Coercion
co1 Id
cv
Bool -> Bool -> Bool
&& Coercion -> Id -> Bool
almost_devoid_co_var_of_co Coercion
co2 Id
cv
almost_devoid_co_var_of_co (CoVarCo v :: Id
v) cv :: Id
cv = Id
v Id -> Id -> Bool
forall a. Eq a => a -> a -> Bool
/= Id
cv
almost_devoid_co_var_of_co (HoleCo h :: CoercionHole
h) cv :: Id
cv = (CoercionHole -> Id
coHoleCoVar CoercionHole
h) Id -> Id -> Bool
forall a. Eq a => a -> a -> Bool
/= Id
cv
almost_devoid_co_var_of_co (AxiomInstCo _ _ cos :: [Coercion]
cos) cv :: Id
cv
= [Coercion] -> Id -> Bool
almost_devoid_co_var_of_cos [Coercion]
cos Id
cv
almost_devoid_co_var_of_co (UnivCo p :: UnivCoProvenance
p _ t1 :: Type
t1 t2 :: Type
t2) cv :: Id
cv
= UnivCoProvenance -> Id -> Bool
almost_devoid_co_var_of_prov UnivCoProvenance
p Id
cv
Bool -> Bool -> Bool
&& Type -> Id -> Bool
almost_devoid_co_var_of_type Type
t1 Id
cv
Bool -> Bool -> Bool
&& Type -> Id -> Bool
almost_devoid_co_var_of_type Type
t2 Id
cv
almost_devoid_co_var_of_co (SymCo co :: Coercion
co) cv :: Id
cv
= Coercion -> Id -> Bool
almost_devoid_co_var_of_co Coercion
co Id
cv
almost_devoid_co_var_of_co (TransCo co1 :: Coercion
co1 co2 :: Coercion
co2) cv :: Id
cv
= Coercion -> Id -> Bool
almost_devoid_co_var_of_co Coercion
co1 Id
cv
Bool -> Bool -> Bool
&& Coercion -> Id -> Bool
almost_devoid_co_var_of_co Coercion
co2 Id
cv
almost_devoid_co_var_of_co (NthCo _ _ co :: Coercion
co) cv :: Id
cv
= Coercion -> Id -> Bool
almost_devoid_co_var_of_co Coercion
co Id
cv
almost_devoid_co_var_of_co (LRCo _ co :: Coercion
co) cv :: Id
cv
= Coercion -> Id -> Bool
almost_devoid_co_var_of_co Coercion
co Id
cv
almost_devoid_co_var_of_co (InstCo co :: Coercion
co arg :: Coercion
arg) cv :: Id
cv
= Coercion -> Id -> Bool
almost_devoid_co_var_of_co Coercion
co Id
cv
Bool -> Bool -> Bool
&& Coercion -> Id -> Bool
almost_devoid_co_var_of_co Coercion
arg Id
cv
almost_devoid_co_var_of_co (KindCo co :: Coercion
co) cv :: Id
cv
= Coercion -> Id -> Bool
almost_devoid_co_var_of_co Coercion
co Id
cv
almost_devoid_co_var_of_co (SubCo co :: Coercion
co) cv :: Id
cv
= Coercion -> Id -> Bool
almost_devoid_co_var_of_co Coercion
co Id
cv
almost_devoid_co_var_of_co (AxiomRuleCo _ cs :: [Coercion]
cs) cv :: Id
cv
= [Coercion] -> Id -> Bool
almost_devoid_co_var_of_cos [Coercion]
cs Id
cv
almost_devoid_co_var_of_cos :: [Coercion] -> CoVar -> Bool
almost_devoid_co_var_of_cos :: [Coercion] -> Id -> Bool
almost_devoid_co_var_of_cos [] _ = Bool
True
almost_devoid_co_var_of_cos (co :: Coercion
co:cos :: [Coercion]
cos) cv :: Id
cv
= Coercion -> Id -> Bool
almost_devoid_co_var_of_co Coercion
co Id
cv
Bool -> Bool -> Bool
&& [Coercion] -> Id -> Bool
almost_devoid_co_var_of_cos [Coercion]
cos Id
cv
almost_devoid_co_var_of_prov :: UnivCoProvenance -> CoVar -> Bool
almost_devoid_co_var_of_prov :: UnivCoProvenance -> Id -> Bool
almost_devoid_co_var_of_prov (PhantomProv co :: Coercion
co) cv :: Id
cv
= Coercion -> Id -> Bool
almost_devoid_co_var_of_co Coercion
co Id
cv
almost_devoid_co_var_of_prov (ProofIrrelProv co :: Coercion
co) cv :: Id
cv
= Coercion -> Id -> Bool
almost_devoid_co_var_of_co Coercion
co Id
cv
almost_devoid_co_var_of_prov UnsafeCoerceProv _ = Bool
True
almost_devoid_co_var_of_prov (PluginProv _) _ = Bool
True
almost_devoid_co_var_of_type :: Type -> CoVar -> Bool
almost_devoid_co_var_of_type :: Type -> Id -> Bool
almost_devoid_co_var_of_type (TyVarTy _) _ = Bool
True
almost_devoid_co_var_of_type (TyConApp _ tys :: [Type]
tys) cv :: Id
cv
= [Type] -> Id -> Bool
almost_devoid_co_var_of_types [Type]
tys Id
cv
almost_devoid_co_var_of_type (LitTy {}) _ = Bool
True
almost_devoid_co_var_of_type (AppTy fun :: Type
fun arg :: Type
arg) cv :: Id
cv
= Type -> Id -> Bool
almost_devoid_co_var_of_type Type
fun Id
cv
Bool -> Bool -> Bool
&& Type -> Id -> Bool
almost_devoid_co_var_of_type Type
arg Id
cv
almost_devoid_co_var_of_type (FunTy arg :: Type
arg res :: Type
res) cv :: Id
cv
= Type -> Id -> Bool
almost_devoid_co_var_of_type Type
arg Id
cv
Bool -> Bool -> Bool
&& Type -> Id -> Bool
almost_devoid_co_var_of_type Type
res Id
cv
almost_devoid_co_var_of_type (ForAllTy (Bndr v :: Id
v _) ty :: Type
ty) cv :: Id
cv
= Type -> Id -> Bool
almost_devoid_co_var_of_type (Id -> Type
varType Id
v) Id
cv
Bool -> Bool -> Bool
&& (Id
v Id -> Id -> Bool
forall a. Eq a => a -> a -> Bool
== Id
cv Bool -> Bool -> Bool
|| Type -> Id -> Bool
almost_devoid_co_var_of_type Type
ty Id
cv)
almost_devoid_co_var_of_type (CastTy ty :: Type
ty co :: Coercion
co) cv :: Id
cv
= Type -> Id -> Bool
almost_devoid_co_var_of_type Type
ty Id
cv
Bool -> Bool -> Bool
&& Coercion -> Id -> Bool
almost_devoid_co_var_of_co Coercion
co Id
cv
almost_devoid_co_var_of_type (CoercionTy co :: Coercion
co) cv :: Id
cv
= Coercion -> Id -> Bool
almost_devoid_co_var_of_co Coercion
co Id
cv
almost_devoid_co_var_of_types :: [Type] -> CoVar -> Bool
almost_devoid_co_var_of_types :: [Type] -> Id -> Bool
almost_devoid_co_var_of_types [] _ = Bool
True
almost_devoid_co_var_of_types (ty :: Type
ty:tys :: [Type]
tys) cv :: Id
cv
= Type -> Id -> Bool
almost_devoid_co_var_of_type Type
ty Id
cv
Bool -> Bool -> Bool
&& [Type] -> Id -> Bool
almost_devoid_co_var_of_types [Type]
tys Id
cv
injectiveVarsOfType :: Type -> FV
injectiveVarsOfType :: Type -> FV
injectiveVarsOfType = Type -> FV
go
where
go :: Type -> FV
go ty :: Type
ty | Just ty' :: Type
ty' <- Type -> Maybe Type
coreView Type
ty
= Type -> FV
go Type
ty'
go (TyVarTy v :: Id
v) = Id -> FV
unitFV Id
v FV -> FV -> FV
`unionFV` Type -> FV
go (Id -> Type
tyVarKind Id
v)
go (AppTy f :: Type
f a :: Type
a) = Type -> FV
go Type
f FV -> FV -> FV
`unionFV` Type -> FV
go Type
a
go (FunTy ty1 :: Type
ty1 ty2 :: Type
ty2) = Type -> FV
go Type
ty1 FV -> FV -> FV
`unionFV` Type -> FV
go Type
ty2
go (TyConApp tc :: TyCon
tc tys :: [Type]
tys) =
case TyCon -> Injectivity
tyConInjectivityInfo TyCon
tc of
NotInjective -> FV
emptyFV
Injective inj :: [Bool]
inj -> (Type -> FV) -> [Type] -> FV
forall a. (a -> FV) -> [a] -> FV
mapUnionFV Type -> FV
go ([Type] -> FV) -> [Type] -> FV
forall a b. (a -> b) -> a -> b
$
[Bool] -> [Type] -> [Type]
forall a. [Bool] -> [a] -> [a]
filterByList ([Bool]
inj [Bool] -> [Bool] -> [Bool]
forall a. [a] -> [a] -> [a]
++ Bool -> [Bool]
forall a. a -> [a]
repeat Bool
True) [Type]
tys
go (ForAllTy tvb :: TyCoVarBinder
tvb ty :: Type
ty) = TyCoVarBinder -> FV -> FV
tyCoFVsBndr TyCoVarBinder
tvb (FV -> FV) -> FV -> FV
forall a b. (a -> b) -> a -> b
$ Type -> FV
go Type
ty
go LitTy{} = FV
emptyFV
go (CastTy ty :: Type
ty _) = Type -> FV
go Type
ty
go CoercionTy{} = FV
emptyFV
tyConAppNeedsKindSig
:: Bool
-> TyCon
-> Int
-> Bool
tyConAppNeedsKindSig :: Bool -> TyCon -> Int -> Bool
tyConAppNeedsKindSig spec_inj_pos :: Bool
spec_inj_pos tc :: TyCon
tc n_args :: Int
n_args
| Ordering
LT <- [TyConBinder] -> Int -> Ordering
forall a. [a] -> Int -> Ordering
listLengthCmp [TyConBinder]
tc_binders Int
n_args
= Bool
False
| Bool
otherwise
= let (dropped_binders :: [TyConBinder]
dropped_binders, remaining_binders :: [TyConBinder]
remaining_binders)
= Int -> [TyConBinder] -> ([TyConBinder], [TyConBinder])
forall a. Int -> [a] -> ([a], [a])
splitAt Int
n_args [TyConBinder]
tc_binders
result_kind :: Type
result_kind = [TyConBinder] -> Type -> Type
mkTyConKind [TyConBinder]
remaining_binders Type
tc_res_kind
result_vars :: VarSet
result_vars = Type -> VarSet
tyCoVarsOfType Type
result_kind
dropped_vars :: VarSet
dropped_vars = FV -> VarSet
fvVarSet (FV -> VarSet) -> FV -> VarSet
forall a b. (a -> b) -> a -> b
$
(TyConBinder -> FV) -> [TyConBinder] -> FV
forall a. (a -> FV) -> [a] -> FV
mapUnionFV (Bool -> TyConBinder -> FV
injective_vars_of_binder Bool
spec_inj_pos)
[TyConBinder]
dropped_binders
in Bool -> Bool
not (VarSet -> VarSet -> Bool
subVarSet VarSet
result_vars VarSet
dropped_vars)
where
tc_binders :: [TyConBinder]
tc_binders = TyCon -> [TyConBinder]
tyConBinders TyCon
tc
tc_res_kind :: Type
tc_res_kind = TyCon -> Type
tyConResKind TyCon
tc
injective_vars_of_binder
:: Bool
-> TyConBinder -> FV
injective_vars_of_binder :: Bool -> TyConBinder -> FV
injective_vars_of_binder spec_inj_pos :: Bool
spec_inj_pos (Bndr tv :: Id
tv vis :: TyConBndrVis
vis) =
case TyConBndrVis
vis of
AnonTCB -> Type -> FV
injectiveVarsOfType (Id -> Type
varType Id
tv)
NamedTCB argf :: ArgFlag
argf
| (ArgFlag
argf ArgFlag -> ArgFlag -> Bool
forall a. Eq a => a -> a -> Bool
== ArgFlag
Required)
Bool -> Bool -> Bool
|| (Bool
spec_inj_pos Bool -> Bool -> Bool
&& (ArgFlag
argf ArgFlag -> ArgFlag -> Bool
forall a. Eq a => a -> a -> Bool
== ArgFlag
Specified))
-> Id -> FV
unitFV Id
tv FV -> FV -> FV
`unionFV` Type -> FV
injectiveVarsOfType (Id -> Type
varType Id
tv)
| Bool
otherwise
-> FV
emptyFV
noFreeVarsOfType :: Type -> Bool
noFreeVarsOfType :: Type -> Bool
noFreeVarsOfType (TyVarTy _) = Bool
False
noFreeVarsOfType (AppTy t1 :: Type
t1 t2 :: Type
t2) = Type -> Bool
noFreeVarsOfType Type
t1 Bool -> Bool -> Bool
&& Type -> Bool
noFreeVarsOfType Type
t2
noFreeVarsOfType (TyConApp _ tys :: [Type]
tys) = (Type -> Bool) -> [Type] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all Type -> Bool
noFreeVarsOfType [Type]
tys
noFreeVarsOfType ty :: Type
ty@(ForAllTy {}) = VarSet -> Bool
isEmptyVarSet (Type -> VarSet
tyCoVarsOfType Type
ty)
noFreeVarsOfType (FunTy t1 :: Type
t1 t2 :: Type
t2) = Type -> Bool
noFreeVarsOfType Type
t1 Bool -> Bool -> Bool
&& Type -> Bool
noFreeVarsOfType Type
t2
noFreeVarsOfType (LitTy _) = Bool
True
noFreeVarsOfType (CastTy ty :: Type
ty co :: Coercion
co) = Type -> Bool
noFreeVarsOfType Type
ty Bool -> Bool -> Bool
&& Coercion -> Bool
noFreeVarsOfCo Coercion
co
noFreeVarsOfType (CoercionTy co :: Coercion
co) = Coercion -> Bool
noFreeVarsOfCo Coercion
co
noFreeVarsOfMCo :: MCoercion -> Bool
noFreeVarsOfMCo :: MCoercion -> Bool
noFreeVarsOfMCo MRefl = Bool
True
noFreeVarsOfMCo (MCo co :: Coercion
co) = Coercion -> Bool
noFreeVarsOfCo Coercion
co
noFreeVarsOfTypes :: [Type] -> Bool
noFreeVarsOfTypes :: [Type] -> Bool
noFreeVarsOfTypes = (Type -> Bool) -> [Type] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all Type -> Bool
noFreeVarsOfType
noFreeVarsOfCo :: Coercion -> Bool
noFreeVarsOfCo :: Coercion -> Bool
noFreeVarsOfCo (Refl ty :: Type
ty) = Type -> Bool
noFreeVarsOfType Type
ty
noFreeVarsOfCo (GRefl _ ty :: Type
ty co :: MCoercion
co) = Type -> Bool
noFreeVarsOfType Type
ty Bool -> Bool -> Bool
&& MCoercion -> Bool
noFreeVarsOfMCo MCoercion
co
noFreeVarsOfCo (TyConAppCo _ _ args :: [Coercion]
args) = (Coercion -> Bool) -> [Coercion] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all Coercion -> Bool
noFreeVarsOfCo [Coercion]
args
noFreeVarsOfCo (AppCo c1 :: Coercion
c1 c2 :: Coercion
c2) = Coercion -> Bool
noFreeVarsOfCo Coercion
c1 Bool -> Bool -> Bool
&& Coercion -> Bool
noFreeVarsOfCo Coercion
c2
noFreeVarsOfCo co :: Coercion
co@(ForAllCo {}) = VarSet -> Bool
isEmptyVarSet (Coercion -> VarSet
tyCoVarsOfCo Coercion
co)
noFreeVarsOfCo (FunCo _ c1 :: Coercion
c1 c2 :: Coercion
c2) = Coercion -> Bool
noFreeVarsOfCo Coercion
c1 Bool -> Bool -> Bool
&& Coercion -> Bool
noFreeVarsOfCo Coercion
c2
noFreeVarsOfCo (CoVarCo _) = Bool
False
noFreeVarsOfCo (HoleCo {}) = Bool
True
noFreeVarsOfCo (AxiomInstCo _ _ args :: [Coercion]
args) = (Coercion -> Bool) -> [Coercion] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all Coercion -> Bool
noFreeVarsOfCo [Coercion]
args
noFreeVarsOfCo (UnivCo p :: UnivCoProvenance
p _ t1 :: Type
t1 t2 :: Type
t2) = UnivCoProvenance -> Bool
noFreeVarsOfProv UnivCoProvenance
p Bool -> Bool -> Bool
&&
Type -> Bool
noFreeVarsOfType Type
t1 Bool -> Bool -> Bool
&&
Type -> Bool
noFreeVarsOfType Type
t2
noFreeVarsOfCo (SymCo co :: Coercion
co) = Coercion -> Bool
noFreeVarsOfCo Coercion
co
noFreeVarsOfCo (TransCo co1 :: Coercion
co1 co2 :: Coercion
co2) = Coercion -> Bool
noFreeVarsOfCo Coercion
co1 Bool -> Bool -> Bool
&& Coercion -> Bool
noFreeVarsOfCo Coercion
co2
noFreeVarsOfCo (NthCo _ _ co :: Coercion
co) = Coercion -> Bool
noFreeVarsOfCo Coercion
co
noFreeVarsOfCo (LRCo _ co :: Coercion
co) = Coercion -> Bool
noFreeVarsOfCo Coercion
co
noFreeVarsOfCo (InstCo co1 :: Coercion
co1 co2 :: Coercion
co2) = Coercion -> Bool
noFreeVarsOfCo Coercion
co1 Bool -> Bool -> Bool
&& Coercion -> Bool
noFreeVarsOfCo Coercion
co2
noFreeVarsOfCo (KindCo co :: Coercion
co) = Coercion -> Bool
noFreeVarsOfCo Coercion
co
noFreeVarsOfCo (SubCo co :: Coercion
co) = Coercion -> Bool
noFreeVarsOfCo Coercion
co
noFreeVarsOfCo (AxiomRuleCo _ cs :: [Coercion]
cs) = (Coercion -> Bool) -> [Coercion] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all Coercion -> Bool
noFreeVarsOfCo [Coercion]
cs
noFreeVarsOfProv :: UnivCoProvenance -> Bool
noFreeVarsOfProv :: UnivCoProvenance -> Bool
noFreeVarsOfProv UnsafeCoerceProv = Bool
True
noFreeVarsOfProv (PhantomProv co :: Coercion
co) = Coercion -> Bool
noFreeVarsOfCo Coercion
co
noFreeVarsOfProv (ProofIrrelProv co :: Coercion
co) = Coercion -> Bool
noFreeVarsOfCo Coercion
co
noFreeVarsOfProv (PluginProv {}) = Bool
True
data TCvSubst
= TCvSubst InScopeSet
TvSubstEnv
CvSubstEnv
type TvSubstEnv = TyVarEnv Type
type CvSubstEnv = CoVarEnv Coercion
emptyTvSubstEnv :: TvSubstEnv
emptyTvSubstEnv :: TyVarEnv Type
emptyTvSubstEnv = TyVarEnv Type
forall a. VarEnv a
emptyVarEnv
emptyCvSubstEnv :: CvSubstEnv
emptyCvSubstEnv :: CoVarEnv Coercion
emptyCvSubstEnv = CoVarEnv Coercion
forall a. VarEnv a
emptyVarEnv
composeTCvSubstEnv :: InScopeSet
-> (TvSubstEnv, CvSubstEnv)
-> (TvSubstEnv, CvSubstEnv)
-> (TvSubstEnv, CvSubstEnv)
composeTCvSubstEnv :: InScopeSet
-> (TyVarEnv Type, CoVarEnv Coercion)
-> (TyVarEnv Type, CoVarEnv Coercion)
-> (TyVarEnv Type, CoVarEnv Coercion)
composeTCvSubstEnv in_scope :: InScopeSet
in_scope (tenv1 :: TyVarEnv Type
tenv1, cenv1 :: CoVarEnv Coercion
cenv1) (tenv2 :: TyVarEnv Type
tenv2, cenv2 :: CoVarEnv Coercion
cenv2)
= ( TyVarEnv Type
tenv1 TyVarEnv Type -> TyVarEnv Type -> TyVarEnv Type
forall a. VarEnv a -> VarEnv a -> VarEnv a
`plusVarEnv` (Type -> Type) -> TyVarEnv Type -> TyVarEnv Type
forall a b. (a -> b) -> VarEnv a -> VarEnv b
mapVarEnv (HasCallStack => TCvSubst -> Type -> Type
TCvSubst -> Type -> Type
substTy TCvSubst
subst1) TyVarEnv Type
tenv2
, CoVarEnv Coercion
cenv1 CoVarEnv Coercion -> CoVarEnv Coercion -> CoVarEnv Coercion
forall a. VarEnv a -> VarEnv a -> VarEnv a
`plusVarEnv` (Coercion -> Coercion) -> CoVarEnv Coercion -> CoVarEnv Coercion
forall a b. (a -> b) -> VarEnv a -> VarEnv b
mapVarEnv (HasCallStack => TCvSubst -> Coercion -> Coercion
TCvSubst -> Coercion -> Coercion
substCo TCvSubst
subst1) CoVarEnv Coercion
cenv2 )
where
subst1 :: TCvSubst
subst1 = InScopeSet -> TyVarEnv Type -> CoVarEnv Coercion -> TCvSubst
TCvSubst InScopeSet
in_scope TyVarEnv Type
tenv1 CoVarEnv Coercion
cenv1
composeTCvSubst :: TCvSubst -> TCvSubst -> TCvSubst
composeTCvSubst :: TCvSubst -> TCvSubst -> TCvSubst
composeTCvSubst (TCvSubst is1 :: InScopeSet
is1 tenv1 :: TyVarEnv Type
tenv1 cenv1 :: CoVarEnv Coercion
cenv1) (TCvSubst is2 :: InScopeSet
is2 tenv2 :: TyVarEnv Type
tenv2 cenv2 :: CoVarEnv Coercion
cenv2)
= InScopeSet -> TyVarEnv Type -> CoVarEnv Coercion -> TCvSubst
TCvSubst InScopeSet
is3 TyVarEnv Type
tenv3 CoVarEnv Coercion
cenv3
where
is3 :: InScopeSet
is3 = InScopeSet
is1 InScopeSet -> InScopeSet -> InScopeSet
`unionInScope` InScopeSet
is2
(tenv3 :: TyVarEnv Type
tenv3, cenv3 :: CoVarEnv Coercion
cenv3) = InScopeSet
-> (TyVarEnv Type, CoVarEnv Coercion)
-> (TyVarEnv Type, CoVarEnv Coercion)
-> (TyVarEnv Type, CoVarEnv Coercion)
composeTCvSubstEnv InScopeSet
is3 (TyVarEnv Type
tenv1, CoVarEnv Coercion
cenv1) (TyVarEnv Type
tenv2, CoVarEnv Coercion
cenv2)
emptyTCvSubst :: TCvSubst
emptyTCvSubst :: TCvSubst
emptyTCvSubst = InScopeSet -> TyVarEnv Type -> CoVarEnv Coercion -> TCvSubst
TCvSubst InScopeSet
emptyInScopeSet TyVarEnv Type
emptyTvSubstEnv CoVarEnv Coercion
emptyCvSubstEnv
mkEmptyTCvSubst :: InScopeSet -> TCvSubst
mkEmptyTCvSubst :: InScopeSet -> TCvSubst
mkEmptyTCvSubst is :: InScopeSet
is = InScopeSet -> TyVarEnv Type -> CoVarEnv Coercion -> TCvSubst
TCvSubst InScopeSet
is TyVarEnv Type
emptyTvSubstEnv CoVarEnv Coercion
emptyCvSubstEnv
isEmptyTCvSubst :: TCvSubst -> Bool
isEmptyTCvSubst :: TCvSubst -> Bool
isEmptyTCvSubst (TCvSubst _ tenv :: TyVarEnv Type
tenv cenv :: CoVarEnv Coercion
cenv) = TyVarEnv Type -> Bool
forall a. VarEnv a -> Bool
isEmptyVarEnv TyVarEnv Type
tenv Bool -> Bool -> Bool
&& CoVarEnv Coercion -> Bool
forall a. VarEnv a -> Bool
isEmptyVarEnv CoVarEnv Coercion
cenv
mkTCvSubst :: InScopeSet -> (TvSubstEnv, CvSubstEnv) -> TCvSubst
mkTCvSubst :: InScopeSet -> (TyVarEnv Type, CoVarEnv Coercion) -> TCvSubst
mkTCvSubst in_scope :: InScopeSet
in_scope (tenv :: TyVarEnv Type
tenv, cenv :: CoVarEnv Coercion
cenv) = InScopeSet -> TyVarEnv Type -> CoVarEnv Coercion -> TCvSubst
TCvSubst InScopeSet
in_scope TyVarEnv Type
tenv CoVarEnv Coercion
cenv
mkTvSubst :: InScopeSet -> TvSubstEnv -> TCvSubst
mkTvSubst :: InScopeSet -> TyVarEnv Type -> TCvSubst
mkTvSubst in_scope :: InScopeSet
in_scope tenv :: TyVarEnv Type
tenv = InScopeSet -> TyVarEnv Type -> CoVarEnv Coercion -> TCvSubst
TCvSubst InScopeSet
in_scope TyVarEnv Type
tenv CoVarEnv Coercion
emptyCvSubstEnv
mkCvSubst :: InScopeSet -> CvSubstEnv -> TCvSubst
mkCvSubst :: InScopeSet -> CoVarEnv Coercion -> TCvSubst
mkCvSubst in_scope :: InScopeSet
in_scope cenv :: CoVarEnv Coercion
cenv = InScopeSet -> TyVarEnv Type -> CoVarEnv Coercion -> TCvSubst
TCvSubst InScopeSet
in_scope TyVarEnv Type
emptyTvSubstEnv CoVarEnv Coercion
cenv
getTvSubstEnv :: TCvSubst -> TvSubstEnv
getTvSubstEnv :: TCvSubst -> TyVarEnv Type
getTvSubstEnv (TCvSubst _ env :: TyVarEnv Type
env _) = TyVarEnv Type
env
getCvSubstEnv :: TCvSubst -> CvSubstEnv
getCvSubstEnv :: TCvSubst -> CoVarEnv Coercion
getCvSubstEnv (TCvSubst _ _ env :: CoVarEnv Coercion
env) = CoVarEnv Coercion
env
getTCvInScope :: TCvSubst -> InScopeSet
getTCvInScope :: TCvSubst -> InScopeSet
getTCvInScope (TCvSubst in_scope :: InScopeSet
in_scope _ _) = InScopeSet
in_scope
getTCvSubstRangeFVs :: TCvSubst -> VarSet
getTCvSubstRangeFVs :: TCvSubst -> VarSet
getTCvSubstRangeFVs (TCvSubst _ tenv :: TyVarEnv Type
tenv cenv :: CoVarEnv Coercion
cenv)
= VarSet -> VarSet -> VarSet
unionVarSet VarSet
tenvFVs VarSet
cenvFVs
where
tenvFVs :: VarSet
tenvFVs = TyVarEnv Type -> VarSet
tyCoVarsOfTypesSet TyVarEnv Type
tenv
cenvFVs :: VarSet
cenvFVs = CoVarEnv Coercion -> VarSet
tyCoVarsOfCosSet CoVarEnv Coercion
cenv
isInScope :: Var -> TCvSubst -> Bool
isInScope :: Id -> TCvSubst -> Bool
isInScope v :: Id
v (TCvSubst in_scope :: InScopeSet
in_scope _ _) = Id
v Id -> InScopeSet -> Bool
`elemInScopeSet` InScopeSet
in_scope
notElemTCvSubst :: Var -> TCvSubst -> Bool
notElemTCvSubst :: Id -> TCvSubst -> Bool
notElemTCvSubst v :: Id
v (TCvSubst _ tenv :: TyVarEnv Type
tenv cenv :: CoVarEnv Coercion
cenv)
| Id -> Bool
isTyVar Id
v
= Bool -> Bool
not (Id
v Id -> TyVarEnv Type -> Bool
forall a. Id -> VarEnv a -> Bool
`elemVarEnv` TyVarEnv Type
tenv)
| Bool
otherwise
= Bool -> Bool
not (Id
v Id -> CoVarEnv Coercion -> Bool
forall a. Id -> VarEnv a -> Bool
`elemVarEnv` CoVarEnv Coercion
cenv)
setTvSubstEnv :: TCvSubst -> TvSubstEnv -> TCvSubst
setTvSubstEnv :: TCvSubst -> TyVarEnv Type -> TCvSubst
setTvSubstEnv (TCvSubst in_scope :: InScopeSet
in_scope _ cenv :: CoVarEnv Coercion
cenv) tenv :: TyVarEnv Type
tenv = InScopeSet -> TyVarEnv Type -> CoVarEnv Coercion -> TCvSubst
TCvSubst InScopeSet
in_scope TyVarEnv Type
tenv CoVarEnv Coercion
cenv
setCvSubstEnv :: TCvSubst -> CvSubstEnv -> TCvSubst
setCvSubstEnv :: TCvSubst -> CoVarEnv Coercion -> TCvSubst
setCvSubstEnv (TCvSubst in_scope :: InScopeSet
in_scope tenv :: TyVarEnv Type
tenv _) cenv :: CoVarEnv Coercion
cenv = InScopeSet -> TyVarEnv Type -> CoVarEnv Coercion -> TCvSubst
TCvSubst InScopeSet
in_scope TyVarEnv Type
tenv CoVarEnv Coercion
cenv
zapTCvSubst :: TCvSubst -> TCvSubst
zapTCvSubst :: TCvSubst -> TCvSubst
zapTCvSubst (TCvSubst in_scope :: InScopeSet
in_scope _ _) = InScopeSet -> TyVarEnv Type -> CoVarEnv Coercion -> TCvSubst
TCvSubst InScopeSet
in_scope TyVarEnv Type
forall a. VarEnv a
emptyVarEnv CoVarEnv Coercion
forall a. VarEnv a
emptyVarEnv
extendTCvInScope :: TCvSubst -> Var -> TCvSubst
extendTCvInScope :: TCvSubst -> Id -> TCvSubst
extendTCvInScope (TCvSubst in_scope :: InScopeSet
in_scope tenv :: TyVarEnv Type
tenv cenv :: CoVarEnv Coercion
cenv) var :: Id
var
= InScopeSet -> TyVarEnv Type -> CoVarEnv Coercion -> TCvSubst
TCvSubst (InScopeSet -> Id -> InScopeSet
extendInScopeSet InScopeSet
in_scope Id
var) TyVarEnv Type
tenv CoVarEnv Coercion
cenv
extendTCvInScopeList :: TCvSubst -> [Var] -> TCvSubst
extendTCvInScopeList :: TCvSubst -> [Id] -> TCvSubst
extendTCvInScopeList (TCvSubst in_scope :: InScopeSet
in_scope tenv :: TyVarEnv Type
tenv cenv :: CoVarEnv Coercion
cenv) vars :: [Id]
vars
= InScopeSet -> TyVarEnv Type -> CoVarEnv Coercion -> TCvSubst
TCvSubst (InScopeSet -> [Id] -> InScopeSet
extendInScopeSetList InScopeSet
in_scope [Id]
vars) TyVarEnv Type
tenv CoVarEnv Coercion
cenv
extendTCvInScopeSet :: TCvSubst -> VarSet -> TCvSubst
extendTCvInScopeSet :: TCvSubst -> VarSet -> TCvSubst
extendTCvInScopeSet (TCvSubst in_scope :: InScopeSet
in_scope tenv :: TyVarEnv Type
tenv cenv :: CoVarEnv Coercion
cenv) vars :: VarSet
vars
= InScopeSet -> TyVarEnv Type -> CoVarEnv Coercion -> TCvSubst
TCvSubst (InScopeSet -> VarSet -> InScopeSet
extendInScopeSetSet InScopeSet
in_scope VarSet
vars) TyVarEnv Type
tenv CoVarEnv Coercion
cenv
extendTCvSubst :: TCvSubst -> TyCoVar -> Type -> TCvSubst
extendTCvSubst :: TCvSubst -> Id -> Type -> TCvSubst
extendTCvSubst subst :: TCvSubst
subst v :: Id
v ty :: Type
ty
| Id -> Bool
isTyVar Id
v
= TCvSubst -> Id -> Type -> TCvSubst
extendTvSubst TCvSubst
subst Id
v Type
ty
| CoercionTy co :: Coercion
co <- Type
ty
= TCvSubst -> Id -> Coercion -> TCvSubst
extendCvSubst TCvSubst
subst Id
v Coercion
co
| Bool
otherwise
= String -> SDoc -> TCvSubst
forall a. HasCallStack => String -> SDoc -> a
pprPanic "extendTCvSubst" (Id -> SDoc
forall a. Outputable a => a -> SDoc
ppr Id
v SDoc -> SDoc -> SDoc
<+> String -> SDoc
text "|->" SDoc -> SDoc -> SDoc
<+> Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
ty)
extendTCvSubstWithClone :: TCvSubst -> TyCoVar -> TyCoVar -> TCvSubst
extendTCvSubstWithClone :: TCvSubst -> Id -> Id -> TCvSubst
extendTCvSubstWithClone subst :: TCvSubst
subst tcv :: Id
tcv
| Id -> Bool
isTyVar Id
tcv = TCvSubst -> Id -> Id -> TCvSubst
extendTvSubstWithClone TCvSubst
subst Id
tcv
| Bool
otherwise = TCvSubst -> Id -> Id -> TCvSubst
extendCvSubstWithClone TCvSubst
subst Id
tcv
extendTvSubst :: TCvSubst -> TyVar -> Type -> TCvSubst
extendTvSubst :: TCvSubst -> Id -> Type -> TCvSubst
extendTvSubst (TCvSubst in_scope :: InScopeSet
in_scope tenv :: TyVarEnv Type
tenv cenv :: CoVarEnv Coercion
cenv) tv :: Id
tv ty :: Type
ty
= InScopeSet -> TyVarEnv Type -> CoVarEnv Coercion -> TCvSubst
TCvSubst InScopeSet
in_scope (TyVarEnv Type -> Id -> Type -> TyVarEnv Type
forall a. VarEnv a -> Id -> a -> VarEnv a
extendVarEnv TyVarEnv Type
tenv Id
tv Type
ty) CoVarEnv Coercion
cenv
extendTvSubstBinderAndInScope :: TCvSubst -> TyCoBinder -> Type -> TCvSubst
extendTvSubstBinderAndInScope :: TCvSubst -> TyCoBinder -> Type -> TCvSubst
extendTvSubstBinderAndInScope subst :: TCvSubst
subst (Named (Bndr v :: Id
v _)) ty :: Type
ty
= ASSERT( isTyVar v )
TCvSubst -> Id -> Type -> TCvSubst
extendTvSubstAndInScope TCvSubst
subst Id
v Type
ty
extendTvSubstBinderAndInScope subst :: TCvSubst
subst (Anon _) _
= TCvSubst
subst
extendTvSubstWithClone :: TCvSubst -> TyVar -> TyVar -> TCvSubst
extendTvSubstWithClone :: TCvSubst -> Id -> Id -> TCvSubst
extendTvSubstWithClone (TCvSubst in_scope :: InScopeSet
in_scope tenv :: TyVarEnv Type
tenv cenv :: CoVarEnv Coercion
cenv) tv :: Id
tv tv' :: Id
tv'
= InScopeSet -> TyVarEnv Type -> CoVarEnv Coercion -> TCvSubst
TCvSubst (InScopeSet -> VarSet -> InScopeSet
extendInScopeSetSet InScopeSet
in_scope VarSet
new_in_scope)
(TyVarEnv Type -> Id -> Type -> TyVarEnv Type
forall a. VarEnv a -> Id -> a -> VarEnv a
extendVarEnv TyVarEnv Type
tenv Id
tv (Id -> Type
mkTyVarTy Id
tv'))
CoVarEnv Coercion
cenv
where
new_in_scope :: VarSet
new_in_scope = Type -> VarSet
tyCoVarsOfType (Id -> Type
tyVarKind Id
tv') VarSet -> Id -> VarSet
`extendVarSet` Id
tv'
extendCvSubst :: TCvSubst -> CoVar -> Coercion -> TCvSubst
extendCvSubst :: TCvSubst -> Id -> Coercion -> TCvSubst
extendCvSubst (TCvSubst in_scope :: InScopeSet
in_scope tenv :: TyVarEnv Type
tenv cenv :: CoVarEnv Coercion
cenv) v :: Id
v co :: Coercion
co
= InScopeSet -> TyVarEnv Type -> CoVarEnv Coercion -> TCvSubst
TCvSubst InScopeSet
in_scope TyVarEnv Type
tenv (CoVarEnv Coercion -> Id -> Coercion -> CoVarEnv Coercion
forall a. VarEnv a -> Id -> a -> VarEnv a
extendVarEnv CoVarEnv Coercion
cenv Id
v Coercion
co)
extendCvSubstWithClone :: TCvSubst -> CoVar -> CoVar -> TCvSubst
extendCvSubstWithClone :: TCvSubst -> Id -> Id -> TCvSubst
extendCvSubstWithClone (TCvSubst in_scope :: InScopeSet
in_scope tenv :: TyVarEnv Type
tenv cenv :: CoVarEnv Coercion
cenv) cv :: Id
cv cv' :: Id
cv'
= InScopeSet -> TyVarEnv Type -> CoVarEnv Coercion -> TCvSubst
TCvSubst (InScopeSet -> VarSet -> InScopeSet
extendInScopeSetSet InScopeSet
in_scope VarSet
new_in_scope)
TyVarEnv Type
tenv
(CoVarEnv Coercion -> Id -> Coercion -> CoVarEnv Coercion
forall a. VarEnv a -> Id -> a -> VarEnv a
extendVarEnv CoVarEnv Coercion
cenv Id
cv (Id -> Coercion
mkCoVarCo Id
cv'))
where
new_in_scope :: VarSet
new_in_scope = Type -> VarSet
tyCoVarsOfType (Id -> Type
varType Id
cv') VarSet -> Id -> VarSet
`extendVarSet` Id
cv'
extendTvSubstAndInScope :: TCvSubst -> TyVar -> Type -> TCvSubst
extendTvSubstAndInScope :: TCvSubst -> Id -> Type -> TCvSubst
extendTvSubstAndInScope (TCvSubst in_scope :: InScopeSet
in_scope tenv :: TyVarEnv Type
tenv cenv :: CoVarEnv Coercion
cenv) tv :: Id
tv ty :: Type
ty
= InScopeSet -> TyVarEnv Type -> CoVarEnv Coercion -> TCvSubst
TCvSubst (InScopeSet
in_scope InScopeSet -> VarSet -> InScopeSet
`extendInScopeSetSet` Type -> VarSet
tyCoVarsOfType Type
ty)
(TyVarEnv Type -> Id -> Type -> TyVarEnv Type
forall a. VarEnv a -> Id -> a -> VarEnv a
extendVarEnv TyVarEnv Type
tenv Id
tv Type
ty)
CoVarEnv Coercion
cenv
extendTvSubstList :: TCvSubst -> [Var] -> [Type] -> TCvSubst
extendTvSubstList :: TCvSubst -> [Id] -> [Type] -> TCvSubst
extendTvSubstList subst :: TCvSubst
subst tvs :: [Id]
tvs tys :: [Type]
tys
= (TCvSubst -> Id -> Type -> TCvSubst)
-> TCvSubst -> [Id] -> [Type] -> TCvSubst
forall acc a b. (acc -> a -> b -> acc) -> acc -> [a] -> [b] -> acc
foldl2 TCvSubst -> Id -> Type -> TCvSubst
extendTvSubst TCvSubst
subst [Id]
tvs [Type]
tys
extendTCvSubstList :: TCvSubst -> [Var] -> [Type] -> TCvSubst
extendTCvSubstList :: TCvSubst -> [Id] -> [Type] -> TCvSubst
extendTCvSubstList subst :: TCvSubst
subst tvs :: [Id]
tvs tys :: [Type]
tys
= (TCvSubst -> Id -> Type -> TCvSubst)
-> TCvSubst -> [Id] -> [Type] -> TCvSubst
forall acc a b. (acc -> a -> b -> acc) -> acc -> [a] -> [b] -> acc
foldl2 TCvSubst -> Id -> Type -> TCvSubst
extendTCvSubst TCvSubst
subst [Id]
tvs [Type]
tys
unionTCvSubst :: TCvSubst -> TCvSubst -> TCvSubst
unionTCvSubst :: TCvSubst -> TCvSubst -> TCvSubst
unionTCvSubst (TCvSubst in_scope1 :: InScopeSet
in_scope1 tenv1 :: TyVarEnv Type
tenv1 cenv1 :: CoVarEnv Coercion
cenv1) (TCvSubst in_scope2 :: InScopeSet
in_scope2 tenv2 :: TyVarEnv Type
tenv2 cenv2 :: CoVarEnv Coercion
cenv2)
= ASSERT( not (tenv1 `intersectsVarEnv` tenv2)
&& not (cenv1 `intersectsVarEnv` cenv2) )
InScopeSet -> TyVarEnv Type -> CoVarEnv Coercion -> TCvSubst
TCvSubst (InScopeSet
in_scope1 InScopeSet -> InScopeSet -> InScopeSet
`unionInScope` InScopeSet
in_scope2)
(TyVarEnv Type
tenv1 TyVarEnv Type -> TyVarEnv Type -> TyVarEnv Type
forall a. VarEnv a -> VarEnv a -> VarEnv a
`plusVarEnv` TyVarEnv Type
tenv2)
(CoVarEnv Coercion
cenv1 CoVarEnv Coercion -> CoVarEnv Coercion -> CoVarEnv Coercion
forall a. VarEnv a -> VarEnv a -> VarEnv a
`plusVarEnv` CoVarEnv Coercion
cenv2)
zipTvSubst :: HasDebugCallStack => [TyVar] -> [Type] -> TCvSubst
zipTvSubst :: [Id] -> [Type] -> TCvSubst
zipTvSubst tvs :: [Id]
tvs tys :: [Type]
tys
= InScopeSet -> TyVarEnv Type -> TCvSubst
mkTvSubst (VarSet -> InScopeSet
mkInScopeSet ([Type] -> VarSet
tyCoVarsOfTypes [Type]
tys)) TyVarEnv Type
tenv
where
tenv :: TyVarEnv Type
tenv = [Id] -> [Type] -> TyVarEnv Type
HasDebugCallStack => [Id] -> [Type] -> TyVarEnv Type
zipTyEnv [Id]
tvs [Type]
tys
zipCvSubst :: HasDebugCallStack => [CoVar] -> [Coercion] -> TCvSubst
zipCvSubst :: [Id] -> [Coercion] -> TCvSubst
zipCvSubst cvs :: [Id]
cvs cos :: [Coercion]
cos
= InScopeSet -> TyVarEnv Type -> CoVarEnv Coercion -> TCvSubst
TCvSubst (VarSet -> InScopeSet
mkInScopeSet ([Coercion] -> VarSet
tyCoVarsOfCos [Coercion]
cos)) TyVarEnv Type
emptyTvSubstEnv CoVarEnv Coercion
cenv
where
cenv :: CoVarEnv Coercion
cenv = [Id] -> [Coercion] -> CoVarEnv Coercion
HasDebugCallStack => [Id] -> [Coercion] -> CoVarEnv Coercion
zipCoEnv [Id]
cvs [Coercion]
cos
zipTCvSubst :: HasDebugCallStack => [TyCoVar] -> [Type] -> TCvSubst
zipTCvSubst :: [Id] -> [Type] -> TCvSubst
zipTCvSubst tcvs :: [Id]
tcvs tys :: [Type]
tys
= [Id] -> [Type] -> TCvSubst -> TCvSubst
zip_tcvsubst [Id]
tcvs [Type]
tys (InScopeSet -> TCvSubst
mkEmptyTCvSubst (InScopeSet -> TCvSubst) -> InScopeSet -> TCvSubst
forall a b. (a -> b) -> a -> b
$ VarSet -> InScopeSet
mkInScopeSet ([Type] -> VarSet
tyCoVarsOfTypes [Type]
tys))
where zip_tcvsubst :: [TyCoVar] -> [Type] -> TCvSubst -> TCvSubst
zip_tcvsubst :: [Id] -> [Type] -> TCvSubst -> TCvSubst
zip_tcvsubst (tv :: Id
tv:tvs :: [Id]
tvs) (ty :: Type
ty:tys :: [Type]
tys) subst :: TCvSubst
subst
= [Id] -> [Type] -> TCvSubst -> TCvSubst
zip_tcvsubst [Id]
tvs [Type]
tys (TCvSubst -> Id -> Type -> TCvSubst
extendTCvSubst TCvSubst
subst Id
tv Type
ty)
zip_tcvsubst [] [] subst :: TCvSubst
subst = TCvSubst
subst
zip_tcvsubst _ _ _ = String -> SDoc -> TCvSubst
forall a. HasCallStack => String -> SDoc -> a
pprPanic "zipTCvSubst: length mismatch"
([Id] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [Id]
tcvs SDoc -> SDoc -> SDoc
<+> [Type] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [Type]
tys)
mkTvSubstPrs :: [(TyVar, Type)] -> TCvSubst
mkTvSubstPrs :: [(Id, Type)] -> TCvSubst
mkTvSubstPrs prs :: [(Id, Type)]
prs =
ASSERT2( onlyTyVarsAndNoCoercionTy, text "prs" <+> ppr prs )
InScopeSet -> TyVarEnv Type -> TCvSubst
mkTvSubst InScopeSet
in_scope TyVarEnv Type
tenv
where tenv :: TyVarEnv Type
tenv = [(Id, Type)] -> TyVarEnv Type
forall a. [(Id, a)] -> VarEnv a
mkVarEnv [(Id, Type)]
prs
in_scope :: InScopeSet
in_scope = VarSet -> InScopeSet
mkInScopeSet (VarSet -> InScopeSet) -> VarSet -> InScopeSet
forall a b. (a -> b) -> a -> b
$ [Type] -> VarSet
tyCoVarsOfTypes ([Type] -> VarSet) -> [Type] -> VarSet
forall a b. (a -> b) -> a -> b
$ ((Id, Type) -> Type) -> [(Id, Type)] -> [Type]
forall a b. (a -> b) -> [a] -> [b]
map (Id, Type) -> Type
forall a b. (a, b) -> b
snd [(Id, Type)]
prs
onlyTyVarsAndNoCoercionTy :: Bool
onlyTyVarsAndNoCoercionTy =
[Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
and [ Id -> Bool
isTyVar Id
tv Bool -> Bool -> Bool
&& Bool -> Bool
not (Type -> Bool
isCoercionTy Type
ty)
| (tv :: Id
tv, ty :: Type
ty) <- [(Id, Type)]
prs ]
zipTyEnv :: HasDebugCallStack => [TyVar] -> [Type] -> TvSubstEnv
zipTyEnv :: [Id] -> [Type] -> TyVarEnv Type
zipTyEnv tyvars :: [Id]
tyvars tys :: [Type]
tys
| Bool
debugIsOn
, Bool -> Bool
not ((Id -> Bool) -> [Id] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all Id -> Bool
isTyVar [Id]
tyvars)
= String -> SDoc -> TyVarEnv Type
forall a. HasCallStack => String -> SDoc -> a
pprPanic "zipTyEnv" ([Id] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [Id]
tyvars SDoc -> SDoc -> SDoc
<+> [Type] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [Type]
tys)
| Bool
otherwise
= ASSERT( all (not . isCoercionTy) tys )
[(Id, Type)] -> TyVarEnv Type
forall a. [(Id, a)] -> VarEnv a
mkVarEnv (String -> [Id] -> [Type] -> [(Id, Type)]
forall a b. String -> [a] -> [b] -> [(a, b)]
zipEqual "zipTyEnv" [Id]
tyvars [Type]
tys)
zipCoEnv :: HasDebugCallStack => [CoVar] -> [Coercion] -> CvSubstEnv
zipCoEnv :: [Id] -> [Coercion] -> CoVarEnv Coercion
zipCoEnv cvs :: [Id]
cvs cos :: [Coercion]
cos
| Bool
debugIsOn
, Bool -> Bool
not ((Id -> Bool) -> [Id] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all Id -> Bool
isCoVar [Id]
cvs)
= String -> SDoc -> CoVarEnv Coercion
forall a. HasCallStack => String -> SDoc -> a
pprPanic "zipCoEnv" ([Id] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [Id]
cvs SDoc -> SDoc -> SDoc
<+> [Coercion] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [Coercion]
cos)
| Bool
otherwise
= [(Id, Coercion)] -> CoVarEnv Coercion
forall a. [(Id, a)] -> VarEnv a
mkVarEnv (String -> [Id] -> [Coercion] -> [(Id, Coercion)]
forall a b. String -> [a] -> [b] -> [(a, b)]
zipEqual "zipCoEnv" [Id]
cvs [Coercion]
cos)
instance Outputable TCvSubst where
ppr :: TCvSubst -> SDoc
ppr (TCvSubst ins :: InScopeSet
ins tenv :: TyVarEnv Type
tenv cenv :: CoVarEnv Coercion
cenv)
= SDoc -> SDoc
brackets (SDoc -> SDoc) -> SDoc -> SDoc
forall a b. (a -> b) -> a -> b
$ [SDoc] -> SDoc
sep[ String -> SDoc
text "TCvSubst",
Int -> SDoc -> SDoc
nest 2 (String -> SDoc
text "In scope:" SDoc -> SDoc -> SDoc
<+> InScopeSet -> SDoc
forall a. Outputable a => a -> SDoc
ppr InScopeSet
ins),
Int -> SDoc -> SDoc
nest 2 (String -> SDoc
text "Type env:" SDoc -> SDoc -> SDoc
<+> TyVarEnv Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr TyVarEnv Type
tenv),
Int -> SDoc -> SDoc
nest 2 (String -> SDoc
text "Co env:" SDoc -> SDoc -> SDoc
<+> CoVarEnv Coercion -> SDoc
forall a. Outputable a => a -> SDoc
ppr CoVarEnv Coercion
cenv) ]
substTyWith :: HasCallStack => [TyVar] -> [Type] -> Type -> Type
substTyWith :: [Id] -> [Type] -> Type -> Type
substTyWith tvs :: [Id]
tvs tys :: [Type]
tys = {-#SCC "substTyWith" #-}
ASSERT( tvs `equalLength` tys )
HasCallStack => TCvSubst -> Type -> Type
TCvSubst -> Type -> Type
substTy ([Id] -> [Type] -> TCvSubst
HasDebugCallStack => [Id] -> [Type] -> TCvSubst
zipTvSubst [Id]
tvs [Type]
tys)
substTyWithUnchecked :: [TyVar] -> [Type] -> Type -> Type
substTyWithUnchecked :: [Id] -> [Type] -> Type -> Type
substTyWithUnchecked tvs :: [Id]
tvs tys :: [Type]
tys
= ASSERT( tvs `equalLength` tys )
TCvSubst -> Type -> Type
substTyUnchecked ([Id] -> [Type] -> TCvSubst
HasDebugCallStack => [Id] -> [Type] -> TCvSubst
zipTvSubst [Id]
tvs [Type]
tys)
substTyWithInScope :: InScopeSet -> [TyVar] -> [Type] -> Type -> Type
substTyWithInScope :: InScopeSet -> [Id] -> [Type] -> Type -> Type
substTyWithInScope in_scope :: InScopeSet
in_scope tvs :: [Id]
tvs tys :: [Type]
tys ty :: Type
ty =
ASSERT( tvs `equalLength` tys )
HasCallStack => TCvSubst -> Type -> Type
TCvSubst -> Type -> Type
substTy (InScopeSet -> TyVarEnv Type -> TCvSubst
mkTvSubst InScopeSet
in_scope TyVarEnv Type
tenv) Type
ty
where tenv :: TyVarEnv Type
tenv = [Id] -> [Type] -> TyVarEnv Type
HasDebugCallStack => [Id] -> [Type] -> TyVarEnv Type
zipTyEnv [Id]
tvs [Type]
tys
substCoWith :: HasCallStack => [TyVar] -> [Type] -> Coercion -> Coercion
substCoWith :: [Id] -> [Type] -> Coercion -> Coercion
substCoWith tvs :: [Id]
tvs tys :: [Type]
tys = ASSERT( tvs `equalLength` tys )
HasCallStack => TCvSubst -> Coercion -> Coercion
TCvSubst -> Coercion -> Coercion
substCo ([Id] -> [Type] -> TCvSubst
HasDebugCallStack => [Id] -> [Type] -> TCvSubst
zipTvSubst [Id]
tvs [Type]
tys)
substCoWithUnchecked :: [TyVar] -> [Type] -> Coercion -> Coercion
substCoWithUnchecked :: [Id] -> [Type] -> Coercion -> Coercion
substCoWithUnchecked tvs :: [Id]
tvs tys :: [Type]
tys
= ASSERT( tvs `equalLength` tys )
TCvSubst -> Coercion -> Coercion
substCoUnchecked ([Id] -> [Type] -> TCvSubst
HasDebugCallStack => [Id] -> [Type] -> TCvSubst
zipTvSubst [Id]
tvs [Type]
tys)
substTyWithCoVars :: [CoVar] -> [Coercion] -> Type -> Type
substTyWithCoVars :: [Id] -> [Coercion] -> Type -> Type
substTyWithCoVars cvs :: [Id]
cvs cos :: [Coercion]
cos = HasCallStack => TCvSubst -> Type -> Type
TCvSubst -> Type -> Type
substTy ([Id] -> [Coercion] -> TCvSubst
HasDebugCallStack => [Id] -> [Coercion] -> TCvSubst
zipCvSubst [Id]
cvs [Coercion]
cos)
substTysWith :: [TyVar] -> [Type] -> [Type] -> [Type]
substTysWith :: [Id] -> [Type] -> [Type] -> [Type]
substTysWith tvs :: [Id]
tvs tys :: [Type]
tys = ASSERT( tvs `equalLength` tys )
HasCallStack => TCvSubst -> [Type] -> [Type]
TCvSubst -> [Type] -> [Type]
substTys ([Id] -> [Type] -> TCvSubst
HasDebugCallStack => [Id] -> [Type] -> TCvSubst
zipTvSubst [Id]
tvs [Type]
tys)
substTysWithCoVars :: [CoVar] -> [Coercion] -> [Type] -> [Type]
substTysWithCoVars :: [Id] -> [Coercion] -> [Type] -> [Type]
substTysWithCoVars cvs :: [Id]
cvs cos :: [Coercion]
cos = ASSERT( cvs `equalLength` cos )
HasCallStack => TCvSubst -> [Type] -> [Type]
TCvSubst -> [Type] -> [Type]
substTys ([Id] -> [Coercion] -> TCvSubst
HasDebugCallStack => [Id] -> [Coercion] -> TCvSubst
zipCvSubst [Id]
cvs [Coercion]
cos)
substTyAddInScope :: TCvSubst -> Type -> Type
substTyAddInScope :: TCvSubst -> Type -> Type
substTyAddInScope subst :: TCvSubst
subst ty :: Type
ty =
HasCallStack => TCvSubst -> Type -> Type
TCvSubst -> Type -> Type
substTy (TCvSubst -> VarSet -> TCvSubst
extendTCvInScopeSet TCvSubst
subst (VarSet -> TCvSubst) -> VarSet -> TCvSubst
forall a b. (a -> b) -> a -> b
$ Type -> VarSet
tyCoVarsOfType Type
ty) Type
ty
isValidTCvSubst :: TCvSubst -> Bool
isValidTCvSubst :: TCvSubst -> Bool
isValidTCvSubst (TCvSubst in_scope :: InScopeSet
in_scope tenv :: TyVarEnv Type
tenv cenv :: CoVarEnv Coercion
cenv) =
(VarSet
tenvFVs VarSet -> InScopeSet -> Bool
`varSetInScope` InScopeSet
in_scope) Bool -> Bool -> Bool
&&
(VarSet
cenvFVs VarSet -> InScopeSet -> Bool
`varSetInScope` InScopeSet
in_scope)
where
tenvFVs :: VarSet
tenvFVs = TyVarEnv Type -> VarSet
tyCoVarsOfTypesSet TyVarEnv Type
tenv
cenvFVs :: VarSet
cenvFVs = CoVarEnv Coercion -> VarSet
tyCoVarsOfCosSet CoVarEnv Coercion
cenv
checkValidSubst :: HasCallStack => TCvSubst -> [Type] -> [Coercion] -> a -> a
checkValidSubst :: TCvSubst -> [Type] -> [Coercion] -> a -> a
checkValidSubst subst :: TCvSubst
subst@(TCvSubst in_scope :: InScopeSet
in_scope tenv :: TyVarEnv Type
tenv cenv :: CoVarEnv Coercion
cenv) tys :: [Type]
tys cos :: [Coercion]
cos a :: a
a
= WARN( not (isValidTCvSubst subst),
text "in_scope" <+> ppr in_scope $$
text "tenv" <+> ppr tenv $$
text "tenvFVs" <+> ppr (tyCoVarsOfTypesSet tenv) $$
text "cenv" <+> ppr cenv $$
text "cenvFVs" <+> ppr (tyCoVarsOfCosSet cenv) $$
text "tys" <+> ppr tys $$
text "cos" <+> ppr cos )
WARN( not tysCosFVsInScope,
text "in_scope" <+> ppr in_scope $$
text "tenv" <+> ppr tenv $$
text "cenv" <+> ppr cenv $$
text "tys" <+> ppr tys $$
text "cos" <+> ppr cos $$
text "needInScope" <+> ppr needInScope )
a
a
where
substDomain :: [Unique]
substDomain = TyVarEnv Type -> [Unique]
forall elt. UniqFM elt -> [Unique]
nonDetKeysUFM TyVarEnv Type
tenv [Unique] -> [Unique] -> [Unique]
forall a. [a] -> [a] -> [a]
++ CoVarEnv Coercion -> [Unique]
forall elt. UniqFM elt -> [Unique]
nonDetKeysUFM CoVarEnv Coercion
cenv
needInScope :: VarSet
needInScope = ([Type] -> VarSet
tyCoVarsOfTypes [Type]
tys VarSet -> VarSet -> VarSet
`unionVarSet` [Coercion] -> VarSet
tyCoVarsOfCos [Coercion]
cos)
VarSet -> [Unique] -> VarSet
forall a. UniqSet a -> [Unique] -> UniqSet a
`delListFromUniqSet_Directly` [Unique]
substDomain
tysCosFVsInScope :: Bool
tysCosFVsInScope = VarSet
needInScope VarSet -> InScopeSet -> Bool
`varSetInScope` InScopeSet
in_scope
substTy :: HasCallStack => TCvSubst -> Type -> Type
substTy :: TCvSubst -> Type -> Type
substTy subst :: TCvSubst
subst ty :: Type
ty
| TCvSubst -> Bool
isEmptyTCvSubst TCvSubst
subst = Type
ty
| Bool
otherwise = TCvSubst -> [Type] -> [Coercion] -> Type -> Type
forall a.
HasCallStack =>
TCvSubst -> [Type] -> [Coercion] -> a -> a
checkValidSubst TCvSubst
subst [Type
ty] [] (Type -> Type) -> Type -> Type
forall a b. (a -> b) -> a -> b
$
TCvSubst -> Type -> Type
subst_ty TCvSubst
subst Type
ty
substTyUnchecked :: TCvSubst -> Type -> Type
substTyUnchecked :: TCvSubst -> Type -> Type
substTyUnchecked subst :: TCvSubst
subst ty :: Type
ty
| TCvSubst -> Bool
isEmptyTCvSubst TCvSubst
subst = Type
ty
| Bool
otherwise = TCvSubst -> Type -> Type
subst_ty TCvSubst
subst Type
ty
substTys :: HasCallStack => TCvSubst -> [Type] -> [Type]
substTys :: TCvSubst -> [Type] -> [Type]
substTys subst :: TCvSubst
subst tys :: [Type]
tys
| TCvSubst -> Bool
isEmptyTCvSubst TCvSubst
subst = [Type]
tys
| Bool
otherwise = TCvSubst -> [Type] -> [Coercion] -> [Type] -> [Type]
forall a.
HasCallStack =>
TCvSubst -> [Type] -> [Coercion] -> a -> a
checkValidSubst TCvSubst
subst [Type]
tys [] ([Type] -> [Type]) -> [Type] -> [Type]
forall a b. (a -> b) -> a -> b
$ (Type -> Type) -> [Type] -> [Type]
forall a b. (a -> b) -> [a] -> [b]
map (TCvSubst -> Type -> Type
subst_ty TCvSubst
subst) [Type]
tys
substTysUnchecked :: TCvSubst -> [Type] -> [Type]
substTysUnchecked :: TCvSubst -> [Type] -> [Type]
substTysUnchecked subst :: TCvSubst
subst tys :: [Type]
tys
| TCvSubst -> Bool
isEmptyTCvSubst TCvSubst
subst = [Type]
tys
| Bool
otherwise = (Type -> Type) -> [Type] -> [Type]
forall a b. (a -> b) -> [a] -> [b]
map (TCvSubst -> Type -> Type
subst_ty TCvSubst
subst) [Type]
tys
substTheta :: HasCallStack => TCvSubst -> ThetaType -> ThetaType
substTheta :: TCvSubst -> [Type] -> [Type]
substTheta = HasCallStack => TCvSubst -> [Type] -> [Type]
TCvSubst -> [Type] -> [Type]
substTys
substThetaUnchecked :: TCvSubst -> ThetaType -> ThetaType
substThetaUnchecked :: TCvSubst -> [Type] -> [Type]
substThetaUnchecked = TCvSubst -> [Type] -> [Type]
substTysUnchecked
subst_ty :: TCvSubst -> Type -> Type
subst_ty :: TCvSubst -> Type -> Type
subst_ty subst :: TCvSubst
subst ty :: Type
ty
= Type -> Type
go Type
ty
where
go :: Type -> Type
go (TyVarTy tv :: Id
tv) = TCvSubst -> Id -> Type
substTyVar TCvSubst
subst Id
tv
go (AppTy fun :: Type
fun arg :: Type
arg) = Type -> Type -> Type
mkAppTy (Type -> Type
go Type
fun) (Type -> Type) -> Type -> Type
forall a b. (a -> b) -> a -> b
$! (Type -> Type
go Type
arg)
go (TyConApp tc :: TyCon
tc tys :: [Type]
tys) = let args :: [Type]
args = (Type -> Type) -> [Type] -> [Type]
forall a b. (a -> b) -> [a] -> [b]
map Type -> Type
go [Type]
tys
in [Type]
args [Type] -> Type -> Type
forall a b. [a] -> b -> b
`seqList` TyCon -> [Type] -> Type
TyConApp TyCon
tc [Type]
args
go (FunTy arg :: Type
arg res :: Type
res) = (Type -> Type -> Type
FunTy (Type -> Type -> Type) -> Type -> Type -> Type
forall a b. (a -> b) -> a -> b
$! Type -> Type
go Type
arg) (Type -> Type) -> Type -> Type
forall a b. (a -> b) -> a -> b
$! Type -> Type
go Type
res
go (ForAllTy (Bndr tv :: Id
tv vis :: ArgFlag
vis) ty :: Type
ty)
= case TCvSubst -> Id -> (TCvSubst, Id)
substVarBndrUnchecked TCvSubst
subst Id
tv of
(subst' :: TCvSubst
subst', tv' :: Id
tv') ->
(TyCoVarBinder -> Type -> Type
ForAllTy (TyCoVarBinder -> Type -> Type) -> TyCoVarBinder -> Type -> Type
forall a b. (a -> b) -> a -> b
$! ((Id -> ArgFlag -> TyCoVarBinder
forall var argf. var -> argf -> VarBndr var argf
Bndr (Id -> ArgFlag -> TyCoVarBinder) -> Id -> ArgFlag -> TyCoVarBinder
forall a b. (a -> b) -> a -> b
$! Id
tv') ArgFlag
vis)) (Type -> Type) -> Type -> Type
forall a b. (a -> b) -> a -> b
$!
(TCvSubst -> Type -> Type
subst_ty TCvSubst
subst' Type
ty)
go (LitTy n :: TyLit
n) = TyLit -> Type
LitTy (TyLit -> Type) -> TyLit -> Type
forall a b. (a -> b) -> a -> b
$! TyLit
n
go (CastTy ty :: Type
ty co :: Coercion
co) = (Type -> Coercion -> Type
mkCastTy (Type -> Coercion -> Type) -> Type -> Coercion -> Type
forall a b. (a -> b) -> a -> b
$! (Type -> Type
go Type
ty)) (Coercion -> Type) -> Coercion -> Type
forall a b. (a -> b) -> a -> b
$! (TCvSubst -> Coercion -> Coercion
subst_co TCvSubst
subst Coercion
co)
go (CoercionTy co :: Coercion
co) = Coercion -> Type
CoercionTy (Coercion -> Type) -> Coercion -> Type
forall a b. (a -> b) -> a -> b
$! (TCvSubst -> Coercion -> Coercion
subst_co TCvSubst
subst Coercion
co)
substTyVar :: TCvSubst -> TyVar -> Type
substTyVar :: TCvSubst -> Id -> Type
substTyVar (TCvSubst _ tenv :: TyVarEnv Type
tenv _) tv :: Id
tv
= ASSERT( isTyVar tv )
case TyVarEnv Type -> Id -> Maybe Type
forall a. VarEnv a -> Id -> Maybe a
lookupVarEnv TyVarEnv Type
tenv Id
tv of
Just ty :: Type
ty -> Type
ty
Nothing -> Id -> Type
TyVarTy Id
tv
substTyVars :: TCvSubst -> [TyVar] -> [Type]
substTyVars :: TCvSubst -> [Id] -> [Type]
substTyVars subst :: TCvSubst
subst = (Id -> Type) -> [Id] -> [Type]
forall a b. (a -> b) -> [a] -> [b]
map ((Id -> Type) -> [Id] -> [Type]) -> (Id -> Type) -> [Id] -> [Type]
forall a b. (a -> b) -> a -> b
$ TCvSubst -> Id -> Type
substTyVar TCvSubst
subst
substTyCoVars :: TCvSubst -> [TyCoVar] -> [Type]
substTyCoVars :: TCvSubst -> [Id] -> [Type]
substTyCoVars subst :: TCvSubst
subst = (Id -> Type) -> [Id] -> [Type]
forall a b. (a -> b) -> [a] -> [b]
map ((Id -> Type) -> [Id] -> [Type]) -> (Id -> Type) -> [Id] -> [Type]
forall a b. (a -> b) -> a -> b
$ TCvSubst -> Id -> Type
substTyCoVar TCvSubst
subst
substTyCoVar :: TCvSubst -> TyCoVar -> Type
substTyCoVar :: TCvSubst -> Id -> Type
substTyCoVar subst :: TCvSubst
subst tv :: Id
tv
| Id -> Bool
isTyVar Id
tv = TCvSubst -> Id -> Type
substTyVar TCvSubst
subst Id
tv
| Bool
otherwise = Coercion -> Type
CoercionTy (Coercion -> Type) -> Coercion -> Type
forall a b. (a -> b) -> a -> b
$ TCvSubst -> Id -> Coercion
substCoVar TCvSubst
subst Id
tv
lookupTyVar :: TCvSubst -> TyVar -> Maybe Type
lookupTyVar :: TCvSubst -> Id -> Maybe Type
lookupTyVar (TCvSubst _ tenv :: TyVarEnv Type
tenv _) tv :: Id
tv
= ASSERT( isTyVar tv )
TyVarEnv Type -> Id -> Maybe Type
forall a. VarEnv a -> Id -> Maybe a
lookupVarEnv TyVarEnv Type
tenv Id
tv
substCo :: HasCallStack => TCvSubst -> Coercion -> Coercion
substCo :: TCvSubst -> Coercion -> Coercion
substCo subst :: TCvSubst
subst co :: Coercion
co
| TCvSubst -> Bool
isEmptyTCvSubst TCvSubst
subst = Coercion
co
| Bool
otherwise = TCvSubst -> [Type] -> [Coercion] -> Coercion -> Coercion
forall a.
HasCallStack =>
TCvSubst -> [Type] -> [Coercion] -> a -> a
checkValidSubst TCvSubst
subst [] [Coercion
co] (Coercion -> Coercion) -> Coercion -> Coercion
forall a b. (a -> b) -> a -> b
$ TCvSubst -> Coercion -> Coercion
subst_co TCvSubst
subst Coercion
co
substCoUnchecked :: TCvSubst -> Coercion -> Coercion
substCoUnchecked :: TCvSubst -> Coercion -> Coercion
substCoUnchecked subst :: TCvSubst
subst co :: Coercion
co
| TCvSubst -> Bool
isEmptyTCvSubst TCvSubst
subst = Coercion
co
| Bool
otherwise = TCvSubst -> Coercion -> Coercion
subst_co TCvSubst
subst Coercion
co
substCos :: HasCallStack => TCvSubst -> [Coercion] -> [Coercion]
substCos :: TCvSubst -> [Coercion] -> [Coercion]
substCos subst :: TCvSubst
subst cos :: [Coercion]
cos
| TCvSubst -> Bool
isEmptyTCvSubst TCvSubst
subst = [Coercion]
cos
| Bool
otherwise = TCvSubst -> [Type] -> [Coercion] -> [Coercion] -> [Coercion]
forall a.
HasCallStack =>
TCvSubst -> [Type] -> [Coercion] -> a -> a
checkValidSubst TCvSubst
subst [] [Coercion]
cos ([Coercion] -> [Coercion]) -> [Coercion] -> [Coercion]
forall a b. (a -> b) -> a -> b
$ (Coercion -> Coercion) -> [Coercion] -> [Coercion]
forall a b. (a -> b) -> [a] -> [b]
map (TCvSubst -> Coercion -> Coercion
subst_co TCvSubst
subst) [Coercion]
cos
subst_co :: TCvSubst -> Coercion -> Coercion
subst_co :: TCvSubst -> Coercion -> Coercion
subst_co subst :: TCvSubst
subst co :: Coercion
co
= Coercion -> Coercion
go Coercion
co
where
go_ty :: Type -> Type
go_ty :: Type -> Type
go_ty = TCvSubst -> Type -> Type
subst_ty TCvSubst
subst
go_mco :: MCoercion -> MCoercion
go_mco :: MCoercion -> MCoercion
go_mco MRefl = MCoercion
MRefl
go_mco (MCo co :: Coercion
co) = Coercion -> MCoercion
MCo (Coercion -> Coercion
go Coercion
co)
go :: Coercion -> Coercion
go :: Coercion -> Coercion
go (Refl ty :: Type
ty) = Type -> Coercion
mkNomReflCo (Type -> Coercion) -> Type -> Coercion
forall a b. (a -> b) -> a -> b
$! (Type -> Type
go_ty Type
ty)
go (GRefl r :: Role
r ty :: Type
ty mco :: MCoercion
mco) = (Role -> Type -> MCoercion -> Coercion
mkGReflCo Role
r (Type -> MCoercion -> Coercion) -> Type -> MCoercion -> Coercion
forall a b. (a -> b) -> a -> b
$! (Type -> Type
go_ty Type
ty)) (MCoercion -> Coercion) -> MCoercion -> Coercion
forall a b. (a -> b) -> a -> b
$! (MCoercion -> MCoercion
go_mco MCoercion
mco)
go (TyConAppCo r :: Role
r tc :: TyCon
tc args :: [Coercion]
args)= let args' :: [Coercion]
args' = (Coercion -> Coercion) -> [Coercion] -> [Coercion]
forall a b. (a -> b) -> [a] -> [b]
map Coercion -> Coercion
go [Coercion]
args
in [Coercion]
args' [Coercion] -> Coercion -> Coercion
forall a b. [a] -> b -> b
`seqList` HasDebugCallStack => Role -> TyCon -> [Coercion] -> Coercion
Role -> TyCon -> [Coercion] -> Coercion
mkTyConAppCo Role
r TyCon
tc [Coercion]
args'
go (AppCo co :: Coercion
co arg :: Coercion
arg) = (Coercion -> Coercion -> Coercion
mkAppCo (Coercion -> Coercion -> Coercion)
-> Coercion -> Coercion -> Coercion
forall a b. (a -> b) -> a -> b
$! Coercion -> Coercion
go Coercion
co) (Coercion -> Coercion) -> Coercion -> Coercion
forall a b. (a -> b) -> a -> b
$! Coercion -> Coercion
go Coercion
arg
go (ForAllCo tv :: Id
tv kind_co :: Coercion
kind_co co :: Coercion
co)
= case TCvSubst -> Id -> Coercion -> (TCvSubst, Id, Coercion)
substForAllCoBndrUnchecked TCvSubst
subst Id
tv Coercion
kind_co of
(subst' :: TCvSubst
subst', tv' :: Id
tv', kind_co' :: Coercion
kind_co') ->
((Id -> Coercion -> Coercion -> Coercion
mkForAllCo (Id -> Coercion -> Coercion -> Coercion)
-> Id -> Coercion -> Coercion -> Coercion
forall a b. (a -> b) -> a -> b
$! Id
tv') (Coercion -> Coercion -> Coercion)
-> Coercion -> Coercion -> Coercion
forall a b. (a -> b) -> a -> b
$! Coercion
kind_co') (Coercion -> Coercion) -> Coercion -> Coercion
forall a b. (a -> b) -> a -> b
$! TCvSubst -> Coercion -> Coercion
subst_co TCvSubst
subst' Coercion
co
go (FunCo r :: Role
r co1 :: Coercion
co1 co2 :: Coercion
co2) = (Role -> Coercion -> Coercion -> Coercion
mkFunCo Role
r (Coercion -> Coercion -> Coercion)
-> Coercion -> Coercion -> Coercion
forall a b. (a -> b) -> a -> b
$! Coercion -> Coercion
go Coercion
co1) (Coercion -> Coercion) -> Coercion -> Coercion
forall a b. (a -> b) -> a -> b
$! Coercion -> Coercion
go Coercion
co2
go (CoVarCo cv :: Id
cv) = TCvSubst -> Id -> Coercion
substCoVar TCvSubst
subst Id
cv
go (AxiomInstCo con :: CoAxiom Branched
con ind :: Int
ind cos :: [Coercion]
cos) = CoAxiom Branched -> Int -> [Coercion] -> Coercion
mkAxiomInstCo CoAxiom Branched
con Int
ind ([Coercion] -> Coercion) -> [Coercion] -> Coercion
forall a b. (a -> b) -> a -> b
$! (Coercion -> Coercion) -> [Coercion] -> [Coercion]
forall a b. (a -> b) -> [a] -> [b]
map Coercion -> Coercion
go [Coercion]
cos
go (UnivCo p :: UnivCoProvenance
p r :: Role
r t1 :: Type
t1 t2 :: Type
t2) = (((UnivCoProvenance -> Role -> Type -> Type -> Coercion
mkUnivCo (UnivCoProvenance -> Role -> Type -> Type -> Coercion)
-> UnivCoProvenance -> Role -> Type -> Type -> Coercion
forall a b. (a -> b) -> a -> b
$! UnivCoProvenance -> UnivCoProvenance
go_prov UnivCoProvenance
p) (Role -> Type -> Type -> Coercion)
-> Role -> Type -> Type -> Coercion
forall a b. (a -> b) -> a -> b
$! Role
r) (Type -> Type -> Coercion) -> Type -> Type -> Coercion
forall a b. (a -> b) -> a -> b
$!
(Type -> Type
go_ty Type
t1)) (Type -> Coercion) -> Type -> Coercion
forall a b. (a -> b) -> a -> b
$! (Type -> Type
go_ty Type
t2)
go (SymCo co :: Coercion
co) = Coercion -> Coercion
mkSymCo (Coercion -> Coercion) -> Coercion -> Coercion
forall a b. (a -> b) -> a -> b
$! (Coercion -> Coercion
go Coercion
co)
go (TransCo co1 :: Coercion
co1 co2 :: Coercion
co2) = (Coercion -> Coercion -> Coercion
mkTransCo (Coercion -> Coercion -> Coercion)
-> Coercion -> Coercion -> Coercion
forall a b. (a -> b) -> a -> b
$! (Coercion -> Coercion
go Coercion
co1)) (Coercion -> Coercion) -> Coercion -> Coercion
forall a b. (a -> b) -> a -> b
$! (Coercion -> Coercion
go Coercion
co2)
go (NthCo r :: Role
r d :: Int
d co :: Coercion
co) = HasDebugCallStack => Role -> Int -> Coercion -> Coercion
Role -> Int -> Coercion -> Coercion
mkNthCo Role
r Int
d (Coercion -> Coercion) -> Coercion -> Coercion
forall a b. (a -> b) -> a -> b
$! (Coercion -> Coercion
go Coercion
co)
go (LRCo lr :: LeftOrRight
lr co :: Coercion
co) = LeftOrRight -> Coercion -> Coercion
mkLRCo LeftOrRight
lr (Coercion -> Coercion) -> Coercion -> Coercion
forall a b. (a -> b) -> a -> b
$! (Coercion -> Coercion
go Coercion
co)
go (InstCo co :: Coercion
co arg :: Coercion
arg) = (Coercion -> Coercion -> Coercion
mkInstCo (Coercion -> Coercion -> Coercion)
-> Coercion -> Coercion -> Coercion
forall a b. (a -> b) -> a -> b
$! (Coercion -> Coercion
go Coercion
co)) (Coercion -> Coercion) -> Coercion -> Coercion
forall a b. (a -> b) -> a -> b
$! Coercion -> Coercion
go Coercion
arg
go (KindCo co :: Coercion
co) = Coercion -> Coercion
mkKindCo (Coercion -> Coercion) -> Coercion -> Coercion
forall a b. (a -> b) -> a -> b
$! (Coercion -> Coercion
go Coercion
co)
go (SubCo co :: Coercion
co) = Coercion -> Coercion
mkSubCo (Coercion -> Coercion) -> Coercion -> Coercion
forall a b. (a -> b) -> a -> b
$! (Coercion -> Coercion
go Coercion
co)
go (AxiomRuleCo c :: CoAxiomRule
c cs :: [Coercion]
cs) = let cs1 :: [Coercion]
cs1 = (Coercion -> Coercion) -> [Coercion] -> [Coercion]
forall a b. (a -> b) -> [a] -> [b]
map Coercion -> Coercion
go [Coercion]
cs
in [Coercion]
cs1 [Coercion] -> Coercion -> Coercion
forall a b. [a] -> b -> b
`seqList` CoAxiomRule -> [Coercion] -> Coercion
AxiomRuleCo CoAxiomRule
c [Coercion]
cs1
go (HoleCo h :: CoercionHole
h) = CoercionHole -> Coercion
HoleCo (CoercionHole -> Coercion) -> CoercionHole -> Coercion
forall a b. (a -> b) -> a -> b
$! CoercionHole -> CoercionHole
go_hole CoercionHole
h
go_prov :: UnivCoProvenance -> UnivCoProvenance
go_prov UnsafeCoerceProv = UnivCoProvenance
UnsafeCoerceProv
go_prov (PhantomProv kco :: Coercion
kco) = Coercion -> UnivCoProvenance
PhantomProv (Coercion -> Coercion
go Coercion
kco)
go_prov (ProofIrrelProv kco :: Coercion
kco) = Coercion -> UnivCoProvenance
ProofIrrelProv (Coercion -> Coercion
go Coercion
kco)
go_prov p :: UnivCoProvenance
p@(PluginProv _) = UnivCoProvenance
p
go_hole :: CoercionHole -> CoercionHole
go_hole h :: CoercionHole
h@(CoercionHole { ch_co_var :: CoercionHole -> Id
ch_co_var = Id
cv })
= CoercionHole
h { ch_co_var :: Id
ch_co_var = (Type -> Type) -> Id -> Id
updateVarType Type -> Type
go_ty Id
cv }
substForAllCoBndr :: TCvSubst -> TyCoVar -> KindCoercion
-> (TCvSubst, TyCoVar, Coercion)
substForAllCoBndr :: TCvSubst -> Id -> Coercion -> (TCvSubst, Id, Coercion)
substForAllCoBndr subst :: TCvSubst
subst
= Bool
-> (Coercion -> Coercion)
-> TCvSubst
-> Id
-> Coercion
-> (TCvSubst, Id, Coercion)
substForAllCoBndrUsing Bool
False (HasCallStack => TCvSubst -> Coercion -> Coercion
TCvSubst -> Coercion -> Coercion
substCo TCvSubst
subst) TCvSubst
subst
substForAllCoBndrUnchecked :: TCvSubst -> TyCoVar -> KindCoercion
-> (TCvSubst, TyCoVar, Coercion)
substForAllCoBndrUnchecked :: TCvSubst -> Id -> Coercion -> (TCvSubst, Id, Coercion)
substForAllCoBndrUnchecked subst :: TCvSubst
subst
= Bool
-> (Coercion -> Coercion)
-> TCvSubst
-> Id
-> Coercion
-> (TCvSubst, Id, Coercion)
substForAllCoBndrUsing Bool
False (TCvSubst -> Coercion -> Coercion
substCoUnchecked TCvSubst
subst) TCvSubst
subst
substForAllCoBndrUsing :: Bool
-> (Coercion -> Coercion)
-> TCvSubst -> TyCoVar -> KindCoercion
-> (TCvSubst, TyCoVar, KindCoercion)
substForAllCoBndrUsing :: Bool
-> (Coercion -> Coercion)
-> TCvSubst
-> Id
-> Coercion
-> (TCvSubst, Id, Coercion)
substForAllCoBndrUsing sym :: Bool
sym sco :: Coercion -> Coercion
sco subst :: TCvSubst
subst old_var :: Id
old_var
| Id -> Bool
isTyVar Id
old_var = Bool
-> (Coercion -> Coercion)
-> TCvSubst
-> Id
-> Coercion
-> (TCvSubst, Id, Coercion)
substForAllCoTyVarBndrUsing Bool
sym Coercion -> Coercion
sco TCvSubst
subst Id
old_var
| Bool
otherwise = Bool
-> (Coercion -> Coercion)
-> TCvSubst
-> Id
-> Coercion
-> (TCvSubst, Id, Coercion)
substForAllCoCoVarBndrUsing Bool
sym Coercion -> Coercion
sco TCvSubst
subst Id
old_var
substForAllCoTyVarBndrUsing :: Bool
-> (Coercion -> Coercion)
-> TCvSubst -> TyVar -> KindCoercion
-> (TCvSubst, TyVar, KindCoercion)
substForAllCoTyVarBndrUsing :: Bool
-> (Coercion -> Coercion)
-> TCvSubst
-> Id
-> Coercion
-> (TCvSubst, Id, Coercion)
substForAllCoTyVarBndrUsing sym :: Bool
sym sco :: Coercion -> Coercion
sco (TCvSubst in_scope :: InScopeSet
in_scope tenv :: TyVarEnv Type
tenv cenv :: CoVarEnv Coercion
cenv) old_var :: Id
old_var old_kind_co :: Coercion
old_kind_co
= ASSERT( isTyVar old_var )
( InScopeSet -> TyVarEnv Type -> CoVarEnv Coercion -> TCvSubst
TCvSubst (InScopeSet
in_scope InScopeSet -> Id -> InScopeSet
`extendInScopeSet` Id
new_var) TyVarEnv Type
new_env CoVarEnv Coercion
cenv
, Id
new_var, Coercion
new_kind_co )
where
new_env :: TyVarEnv Type
new_env | Bool
no_change Bool -> Bool -> Bool
&& Bool -> Bool
not Bool
sym = TyVarEnv Type -> Id -> TyVarEnv Type
forall a. VarEnv a -> Id -> VarEnv a
delVarEnv TyVarEnv Type
tenv Id
old_var
| Bool
sym = TyVarEnv Type -> Id -> Type -> TyVarEnv Type
forall a. VarEnv a -> Id -> a -> VarEnv a
extendVarEnv TyVarEnv Type
tenv Id
old_var (Type -> TyVarEnv Type) -> Type -> TyVarEnv Type
forall a b. (a -> b) -> a -> b
$
Id -> Type
TyVarTy Id
new_var Type -> Coercion -> Type
`CastTy` Coercion
new_kind_co
| Bool
otherwise = TyVarEnv Type -> Id -> Type -> TyVarEnv Type
forall a. VarEnv a -> Id -> a -> VarEnv a
extendVarEnv TyVarEnv Type
tenv Id
old_var (Id -> Type
TyVarTy Id
new_var)
no_kind_change :: Bool
no_kind_change = Coercion -> Bool
noFreeVarsOfCo Coercion
old_kind_co
no_change :: Bool
no_change = Bool
no_kind_change Bool -> Bool -> Bool
&& (Id
new_var Id -> Id -> Bool
forall a. Eq a => a -> a -> Bool
== Id
old_var)
new_kind_co :: Coercion
new_kind_co | Bool
no_kind_change = Coercion
old_kind_co
| Bool
otherwise = Coercion -> Coercion
sco Coercion
old_kind_co
Pair new_ki1 :: Type
new_ki1 _ = Coercion -> Pair Type
coercionKind Coercion
new_kind_co
new_var :: Id
new_var = InScopeSet -> Id -> Id
uniqAway InScopeSet
in_scope (Id -> Type -> Id
setTyVarKind Id
old_var Type
new_ki1)
substForAllCoCoVarBndrUsing :: Bool
-> (Coercion -> Coercion)
-> TCvSubst -> CoVar -> KindCoercion
-> (TCvSubst, CoVar, KindCoercion)
substForAllCoCoVarBndrUsing :: Bool
-> (Coercion -> Coercion)
-> TCvSubst
-> Id
-> Coercion
-> (TCvSubst, Id, Coercion)
substForAllCoCoVarBndrUsing sym :: Bool
sym sco :: Coercion -> Coercion
sco (TCvSubst in_scope :: InScopeSet
in_scope tenv :: TyVarEnv Type
tenv cenv :: CoVarEnv Coercion
cenv)
old_var :: Id
old_var old_kind_co :: Coercion
old_kind_co
= ASSERT( isCoVar old_var )
( InScopeSet -> TyVarEnv Type -> CoVarEnv Coercion -> TCvSubst
TCvSubst (InScopeSet
in_scope InScopeSet -> Id -> InScopeSet
`extendInScopeSet` Id
new_var) TyVarEnv Type
tenv CoVarEnv Coercion
new_cenv
, Id
new_var, Coercion
new_kind_co )
where
new_cenv :: CoVarEnv Coercion
new_cenv | Bool
no_change Bool -> Bool -> Bool
&& Bool -> Bool
not Bool
sym = CoVarEnv Coercion -> Id -> CoVarEnv Coercion
forall a. VarEnv a -> Id -> VarEnv a
delVarEnv CoVarEnv Coercion
cenv Id
old_var
| Bool
otherwise = CoVarEnv Coercion -> Id -> Coercion -> CoVarEnv Coercion
forall a. VarEnv a -> Id -> a -> VarEnv a
extendVarEnv CoVarEnv Coercion
cenv Id
old_var (Id -> Coercion
mkCoVarCo Id
new_var)
no_kind_change :: Bool
no_kind_change = Coercion -> Bool
noFreeVarsOfCo Coercion
old_kind_co
no_change :: Bool
no_change = Bool
no_kind_change Bool -> Bool -> Bool
&& (Id
new_var Id -> Id -> Bool
forall a. Eq a => a -> a -> Bool
== Id
old_var)
new_kind_co :: Coercion
new_kind_co | Bool
no_kind_change = Coercion
old_kind_co
| Bool
otherwise = Coercion -> Coercion
sco Coercion
old_kind_co
Pair h1 :: Type
h1 h2 :: Type
h2 = Coercion -> Pair Type
coercionKind Coercion
new_kind_co
new_var :: Id
new_var = InScopeSet -> Id -> Id
uniqAway InScopeSet
in_scope (Id -> Id) -> Id -> Id
forall a b. (a -> b) -> a -> b
$ Name -> Type -> Id
mkCoVar (Id -> Name
varName Id
old_var) Type
new_var_type
new_var_type :: Type
new_var_type | Bool
sym = Type
h2
| Bool
otherwise = Type
h1
substCoVar :: TCvSubst -> CoVar -> Coercion
substCoVar :: TCvSubst -> Id -> Coercion
substCoVar (TCvSubst _ _ cenv :: CoVarEnv Coercion
cenv) cv :: Id
cv
= case CoVarEnv Coercion -> Id -> Maybe Coercion
forall a. VarEnv a -> Id -> Maybe a
lookupVarEnv CoVarEnv Coercion
cenv Id
cv of
Just co :: Coercion
co -> Coercion
co
Nothing -> Id -> Coercion
CoVarCo Id
cv
substCoVars :: TCvSubst -> [CoVar] -> [Coercion]
substCoVars :: TCvSubst -> [Id] -> [Coercion]
substCoVars subst :: TCvSubst
subst cvs :: [Id]
cvs = (Id -> Coercion) -> [Id] -> [Coercion]
forall a b. (a -> b) -> [a] -> [b]
map (TCvSubst -> Id -> Coercion
substCoVar TCvSubst
subst) [Id]
cvs
lookupCoVar :: TCvSubst -> Var -> Maybe Coercion
lookupCoVar :: TCvSubst -> Id -> Maybe Coercion
lookupCoVar (TCvSubst _ _ cenv :: CoVarEnv Coercion
cenv) v :: Id
v = CoVarEnv Coercion -> Id -> Maybe Coercion
forall a. VarEnv a -> Id -> Maybe a
lookupVarEnv CoVarEnv Coercion
cenv Id
v
substTyVarBndr :: HasCallStack => TCvSubst -> TyVar -> (TCvSubst, TyVar)
substTyVarBndr :: TCvSubst -> Id -> (TCvSubst, Id)
substTyVarBndr = (TCvSubst -> Type -> Type) -> TCvSubst -> Id -> (TCvSubst, Id)
substTyVarBndrUsing HasCallStack => TCvSubst -> Type -> Type
TCvSubst -> Type -> Type
substTy
substTyVarBndrs :: HasCallStack => TCvSubst -> [TyVar] -> (TCvSubst, [TyVar])
substTyVarBndrs :: TCvSubst -> [Id] -> (TCvSubst, [Id])
substTyVarBndrs = (TCvSubst -> Id -> (TCvSubst, Id))
-> TCvSubst -> [Id] -> (TCvSubst, [Id])
forall (t :: * -> *) a b c.
Traversable t =>
(a -> b -> (a, c)) -> a -> t b -> (a, t c)
mapAccumL HasCallStack => TCvSubst -> Id -> (TCvSubst, Id)
TCvSubst -> Id -> (TCvSubst, Id)
substTyVarBndr
substVarBndr :: HasCallStack => TCvSubst -> TyCoVar -> (TCvSubst, TyCoVar)
substVarBndr :: TCvSubst -> Id -> (TCvSubst, Id)
substVarBndr = (TCvSubst -> Type -> Type) -> TCvSubst -> Id -> (TCvSubst, Id)
substVarBndrUsing HasCallStack => TCvSubst -> Type -> Type
TCvSubst -> Type -> Type
substTy
substVarBndrs :: HasCallStack => TCvSubst -> [TyCoVar] -> (TCvSubst, [TyCoVar])
substVarBndrs :: TCvSubst -> [Id] -> (TCvSubst, [Id])
substVarBndrs = (TCvSubst -> Id -> (TCvSubst, Id))
-> TCvSubst -> [Id] -> (TCvSubst, [Id])
forall (t :: * -> *) a b c.
Traversable t =>
(a -> b -> (a, c)) -> a -> t b -> (a, t c)
mapAccumL HasCallStack => TCvSubst -> Id -> (TCvSubst, Id)
TCvSubst -> Id -> (TCvSubst, Id)
substVarBndr
substCoVarBndr :: HasCallStack => TCvSubst -> CoVar -> (TCvSubst, CoVar)
substCoVarBndr :: TCvSubst -> Id -> (TCvSubst, Id)
substCoVarBndr = (TCvSubst -> Type -> Type) -> TCvSubst -> Id -> (TCvSubst, Id)
substCoVarBndrUsing HasCallStack => TCvSubst -> Type -> Type
TCvSubst -> Type -> Type
substTy
substVarBndrUnchecked :: TCvSubst -> TyCoVar -> (TCvSubst, TyCoVar)
substVarBndrUnchecked :: TCvSubst -> Id -> (TCvSubst, Id)
substVarBndrUnchecked = (TCvSubst -> Type -> Type) -> TCvSubst -> Id -> (TCvSubst, Id)
substVarBndrUsing TCvSubst -> Type -> Type
substTyUnchecked
substVarBndrUsing :: (TCvSubst -> Type -> Type)
-> TCvSubst -> TyCoVar -> (TCvSubst, TyCoVar)
substVarBndrUsing :: (TCvSubst -> Type -> Type) -> TCvSubst -> Id -> (TCvSubst, Id)
substVarBndrUsing subst_fn :: TCvSubst -> Type -> Type
subst_fn subst :: TCvSubst
subst v :: Id
v
| Id -> Bool
isTyVar Id
v = (TCvSubst -> Type -> Type) -> TCvSubst -> Id -> (TCvSubst, Id)
substTyVarBndrUsing TCvSubst -> Type -> Type
subst_fn TCvSubst
subst Id
v
| Bool
otherwise = (TCvSubst -> Type -> Type) -> TCvSubst -> Id -> (TCvSubst, Id)
substCoVarBndrUsing TCvSubst -> Type -> Type
subst_fn TCvSubst
subst Id
v
substTyVarBndrUsing
:: (TCvSubst -> Type -> Type)
-> TCvSubst -> TyVar -> (TCvSubst, TyVar)
substTyVarBndrUsing :: (TCvSubst -> Type -> Type) -> TCvSubst -> Id -> (TCvSubst, Id)
substTyVarBndrUsing subst_fn :: TCvSubst -> Type -> Type
subst_fn subst :: TCvSubst
subst@(TCvSubst in_scope :: InScopeSet
in_scope tenv :: TyVarEnv Type
tenv cenv :: CoVarEnv Coercion
cenv) old_var :: Id
old_var
= ASSERT2( _no_capture, pprTyVar old_var $$ pprTyVar new_var $$ ppr subst )
ASSERT( isTyVar old_var )
(InScopeSet -> TyVarEnv Type -> CoVarEnv Coercion -> TCvSubst
TCvSubst (InScopeSet
in_scope InScopeSet -> Id -> InScopeSet
`extendInScopeSet` Id
new_var) TyVarEnv Type
new_env CoVarEnv Coercion
cenv, Id
new_var)
where
new_env :: TyVarEnv Type
new_env | Bool
no_change = TyVarEnv Type -> Id -> TyVarEnv Type
forall a. VarEnv a -> Id -> VarEnv a
delVarEnv TyVarEnv Type
tenv Id
old_var
| Bool
otherwise = TyVarEnv Type -> Id -> Type -> TyVarEnv Type
forall a. VarEnv a -> Id -> a -> VarEnv a
extendVarEnv TyVarEnv Type
tenv Id
old_var (Id -> Type
TyVarTy Id
new_var)
_no_capture :: Bool
_no_capture = Bool -> Bool
not (Id
new_var Id -> VarSet -> Bool
`elemVarSet` TyVarEnv Type -> VarSet
tyCoVarsOfTypesSet TyVarEnv Type
tenv)
old_ki :: Type
old_ki = Id -> Type
tyVarKind Id
old_var
no_kind_change :: Bool
no_kind_change = Type -> Bool
noFreeVarsOfType Type
old_ki
no_change :: Bool
no_change = Bool
no_kind_change Bool -> Bool -> Bool
&& (Id
new_var Id -> Id -> Bool
forall a. Eq a => a -> a -> Bool
== Id
old_var)
new_var :: Id
new_var | Bool
no_kind_change = InScopeSet -> Id -> Id
uniqAway InScopeSet
in_scope Id
old_var
| Bool
otherwise = InScopeSet -> Id -> Id
uniqAway InScopeSet
in_scope (Id -> Id) -> Id -> Id
forall a b. (a -> b) -> a -> b
$
Id -> Type -> Id
setTyVarKind Id
old_var (TCvSubst -> Type -> Type
subst_fn TCvSubst
subst Type
old_ki)
substCoVarBndrUsing
:: (TCvSubst -> Type -> Type)
-> TCvSubst -> CoVar -> (TCvSubst, CoVar)
substCoVarBndrUsing :: (TCvSubst -> Type -> Type) -> TCvSubst -> Id -> (TCvSubst, Id)
substCoVarBndrUsing subst_fn :: TCvSubst -> Type -> Type
subst_fn subst :: TCvSubst
subst@(TCvSubst in_scope :: InScopeSet
in_scope tenv :: TyVarEnv Type
tenv cenv :: CoVarEnv Coercion
cenv) old_var :: Id
old_var
= ASSERT( isCoVar old_var )
(InScopeSet -> TyVarEnv Type -> CoVarEnv Coercion -> TCvSubst
TCvSubst (InScopeSet
in_scope InScopeSet -> Id -> InScopeSet
`extendInScopeSet` Id
new_var) TyVarEnv Type
tenv CoVarEnv Coercion
new_cenv, Id
new_var)
where
new_co :: Coercion
new_co = Id -> Coercion
mkCoVarCo Id
new_var
no_kind_change :: Bool
no_kind_change = [Type] -> Bool
noFreeVarsOfTypes [Type
t1, Type
t2]
no_change :: Bool
no_change = Id
new_var Id -> Id -> Bool
forall a. Eq a => a -> a -> Bool
== Id
old_var Bool -> Bool -> Bool
&& Bool
no_kind_change
new_cenv :: CoVarEnv Coercion
new_cenv | Bool
no_change = CoVarEnv Coercion -> Id -> CoVarEnv Coercion
forall a. VarEnv a -> Id -> VarEnv a
delVarEnv CoVarEnv Coercion
cenv Id
old_var
| Bool
otherwise = CoVarEnv Coercion -> Id -> Coercion -> CoVarEnv Coercion
forall a. VarEnv a -> Id -> a -> VarEnv a
extendVarEnv CoVarEnv Coercion
cenv Id
old_var Coercion
new_co
new_var :: Id
new_var = InScopeSet -> Id -> Id
uniqAway InScopeSet
in_scope Id
subst_old_var
subst_old_var :: Id
subst_old_var = Name -> Type -> Id
mkCoVar (Id -> Name
varName Id
old_var) Type
new_var_type
(_, _, t1 :: Type
t1, t2 :: Type
t2, role :: Role
role) = HasDebugCallStack => Id -> (Type, Type, Type, Type, Role)
Id -> (Type, Type, Type, Type, Role)
coVarKindsTypesRole Id
old_var
t1' :: Type
t1' = TCvSubst -> Type -> Type
subst_fn TCvSubst
subst Type
t1
t2' :: Type
t2' = TCvSubst -> Type -> Type
subst_fn TCvSubst
subst Type
t2
new_var_type :: Type
new_var_type = Role -> Type -> Type -> Type
mkCoercionType Role
role Type
t1' Type
t2'
cloneTyVarBndr :: TCvSubst -> TyVar -> Unique -> (TCvSubst, TyVar)
cloneTyVarBndr :: TCvSubst -> Id -> Unique -> (TCvSubst, Id)
cloneTyVarBndr subst :: TCvSubst
subst@(TCvSubst in_scope :: InScopeSet
in_scope tv_env :: TyVarEnv Type
tv_env cv_env :: CoVarEnv Coercion
cv_env) tv :: Id
tv uniq :: Unique
uniq
= ASSERT2( isTyVar tv, ppr tv )
(InScopeSet -> TyVarEnv Type -> CoVarEnv Coercion -> TCvSubst
TCvSubst (InScopeSet -> Id -> InScopeSet
extendInScopeSet InScopeSet
in_scope Id
tv')
(TyVarEnv Type -> Id -> Type -> TyVarEnv Type
forall a. VarEnv a -> Id -> a -> VarEnv a
extendVarEnv TyVarEnv Type
tv_env Id
tv (Id -> Type
mkTyVarTy Id
tv')) CoVarEnv Coercion
cv_env, Id
tv')
where
old_ki :: Type
old_ki = Id -> Type
tyVarKind Id
tv
no_kind_change :: Bool
no_kind_change = Type -> Bool
noFreeVarsOfType Type
old_ki
tv1 :: Id
tv1 | Bool
no_kind_change = Id
tv
| Bool
otherwise = Id -> Type -> Id
setTyVarKind Id
tv (HasCallStack => TCvSubst -> Type -> Type
TCvSubst -> Type -> Type
substTy TCvSubst
subst Type
old_ki)
tv' :: Id
tv' = Id -> Unique -> Id
setVarUnique Id
tv1 Unique
uniq
cloneTyVarBndrs :: TCvSubst -> [TyVar] -> UniqSupply -> (TCvSubst, [TyVar])
cloneTyVarBndrs :: TCvSubst -> [Id] -> UniqSupply -> (TCvSubst, [Id])
cloneTyVarBndrs subst :: TCvSubst
subst [] _usupply :: UniqSupply
_usupply = (TCvSubst
subst, [])
cloneTyVarBndrs subst :: TCvSubst
subst (t :: Id
t:ts :: [Id]
ts) usupply :: UniqSupply
usupply = (TCvSubst
subst'', Id
tvId -> [Id] -> [Id]
forall a. a -> [a] -> [a]
:[Id]
tvs)
where
(uniq :: Unique
uniq, usupply' :: UniqSupply
usupply') = UniqSupply -> (Unique, UniqSupply)
takeUniqFromSupply UniqSupply
usupply
(subst' :: TCvSubst
subst' , tv :: Id
tv ) = TCvSubst -> Id -> Unique -> (TCvSubst, Id)
cloneTyVarBndr TCvSubst
subst Id
t Unique
uniq
(subst'' :: TCvSubst
subst'', tvs :: [Id]
tvs) = TCvSubst -> [Id] -> UniqSupply -> (TCvSubst, [Id])
cloneTyVarBndrs TCvSubst
subst' [Id]
ts UniqSupply
usupply'
pprType, pprParendType :: Type -> SDoc
pprType :: Type -> SDoc
pprType = PprPrec -> Type -> SDoc
pprPrecType PprPrec
topPrec
pprParendType :: Type -> SDoc
pprParendType = PprPrec -> Type -> SDoc
pprPrecType PprPrec
appPrec
pprPrecType :: PprPrec -> Type -> SDoc
pprPrecType :: PprPrec -> Type -> SDoc
pprPrecType = TidyEnv -> PprPrec -> Type -> SDoc
pprPrecTypeX TidyEnv
emptyTidyEnv
pprPrecTypeX :: TidyEnv -> PprPrec -> Type -> SDoc
pprPrecTypeX :: TidyEnv -> PprPrec -> Type -> SDoc
pprPrecTypeX env :: TidyEnv
env prec :: PprPrec
prec ty :: Type
ty
= (PprStyle -> SDoc) -> SDoc
getPprStyle ((PprStyle -> SDoc) -> SDoc) -> (PprStyle -> SDoc) -> SDoc
forall a b. (a -> b) -> a -> b
$ \sty :: PprStyle
sty ->
if PprStyle -> Bool
debugStyle PprStyle
sty
then PprPrec -> Type -> SDoc
debug_ppr_ty PprPrec
prec Type
ty
else PprPrec -> IfaceType -> SDoc
pprPrecIfaceType PprPrec
prec (TidyEnv -> Type -> PprStyle -> IfaceType
tidyToIfaceTypeStyX TidyEnv
env Type
ty PprStyle
sty)
pprTyLit :: TyLit -> SDoc
pprTyLit :: TyLit -> SDoc
pprTyLit = IfaceTyLit -> SDoc
pprIfaceTyLit (IfaceTyLit -> SDoc) -> (TyLit -> IfaceTyLit) -> TyLit -> SDoc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TyLit -> IfaceTyLit
toIfaceTyLit
pprKind, pprParendKind :: Kind -> SDoc
pprKind :: Type -> SDoc
pprKind = Type -> SDoc
pprType
pprParendKind :: Type -> SDoc
pprParendKind = Type -> SDoc
pprParendType
tidyToIfaceTypeStyX :: TidyEnv -> Type -> PprStyle -> IfaceType
tidyToIfaceTypeStyX :: TidyEnv -> Type -> PprStyle -> IfaceType
tidyToIfaceTypeStyX env :: TidyEnv
env ty :: Type
ty sty :: PprStyle
sty
| PprStyle -> Bool
userStyle PprStyle
sty = TidyEnv -> Type -> IfaceType
tidyToIfaceTypeX TidyEnv
env Type
ty
| Bool
otherwise = VarSet -> Type -> IfaceType
toIfaceTypeX (Type -> VarSet
tyCoVarsOfType Type
ty) Type
ty
tidyToIfaceType :: Type -> IfaceType
tidyToIfaceType :: Type -> IfaceType
tidyToIfaceType = TidyEnv -> Type -> IfaceType
tidyToIfaceTypeX TidyEnv
emptyTidyEnv
tidyToIfaceTypeX :: TidyEnv -> Type -> IfaceType
tidyToIfaceTypeX :: TidyEnv -> Type -> IfaceType
tidyToIfaceTypeX env :: TidyEnv
env ty :: Type
ty = VarSet -> Type -> IfaceType
toIfaceTypeX ([Id] -> VarSet
mkVarSet [Id]
free_tcvs) (TidyEnv -> Type -> Type
tidyType TidyEnv
env' Type
ty)
where
env' :: TidyEnv
env' = TidyEnv -> [Id] -> TidyEnv
tidyFreeTyCoVars TidyEnv
env [Id]
free_tcvs
free_tcvs :: [Id]
free_tcvs = Type -> [Id]
tyCoVarsOfTypeWellScoped Type
ty
pprCo, pprParendCo :: Coercion -> SDoc
pprCo :: Coercion -> SDoc
pprCo co :: Coercion
co = (PprStyle -> SDoc) -> SDoc
getPprStyle ((PprStyle -> SDoc) -> SDoc) -> (PprStyle -> SDoc) -> SDoc
forall a b. (a -> b) -> a -> b
$ \ sty :: PprStyle
sty -> IfaceCoercion -> SDoc
pprIfaceCoercion (Coercion -> PprStyle -> IfaceCoercion
tidyToIfaceCoSty Coercion
co PprStyle
sty)
pprParendCo :: Coercion -> SDoc
pprParendCo co :: Coercion
co = (PprStyle -> SDoc) -> SDoc
getPprStyle ((PprStyle -> SDoc) -> SDoc) -> (PprStyle -> SDoc) -> SDoc
forall a b. (a -> b) -> a -> b
$ \ sty :: PprStyle
sty -> IfaceCoercion -> SDoc
pprParendIfaceCoercion (Coercion -> PprStyle -> IfaceCoercion
tidyToIfaceCoSty Coercion
co PprStyle
sty)
tidyToIfaceCoSty :: Coercion -> PprStyle -> IfaceCoercion
tidyToIfaceCoSty :: Coercion -> PprStyle -> IfaceCoercion
tidyToIfaceCoSty co :: Coercion
co sty :: PprStyle
sty
| PprStyle -> Bool
userStyle PprStyle
sty = Coercion -> IfaceCoercion
tidyToIfaceCo Coercion
co
| Bool
otherwise = VarSet -> Coercion -> IfaceCoercion
toIfaceCoercionX (Coercion -> VarSet
tyCoVarsOfCo Coercion
co) Coercion
co
tidyToIfaceCo :: Coercion -> IfaceCoercion
tidyToIfaceCo :: Coercion -> IfaceCoercion
tidyToIfaceCo co :: Coercion
co = VarSet -> Coercion -> IfaceCoercion
toIfaceCoercionX ([Id] -> VarSet
mkVarSet [Id]
free_tcvs) (TidyEnv -> Coercion -> Coercion
tidyCo TidyEnv
env Coercion
co)
where
env :: TidyEnv
env = TidyEnv -> [Id] -> TidyEnv
tidyFreeTyCoVars TidyEnv
emptyTidyEnv [Id]
free_tcvs
free_tcvs :: [Id]
free_tcvs = [Id] -> [Id]
scopedSort ([Id] -> [Id]) -> [Id] -> [Id]
forall a b. (a -> b) -> a -> b
$ Coercion -> [Id]
tyCoVarsOfCoList Coercion
co
pprClassPred :: Class -> [Type] -> SDoc
pprClassPred :: Class -> [Type] -> SDoc
pprClassPred clas :: Class
clas tys :: [Type]
tys = TyCon -> [Type] -> SDoc
pprTypeApp (Class -> TyCon
classTyCon Class
clas) [Type]
tys
pprTheta :: ThetaType -> SDoc
pprTheta :: [Type] -> SDoc
pprTheta = PprPrec -> [IfaceType] -> SDoc
pprIfaceContext PprPrec
topPrec ([IfaceType] -> SDoc) -> ([Type] -> [IfaceType]) -> [Type] -> SDoc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Type -> IfaceType) -> [Type] -> [IfaceType]
forall a b. (a -> b) -> [a] -> [b]
map Type -> IfaceType
tidyToIfaceType
pprParendTheta :: ThetaType -> SDoc
pprParendTheta :: [Type] -> SDoc
pprParendTheta = PprPrec -> [IfaceType] -> SDoc
pprIfaceContext PprPrec
appPrec ([IfaceType] -> SDoc) -> ([Type] -> [IfaceType]) -> [Type] -> SDoc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Type -> IfaceType) -> [Type] -> [IfaceType]
forall a b. (a -> b) -> [a] -> [b]
map Type -> IfaceType
tidyToIfaceType
pprThetaArrowTy :: ThetaType -> SDoc
pprThetaArrowTy :: [Type] -> SDoc
pprThetaArrowTy = [IfaceType] -> SDoc
pprIfaceContextArr ([IfaceType] -> SDoc) -> ([Type] -> [IfaceType]) -> [Type] -> SDoc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Type -> IfaceType) -> [Type] -> [IfaceType]
forall a b. (a -> b) -> [a] -> [b]
map Type -> IfaceType
tidyToIfaceType
instance Outputable Type where
ppr :: Type -> SDoc
ppr ty :: Type
ty = Type -> SDoc
pprType Type
ty
instance Outputable TyLit where
ppr :: TyLit -> SDoc
ppr = TyLit -> SDoc
pprTyLit
pprSigmaType :: Type -> SDoc
pprSigmaType :: Type -> SDoc
pprSigmaType = ShowForAllFlag -> IfaceType -> SDoc
pprIfaceSigmaType ShowForAllFlag
ShowForAllWhen (IfaceType -> SDoc) -> (Type -> IfaceType) -> Type -> SDoc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Type -> IfaceType
tidyToIfaceType
pprForAll :: [TyCoVarBinder] -> SDoc
pprForAll :: [TyCoVarBinder] -> SDoc
pprForAll tvs :: [TyCoVarBinder]
tvs = [IfaceForAllBndr] -> SDoc
pprIfaceForAll ((TyCoVarBinder -> IfaceForAllBndr)
-> [TyCoVarBinder] -> [IfaceForAllBndr]
forall a b. (a -> b) -> [a] -> [b]
map TyCoVarBinder -> IfaceForAllBndr
toIfaceForAllBndr [TyCoVarBinder]
tvs)
pprUserForAll :: [TyCoVarBinder] -> SDoc
pprUserForAll :: [TyCoVarBinder] -> SDoc
pprUserForAll = [IfaceForAllBndr] -> SDoc
pprUserIfaceForAll ([IfaceForAllBndr] -> SDoc)
-> ([TyCoVarBinder] -> [IfaceForAllBndr])
-> [TyCoVarBinder]
-> SDoc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (TyCoVarBinder -> IfaceForAllBndr)
-> [TyCoVarBinder] -> [IfaceForAllBndr]
forall a b. (a -> b) -> [a] -> [b]
map TyCoVarBinder -> IfaceForAllBndr
toIfaceForAllBndr
pprTCvBndrs :: [TyCoVarBinder] -> SDoc
pprTCvBndrs :: [TyCoVarBinder] -> SDoc
pprTCvBndrs tvs :: [TyCoVarBinder]
tvs = [SDoc] -> SDoc
sep ((TyCoVarBinder -> SDoc) -> [TyCoVarBinder] -> [SDoc]
forall a b. (a -> b) -> [a] -> [b]
map TyCoVarBinder -> SDoc
pprTCvBndr [TyCoVarBinder]
tvs)
pprTCvBndr :: TyCoVarBinder -> SDoc
pprTCvBndr :: TyCoVarBinder -> SDoc
pprTCvBndr = Id -> SDoc
pprTyVar (Id -> SDoc) -> (TyCoVarBinder -> Id) -> TyCoVarBinder -> SDoc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TyCoVarBinder -> Id
forall tv argf. VarBndr tv argf -> tv
binderVar
pprTyVars :: [TyVar] -> SDoc
pprTyVars :: [Id] -> SDoc
pprTyVars tvs :: [Id]
tvs = [SDoc] -> SDoc
sep ((Id -> SDoc) -> [Id] -> [SDoc]
forall a b. (a -> b) -> [a] -> [b]
map Id -> SDoc
pprTyVar [Id]
tvs)
pprTyVar :: TyVar -> SDoc
pprTyVar :: Id -> SDoc
pprTyVar tv :: Id
tv
| Type -> Bool
isLiftedTypeKind Type
kind = Id -> SDoc
forall a. Outputable a => a -> SDoc
ppr Id
tv
| Bool
otherwise = SDoc -> SDoc
parens (Id -> SDoc
forall a. Outputable a => a -> SDoc
ppr Id
tv SDoc -> SDoc -> SDoc
<+> SDoc
dcolon SDoc -> SDoc -> SDoc
<+> Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
kind)
where
kind :: Type
kind = Id -> Type
tyVarKind Id
tv
instance Outputable TyCoBinder where
ppr :: TyCoBinder -> SDoc
ppr (Anon ty :: Type
ty) = String -> SDoc
text "[anon]" SDoc -> SDoc -> SDoc
<+> Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
ty
ppr (Named (Bndr v :: Id
v Required)) = Id -> SDoc
forall a. Outputable a => a -> SDoc
ppr Id
v
ppr (Named (Bndr v :: Id
v Specified)) = Char -> SDoc
char '@' SDoc -> SDoc -> SDoc
<> Id -> SDoc
forall a. Outputable a => a -> SDoc
ppr Id
v
ppr (Named (Bndr v :: Id
v Inferred)) = SDoc -> SDoc
braces (Id -> SDoc
forall a. Outputable a => a -> SDoc
ppr Id
v)
instance Outputable Coercion where
ppr :: Coercion -> SDoc
ppr = Coercion -> SDoc
pprCo
debugPprType :: Type -> SDoc
debugPprType :: Type -> SDoc
debugPprType ty :: Type
ty = PprPrec -> Type -> SDoc
debug_ppr_ty PprPrec
topPrec Type
ty
debug_ppr_ty :: PprPrec -> Type -> SDoc
debug_ppr_ty :: PprPrec -> Type -> SDoc
debug_ppr_ty _ (LitTy l :: TyLit
l)
= TyLit -> SDoc
forall a. Outputable a => a -> SDoc
ppr TyLit
l
debug_ppr_ty _ (TyVarTy tv :: Id
tv)
= Id -> SDoc
forall a. Outputable a => a -> SDoc
ppr Id
tv
debug_ppr_ty prec :: PprPrec
prec (FunTy arg :: Type
arg res :: Type
res)
= PprPrec -> PprPrec -> SDoc -> SDoc
maybeParen PprPrec
prec PprPrec
funPrec (SDoc -> SDoc) -> SDoc -> SDoc
forall a b. (a -> b) -> a -> b
$
[SDoc] -> SDoc
sep [PprPrec -> Type -> SDoc
debug_ppr_ty PprPrec
funPrec Type
arg, SDoc
arrow SDoc -> SDoc -> SDoc
<+> PprPrec -> Type -> SDoc
debug_ppr_ty PprPrec
prec Type
res]
debug_ppr_ty prec :: PprPrec
prec (TyConApp tc :: TyCon
tc tys :: [Type]
tys)
| [Type] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Type]
tys = TyCon -> SDoc
forall a. Outputable a => a -> SDoc
ppr TyCon
tc
| Bool
otherwise = PprPrec -> PprPrec -> SDoc -> SDoc
maybeParen PprPrec
prec PprPrec
appPrec (SDoc -> SDoc) -> SDoc -> SDoc
forall a b. (a -> b) -> a -> b
$
SDoc -> Int -> SDoc -> SDoc
hang (TyCon -> SDoc
forall a. Outputable a => a -> SDoc
ppr TyCon
tc) 2 ([SDoc] -> SDoc
sep ((Type -> SDoc) -> [Type] -> [SDoc]
forall a b. (a -> b) -> [a] -> [b]
map (PprPrec -> Type -> SDoc
debug_ppr_ty PprPrec
appPrec) [Type]
tys))
debug_ppr_ty _ (AppTy t1 :: Type
t1 t2 :: Type
t2)
= SDoc -> Int -> SDoc -> SDoc
hang (PprPrec -> Type -> SDoc
debug_ppr_ty PprPrec
appPrec Type
t1)
2 (PprPrec -> Type -> SDoc
debug_ppr_ty PprPrec
appPrec Type
t2)
debug_ppr_ty prec :: PprPrec
prec (CastTy ty :: Type
ty co :: Coercion
co)
= PprPrec -> PprPrec -> SDoc -> SDoc
maybeParen PprPrec
prec PprPrec
topPrec (SDoc -> SDoc) -> SDoc -> SDoc
forall a b. (a -> b) -> a -> b
$
SDoc -> Int -> SDoc -> SDoc
hang (PprPrec -> Type -> SDoc
debug_ppr_ty PprPrec
topPrec Type
ty)
2 (String -> SDoc
text "|>" SDoc -> SDoc -> SDoc
<+> Coercion -> SDoc
forall a. Outputable a => a -> SDoc
ppr Coercion
co)
debug_ppr_ty _ (CoercionTy co :: Coercion
co)
= SDoc -> SDoc
parens (String -> SDoc
text "CO" SDoc -> SDoc -> SDoc
<+> Coercion -> SDoc
forall a. Outputable a => a -> SDoc
ppr Coercion
co)
debug_ppr_ty prec :: PprPrec
prec ty :: Type
ty@(ForAllTy {})
| (tvs :: [TyCoVarBinder]
tvs, body :: Type
body) <- Type -> ([TyCoVarBinder], Type)
split Type
ty
= PprPrec -> PprPrec -> SDoc -> SDoc
maybeParen PprPrec
prec PprPrec
funPrec (SDoc -> SDoc) -> SDoc -> SDoc
forall a b. (a -> b) -> a -> b
$
SDoc -> Int -> SDoc -> SDoc
hang (String -> SDoc
text "forall" SDoc -> SDoc -> SDoc
<+> [SDoc] -> SDoc
fsep ((TyCoVarBinder -> SDoc) -> [TyCoVarBinder] -> [SDoc]
forall a b. (a -> b) -> [a] -> [b]
map TyCoVarBinder -> SDoc
forall a. Outputable a => a -> SDoc
ppr [TyCoVarBinder]
tvs) SDoc -> SDoc -> SDoc
<> SDoc
dot)
2 (Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
body)
where
split :: Type -> ([TyCoVarBinder], Type)
split ty :: Type
ty | ForAllTy tv :: TyCoVarBinder
tv ty' :: Type
ty' <- Type
ty
, (tvs :: [TyCoVarBinder]
tvs, body :: Type
body) <- Type -> ([TyCoVarBinder], Type)
split Type
ty'
= (TyCoVarBinder
tvTyCoVarBinder -> [TyCoVarBinder] -> [TyCoVarBinder]
forall a. a -> [a] -> [a]
:[TyCoVarBinder]
tvs, Type
body)
| Bool
otherwise
= ([], Type
ty)
pprDataCons :: TyCon -> SDoc
pprDataCons :: TyCon -> SDoc
pprDataCons = [SDoc] -> SDoc
sepWithVBars ([SDoc] -> SDoc) -> (TyCon -> [SDoc]) -> TyCon -> SDoc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (DataCon -> SDoc) -> [DataCon] -> [SDoc]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap DataCon -> SDoc
pprDataConWithArgs ([DataCon] -> [SDoc]) -> (TyCon -> [DataCon]) -> TyCon -> [SDoc]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TyCon -> [DataCon]
tyConDataCons
where
sepWithVBars :: [SDoc] -> SDoc
sepWithVBars [] = SDoc
empty
sepWithVBars docs :: [SDoc]
docs = [SDoc] -> SDoc
sep (SDoc -> [SDoc] -> [SDoc]
punctuate (SDoc
space SDoc -> SDoc -> SDoc
<> SDoc
vbar) [SDoc]
docs)
pprDataConWithArgs :: DataCon -> SDoc
pprDataConWithArgs :: DataCon -> SDoc
pprDataConWithArgs dc :: DataCon
dc = [SDoc] -> SDoc
sep [SDoc
forAllDoc, SDoc
thetaDoc, DataCon -> SDoc
forall a. Outputable a => a -> SDoc
ppr DataCon
dc SDoc -> SDoc -> SDoc
<+> SDoc
argsDoc]
where
(_univ_tvs :: [Id]
_univ_tvs, _ex_tvs :: [Id]
_ex_tvs, _eq_spec :: [EqSpec]
_eq_spec, theta :: [Type]
theta, arg_tys :: [Type]
arg_tys, _res_ty :: Type
_res_ty) = DataCon -> ([Id], [Id], [EqSpec], [Type], [Type], Type)
dataConFullSig DataCon
dc
user_bndrs :: [TyCoVarBinder]
user_bndrs = DataCon -> [TyCoVarBinder]
dataConUserTyVarBinders DataCon
dc
forAllDoc :: SDoc
forAllDoc = [TyCoVarBinder] -> SDoc
pprUserForAll [TyCoVarBinder]
user_bndrs
thetaDoc :: SDoc
thetaDoc = [Type] -> SDoc
pprThetaArrowTy [Type]
theta
argsDoc :: SDoc
argsDoc = [SDoc] -> SDoc
hsep ((Type -> SDoc) -> [Type] -> [SDoc]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Type -> SDoc
pprParendType [Type]
arg_tys)
pprTypeApp :: TyCon -> [Type] -> SDoc
pprTypeApp :: TyCon -> [Type] -> SDoc
pprTypeApp tc :: TyCon
tc tys :: [Type]
tys
= PprPrec -> IfaceTyCon -> IfaceAppArgs -> SDoc
pprIfaceTypeApp PprPrec
topPrec (TyCon -> IfaceTyCon
toIfaceTyCon TyCon
tc)
(TyCon -> [Type] -> IfaceAppArgs
toIfaceTcArgs TyCon
tc [Type]
tys)
pprWithExplicitKindsWhen :: Bool -> SDoc -> SDoc
pprWithExplicitKindsWhen :: Bool -> SDoc -> SDoc
pprWithExplicitKindsWhen b :: Bool
b
= (DynFlags -> DynFlags) -> SDoc -> SDoc
updSDocDynFlags ((DynFlags -> DynFlags) -> SDoc -> SDoc)
-> (DynFlags -> DynFlags) -> SDoc -> SDoc
forall a b. (a -> b) -> a -> b
$ \dflags :: DynFlags
dflags ->
if Bool
b then DynFlags -> GeneralFlag -> DynFlags
gopt_set DynFlags
dflags GeneralFlag
Opt_PrintExplicitKinds
else DynFlags
dflags
tidyVarBndrs :: TidyEnv -> [TyCoVar] -> (TidyEnv, [TyCoVar])
tidyVarBndrs :: TidyEnv -> [Id] -> (TidyEnv, [Id])
tidyVarBndrs tidy_env :: TidyEnv
tidy_env tvs :: [Id]
tvs
= (TidyEnv -> Id -> (TidyEnv, Id))
-> TidyEnv -> [Id] -> (TidyEnv, [Id])
forall (t :: * -> *) a b c.
Traversable t =>
(a -> b -> (a, c)) -> a -> t b -> (a, t c)
mapAccumL TidyEnv -> Id -> (TidyEnv, Id)
tidyVarBndr ([Id] -> TidyEnv -> TidyEnv
avoidNameClashes [Id]
tvs TidyEnv
tidy_env) [Id]
tvs
tidyVarBndr :: TidyEnv -> TyCoVar -> (TidyEnv, TyCoVar)
tidyVarBndr :: TidyEnv -> Id -> (TidyEnv, Id)
tidyVarBndr tidy_env :: TidyEnv
tidy_env@(occ_env :: TidyOccEnv
occ_env, subst :: VarEnv Id
subst) var :: Id
var
= case TidyOccEnv -> OccName -> (TidyOccEnv, OccName)
tidyOccName TidyOccEnv
occ_env (Id -> OccName
getHelpfulOccName Id
var) of
(occ_env' :: TidyOccEnv
occ_env', occ' :: OccName
occ') -> ((TidyOccEnv
occ_env', VarEnv Id
subst'), Id
var')
where
subst' :: VarEnv Id
subst' = VarEnv Id -> Id -> Id -> VarEnv Id
forall a. VarEnv a -> Id -> a -> VarEnv a
extendVarEnv VarEnv Id
subst Id
var Id
var'
var' :: Id
var' = Id -> Type -> Id
setVarType (Id -> Name -> Id
setVarName Id
var Name
name') Type
type'
type' :: Type
type' = TidyEnv -> Type -> Type
tidyType TidyEnv
tidy_env (Id -> Type
varType Id
var)
name' :: Name
name' = Name -> OccName -> Name
tidyNameOcc Name
name OccName
occ'
name :: Name
name = Id -> Name
varName Id
var
avoidNameClashes :: [TyCoVar] -> TidyEnv -> TidyEnv
avoidNameClashes :: [Id] -> TidyEnv -> TidyEnv
avoidNameClashes tvs :: [Id]
tvs (occ_env :: TidyOccEnv
occ_env, subst :: VarEnv Id
subst)
= (TidyOccEnv -> [OccName] -> TidyOccEnv
avoidClashesOccEnv TidyOccEnv
occ_env [OccName]
occs, VarEnv Id
subst)
where
occs :: [OccName]
occs = (Id -> OccName) -> [Id] -> [OccName]
forall a b. (a -> b) -> [a] -> [b]
map Id -> OccName
getHelpfulOccName [Id]
tvs
getHelpfulOccName :: TyCoVar -> OccName
getHelpfulOccName :: Id -> OccName
getHelpfulOccName tv :: Id
tv
| Name -> Bool
isSystemName Name
name, Id -> Bool
isTcTyVar Id
tv
= String -> OccName
mkTyVarOcc (OccName -> String
occNameString OccName
occ String -> String -> String
forall a. [a] -> [a] -> [a]
++ "0")
| Bool
otherwise
= OccName
occ
where
name :: Name
name = Id -> Name
varName Id
tv
occ :: OccName
occ = Name -> OccName
forall a. NamedThing a => a -> OccName
getOccName Name
name
tidyTyCoVarBinder :: TidyEnv -> VarBndr TyCoVar vis
-> (TidyEnv, VarBndr TyCoVar vis)
tidyTyCoVarBinder :: TidyEnv -> VarBndr Id vis -> (TidyEnv, VarBndr Id vis)
tidyTyCoVarBinder tidy_env :: TidyEnv
tidy_env (Bndr tv :: Id
tv vis :: vis
vis)
= (TidyEnv
tidy_env', Id -> vis -> VarBndr Id vis
forall var argf. var -> argf -> VarBndr var argf
Bndr Id
tv' vis
vis)
where
(tidy_env' :: TidyEnv
tidy_env', tv' :: Id
tv') = TidyEnv -> Id -> (TidyEnv, Id)
tidyVarBndr TidyEnv
tidy_env Id
tv
tidyTyCoVarBinders :: TidyEnv -> [VarBndr TyCoVar vis]
-> (TidyEnv, [VarBndr TyCoVar vis])
tidyTyCoVarBinders :: TidyEnv -> [VarBndr Id vis] -> (TidyEnv, [VarBndr Id vis])
tidyTyCoVarBinders = (TidyEnv -> VarBndr Id vis -> (TidyEnv, VarBndr Id vis))
-> TidyEnv -> [VarBndr Id vis] -> (TidyEnv, [VarBndr Id vis])
forall (t :: * -> *) a b c.
Traversable t =>
(a -> b -> (a, c)) -> a -> t b -> (a, t c)
mapAccumL TidyEnv -> VarBndr Id vis -> (TidyEnv, VarBndr Id vis)
forall vis. TidyEnv -> VarBndr Id vis -> (TidyEnv, VarBndr Id vis)
tidyTyCoVarBinder
tidyFreeTyCoVars :: TidyEnv -> [TyCoVar] -> TidyEnv
tidyFreeTyCoVars :: TidyEnv -> [Id] -> TidyEnv
tidyFreeTyCoVars (full_occ_env :: TidyOccEnv
full_occ_env, var_env :: VarEnv Id
var_env) tyvars :: [Id]
tyvars
= (TidyEnv, [Id]) -> TidyEnv
forall a b. (a, b) -> a
fst (TidyEnv -> [Id] -> (TidyEnv, [Id])
tidyOpenTyCoVars (TidyOccEnv
full_occ_env, VarEnv Id
var_env) [Id]
tyvars)
tidyOpenTyCoVars :: TidyEnv -> [TyCoVar] -> (TidyEnv, [TyCoVar])
tidyOpenTyCoVars :: TidyEnv -> [Id] -> (TidyEnv, [Id])
tidyOpenTyCoVars env :: TidyEnv
env tyvars :: [Id]
tyvars = (TidyEnv -> Id -> (TidyEnv, Id))
-> TidyEnv -> [Id] -> (TidyEnv, [Id])
forall (t :: * -> *) a b c.
Traversable t =>
(a -> b -> (a, c)) -> a -> t b -> (a, t c)
mapAccumL TidyEnv -> Id -> (TidyEnv, Id)
tidyOpenTyCoVar TidyEnv
env [Id]
tyvars
tidyOpenTyCoVar :: TidyEnv -> TyCoVar -> (TidyEnv, TyCoVar)
tidyOpenTyCoVar :: TidyEnv -> Id -> (TidyEnv, Id)
tidyOpenTyCoVar env :: TidyEnv
env@(_, subst :: VarEnv Id
subst) tyvar :: Id
tyvar
= case VarEnv Id -> Id -> Maybe Id
forall a. VarEnv a -> Id -> Maybe a
lookupVarEnv VarEnv Id
subst Id
tyvar of
Just tyvar' :: Id
tyvar' -> (TidyEnv
env, Id
tyvar')
Nothing ->
let env' :: TidyEnv
env' = TidyEnv -> [Id] -> TidyEnv
tidyFreeTyCoVars TidyEnv
env (Type -> [Id]
tyCoVarsOfTypeList (Id -> Type
tyVarKind Id
tyvar))
in TidyEnv -> Id -> (TidyEnv, Id)
tidyVarBndr TidyEnv
env' Id
tyvar
tidyTyCoVarOcc :: TidyEnv -> TyCoVar -> TyCoVar
tidyTyCoVarOcc :: TidyEnv -> Id -> Id
tidyTyCoVarOcc env :: TidyEnv
env@(_, subst :: VarEnv Id
subst) tv :: Id
tv
= case VarEnv Id -> Id -> Maybe Id
forall a. VarEnv a -> Id -> Maybe a
lookupVarEnv VarEnv Id
subst Id
tv of
Nothing -> (Type -> Type) -> Id -> Id
updateVarType (TidyEnv -> Type -> Type
tidyType TidyEnv
env) Id
tv
Just tv' :: Id
tv' -> Id
tv'
tidyTypes :: TidyEnv -> [Type] -> [Type]
tidyTypes :: TidyEnv -> [Type] -> [Type]
tidyTypes env :: TidyEnv
env tys :: [Type]
tys = (Type -> Type) -> [Type] -> [Type]
forall a b. (a -> b) -> [a] -> [b]
map (TidyEnv -> Type -> Type
tidyType TidyEnv
env) [Type]
tys
tidyType :: TidyEnv -> Type -> Type
tidyType :: TidyEnv -> Type -> Type
tidyType _ (LitTy n :: TyLit
n) = TyLit -> Type
LitTy TyLit
n
tidyType env :: TidyEnv
env (TyVarTy tv :: Id
tv) = Id -> Type
TyVarTy (TidyEnv -> Id -> Id
tidyTyCoVarOcc TidyEnv
env Id
tv)
tidyType env :: TidyEnv
env (TyConApp tycon :: TyCon
tycon tys :: [Type]
tys) = let args :: [Type]
args = TidyEnv -> [Type] -> [Type]
tidyTypes TidyEnv
env [Type]
tys
in [Type]
args [Type] -> Type -> Type
forall a b. [a] -> b -> b
`seqList` TyCon -> [Type] -> Type
TyConApp TyCon
tycon [Type]
args
tidyType env :: TidyEnv
env (AppTy fun :: Type
fun arg :: Type
arg) = (Type -> Type -> Type
AppTy (Type -> Type -> Type) -> Type -> Type -> Type
forall a b. (a -> b) -> a -> b
$! (TidyEnv -> Type -> Type
tidyType TidyEnv
env Type
fun)) (Type -> Type) -> Type -> Type
forall a b. (a -> b) -> a -> b
$! (TidyEnv -> Type -> Type
tidyType TidyEnv
env Type
arg)
tidyType env :: TidyEnv
env (FunTy fun :: Type
fun arg :: Type
arg) = (Type -> Type -> Type
FunTy (Type -> Type -> Type) -> Type -> Type -> Type
forall a b. (a -> b) -> a -> b
$! (TidyEnv -> Type -> Type
tidyType TidyEnv
env Type
fun)) (Type -> Type) -> Type -> Type
forall a b. (a -> b) -> a -> b
$! (TidyEnv -> Type -> Type
tidyType TidyEnv
env Type
arg)
tidyType env :: TidyEnv
env (ty :: Type
ty@(ForAllTy{})) = [(Id, ArgFlag)] -> Type -> Type
mkForAllTys' ([Id] -> [ArgFlag] -> [(Id, ArgFlag)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Id]
tvs' [ArgFlag]
vis) (Type -> Type) -> Type -> Type
forall a b. (a -> b) -> a -> b
$! TidyEnv -> Type -> Type
tidyType TidyEnv
env' Type
body_ty
where
(tvs :: [Id]
tvs, vis :: [ArgFlag]
vis, body_ty :: Type
body_ty) = Type -> ([Id], [ArgFlag], Type)
splitForAllTys' Type
ty
(env' :: TidyEnv
env', tvs' :: [Id]
tvs') = TidyEnv -> [Id] -> (TidyEnv, [Id])
tidyVarBndrs TidyEnv
env [Id]
tvs
tidyType env :: TidyEnv
env (CastTy ty :: Type
ty co :: Coercion
co) = (Type -> Coercion -> Type
CastTy (Type -> Coercion -> Type) -> Type -> Coercion -> Type
forall a b. (a -> b) -> a -> b
$! TidyEnv -> Type -> Type
tidyType TidyEnv
env Type
ty) (Coercion -> Type) -> Coercion -> Type
forall a b. (a -> b) -> a -> b
$! (TidyEnv -> Coercion -> Coercion
tidyCo TidyEnv
env Coercion
co)
tidyType env :: TidyEnv
env (CoercionTy co :: Coercion
co) = Coercion -> Type
CoercionTy (Coercion -> Type) -> Coercion -> Type
forall a b. (a -> b) -> a -> b
$! (TidyEnv -> Coercion -> Coercion
tidyCo TidyEnv
env Coercion
co)
mkForAllTys' :: [(TyCoVar, ArgFlag)] -> Type -> Type
mkForAllTys' :: [(Id, ArgFlag)] -> Type -> Type
mkForAllTys' tvvs :: [(Id, ArgFlag)]
tvvs ty :: Type
ty = ((Id, ArgFlag) -> Type -> Type) -> Type -> [(Id, ArgFlag)] -> Type
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (Id, ArgFlag) -> Type -> Type
strictMkForAllTy Type
ty [(Id, ArgFlag)]
tvvs
where
strictMkForAllTy :: (Id, ArgFlag) -> Type -> Type
strictMkForAllTy (tv :: Id
tv,vis :: ArgFlag
vis) ty :: Type
ty = (TyCoVarBinder -> Type -> Type
ForAllTy (TyCoVarBinder -> Type -> Type) -> TyCoVarBinder -> Type -> Type
forall a b. (a -> b) -> a -> b
$! ((Id -> ArgFlag -> TyCoVarBinder
forall var argf. var -> argf -> VarBndr var argf
Bndr (Id -> ArgFlag -> TyCoVarBinder) -> Id -> ArgFlag -> TyCoVarBinder
forall a b. (a -> b) -> a -> b
$! Id
tv) (ArgFlag -> TyCoVarBinder) -> ArgFlag -> TyCoVarBinder
forall a b. (a -> b) -> a -> b
$! ArgFlag
vis)) (Type -> Type) -> Type -> Type
forall a b. (a -> b) -> a -> b
$! Type
ty
splitForAllTys' :: Type -> ([TyCoVar], [ArgFlag], Type)
splitForAllTys' :: Type -> ([Id], [ArgFlag], Type)
splitForAllTys' ty :: Type
ty = Type -> [Id] -> [ArgFlag] -> ([Id], [ArgFlag], Type)
go Type
ty [] []
where
go :: Type -> [Id] -> [ArgFlag] -> ([Id], [ArgFlag], Type)
go (ForAllTy (Bndr tv :: Id
tv vis :: ArgFlag
vis) ty :: Type
ty) tvs :: [Id]
tvs viss :: [ArgFlag]
viss = Type -> [Id] -> [ArgFlag] -> ([Id], [ArgFlag], Type)
go Type
ty (Id
tvId -> [Id] -> [Id]
forall a. a -> [a] -> [a]
:[Id]
tvs) (ArgFlag
visArgFlag -> [ArgFlag] -> [ArgFlag]
forall a. a -> [a] -> [a]
:[ArgFlag]
viss)
go ty :: Type
ty tvs :: [Id]
tvs viss :: [ArgFlag]
viss = ([Id] -> [Id]
forall a. [a] -> [a]
reverse [Id]
tvs, [ArgFlag] -> [ArgFlag]
forall a. [a] -> [a]
reverse [ArgFlag]
viss, Type
ty)
tidyOpenTypes :: TidyEnv -> [Type] -> (TidyEnv, [Type])
tidyOpenTypes :: TidyEnv -> [Type] -> (TidyEnv, [Type])
tidyOpenTypes env :: TidyEnv
env tys :: [Type]
tys
= (TidyEnv
env', TidyEnv -> [Type] -> [Type]
tidyTypes (TidyOccEnv
trimmed_occ_env, VarEnv Id
var_env) [Type]
tys)
where
(env' :: TidyEnv
env'@(_, var_env :: VarEnv Id
var_env), tvs' :: [Id]
tvs') = TidyEnv -> [Id] -> (TidyEnv, [Id])
tidyOpenTyCoVars TidyEnv
env ([Id] -> (TidyEnv, [Id])) -> [Id] -> (TidyEnv, [Id])
forall a b. (a -> b) -> a -> b
$
[Type] -> [Id]
tyCoVarsOfTypesWellScoped [Type]
tys
trimmed_occ_env :: TidyOccEnv
trimmed_occ_env = [OccName] -> TidyOccEnv
initTidyOccEnv ((Id -> OccName) -> [Id] -> [OccName]
forall a b. (a -> b) -> [a] -> [b]
map Id -> OccName
forall a. NamedThing a => a -> OccName
getOccName [Id]
tvs')
tidyOpenType :: TidyEnv -> Type -> (TidyEnv, Type)
tidyOpenType :: TidyEnv -> Type -> (TidyEnv, Type)
tidyOpenType env :: TidyEnv
env ty :: Type
ty = let (env' :: TidyEnv
env', [ty' :: Type
ty']) = TidyEnv -> [Type] -> (TidyEnv, [Type])
tidyOpenTypes TidyEnv
env [Type
ty] in
(TidyEnv
env', Type
ty')
tidyTopType :: Type -> Type
tidyTopType :: Type -> Type
tidyTopType ty :: Type
ty = TidyEnv -> Type -> Type
tidyType TidyEnv
emptyTidyEnv Type
ty
tidyOpenKind :: TidyEnv -> Kind -> (TidyEnv, Kind)
tidyOpenKind :: TidyEnv -> Type -> (TidyEnv, Type)
tidyOpenKind = TidyEnv -> Type -> (TidyEnv, Type)
tidyOpenType
tidyKind :: TidyEnv -> Kind -> Kind
tidyKind :: TidyEnv -> Type -> Type
tidyKind = TidyEnv -> Type -> Type
tidyType
tidyCo :: TidyEnv -> Coercion -> Coercion
tidyCo :: TidyEnv -> Coercion -> Coercion
tidyCo env :: TidyEnv
env@(_, subst :: VarEnv Id
subst) co :: Coercion
co
= Coercion -> Coercion
go Coercion
co
where
go_mco :: MCoercion -> MCoercion
go_mco MRefl = MCoercion
MRefl
go_mco (MCo co :: Coercion
co) = Coercion -> MCoercion
MCo (Coercion -> Coercion
go Coercion
co)
go :: Coercion -> Coercion
go (Refl ty :: Type
ty) = Type -> Coercion
Refl (TidyEnv -> Type -> Type
tidyType TidyEnv
env Type
ty)
go (GRefl r :: Role
r ty :: Type
ty mco :: MCoercion
mco) = Role -> Type -> MCoercion -> Coercion
GRefl Role
r (TidyEnv -> Type -> Type
tidyType TidyEnv
env Type
ty) (MCoercion -> Coercion) -> MCoercion -> Coercion
forall a b. (a -> b) -> a -> b
$! MCoercion -> MCoercion
go_mco MCoercion
mco
go (TyConAppCo r :: Role
r tc :: TyCon
tc cos :: [Coercion]
cos) = let args :: [Coercion]
args = (Coercion -> Coercion) -> [Coercion] -> [Coercion]
forall a b. (a -> b) -> [a] -> [b]
map Coercion -> Coercion
go [Coercion]
cos
in [Coercion]
args [Coercion] -> Coercion -> Coercion
forall a b. [a] -> b -> b
`seqList` Role -> TyCon -> [Coercion] -> Coercion
TyConAppCo Role
r TyCon
tc [Coercion]
args
go (AppCo co1 :: Coercion
co1 co2 :: Coercion
co2) = (Coercion -> Coercion -> Coercion
AppCo (Coercion -> Coercion -> Coercion)
-> Coercion -> Coercion -> Coercion
forall a b. (a -> b) -> a -> b
$! Coercion -> Coercion
go Coercion
co1) (Coercion -> Coercion) -> Coercion -> Coercion
forall a b. (a -> b) -> a -> b
$! Coercion -> Coercion
go Coercion
co2
go (ForAllCo tv :: Id
tv h :: Coercion
h co :: Coercion
co) = ((Id -> Coercion -> Coercion -> Coercion
ForAllCo (Id -> Coercion -> Coercion -> Coercion)
-> Id -> Coercion -> Coercion -> Coercion
forall a b. (a -> b) -> a -> b
$! Id
tvp) (Coercion -> Coercion -> Coercion)
-> Coercion -> Coercion -> Coercion
forall a b. (a -> b) -> a -> b
$! (Coercion -> Coercion
go Coercion
h)) (Coercion -> Coercion) -> Coercion -> Coercion
forall a b. (a -> b) -> a -> b
$! (TidyEnv -> Coercion -> Coercion
tidyCo TidyEnv
envp Coercion
co)
where (envp :: TidyEnv
envp, tvp :: Id
tvp) = TidyEnv -> Id -> (TidyEnv, Id)
tidyVarBndr TidyEnv
env Id
tv
go (FunCo r :: Role
r co1 :: Coercion
co1 co2 :: Coercion
co2) = (Role -> Coercion -> Coercion -> Coercion
FunCo Role
r (Coercion -> Coercion -> Coercion)
-> Coercion -> Coercion -> Coercion
forall a b. (a -> b) -> a -> b
$! Coercion -> Coercion
go Coercion
co1) (Coercion -> Coercion) -> Coercion -> Coercion
forall a b. (a -> b) -> a -> b
$! Coercion -> Coercion
go Coercion
co2
go (CoVarCo cv :: Id
cv) = case VarEnv Id -> Id -> Maybe Id
forall a. VarEnv a -> Id -> Maybe a
lookupVarEnv VarEnv Id
subst Id
cv of
Nothing -> Id -> Coercion
CoVarCo Id
cv
Just cv' :: Id
cv' -> Id -> Coercion
CoVarCo Id
cv'
go (HoleCo h :: CoercionHole
h) = CoercionHole -> Coercion
HoleCo CoercionHole
h
go (AxiomInstCo con :: CoAxiom Branched
con ind :: Int
ind cos :: [Coercion]
cos) = let args :: [Coercion]
args = (Coercion -> Coercion) -> [Coercion] -> [Coercion]
forall a b. (a -> b) -> [a] -> [b]
map Coercion -> Coercion
go [Coercion]
cos
in [Coercion]
args [Coercion] -> Coercion -> Coercion
forall a b. [a] -> b -> b
`seqList` CoAxiom Branched -> Int -> [Coercion] -> Coercion
AxiomInstCo CoAxiom Branched
con Int
ind [Coercion]
args
go (UnivCo p :: UnivCoProvenance
p r :: Role
r t1 :: Type
t1 t2 :: Type
t2) = (((UnivCoProvenance -> Role -> Type -> Type -> Coercion
UnivCo (UnivCoProvenance -> Role -> Type -> Type -> Coercion)
-> UnivCoProvenance -> Role -> Type -> Type -> Coercion
forall a b. (a -> b) -> a -> b
$! (UnivCoProvenance -> UnivCoProvenance
go_prov UnivCoProvenance
p)) (Role -> Type -> Type -> Coercion)
-> Role -> Type -> Type -> Coercion
forall a b. (a -> b) -> a -> b
$! Role
r) (Type -> Type -> Coercion) -> Type -> Type -> Coercion
forall a b. (a -> b) -> a -> b
$!
TidyEnv -> Type -> Type
tidyType TidyEnv
env Type
t1) (Type -> Coercion) -> Type -> Coercion
forall a b. (a -> b) -> a -> b
$! TidyEnv -> Type -> Type
tidyType TidyEnv
env Type
t2
go (SymCo co :: Coercion
co) = Coercion -> Coercion
SymCo (Coercion -> Coercion) -> Coercion -> Coercion
forall a b. (a -> b) -> a -> b
$! Coercion -> Coercion
go Coercion
co
go (TransCo co1 :: Coercion
co1 co2 :: Coercion
co2) = (Coercion -> Coercion -> Coercion
TransCo (Coercion -> Coercion -> Coercion)
-> Coercion -> Coercion -> Coercion
forall a b. (a -> b) -> a -> b
$! Coercion -> Coercion
go Coercion
co1) (Coercion -> Coercion) -> Coercion -> Coercion
forall a b. (a -> b) -> a -> b
$! Coercion -> Coercion
go Coercion
co2
go (NthCo r :: Role
r d :: Int
d co :: Coercion
co) = Role -> Int -> Coercion -> Coercion
NthCo Role
r Int
d (Coercion -> Coercion) -> Coercion -> Coercion
forall a b. (a -> b) -> a -> b
$! Coercion -> Coercion
go Coercion
co
go (LRCo lr :: LeftOrRight
lr co :: Coercion
co) = LeftOrRight -> Coercion -> Coercion
LRCo LeftOrRight
lr (Coercion -> Coercion) -> Coercion -> Coercion
forall a b. (a -> b) -> a -> b
$! Coercion -> Coercion
go Coercion
co
go (InstCo co :: Coercion
co ty :: Coercion
ty) = (Coercion -> Coercion -> Coercion
InstCo (Coercion -> Coercion -> Coercion)
-> Coercion -> Coercion -> Coercion
forall a b. (a -> b) -> a -> b
$! Coercion -> Coercion
go Coercion
co) (Coercion -> Coercion) -> Coercion -> Coercion
forall a b. (a -> b) -> a -> b
$! Coercion -> Coercion
go Coercion
ty
go (KindCo co :: Coercion
co) = Coercion -> Coercion
KindCo (Coercion -> Coercion) -> Coercion -> Coercion
forall a b. (a -> b) -> a -> b
$! Coercion -> Coercion
go Coercion
co
go (SubCo co :: Coercion
co) = Coercion -> Coercion
SubCo (Coercion -> Coercion) -> Coercion -> Coercion
forall a b. (a -> b) -> a -> b
$! Coercion -> Coercion
go Coercion
co
go (AxiomRuleCo ax :: CoAxiomRule
ax cos :: [Coercion]
cos) = let cos1 :: [Coercion]
cos1 = TidyEnv -> [Coercion] -> [Coercion]
tidyCos TidyEnv
env [Coercion]
cos
in [Coercion]
cos1 [Coercion] -> Coercion -> Coercion
forall a b. [a] -> b -> b
`seqList` CoAxiomRule -> [Coercion] -> Coercion
AxiomRuleCo CoAxiomRule
ax [Coercion]
cos1
go_prov :: UnivCoProvenance -> UnivCoProvenance
go_prov UnsafeCoerceProv = UnivCoProvenance
UnsafeCoerceProv
go_prov (PhantomProv co :: Coercion
co) = Coercion -> UnivCoProvenance
PhantomProv (Coercion -> Coercion
go Coercion
co)
go_prov (ProofIrrelProv co :: Coercion
co) = Coercion -> UnivCoProvenance
ProofIrrelProv (Coercion -> Coercion
go Coercion
co)
go_prov p :: UnivCoProvenance
p@(PluginProv _) = UnivCoProvenance
p
tidyCos :: TidyEnv -> [Coercion] -> [Coercion]
tidyCos :: TidyEnv -> [Coercion] -> [Coercion]
tidyCos env :: TidyEnv
env = (Coercion -> Coercion) -> [Coercion] -> [Coercion]
forall a b. (a -> b) -> [a] -> [b]
map (TidyEnv -> Coercion -> Coercion
tidyCo TidyEnv
env)
typeSize :: Type -> Int
typeSize :: Type -> Int
typeSize (LitTy {}) = 1
typeSize (TyVarTy {}) = 1
typeSize (AppTy t1 :: Type
t1 t2 :: Type
t2) = Type -> Int
typeSize Type
t1 Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Type -> Int
typeSize Type
t2
typeSize (FunTy t1 :: Type
t1 t2 :: Type
t2) = Type -> Int
typeSize Type
t1 Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Type -> Int
typeSize Type
t2
typeSize (ForAllTy (Bndr tv :: Id
tv _) t :: Type
t) = Type -> Int
typeSize (Id -> Type
varType Id
tv) Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Type -> Int
typeSize Type
t
typeSize (TyConApp _ ts :: [Type]
ts) = 1 Int -> Int -> Int
forall a. Num a => a -> a -> a
+ [Int] -> Int
forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
sum ((Type -> Int) -> [Type] -> [Int]
forall a b. (a -> b) -> [a] -> [b]
map Type -> Int
typeSize [Type]
ts)
typeSize (CastTy ty :: Type
ty co :: Coercion
co) = Type -> Int
typeSize Type
ty Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Coercion -> Int
coercionSize Coercion
co
typeSize (CoercionTy co :: Coercion
co) = Coercion -> Int
coercionSize Coercion
co
coercionSize :: Coercion -> Int
coercionSize :: Coercion -> Int
coercionSize (Refl ty :: Type
ty) = Type -> Int
typeSize Type
ty
coercionSize (GRefl _ ty :: Type
ty MRefl) = Type -> Int
typeSize Type
ty
coercionSize (GRefl _ ty :: Type
ty (MCo co :: Coercion
co)) = 1 Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Type -> Int
typeSize Type
ty Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Coercion -> Int
coercionSize Coercion
co
coercionSize (TyConAppCo _ _ args :: [Coercion]
args) = 1 Int -> Int -> Int
forall a. Num a => a -> a -> a
+ [Int] -> Int
forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
sum ((Coercion -> Int) -> [Coercion] -> [Int]
forall a b. (a -> b) -> [a] -> [b]
map Coercion -> Int
coercionSize [Coercion]
args)
coercionSize (AppCo co :: Coercion
co arg :: Coercion
arg) = Coercion -> Int
coercionSize Coercion
co Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Coercion -> Int
coercionSize Coercion
arg
coercionSize (ForAllCo _ h :: Coercion
h co :: Coercion
co) = 1 Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Coercion -> Int
coercionSize Coercion
co Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Coercion -> Int
coercionSize Coercion
h
coercionSize (FunCo _ co1 :: Coercion
co1 co2 :: Coercion
co2) = 1 Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Coercion -> Int
coercionSize Coercion
co1 Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Coercion -> Int
coercionSize Coercion
co2
coercionSize (CoVarCo _) = 1
coercionSize (HoleCo _) = 1
coercionSize (AxiomInstCo _ _ args :: [Coercion]
args) = 1 Int -> Int -> Int
forall a. Num a => a -> a -> a
+ [Int] -> Int
forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
sum ((Coercion -> Int) -> [Coercion] -> [Int]
forall a b. (a -> b) -> [a] -> [b]
map Coercion -> Int
coercionSize [Coercion]
args)
coercionSize (UnivCo p :: UnivCoProvenance
p _ t1 :: Type
t1 t2 :: Type
t2) = 1 Int -> Int -> Int
forall a. Num a => a -> a -> a
+ UnivCoProvenance -> Int
provSize UnivCoProvenance
p Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Type -> Int
typeSize Type
t1 Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Type -> Int
typeSize Type
t2
coercionSize (SymCo co :: Coercion
co) = 1 Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Coercion -> Int
coercionSize Coercion
co
coercionSize (TransCo co1 :: Coercion
co1 co2 :: Coercion
co2) = 1 Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Coercion -> Int
coercionSize Coercion
co1 Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Coercion -> Int
coercionSize Coercion
co2
coercionSize (NthCo _ _ co :: Coercion
co) = 1 Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Coercion -> Int
coercionSize Coercion
co
coercionSize (LRCo _ co :: Coercion
co) = 1 Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Coercion -> Int
coercionSize Coercion
co
coercionSize (InstCo co :: Coercion
co arg :: Coercion
arg) = 1 Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Coercion -> Int
coercionSize Coercion
co Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Coercion -> Int
coercionSize Coercion
arg
coercionSize (KindCo co :: Coercion
co) = 1 Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Coercion -> Int
coercionSize Coercion
co
coercionSize (SubCo co :: Coercion
co) = 1 Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Coercion -> Int
coercionSize Coercion
co
coercionSize (AxiomRuleCo _ cs :: [Coercion]
cs) = 1 Int -> Int -> Int
forall a. Num a => a -> a -> a
+ [Int] -> Int
forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
sum ((Coercion -> Int) -> [Coercion] -> [Int]
forall a b. (a -> b) -> [a] -> [b]
map Coercion -> Int
coercionSize [Coercion]
cs)
provSize :: UnivCoProvenance -> Int
provSize :: UnivCoProvenance -> Int
provSize UnsafeCoerceProv = 1
provSize (PhantomProv co :: Coercion
co) = 1 Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Coercion -> Int
coercionSize Coercion
co
provSize (ProofIrrelProv co :: Coercion
co) = 1 Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Coercion -> Int
coercionSize Coercion
co
provSize (PluginProv _) = 1