{-# OPTIONS_HADDOCK not-home #-}
{-# LANGUAGE CPP, DeriveDataTypeable, MultiWayIf, PatternSynonyms, BangPatterns #-}
module TyCoRep (
TyThing(..), tyThingCategory, pprTyThingCategory, pprShortTyThing,
Type( TyVarTy, AppTy, TyConApp, ForAllTy
, LitTy, CastTy, CoercionTy
, FunTy, ft_arg, ft_res, ft_af
),
TyLit(..),
KindOrType, Kind,
KnotTied,
PredType, ThetaType,
ArgFlag(..), AnonArgFlag(..), ForallVisFlag(..),
Coercion(..),
UnivCoProvenance(..),
CoercionHole(..), coHoleCoVar, setCoHoleCoVar,
CoercionN, CoercionR, CoercionP, KindCoercion,
MCoercion(..), MCoercionR, MCoercionN,
mkTyConTy, mkTyVarTy, mkTyVarTys,
mkTyCoVarTy, mkTyCoVarTys,
mkFunTy, mkVisFunTy, mkInvisFunTy, mkVisFunTys, mkInvisFunTys,
mkForAllTy, mkForAllTys,
mkPiTy, mkPiTys,
TyCoBinder(..), TyCoVarBinder, TyBinder,
binderVar, binderVars, binderType, binderArgFlag,
delBinderVar,
isInvisibleArgFlag, isVisibleArgFlag,
isInvisibleBinder, isVisibleBinder,
isTyBinder, isNamedBinder,
pickLR,
typeSize, coercionSize, provSize
) where
#include "GhclibHsVersions.h"
import GhcPrelude
import {-# SOURCE #-} TyCoPpr ( pprType, pprCo, pprTyLit )
import {-# SOURCE #-} ConLike ( ConLike(..), conLikeName )
import IfaceType
import Var
import VarSet
import Name hiding ( varName )
import TyCon
import CoAxiom
import BasicTypes ( LeftOrRight(..), pickLR )
import Outputable
import FastString
import Util
import qualified Data.Data as Data hiding ( TyCon )
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 -> AnonArgFlag
ft_af :: AnonArgFlag
, Type -> Type
ft_arg :: Type
, Type -> Type
ft_res :: 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
instance Outputable Type where
ppr :: Type -> SDoc
ppr = Type -> SDoc
pprType
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)
instance Outputable TyLit where
ppr :: TyLit -> SDoc
ppr = TyLit -> SDoc
pprTyLit
type KnotTied ty = ty
data TyCoBinder
= Named TyCoVarBinder
| Anon AnonArgFlag 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
instance Outputable TyCoBinder where
ppr :: TyCoBinder -> SDoc
ppr (Anon af :: AnonArgFlag
af ty :: Type
ty) = AnonArgFlag -> SDoc
forall a. Outputable a => a -> SDoc
ppr AnonArgFlag
af 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)
type TyBinder = TyCoBinder
delBinderVar :: VarSet -> TyCoVarBinder -> VarSet
delBinderVar :: VarSet -> VarBndr Id ArgFlag -> 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 InvisArg _) = Bool
True
isInvisibleBinder (Anon VisArg _) = Bool
False
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 :: VarBndr Id ArgFlag
bnd) = VarBndr Id ArgFlag -> Bool
isTyVarBinder VarBndr Id ArgFlag
bnd
isTyBinder _ = Bool
True
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`, `mkVisFunTy`, `mkInvisFunTy`
mkFunTy :: AnonArgFlag -> Type -> Type -> Type
mkFunTy :: AnonArgFlag -> Type -> Type -> Type
mkFunTy af :: AnonArgFlag
af arg :: Type
arg res :: Type
res = FunTy :: AnonArgFlag -> Type -> Type -> Type
FunTy { ft_af :: AnonArgFlag
ft_af = AnonArgFlag
af, ft_arg :: Type
ft_arg = Type
arg, ft_res :: Type
ft_res = Type
res }
mkVisFunTy, mkInvisFunTy :: Type -> Type -> Type
mkVisFunTy :: Type -> Type -> Type
mkVisFunTy = AnonArgFlag -> Type -> Type -> Type
mkFunTy AnonArgFlag
VisArg
mkInvisFunTy :: Type -> Type -> Type
mkInvisFunTy = AnonArgFlag -> Type -> Type -> Type
mkFunTy AnonArgFlag
InvisArg
mkVisFunTys, mkInvisFunTys :: [Type] -> Type -> Type
mkVisFunTys :: [Type] -> Type -> Type
mkVisFunTys 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
mkVisFunTy Type
ty [Type]
tys
mkInvisFunTys :: [Type] -> Type -> Type
mkInvisFunTys 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
mkInvisFunTy Type
ty [Type]
tys
mkForAllTy :: TyCoVar -> ArgFlag -> Type -> Type
mkForAllTy :: Id -> ArgFlag -> Type -> Type
mkForAllTy tv :: Id
tv vis :: ArgFlag
vis ty :: Type
ty = VarBndr Id ArgFlag -> Type -> Type
ForAllTy (Id -> ArgFlag -> VarBndr Id ArgFlag
forall var argf. var -> argf -> VarBndr var argf
Bndr Id
tv ArgFlag
vis) Type
ty
mkForAllTys :: [TyCoVarBinder] -> Type -> Type
mkForAllTys :: [VarBndr Id ArgFlag] -> Type -> Type
mkForAllTys tyvars :: [VarBndr Id ArgFlag]
tyvars ty :: Type
ty = (VarBndr Id ArgFlag -> Type -> Type)
-> Type -> [VarBndr Id ArgFlag] -> Type
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr VarBndr Id ArgFlag -> Type -> Type
ForAllTy Type
ty [VarBndr Id ArgFlag]
tyvars
mkPiTy:: TyCoBinder -> Type -> Type
mkPiTy :: TyCoBinder -> Type -> Type
mkPiTy (Anon af :: AnonArgFlag
af ty1 :: Type
ty1) ty2 :: Type
ty2 = FunTy :: AnonArgFlag -> Type -> Type -> Type
FunTy { ft_af :: AnonArgFlag
ft_af = AnonArgFlag
af, ft_arg :: Type
ft_arg = Type
ty1, ft_res :: Type
ft_res = 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
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 []
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
instance Outputable Coercion where
ppr :: Coercion -> SDoc
ppr = Coercion -> SDoc
pprCo
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)
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