{-# LANGUAGE DeriveDataTypeable #-}
{-# OPTIONS_HADDOCK not-home #-}
module GHC.Core.TyCo.Rep (
Type(..),
TyLit(..),
KindOrType, Kind,
RuntimeRepType, LevityType,
KnotTied,
PredType, ThetaType, FRRType,
ForAllTyFlag(..), FunTyFlag(..),
Coercion(..), CoSel(..), FunSel(..),
UnivCoProvenance(..),
CoercionHole(..), coHoleCoVar, setCoHoleCoVar,
CoercionN, CoercionR, CoercionP, KindCoercion,
MCoercion(..), MCoercionR, MCoercionN,
mkNakedTyConTy, mkTyVarTy, mkTyVarTys,
mkTyCoVarTy, mkTyCoVarTys,
mkFunTy, mkNakedFunTy,
mkVisFunTy, mkScaledFunTys,
mkInvisFunTy, mkInvisFunTys,
tcMkVisFunTy, tcMkInvisFunTy, tcMkScaledFunTys,
mkForAllTy, mkForAllTys, mkInvisForAllTys,
mkPiTy, mkPiTys,
mkVisFunTyMany, mkVisFunTysMany,
nonDetCmpTyLit, cmpTyLit,
pickLR,
TyCoFolder(..), foldTyCo, noView,
typeSize, coercionSize, provSize,
Scaled(..), scaledMult, scaledThing, mapScaledType, Mult
) where
import GHC.Prelude
import {-# SOURCE #-} GHC.Core.TyCo.Ppr ( pprType, pprCo, pprTyLit )
import {-# SOURCE #-} GHC.Builtin.Types
import {-# SOURCE #-} GHC.Core.Type( chooseFunTyFlag, typeKind, typeTypeOrConstraint )
import GHC.Types.Var
import GHC.Core.TyCon
import GHC.Core.Coercion.Axiom
import GHC.Builtin.Names
import GHC.Types.Basic ( LeftOrRight(..), pickLR )
import GHC.Utils.Outputable
import GHC.Data.FastString
import GHC.Utils.Misc
import GHC.Utils.Panic
import GHC.Utils.Binary
import qualified Data.Data as Data hiding ( TyCon )
import Data.IORef ( IORef )
import Control.DeepSeq
type KindOrType = Type
type Kind = Type
type RuntimeRepType = Type
type LevityType = Type
type FRRType = Type
data Type
= TyVarTy Var
| AppTy
Type
Type
| TyConApp
TyCon
[KindOrType]
| ForAllTy
{-# UNPACK #-} !ForAllTyBinder
Type
| FunTy
{ Kind -> FunTyFlag
ft_af :: FunTyFlag
, Kind -> Kind
ft_mult :: Mult
, Kind -> Kind
ft_arg :: Type
, Kind -> Kind
ft_res :: Type }
| LitTy TyLit
| CastTy
Type
KindCoercion
| CoercionTy
Coercion
deriving Typeable Kind
Typeable Kind =>
(forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Kind -> c Kind)
-> (forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Kind)
-> (Kind -> Constr)
-> (Kind -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Kind))
-> (forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Kind))
-> ((forall b. Data b => b -> b) -> Kind -> Kind)
-> (forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Kind -> r)
-> (forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Kind -> r)
-> (forall u. (forall d. Data d => d -> u) -> Kind -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> Kind -> u)
-> (forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Kind -> m Kind)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Kind -> m Kind)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Kind -> m Kind)
-> Data Kind
Kind -> Constr
Kind -> DataType
(forall b. Data b => b -> b) -> Kind -> Kind
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) -> Kind -> u
forall u. (forall d. Data d => d -> u) -> Kind -> [u]
forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Kind -> r
forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Kind -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Kind -> m Kind
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Kind -> m Kind
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Kind
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Kind -> c Kind
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Kind)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Kind)
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Kind -> c Kind
gfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Kind -> c Kind
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Kind
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Kind
$ctoConstr :: Kind -> Constr
toConstr :: Kind -> Constr
$cdataTypeOf :: Kind -> DataType
dataTypeOf :: Kind -> DataType
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Kind)
dataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Kind)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Kind)
dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Kind)
$cgmapT :: (forall b. Data b => b -> b) -> Kind -> Kind
gmapT :: (forall b. Data b => b -> b) -> Kind -> Kind
$cgmapQl :: forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Kind -> r
gmapQl :: forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Kind -> r
$cgmapQr :: forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Kind -> r
gmapQr :: forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Kind -> r
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> Kind -> [u]
gmapQ :: forall u. (forall d. Data d => d -> u) -> Kind -> [u]
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Kind -> u
gmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Kind -> u
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Kind -> m Kind
gmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Kind -> m Kind
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Kind -> m Kind
gmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Kind -> m Kind
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Kind -> m Kind
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Kind -> m Kind
Data.Data
instance Outputable Type where
ppr :: Kind -> SDoc
ppr = Kind -> SDoc
pprType
data TyLit
= NumTyLit Integer
| StrTyLit FastString
| CharTyLit Char
deriving (TyLit -> TyLit -> Bool
(TyLit -> TyLit -> Bool) -> (TyLit -> TyLit -> Bool) -> Eq TyLit
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: TyLit -> TyLit -> Bool
== :: TyLit -> TyLit -> Bool
$c/= :: TyLit -> TyLit -> Bool
/= :: TyLit -> TyLit -> Bool
Eq, Typeable TyLit
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 -> Constr
TyLit -> DataType
(forall b. Data b => b -> b) -> TyLit -> 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)
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> TyLit -> c TyLit
gfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> TyLit -> c TyLit
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c TyLit
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c TyLit
$ctoConstr :: TyLit -> Constr
toConstr :: TyLit -> Constr
$cdataTypeOf :: TyLit -> DataType
dataTypeOf :: TyLit -> DataType
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c TyLit)
dataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c TyLit)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c TyLit)
dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c TyLit)
$cgmapT :: (forall b. Data b => b -> b) -> TyLit -> TyLit
gmapT :: (forall b. Data b => b -> b) -> TyLit -> TyLit
$cgmapQl :: forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> TyLit -> r
gmapQl :: forall r r'.
(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
gmapQr :: forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> TyLit -> r
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> TyLit -> [u]
gmapQ :: forall u. (forall d. Data d => d -> u) -> TyLit -> [u]
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> TyLit -> u
gmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> TyLit -> u
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> TyLit -> m TyLit
gmapM :: forall (m :: * -> *).
Monad m =>
(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
gmapMp :: forall (m :: * -> *).
MonadPlus m =>
(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
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> TyLit -> m TyLit
Data.Data)
nonDetCmpTyLit :: TyLit -> TyLit -> Ordering
nonDetCmpTyLit :: TyLit -> TyLit -> Ordering
nonDetCmpTyLit = (FastString -> NonDetFastString) -> TyLit -> TyLit -> Ordering
forall r. Ord r => (FastString -> r) -> TyLit -> TyLit -> Ordering
cmpTyLitWith FastString -> NonDetFastString
NonDetFastString
cmpTyLit :: TyLit -> TyLit -> Ordering
cmpTyLit :: TyLit -> TyLit -> Ordering
cmpTyLit = (FastString -> LexicalFastString) -> TyLit -> TyLit -> Ordering
forall r. Ord r => (FastString -> r) -> TyLit -> TyLit -> Ordering
cmpTyLitWith FastString -> LexicalFastString
LexicalFastString
{-# INLINE cmpTyLitWith #-}
cmpTyLitWith :: Ord r => (FastString -> r) -> TyLit -> TyLit -> Ordering
cmpTyLitWith :: forall r. Ord r => (FastString -> r) -> TyLit -> TyLit -> Ordering
cmpTyLitWith FastString -> r
_ (NumTyLit Integer
x) (NumTyLit Integer
y) = Integer -> Integer -> Ordering
forall a. Ord a => a -> a -> Ordering
compare Integer
x Integer
y
cmpTyLitWith FastString -> r
w (StrTyLit FastString
x) (StrTyLit FastString
y) = r -> r -> Ordering
forall a. Ord a => a -> a -> Ordering
compare (FastString -> r
w FastString
x) (FastString -> r
w FastString
y)
cmpTyLitWith FastString -> r
_ (CharTyLit Char
x) (CharTyLit Char
y) = Char -> Char -> Ordering
forall a. Ord a => a -> a -> Ordering
compare Char
x Char
y
cmpTyLitWith FastString -> r
_ TyLit
a TyLit
b = Int -> Int -> Ordering
forall a. Ord a => a -> a -> Ordering
compare (TyLit -> Int
tag TyLit
a) (TyLit -> Int
tag TyLit
b)
where
tag :: TyLit -> Int
tag :: TyLit -> Int
tag NumTyLit{} = Int
0
tag StrTyLit{} = Int
1
tag CharTyLit{} = Int
2
instance Outputable TyLit where
ppr :: TyLit -> SDoc
ppr = TyLit -> SDoc
pprTyLit
type KnotTied ty = ty
type PredType = Type
type ThetaType = [PredType]
mkTyVarTy :: TyVar -> Type
mkTyVarTy :: TyVar -> Kind
mkTyVarTy TyVar
v = Bool -> SDoc -> Kind -> Kind
forall a. HasCallStack => Bool -> SDoc -> a -> a
assertPpr (TyVar -> Bool
isTyVar TyVar
v) (TyVar -> SDoc
forall a. Outputable a => a -> SDoc
ppr TyVar
v SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> SDoc
dcolon SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> Kind -> SDoc
forall a. Outputable a => a -> SDoc
ppr (TyVar -> Kind
tyVarKind TyVar
v)) (Kind -> Kind) -> Kind -> Kind
forall a b. (a -> b) -> a -> b
$
TyVar -> Kind
TyVarTy TyVar
v
mkTyVarTys :: [TyVar] -> [Type]
mkTyVarTys :: [TyVar] -> [Kind]
mkTyVarTys = (TyVar -> Kind) -> [TyVar] -> [Kind]
forall a b. (a -> b) -> [a] -> [b]
map TyVar -> Kind
mkTyVarTy
mkTyCoVarTy :: TyCoVar -> Type
mkTyCoVarTy :: TyVar -> Kind
mkTyCoVarTy TyVar
v
| TyVar -> Bool
isTyVar TyVar
v
= TyVar -> Kind
TyVarTy TyVar
v
| Bool
otherwise
= KindCoercion -> Kind
CoercionTy (TyVar -> KindCoercion
CoVarCo TyVar
v)
mkTyCoVarTys :: [TyCoVar] -> [Type]
mkTyCoVarTys :: [TyVar] -> [Kind]
mkTyCoVarTys = (TyVar -> Kind) -> [TyVar] -> [Kind]
forall a b. (a -> b) -> [a] -> [b]
map TyVar -> Kind
mkTyCoVarTy
infixr 3 `mkFunTy`, `mkInvisFunTy`, `mkVisFunTyMany`
mkNakedFunTy :: FunTyFlag -> Kind -> Kind -> Kind
mkNakedFunTy :: FunTyFlag -> Kind -> Kind -> Kind
mkNakedFunTy FunTyFlag
af Kind
arg Kind
res
= FunTy { ft_af :: FunTyFlag
ft_af = FunTyFlag
af, ft_mult :: Kind
ft_mult = Kind
manyDataConTy
, ft_arg :: Kind
ft_arg = Kind
arg, ft_res :: Kind
ft_res = Kind
res }
mkFunTy :: HasDebugCallStack => FunTyFlag -> Mult -> Type -> Type -> Type
mkFunTy :: (() :: Constraint) => FunTyFlag -> Kind -> Kind -> Kind -> Kind
mkFunTy FunTyFlag
af Kind
mult Kind
arg Kind
res
= Bool -> SDoc -> Kind -> Kind
forall a. HasCallStack => Bool -> SDoc -> a -> a
assertPpr (FunTyFlag
af FunTyFlag -> FunTyFlag -> Bool
forall a. Eq a => a -> a -> Bool
== (() :: Constraint) => Kind -> Kind -> FunTyFlag
Kind -> Kind -> FunTyFlag
chooseFunTyFlag Kind
arg Kind
res) ([SDoc] -> SDoc
forall doc. IsDoc doc => [doc] -> doc
vcat
[ String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"af" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> FunTyFlag -> SDoc
forall a. Outputable a => a -> SDoc
ppr FunTyFlag
af
, String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"chooseAAF" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> FunTyFlag -> SDoc
forall a. Outputable a => a -> SDoc
ppr ((() :: Constraint) => Kind -> Kind -> FunTyFlag
Kind -> Kind -> FunTyFlag
chooseFunTyFlag Kind
arg Kind
res)
, String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"arg" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> Kind -> SDoc
forall a. Outputable a => a -> SDoc
ppr Kind
arg SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> SDoc
dcolon SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> Kind -> SDoc
forall a. Outputable a => a -> SDoc
ppr ((() :: Constraint) => Kind -> Kind
Kind -> Kind
typeKind Kind
arg)
, String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"res" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> Kind -> SDoc
forall a. Outputable a => a -> SDoc
ppr Kind
res SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> SDoc
dcolon SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> Kind -> SDoc
forall a. Outputable a => a -> SDoc
ppr ((() :: Constraint) => Kind -> Kind
Kind -> Kind
typeKind Kind
res) ]) (Kind -> Kind) -> Kind -> Kind
forall a b. (a -> b) -> a -> b
$
FunTy { ft_af :: FunTyFlag
ft_af = FunTyFlag
af
, ft_mult :: Kind
ft_mult = Kind
mult
, ft_arg :: Kind
ft_arg = Kind
arg
, ft_res :: Kind
ft_res = Kind
res }
mkInvisFunTy :: HasDebugCallStack => Type -> Type -> Type
mkInvisFunTy :: (() :: Constraint) => Kind -> Kind -> Kind
mkInvisFunTy Kind
arg Kind
res
= (() :: Constraint) => FunTyFlag -> Kind -> Kind -> Kind -> Kind
FunTyFlag -> Kind -> Kind -> Kind -> Kind
mkFunTy (TypeOrConstraint -> FunTyFlag
invisArg ((() :: Constraint) => Kind -> TypeOrConstraint
Kind -> TypeOrConstraint
typeTypeOrConstraint Kind
res)) Kind
manyDataConTy Kind
arg Kind
res
mkInvisFunTys :: HasDebugCallStack => [Type] -> Type -> Type
mkInvisFunTys :: (() :: Constraint) => [Kind] -> Kind -> Kind
mkInvisFunTys [Kind]
args Kind
res
= (Kind -> Kind -> Kind) -> Kind -> [Kind] -> Kind
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr ((() :: Constraint) => FunTyFlag -> Kind -> Kind -> Kind -> Kind
FunTyFlag -> Kind -> Kind -> Kind -> Kind
mkFunTy FunTyFlag
af Kind
manyDataConTy) Kind
res [Kind]
args
where
af :: FunTyFlag
af = TypeOrConstraint -> FunTyFlag
invisArg ((() :: Constraint) => Kind -> TypeOrConstraint
Kind -> TypeOrConstraint
typeTypeOrConstraint Kind
res)
tcMkVisFunTy :: Mult -> Type -> Type -> Type
tcMkVisFunTy :: Kind -> Kind -> Kind -> Kind
tcMkVisFunTy Kind
mult Kind
arg Kind
res
= FunTy { ft_af :: FunTyFlag
ft_af = FunTyFlag
visArgTypeLike, ft_mult :: Kind
ft_mult = Kind
mult
, ft_arg :: Kind
ft_arg = Kind
arg, ft_res :: Kind
ft_res = Kind
res }
tcMkInvisFunTy :: TypeOrConstraint -> Type -> Type -> Type
tcMkInvisFunTy :: TypeOrConstraint -> Kind -> Kind -> Kind
tcMkInvisFunTy TypeOrConstraint
res_torc Kind
arg Kind
res
= FunTy { ft_af :: FunTyFlag
ft_af = TypeOrConstraint -> FunTyFlag
invisArg TypeOrConstraint
res_torc, ft_mult :: Kind
ft_mult = Kind
manyDataConTy
, ft_arg :: Kind
ft_arg = Kind
arg, ft_res :: Kind
ft_res = Kind
res }
mkVisFunTy :: HasDebugCallStack => Mult -> Type -> Type -> Type
mkVisFunTy :: (() :: Constraint) => Kind -> Kind -> Kind -> Kind
mkVisFunTy = (() :: Constraint) => FunTyFlag -> Kind -> Kind -> Kind -> Kind
FunTyFlag -> Kind -> Kind -> Kind -> Kind
mkFunTy FunTyFlag
visArgTypeLike
mkVisFunTyMany :: HasDebugCallStack => Type -> Type -> Type
mkVisFunTyMany :: (() :: Constraint) => Kind -> Kind -> Kind
mkVisFunTyMany = (() :: Constraint) => Kind -> Kind -> Kind -> Kind
Kind -> Kind -> Kind -> Kind
mkVisFunTy Kind
manyDataConTy
mkVisFunTysMany :: [Type] -> Type -> Type
mkVisFunTysMany :: [Kind] -> Kind -> Kind
mkVisFunTysMany [Kind]
tys Kind
ty = (Kind -> Kind -> Kind) -> Kind -> [Kind] -> Kind
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (() :: Constraint) => Kind -> Kind -> Kind
Kind -> Kind -> Kind
mkVisFunTyMany Kind
ty [Kind]
tys
mkScaledFunTy :: HasDebugCallStack => FunTyFlag -> Scaled Type -> Type -> Type
mkScaledFunTy :: (() :: Constraint) => FunTyFlag -> Scaled Kind -> Kind -> Kind
mkScaledFunTy FunTyFlag
af (Scaled Kind
mult Kind
arg) Kind
res = (() :: Constraint) => FunTyFlag -> Kind -> Kind -> Kind -> Kind
FunTyFlag -> Kind -> Kind -> Kind -> Kind
mkFunTy FunTyFlag
af Kind
mult Kind
arg Kind
res
mkScaledFunTys :: HasDebugCallStack => [Scaled Type] -> Type -> Type
mkScaledFunTys :: (() :: Constraint) => [Scaled Kind] -> Kind -> Kind
mkScaledFunTys [Scaled Kind]
tys Kind
ty = (Scaled Kind -> Kind -> Kind) -> Kind -> [Scaled Kind] -> Kind
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr ((() :: Constraint) => FunTyFlag -> Scaled Kind -> Kind -> Kind
FunTyFlag -> Scaled Kind -> Kind -> Kind
mkScaledFunTy FunTyFlag
af) Kind
ty [Scaled Kind]
tys
where
af :: FunTyFlag
af = TypeOrConstraint -> FunTyFlag
visArg ((() :: Constraint) => Kind -> TypeOrConstraint
Kind -> TypeOrConstraint
typeTypeOrConstraint Kind
ty)
tcMkScaledFunTys :: [Scaled Type] -> Type -> Type
tcMkScaledFunTys :: [Scaled Kind] -> Kind -> Kind
tcMkScaledFunTys [Scaled Kind]
tys Kind
ty = (Scaled Kind -> Kind -> Kind) -> Kind -> [Scaled Kind] -> Kind
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr Scaled Kind -> Kind -> Kind
mk Kind
ty [Scaled Kind]
tys
where
mk :: Scaled Kind -> Kind -> Kind
mk (Scaled Kind
mult Kind
arg) Kind
res = Kind -> Kind -> Kind -> Kind
tcMkVisFunTy Kind
mult Kind
arg Kind
res
mkForAllTy :: ForAllTyBinder -> Type -> Type
mkForAllTy :: ForAllTyBinder -> Kind -> Kind
mkForAllTy = ForAllTyBinder -> Kind -> Kind
ForAllTy
mkForAllTys :: [ForAllTyBinder] -> Type -> Type
mkForAllTys :: [ForAllTyBinder] -> Kind -> Kind
mkForAllTys [ForAllTyBinder]
tyvars Kind
ty = (ForAllTyBinder -> Kind -> Kind)
-> Kind -> [ForAllTyBinder] -> Kind
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr ForAllTyBinder -> Kind -> Kind
ForAllTy Kind
ty [ForAllTyBinder]
tyvars
mkInvisForAllTys :: [InvisTVBinder] -> Type -> Type
mkInvisForAllTys :: [InvisTVBinder] -> Kind -> Kind
mkInvisForAllTys [InvisTVBinder]
tyvars = [ForAllTyBinder] -> Kind -> Kind
mkForAllTys ([InvisTVBinder] -> [ForAllTyBinder]
forall a. [VarBndr a Specificity] -> [VarBndr a ForAllTyFlag]
tyVarSpecToBinders [InvisTVBinder]
tyvars)
mkPiTy :: PiTyBinder -> Type -> Type
mkPiTy :: PiTyBinder -> Kind -> Kind
mkPiTy (Anon Scaled Kind
ty1 FunTyFlag
af) Kind
ty2 = (() :: Constraint) => FunTyFlag -> Scaled Kind -> Kind -> Kind
FunTyFlag -> Scaled Kind -> Kind -> Kind
mkScaledFunTy FunTyFlag
af Scaled Kind
ty1 Kind
ty2
mkPiTy (Named ForAllTyBinder
bndr) Kind
ty = ForAllTyBinder -> Kind -> Kind
mkForAllTy ForAllTyBinder
bndr Kind
ty
mkPiTys :: [PiTyBinder] -> Type -> Type
mkPiTys :: [PiTyBinder] -> Kind -> Kind
mkPiTys [PiTyBinder]
tbs Kind
ty = (PiTyBinder -> Kind -> Kind) -> Kind -> [PiTyBinder] -> Kind
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr PiTyBinder -> Kind -> Kind
mkPiTy Kind
ty [PiTyBinder]
tbs
mkNakedTyConTy :: TyCon -> Type
mkNakedTyConTy :: TyCon -> Kind
mkNakedTyConTy TyCon
tycon = TyCon -> [Kind] -> Kind
TyConApp TyCon
tycon []
data Coercion
=
Refl Type
| GRefl Role Type MCoercionN
| TyConAppCo Role TyCon [Coercion]
| AppCo Coercion CoercionN
| ForAllCo TyCoVar KindCoercion Coercion
| FunCo
{ KindCoercion -> Role
fco_role :: Role
, KindCoercion -> FunTyFlag
fco_afl :: FunTyFlag
, KindCoercion -> FunTyFlag
fco_afr :: FunTyFlag
, KindCoercion -> KindCoercion
fco_mult :: CoercionN
, KindCoercion -> KindCoercion
fco_arg, KindCoercion -> KindCoercion
fco_res :: Coercion }
| CoVarCo CoVar
| AxiomInstCo (CoAxiom Branched) BranchIndex [Coercion]
| AxiomRuleCo CoAxiomRule [Coercion]
| UnivCo UnivCoProvenance Role Type Type
| SymCo Coercion
| TransCo Coercion Coercion
| SelCo CoSel Coercion
| LRCo LeftOrRight CoercionN
| InstCo Coercion CoercionN
| KindCo Coercion
| SubCo CoercionN
| HoleCo CoercionHole
deriving Typeable KindCoercion
Typeable KindCoercion =>
(forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> KindCoercion -> c KindCoercion)
-> (forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c KindCoercion)
-> (KindCoercion -> Constr)
-> (KindCoercion -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c KindCoercion))
-> (forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c KindCoercion))
-> ((forall b. Data b => b -> b) -> KindCoercion -> KindCoercion)
-> (forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> KindCoercion -> r)
-> (forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> KindCoercion -> r)
-> (forall u. (forall d. Data d => d -> u) -> KindCoercion -> [u])
-> (forall u.
Int -> (forall d. Data d => d -> u) -> KindCoercion -> u)
-> (forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> KindCoercion -> m KindCoercion)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> KindCoercion -> m KindCoercion)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> KindCoercion -> m KindCoercion)
-> Data KindCoercion
KindCoercion -> Constr
KindCoercion -> DataType
(forall b. Data b => b -> b) -> KindCoercion -> KindCoercion
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) -> KindCoercion -> u
forall u. (forall d. Data d => d -> u) -> KindCoercion -> [u]
forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> KindCoercion -> r
forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> KindCoercion -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> KindCoercion -> m KindCoercion
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> KindCoercion -> m KindCoercion
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c KindCoercion
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> KindCoercion -> c KindCoercion
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c KindCoercion)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c KindCoercion)
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> KindCoercion -> c KindCoercion
gfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> KindCoercion -> c KindCoercion
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c KindCoercion
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c KindCoercion
$ctoConstr :: KindCoercion -> Constr
toConstr :: KindCoercion -> Constr
$cdataTypeOf :: KindCoercion -> DataType
dataTypeOf :: KindCoercion -> DataType
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c KindCoercion)
dataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c KindCoercion)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c KindCoercion)
dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c KindCoercion)
$cgmapT :: (forall b. Data b => b -> b) -> KindCoercion -> KindCoercion
gmapT :: (forall b. Data b => b -> b) -> KindCoercion -> KindCoercion
$cgmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> KindCoercion -> r
gmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> KindCoercion -> r
$cgmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> KindCoercion -> r
gmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> KindCoercion -> r
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> KindCoercion -> [u]
gmapQ :: forall u. (forall d. Data d => d -> u) -> KindCoercion -> [u]
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> KindCoercion -> u
gmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> KindCoercion -> u
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> KindCoercion -> m KindCoercion
gmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> KindCoercion -> m KindCoercion
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> KindCoercion -> m KindCoercion
gmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> KindCoercion -> m KindCoercion
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> KindCoercion -> m KindCoercion
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> KindCoercion -> m KindCoercion
Data.Data
data CoSel
= SelTyCon Int Role
| SelFun FunSel
| SelForAll
deriving( CoSel -> CoSel -> Bool
(CoSel -> CoSel -> Bool) -> (CoSel -> CoSel -> Bool) -> Eq CoSel
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: CoSel -> CoSel -> Bool
== :: CoSel -> CoSel -> Bool
$c/= :: CoSel -> CoSel -> Bool
/= :: CoSel -> CoSel -> Bool
Eq, Typeable CoSel
Typeable CoSel =>
(forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> CoSel -> c CoSel)
-> (forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c CoSel)
-> (CoSel -> Constr)
-> (CoSel -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c CoSel))
-> (forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c CoSel))
-> ((forall b. Data b => b -> b) -> CoSel -> CoSel)
-> (forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> CoSel -> r)
-> (forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> CoSel -> r)
-> (forall u. (forall d. Data d => d -> u) -> CoSel -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> CoSel -> u)
-> (forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> CoSel -> m CoSel)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> CoSel -> m CoSel)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> CoSel -> m CoSel)
-> Data CoSel
CoSel -> Constr
CoSel -> DataType
(forall b. Data b => b -> b) -> CoSel -> CoSel
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) -> CoSel -> u
forall u. (forall d. Data d => d -> u) -> CoSel -> [u]
forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> CoSel -> r
forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> CoSel -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> CoSel -> m CoSel
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> CoSel -> m CoSel
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c CoSel
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> CoSel -> c CoSel
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c CoSel)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c CoSel)
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> CoSel -> c CoSel
gfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> CoSel -> c CoSel
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c CoSel
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c CoSel
$ctoConstr :: CoSel -> Constr
toConstr :: CoSel -> Constr
$cdataTypeOf :: CoSel -> DataType
dataTypeOf :: CoSel -> DataType
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c CoSel)
dataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c CoSel)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c CoSel)
dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c CoSel)
$cgmapT :: (forall b. Data b => b -> b) -> CoSel -> CoSel
gmapT :: (forall b. Data b => b -> b) -> CoSel -> CoSel
$cgmapQl :: forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> CoSel -> r
gmapQl :: forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> CoSel -> r
$cgmapQr :: forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> CoSel -> r
gmapQr :: forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> CoSel -> r
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> CoSel -> [u]
gmapQ :: forall u. (forall d. Data d => d -> u) -> CoSel -> [u]
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> CoSel -> u
gmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> CoSel -> u
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> CoSel -> m CoSel
gmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> CoSel -> m CoSel
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> CoSel -> m CoSel
gmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> CoSel -> m CoSel
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> CoSel -> m CoSel
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> CoSel -> m CoSel
Data.Data )
data FunSel
= SelMult
| SelArg
| SelRes
deriving( FunSel -> FunSel -> Bool
(FunSel -> FunSel -> Bool)
-> (FunSel -> FunSel -> Bool) -> Eq FunSel
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: FunSel -> FunSel -> Bool
== :: FunSel -> FunSel -> Bool
$c/= :: FunSel -> FunSel -> Bool
/= :: FunSel -> FunSel -> Bool
Eq, Typeable FunSel
Typeable FunSel =>
(forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> FunSel -> c FunSel)
-> (forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c FunSel)
-> (FunSel -> Constr)
-> (FunSel -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c FunSel))
-> (forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c FunSel))
-> ((forall b. Data b => b -> b) -> FunSel -> FunSel)
-> (forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> FunSel -> r)
-> (forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> FunSel -> r)
-> (forall u. (forall d. Data d => d -> u) -> FunSel -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> FunSel -> u)
-> (forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> FunSel -> m FunSel)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> FunSel -> m FunSel)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> FunSel -> m FunSel)
-> Data FunSel
FunSel -> Constr
FunSel -> DataType
(forall b. Data b => b -> b) -> FunSel -> FunSel
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) -> FunSel -> u
forall u. (forall d. Data d => d -> u) -> FunSel -> [u]
forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> FunSel -> r
forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> FunSel -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> FunSel -> m FunSel
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> FunSel -> m FunSel
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c FunSel
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> FunSel -> c FunSel
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c FunSel)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c FunSel)
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> FunSel -> c FunSel
gfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> FunSel -> c FunSel
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c FunSel
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c FunSel
$ctoConstr :: FunSel -> Constr
toConstr :: FunSel -> Constr
$cdataTypeOf :: FunSel -> DataType
dataTypeOf :: FunSel -> DataType
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c FunSel)
dataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c FunSel)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c FunSel)
dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c FunSel)
$cgmapT :: (forall b. Data b => b -> b) -> FunSel -> FunSel
gmapT :: (forall b. Data b => b -> b) -> FunSel -> FunSel
$cgmapQl :: forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> FunSel -> r
gmapQl :: forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> FunSel -> r
$cgmapQr :: forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> FunSel -> r
gmapQr :: forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> FunSel -> r
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> FunSel -> [u]
gmapQ :: forall u. (forall d. Data d => d -> u) -> FunSel -> [u]
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> FunSel -> u
gmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> FunSel -> u
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> FunSel -> m FunSel
gmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> FunSel -> m FunSel
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> FunSel -> m FunSel
gmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> FunSel -> m FunSel
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> FunSel -> m FunSel
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> FunSel -> m FunSel
Data.Data )
type CoercionN = Coercion
type CoercionR = Coercion
type CoercionP = Coercion
type KindCoercion = CoercionN
instance Outputable Coercion where
ppr :: KindCoercion -> SDoc
ppr = KindCoercion -> SDoc
pprCo
instance Outputable CoSel where
ppr :: CoSel -> SDoc
ppr (SelTyCon Int
n Role
_r) = String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"Tc" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc
parens (Int -> SDoc
forall doc. IsLine doc => Int -> doc
int Int
n)
ppr CoSel
SelForAll = String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"All"
ppr (SelFun FunSel
fs) = String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"Fun" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc
parens (FunSel -> SDoc
forall a. Outputable a => a -> SDoc
ppr FunSel
fs)
instance Outputable FunSel where
ppr :: FunSel -> SDoc
ppr FunSel
SelMult = String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"mult"
ppr FunSel
SelArg = String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"arg"
ppr FunSel
SelRes = String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"res"
instance Binary CoSel where
put_ :: BinHandle -> CoSel -> IO ()
put_ BinHandle
bh (SelTyCon Int
n Role
r) = do { BinHandle -> Word8 -> IO ()
putByte BinHandle
bh Word8
0; BinHandle -> Int -> IO ()
forall a. Binary a => BinHandle -> a -> IO ()
put_ BinHandle
bh Int
n; BinHandle -> Role -> IO ()
forall a. Binary a => BinHandle -> a -> IO ()
put_ BinHandle
bh Role
r }
put_ BinHandle
bh CoSel
SelForAll = BinHandle -> Word8 -> IO ()
putByte BinHandle
bh Word8
1
put_ BinHandle
bh (SelFun FunSel
SelMult) = BinHandle -> Word8 -> IO ()
putByte BinHandle
bh Word8
2
put_ BinHandle
bh (SelFun FunSel
SelArg) = BinHandle -> Word8 -> IO ()
putByte BinHandle
bh Word8
3
put_ BinHandle
bh (SelFun FunSel
SelRes) = BinHandle -> Word8 -> IO ()
putByte BinHandle
bh Word8
4
get :: BinHandle -> IO CoSel
get BinHandle
bh = do { Word8
h <- BinHandle -> IO Word8
getByte BinHandle
bh
; case Word8
h of
Word8
0 -> do { Int
n <- BinHandle -> IO Int
forall a. Binary a => BinHandle -> IO a
get BinHandle
bh; Role
r <- BinHandle -> IO Role
forall a. Binary a => BinHandle -> IO a
get BinHandle
bh; CoSel -> IO CoSel
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Int -> Role -> CoSel
SelTyCon Int
n Role
r) }
Word8
1 -> CoSel -> IO CoSel
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return CoSel
SelForAll
Word8
2 -> CoSel -> IO CoSel
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (FunSel -> CoSel
SelFun FunSel
SelMult)
Word8
3 -> CoSel -> IO CoSel
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (FunSel -> CoSel
SelFun FunSel
SelArg)
Word8
_ -> CoSel -> IO CoSel
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (FunSel -> CoSel
SelFun FunSel
SelRes) }
instance NFData CoSel where
rnf :: CoSel -> ()
rnf (SelTyCon Int
n Role
r) = Int
n Int -> () -> ()
forall a b. a -> b -> b
`seq` Role
r Role -> () -> ()
forall a b. a -> b -> b
`seq` ()
rnf CoSel
SelForAll = ()
rnf (SelFun FunSel
fs) = FunSel
fs FunSel -> () -> ()
forall a b. a -> b -> b
`seq` ()
data MCoercion
= MRefl
| MCo Coercion
deriving Typeable MCoercionN
Typeable MCoercionN =>
(forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> MCoercionN -> c MCoercionN)
-> (forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c MCoercionN)
-> (MCoercionN -> Constr)
-> (MCoercionN -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c MCoercionN))
-> (forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c MCoercionN))
-> ((forall b. Data b => b -> b) -> MCoercionN -> MCoercionN)
-> (forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> MCoercionN -> r)
-> (forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> MCoercionN -> r)
-> (forall u. (forall d. Data d => d -> u) -> MCoercionN -> [u])
-> (forall u.
Int -> (forall d. Data d => d -> u) -> MCoercionN -> u)
-> (forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> MCoercionN -> m MCoercionN)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> MCoercionN -> m MCoercionN)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> MCoercionN -> m MCoercionN)
-> Data MCoercionN
MCoercionN -> Constr
MCoercionN -> DataType
(forall b. Data b => b -> b) -> MCoercionN -> MCoercionN
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) -> MCoercionN -> u
forall u. (forall d. Data d => d -> u) -> MCoercionN -> [u]
forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> MCoercionN -> r
forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> MCoercionN -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> MCoercionN -> m MCoercionN
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> MCoercionN -> m MCoercionN
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c MCoercionN
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> MCoercionN -> c MCoercionN
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c MCoercionN)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c MCoercionN)
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> MCoercionN -> c MCoercionN
gfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> MCoercionN -> c MCoercionN
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c MCoercionN
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c MCoercionN
$ctoConstr :: MCoercionN -> Constr
toConstr :: MCoercionN -> Constr
$cdataTypeOf :: MCoercionN -> DataType
dataTypeOf :: MCoercionN -> DataType
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c MCoercionN)
dataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c MCoercionN)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c MCoercionN)
dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c MCoercionN)
$cgmapT :: (forall b. Data b => b -> b) -> MCoercionN -> MCoercionN
gmapT :: (forall b. Data b => b -> b) -> MCoercionN -> MCoercionN
$cgmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> MCoercionN -> r
gmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> MCoercionN -> r
$cgmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> MCoercionN -> r
gmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> MCoercionN -> r
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> MCoercionN -> [u]
gmapQ :: forall u. (forall d. Data d => d -> u) -> MCoercionN -> [u]
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> MCoercionN -> u
gmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> MCoercionN -> u
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> MCoercionN -> m MCoercionN
gmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> MCoercionN -> m MCoercionN
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> MCoercionN -> m MCoercionN
gmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> MCoercionN -> m MCoercionN
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> MCoercionN -> m MCoercionN
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> MCoercionN -> m MCoercionN
Data.Data
type MCoercionR = MCoercion
type MCoercionN = MCoercion
instance Outputable MCoercion where
ppr :: MCoercionN -> SDoc
ppr MCoercionN
MRefl = String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"MRefl"
ppr (MCo KindCoercion
co) = String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"MCo" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> KindCoercion -> SDoc
forall a. Outputable a => a -> SDoc
ppr KindCoercion
co
data UnivCoProvenance
= PhantomProv KindCoercion
| ProofIrrelProv KindCoercion
| PluginProv String
| CorePrepProv
Bool
deriving Typeable UnivCoProvenance
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 -> Constr
UnivCoProvenance -> DataType
(forall b. Data b => b -> b)
-> UnivCoProvenance -> 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)
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> UnivCoProvenance -> c UnivCoProvenance
gfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> UnivCoProvenance -> c UnivCoProvenance
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c UnivCoProvenance
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c UnivCoProvenance
$ctoConstr :: UnivCoProvenance -> Constr
toConstr :: UnivCoProvenance -> Constr
$cdataTypeOf :: UnivCoProvenance -> DataType
dataTypeOf :: UnivCoProvenance -> DataType
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c UnivCoProvenance)
dataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c UnivCoProvenance)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c UnivCoProvenance)
dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c UnivCoProvenance)
$cgmapT :: (forall b. Data b => b -> b)
-> UnivCoProvenance -> UnivCoProvenance
gmapT :: (forall b. Data b => b -> b)
-> UnivCoProvenance -> UnivCoProvenance
$cgmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> UnivCoProvenance -> r
gmapQl :: forall r r'.
(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
gmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> UnivCoProvenance -> r
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> UnivCoProvenance -> [u]
gmapQ :: forall u. (forall d. Data d => d -> u) -> UnivCoProvenance -> [u]
$cgmapQi :: forall u.
Int -> (forall d. Data d => d -> u) -> UnivCoProvenance -> u
gmapQi :: forall u.
Int -> (forall d. Data d => d -> u) -> UnivCoProvenance -> u
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d)
-> UnivCoProvenance -> m UnivCoProvenance
gmapM :: forall (m :: * -> *).
Monad m =>
(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
gmapMp :: forall (m :: * -> *).
MonadPlus m =>
(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
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d)
-> UnivCoProvenance -> m UnivCoProvenance
Data.Data
instance Outputable UnivCoProvenance where
ppr :: UnivCoProvenance -> SDoc
ppr (PhantomProv KindCoercion
_) = String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"(phantom)"
ppr (ProofIrrelProv KindCoercion
_) = String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"(proof irrel.)"
ppr (PluginProv String
str) = SDoc -> SDoc
forall doc. IsLine doc => doc -> doc
parens (String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"plugin" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc
brackets (String -> SDoc
forall doc. IsLine doc => String -> doc
text String
str))
ppr (CorePrepProv Bool
_) = String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"(CorePrep)"
data CoercionHole
= CoercionHole { CoercionHole -> TyVar
ch_co_var :: CoVar
, CoercionHole -> IORef (Maybe KindCoercion)
ch_ref :: IORef (Maybe Coercion)
}
coHoleCoVar :: CoercionHole -> CoVar
coHoleCoVar :: CoercionHole -> TyVar
coHoleCoVar = CoercionHole -> TyVar
ch_co_var
setCoHoleCoVar :: CoercionHole -> CoVar -> CoercionHole
setCoHoleCoVar :: CoercionHole -> TyVar -> CoercionHole
setCoHoleCoVar CoercionHole
h TyVar
cv = CoercionHole
h { ch_co_var = cv }
instance Data.Data CoercionHole where
toConstr :: CoercionHole -> Constr
toConstr CoercionHole
_ = String -> Constr
abstractConstr String
"CoercionHole"
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c CoercionHole
gunfold forall b r. Data b => c (b -> r) -> c r
_ forall r. r -> c r
_ = String -> Constr -> c CoercionHole
forall a. HasCallStack => String -> a
error String
"gunfold"
dataTypeOf :: CoercionHole -> DataType
dataTypeOf CoercionHole
_ = String -> DataType
mkNoRepType String
"CoercionHole"
instance Outputable CoercionHole where
ppr :: CoercionHole -> SDoc
ppr (CoercionHole { ch_co_var :: CoercionHole -> TyVar
ch_co_var = TyVar
cv }) = SDoc -> SDoc
forall doc. IsLine doc => doc -> doc
braces (TyVar -> SDoc
forall a. Outputable a => a -> SDoc
ppr TyVar
cv)
instance Uniquable CoercionHole where
getUnique :: CoercionHole -> Unique
getUnique (CoercionHole { ch_co_var :: CoercionHole -> TyVar
ch_co_var = TyVar
cv }) = TyVar -> Unique
forall a. Uniquable a => a -> Unique
getUnique TyVar
cv
data TyCoFolder env a
= TyCoFolder
{ forall env a. TyCoFolder env a -> Kind -> Maybe Kind
tcf_view :: Type -> Maybe Type
, forall env a. TyCoFolder env a -> env -> TyVar -> a
tcf_tyvar :: env -> TyVar -> a
, forall env a. TyCoFolder env a -> env -> TyVar -> a
tcf_covar :: env -> CoVar -> a
, forall env a. TyCoFolder env a -> env -> CoercionHole -> a
tcf_hole :: env -> CoercionHole -> a
, forall env a.
TyCoFolder env a -> env -> TyVar -> ForAllTyFlag -> env
tcf_tycobinder :: env -> TyCoVar -> ForAllTyFlag -> env
}
{-# INLINE foldTyCo #-}
foldTyCo :: Monoid a => TyCoFolder env a -> env
-> (Type -> a, [Type] -> a, Coercion -> a, [Coercion] -> a)
foldTyCo :: forall a env.
Monoid a =>
TyCoFolder env a
-> env
-> (Kind -> a, [Kind] -> a, KindCoercion -> a, [KindCoercion] -> a)
foldTyCo (TyCoFolder { tcf_view :: forall env a. TyCoFolder env a -> Kind -> Maybe Kind
tcf_view = Kind -> Maybe Kind
view
, tcf_tyvar :: forall env a. TyCoFolder env a -> env -> TyVar -> a
tcf_tyvar = env -> TyVar -> a
tyvar
, tcf_tycobinder :: forall env a.
TyCoFolder env a -> env -> TyVar -> ForAllTyFlag -> env
tcf_tycobinder = env -> TyVar -> ForAllTyFlag -> env
tycobinder
, tcf_covar :: forall env a. TyCoFolder env a -> env -> TyVar -> a
tcf_covar = env -> TyVar -> a
covar
, tcf_hole :: forall env a. TyCoFolder env a -> env -> CoercionHole -> a
tcf_hole = env -> CoercionHole -> a
cohole }) env
env
= (env -> Kind -> a
go_ty env
env, env -> [Kind] -> a
go_tys env
env, env -> KindCoercion -> a
go_co env
env, env -> [KindCoercion] -> a
go_cos env
env)
where
go_ty :: env -> Kind -> a
go_ty env
env Kind
ty | Just Kind
ty' <- Kind -> Maybe Kind
view Kind
ty = env -> Kind -> a
go_ty env
env Kind
ty'
go_ty env
env (TyVarTy TyVar
tv) = env -> TyVar -> a
tyvar env
env TyVar
tv
go_ty env
env (AppTy Kind
t1 Kind
t2) = env -> Kind -> a
go_ty env
env Kind
t1 a -> a -> a
forall a. Monoid a => a -> a -> a
`mappend` env -> Kind -> a
go_ty env
env Kind
t2
go_ty env
_ (LitTy {}) = a
forall a. Monoid a => a
mempty
go_ty env
env (CastTy Kind
ty KindCoercion
co) = env -> Kind -> a
go_ty env
env Kind
ty a -> a -> a
forall a. Monoid a => a -> a -> a
`mappend` env -> KindCoercion -> a
go_co env
env KindCoercion
co
go_ty env
env (CoercionTy KindCoercion
co) = env -> KindCoercion -> a
go_co env
env KindCoercion
co
go_ty env
env (FunTy FunTyFlag
_ Kind
w Kind
arg Kind
res) = env -> Kind -> a
go_ty env
env Kind
w a -> a -> a
forall a. Monoid a => a -> a -> a
`mappend` env -> Kind -> a
go_ty env
env Kind
arg a -> a -> a
forall a. Monoid a => a -> a -> a
`mappend` env -> Kind -> a
go_ty env
env Kind
res
go_ty env
env (TyConApp TyCon
_ [Kind]
tys) = env -> [Kind] -> a
go_tys env
env [Kind]
tys
go_ty env
env (ForAllTy (Bndr TyVar
tv ForAllTyFlag
vis) Kind
inner)
= let !env' :: env
env' = env -> TyVar -> ForAllTyFlag -> env
tycobinder env
env TyVar
tv ForAllTyFlag
vis
in env -> Kind -> a
go_ty env
env (TyVar -> Kind
varType TyVar
tv) a -> a -> a
forall a. Monoid a => a -> a -> a
`mappend` env -> Kind -> a
go_ty env
env' Kind
inner
go_tys :: env -> [Kind] -> a
go_tys env
_ [] = a
forall a. Monoid a => a
mempty
go_tys env
env (Kind
t:[Kind]
ts) = env -> Kind -> a
go_ty env
env Kind
t a -> a -> a
forall a. Monoid a => a -> a -> a
`mappend` env -> [Kind] -> a
go_tys env
env [Kind]
ts
go_cos :: env -> [KindCoercion] -> a
go_cos env
_ [] = a
forall a. Monoid a => a
mempty
go_cos env
env (KindCoercion
c:[KindCoercion]
cs) = env -> KindCoercion -> a
go_co env
env KindCoercion
c a -> a -> a
forall a. Monoid a => a -> a -> a
`mappend` env -> [KindCoercion] -> a
go_cos env
env [KindCoercion]
cs
go_co :: env -> KindCoercion -> a
go_co env
env (Refl Kind
ty) = env -> Kind -> a
go_ty env
env Kind
ty
go_co env
env (GRefl Role
_ Kind
ty MCoercionN
MRefl) = env -> Kind -> a
go_ty env
env Kind
ty
go_co env
env (GRefl Role
_ Kind
ty (MCo KindCoercion
co)) = env -> Kind -> a
go_ty env
env Kind
ty a -> a -> a
forall a. Monoid a => a -> a -> a
`mappend` env -> KindCoercion -> a
go_co env
env KindCoercion
co
go_co env
env (TyConAppCo Role
_ TyCon
_ [KindCoercion]
args) = env -> [KindCoercion] -> a
go_cos env
env [KindCoercion]
args
go_co env
env (AppCo KindCoercion
c1 KindCoercion
c2) = env -> KindCoercion -> a
go_co env
env KindCoercion
c1 a -> a -> a
forall a. Monoid a => a -> a -> a
`mappend` env -> KindCoercion -> a
go_co env
env KindCoercion
c2
go_co env
env (CoVarCo TyVar
cv) = env -> TyVar -> a
covar env
env TyVar
cv
go_co env
env (AxiomInstCo CoAxiom Branched
_ Int
_ [KindCoercion]
args) = env -> [KindCoercion] -> a
go_cos env
env [KindCoercion]
args
go_co env
env (HoleCo CoercionHole
hole) = env -> CoercionHole -> a
cohole env
env CoercionHole
hole
go_co env
env (UnivCo UnivCoProvenance
p Role
_ Kind
t1 Kind
t2) = env -> UnivCoProvenance -> a
go_prov env
env UnivCoProvenance
p a -> a -> a
forall a. Monoid a => a -> a -> a
`mappend` env -> Kind -> a
go_ty env
env Kind
t1
a -> a -> a
forall a. Monoid a => a -> a -> a
`mappend` env -> Kind -> a
go_ty env
env Kind
t2
go_co env
env (SymCo KindCoercion
co) = env -> KindCoercion -> a
go_co env
env KindCoercion
co
go_co env
env (TransCo KindCoercion
c1 KindCoercion
c2) = env -> KindCoercion -> a
go_co env
env KindCoercion
c1 a -> a -> a
forall a. Monoid a => a -> a -> a
`mappend` env -> KindCoercion -> a
go_co env
env KindCoercion
c2
go_co env
env (AxiomRuleCo CoAxiomRule
_ [KindCoercion]
cos) = env -> [KindCoercion] -> a
go_cos env
env [KindCoercion]
cos
go_co env
env (SelCo CoSel
_ KindCoercion
co) = env -> KindCoercion -> a
go_co env
env KindCoercion
co
go_co env
env (LRCo LeftOrRight
_ KindCoercion
co) = env -> KindCoercion -> a
go_co env
env KindCoercion
co
go_co env
env (InstCo KindCoercion
co KindCoercion
arg) = env -> KindCoercion -> a
go_co env
env KindCoercion
co a -> a -> a
forall a. Monoid a => a -> a -> a
`mappend` env -> KindCoercion -> a
go_co env
env KindCoercion
arg
go_co env
env (KindCo KindCoercion
co) = env -> KindCoercion -> a
go_co env
env KindCoercion
co
go_co env
env (SubCo KindCoercion
co) = env -> KindCoercion -> a
go_co env
env KindCoercion
co
go_co env
env (FunCo { fco_mult :: KindCoercion -> KindCoercion
fco_mult = KindCoercion
cw, fco_arg :: KindCoercion -> KindCoercion
fco_arg = KindCoercion
c1, fco_res :: KindCoercion -> KindCoercion
fco_res = KindCoercion
c2 })
= env -> KindCoercion -> a
go_co env
env KindCoercion
cw a -> a -> a
forall a. Monoid a => a -> a -> a
`mappend` env -> KindCoercion -> a
go_co env
env KindCoercion
c1 a -> a -> a
forall a. Monoid a => a -> a -> a
`mappend` env -> KindCoercion -> a
go_co env
env KindCoercion
c2
go_co env
env (ForAllCo TyVar
tv KindCoercion
kind_co KindCoercion
co)
= env -> KindCoercion -> a
go_co env
env KindCoercion
kind_co a -> a -> a
forall a. Monoid a => a -> a -> a
`mappend` env -> Kind -> a
go_ty env
env (TyVar -> Kind
varType TyVar
tv)
a -> a -> a
forall a. Monoid a => a -> a -> a
`mappend` env -> KindCoercion -> a
go_co env
env' KindCoercion
co
where
env' :: env
env' = env -> TyVar -> ForAllTyFlag -> env
tycobinder env
env TyVar
tv ForAllTyFlag
Inferred
go_prov :: env -> UnivCoProvenance -> a
go_prov env
env (PhantomProv KindCoercion
co) = env -> KindCoercion -> a
go_co env
env KindCoercion
co
go_prov env
env (ProofIrrelProv KindCoercion
co) = env -> KindCoercion -> a
go_co env
env KindCoercion
co
go_prov env
_ (PluginProv String
_) = a
forall a. Monoid a => a
mempty
go_prov env
_ (CorePrepProv Bool
_) = a
forall a. Monoid a => a
mempty
noView :: Type -> Maybe Type
noView :: Kind -> Maybe Kind
noView Kind
_ = Maybe Kind
forall a. Maybe a
Nothing
typeSize :: Type -> Int
typeSize :: Kind -> Int
typeSize (LitTy {}) = Int
1
typeSize (TyVarTy {}) = Int
1
typeSize (AppTy Kind
t1 Kind
t2) = Kind -> Int
typeSize Kind
t1 Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Kind -> Int
typeSize Kind
t2
typeSize (FunTy FunTyFlag
_ Kind
_ Kind
t1 Kind
t2) = Kind -> Int
typeSize Kind
t1 Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Kind -> Int
typeSize Kind
t2
typeSize (ForAllTy (Bndr TyVar
tv ForAllTyFlag
_) Kind
t) = Kind -> Int
typeSize (TyVar -> Kind
varType TyVar
tv) Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Kind -> Int
typeSize Kind
t
typeSize (TyConApp TyCon
_ [Kind]
ts) = Int
1 Int -> Int -> Int
forall a. Num a => a -> a -> a
+ [Int] -> Int
forall a. Num a => [a] -> a
forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
sum ((Kind -> Int) -> [Kind] -> [Int]
forall a b. (a -> b) -> [a] -> [b]
map Kind -> Int
typeSize [Kind]
ts)
typeSize (CastTy Kind
ty KindCoercion
co) = Kind -> Int
typeSize Kind
ty Int -> Int -> Int
forall a. Num a => a -> a -> a
+ KindCoercion -> Int
coercionSize KindCoercion
co
typeSize (CoercionTy KindCoercion
co) = KindCoercion -> Int
coercionSize KindCoercion
co
coercionSize :: Coercion -> Int
coercionSize :: KindCoercion -> Int
coercionSize (Refl Kind
ty) = Kind -> Int
typeSize Kind
ty
coercionSize (GRefl Role
_ Kind
ty MCoercionN
MRefl) = Kind -> Int
typeSize Kind
ty
coercionSize (GRefl Role
_ Kind
ty (MCo KindCoercion
co)) = Int
1 Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Kind -> Int
typeSize Kind
ty Int -> Int -> Int
forall a. Num a => a -> a -> a
+ KindCoercion -> Int
coercionSize KindCoercion
co
coercionSize (TyConAppCo Role
_ TyCon
_ [KindCoercion]
args) = Int
1 Int -> Int -> Int
forall a. Num a => a -> a -> a
+ [Int] -> Int
forall a. Num a => [a] -> a
forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
sum ((KindCoercion -> Int) -> [KindCoercion] -> [Int]
forall a b. (a -> b) -> [a] -> [b]
map KindCoercion -> Int
coercionSize [KindCoercion]
args)
coercionSize (AppCo KindCoercion
co KindCoercion
arg) = KindCoercion -> Int
coercionSize KindCoercion
co Int -> Int -> Int
forall a. Num a => a -> a -> a
+ KindCoercion -> Int
coercionSize KindCoercion
arg
coercionSize (ForAllCo TyVar
_ KindCoercion
h KindCoercion
co) = Int
1 Int -> Int -> Int
forall a. Num a => a -> a -> a
+ KindCoercion -> Int
coercionSize KindCoercion
co Int -> Int -> Int
forall a. Num a => a -> a -> a
+ KindCoercion -> Int
coercionSize KindCoercion
h
coercionSize (FunCo Role
_ FunTyFlag
_ FunTyFlag
_ KindCoercion
w KindCoercion
c1 KindCoercion
c2) = Int
1 Int -> Int -> Int
forall a. Num a => a -> a -> a
+ KindCoercion -> Int
coercionSize KindCoercion
c1 Int -> Int -> Int
forall a. Num a => a -> a -> a
+ KindCoercion -> Int
coercionSize KindCoercion
c2
Int -> Int -> Int
forall a. Num a => a -> a -> a
+ KindCoercion -> Int
coercionSize KindCoercion
w
coercionSize (CoVarCo TyVar
_) = Int
1
coercionSize (HoleCo CoercionHole
_) = Int
1
coercionSize (AxiomInstCo CoAxiom Branched
_ Int
_ [KindCoercion]
args) = Int
1 Int -> Int -> Int
forall a. Num a => a -> a -> a
+ [Int] -> Int
forall a. Num a => [a] -> a
forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
sum ((KindCoercion -> Int) -> [KindCoercion] -> [Int]
forall a b. (a -> b) -> [a] -> [b]
map KindCoercion -> Int
coercionSize [KindCoercion]
args)
coercionSize (UnivCo UnivCoProvenance
p Role
_ Kind
t1 Kind
t2) = Int
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
+ Kind -> Int
typeSize Kind
t1 Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Kind -> Int
typeSize Kind
t2
coercionSize (SymCo KindCoercion
co) = Int
1 Int -> Int -> Int
forall a. Num a => a -> a -> a
+ KindCoercion -> Int
coercionSize KindCoercion
co
coercionSize (TransCo KindCoercion
co1 KindCoercion
co2) = Int
1 Int -> Int -> Int
forall a. Num a => a -> a -> a
+ KindCoercion -> Int
coercionSize KindCoercion
co1 Int -> Int -> Int
forall a. Num a => a -> a -> a
+ KindCoercion -> Int
coercionSize KindCoercion
co2
coercionSize (SelCo CoSel
_ KindCoercion
co) = Int
1 Int -> Int -> Int
forall a. Num a => a -> a -> a
+ KindCoercion -> Int
coercionSize KindCoercion
co
coercionSize (LRCo LeftOrRight
_ KindCoercion
co) = Int
1 Int -> Int -> Int
forall a. Num a => a -> a -> a
+ KindCoercion -> Int
coercionSize KindCoercion
co
coercionSize (InstCo KindCoercion
co KindCoercion
arg) = Int
1 Int -> Int -> Int
forall a. Num a => a -> a -> a
+ KindCoercion -> Int
coercionSize KindCoercion
co Int -> Int -> Int
forall a. Num a => a -> a -> a
+ KindCoercion -> Int
coercionSize KindCoercion
arg
coercionSize (KindCo KindCoercion
co) = Int
1 Int -> Int -> Int
forall a. Num a => a -> a -> a
+ KindCoercion -> Int
coercionSize KindCoercion
co
coercionSize (SubCo KindCoercion
co) = Int
1 Int -> Int -> Int
forall a. Num a => a -> a -> a
+ KindCoercion -> Int
coercionSize KindCoercion
co
coercionSize (AxiomRuleCo CoAxiomRule
_ [KindCoercion]
cs) = Int
1 Int -> Int -> Int
forall a. Num a => a -> a -> a
+ [Int] -> Int
forall a. Num a => [a] -> a
forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
sum ((KindCoercion -> Int) -> [KindCoercion] -> [Int]
forall a b. (a -> b) -> [a] -> [b]
map KindCoercion -> Int
coercionSize [KindCoercion]
cs)
provSize :: UnivCoProvenance -> Int
provSize :: UnivCoProvenance -> Int
provSize (PhantomProv KindCoercion
co) = Int
1 Int -> Int -> Int
forall a. Num a => a -> a -> a
+ KindCoercion -> Int
coercionSize KindCoercion
co
provSize (ProofIrrelProv KindCoercion
co) = Int
1 Int -> Int -> Int
forall a. Num a => a -> a -> a
+ KindCoercion -> Int
coercionSize KindCoercion
co
provSize (PluginProv String
_) = Int
1
provSize (CorePrepProv Bool
_) = Int
1
data Scaled a = Scaled !Mult a
deriving (Typeable (Scaled a)
Typeable (Scaled a) =>
(forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Scaled a -> c (Scaled a))
-> (forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (Scaled a))
-> (Scaled a -> Constr)
-> (Scaled a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c (Scaled a)))
-> (forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c (Scaled a)))
-> ((forall b. Data b => b -> b) -> Scaled a -> Scaled a)
-> (forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> Scaled a -> r)
-> (forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> Scaled a -> r)
-> (forall u. (forall d. Data d => d -> u) -> Scaled a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> Scaled a -> u)
-> (forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Scaled a -> m (Scaled a))
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Scaled a -> m (Scaled a))
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Scaled a -> m (Scaled a))
-> Data (Scaled a)
Scaled a -> Constr
Scaled a -> DataType
(forall b. Data b => b -> b) -> Scaled a -> Scaled a
forall a. Data a => Typeable (Scaled a)
forall a. Data a => Scaled a -> Constr
forall a. Data a => Scaled a -> DataType
forall a.
Data a =>
(forall b. Data b => b -> b) -> Scaled a -> Scaled a
forall a u.
Data a =>
Int -> (forall d. Data d => d -> u) -> Scaled a -> u
forall a u.
Data a =>
(forall d. Data d => d -> u) -> Scaled a -> [u]
forall a r r'.
Data a =>
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> Scaled a -> r
forall a r r'.
Data a =>
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> Scaled a -> r
forall a (m :: * -> *).
(Data a, Monad m) =>
(forall d. Data d => d -> m d) -> Scaled a -> m (Scaled a)
forall a (m :: * -> *).
(Data a, MonadPlus m) =>
(forall d. Data d => d -> m d) -> Scaled a -> m (Scaled a)
forall a (c :: * -> *).
Data a =>
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (Scaled a)
forall a (c :: * -> *).
Data a =>
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Scaled a -> c (Scaled a)
forall a (t :: * -> *) (c :: * -> *).
(Data a, Typeable t) =>
(forall d. Data d => c (t d)) -> Maybe (c (Scaled a))
forall a (t :: * -> * -> *) (c :: * -> *).
(Data a, Typeable t) =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (Scaled a))
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) -> Scaled a -> u
forall u. (forall d. Data d => d -> u) -> Scaled a -> [u]
forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> Scaled a -> r
forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> Scaled a -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Scaled a -> m (Scaled a)
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Scaled a -> m (Scaled a)
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (Scaled a)
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Scaled a -> c (Scaled a)
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c (Scaled a))
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (Scaled a))
$cgfoldl :: forall a (c :: * -> *).
Data a =>
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Scaled a -> c (Scaled a)
gfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Scaled a -> c (Scaled a)
$cgunfold :: forall a (c :: * -> *).
Data a =>
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (Scaled a)
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (Scaled a)
$ctoConstr :: forall a. Data a => Scaled a -> Constr
toConstr :: Scaled a -> Constr
$cdataTypeOf :: forall a. Data a => Scaled a -> DataType
dataTypeOf :: Scaled a -> DataType
$cdataCast1 :: forall a (t :: * -> *) (c :: * -> *).
(Data a, Typeable t) =>
(forall d. Data d => c (t d)) -> Maybe (c (Scaled a))
dataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c (Scaled a))
$cdataCast2 :: forall a (t :: * -> * -> *) (c :: * -> *).
(Data a, Typeable t) =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (Scaled a))
dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (Scaled a))
$cgmapT :: forall a.
Data a =>
(forall b. Data b => b -> b) -> Scaled a -> Scaled a
gmapT :: (forall b. Data b => b -> b) -> Scaled a -> Scaled a
$cgmapQl :: forall a r r'.
Data a =>
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> Scaled a -> r
gmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> Scaled a -> r
$cgmapQr :: forall a r r'.
Data a =>
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> Scaled a -> r
gmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> Scaled a -> r
$cgmapQ :: forall a u.
Data a =>
(forall d. Data d => d -> u) -> Scaled a -> [u]
gmapQ :: forall u. (forall d. Data d => d -> u) -> Scaled a -> [u]
$cgmapQi :: forall a u.
Data a =>
Int -> (forall d. Data d => d -> u) -> Scaled a -> u
gmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Scaled a -> u
$cgmapM :: forall a (m :: * -> *).
(Data a, Monad m) =>
(forall d. Data d => d -> m d) -> Scaled a -> m (Scaled a)
gmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Scaled a -> m (Scaled a)
$cgmapMp :: forall a (m :: * -> *).
(Data a, MonadPlus m) =>
(forall d. Data d => d -> m d) -> Scaled a -> m (Scaled a)
gmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Scaled a -> m (Scaled a)
$cgmapMo :: forall a (m :: * -> *).
(Data a, MonadPlus m) =>
(forall d. Data d => d -> m d) -> Scaled a -> m (Scaled a)
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Scaled a -> m (Scaled a)
Data.Data)
instance (Outputable a) => Outputable (Scaled a) where
ppr :: Scaled a -> SDoc
ppr (Scaled Kind
_cnt a
t) = a -> SDoc
forall a. Outputable a => a -> SDoc
ppr a
t
scaledMult :: Scaled a -> Mult
scaledMult :: forall a. Scaled a -> Kind
scaledMult (Scaled Kind
m a
_) = Kind
m
scaledThing :: Scaled a -> a
scaledThing :: forall a. Scaled a -> a
scaledThing (Scaled Kind
_ a
t) = a
t
mapScaledType :: (Type -> Type) -> Scaled Type -> Scaled Type
mapScaledType :: (Kind -> Kind) -> Scaled Kind -> Scaled Kind
mapScaledType Kind -> Kind
f (Scaled Kind
m Kind
t) = Kind -> Kind -> Scaled Kind
forall a. Kind -> a -> Scaled a
Scaled (Kind -> Kind
f Kind
m) (Kind -> Kind
f Kind
t)
type Mult = Type