{-# 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, isHeteroKindCoHole,
CoercionN, CoercionR, CoercionP, KindCoercion,
MCoercion(..), MCoercionR, MCoercionN,
mkNakedTyConTy, mkTyVarTy, mkTyVarTys,
mkTyCoVarTy, mkTyCoVarTys,
mkFunTy, mkNakedFunTy,
mkVisFunTy, mkScaledFunTys,
mkInvisFunTy, mkInvisFunTys,
tcMkVisFunTy, tcMkInvisFunTy, tcMkScaledFunTy, tcMkScaledFunTys,
mkForAllTy, mkForAllTys, mkInvisForAllTys,
mkPiTy, mkPiTys,
mkVisFunTyMany, mkVisFunTysMany,
nonDetCmpTyLit, cmpTyLit,
pickLR,
TyCoFolder(..), foldTyCo, noView,
typeSize, typesSize, coercionSize,
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.TyCo.FVs( tyCoVarsOfType )
import {-# SOURCE #-} GHC.Core.Type( chooseFunTyFlag, typeKind, typeTypeOrConstraint )
import GHC.Types.Var
import GHC.Types.Var.Set( elemVarSet )
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
{ Type -> FunTyFlag
ft_af :: FunTyFlag
, Type -> Type
ft_mult :: Mult
, Type -> Type
ft_arg :: Type
, Type -> Type
ft_res :: Type }
| LitTy TyLit
| CastTy
Type
KindCoercion
| CoercionTy
Coercion
deriving Typeable Type
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 -> Constr
Type -> DataType
(forall b. Data b => b -> b) -> Type -> 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)
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Type -> c Type
gfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Type -> c Type
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Type
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Type
$ctoConstr :: Type -> Constr
toConstr :: Type -> Constr
$cdataTypeOf :: Type -> DataType
dataTypeOf :: Type -> DataType
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Type)
dataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Type)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Type)
dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Type)
$cgmapT :: (forall b. Data b => b -> b) -> Type -> Type
gmapT :: (forall b. Data b => b -> b) -> Type -> Type
$cgmapQl :: forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Type -> r
gmapQl :: forall r r'.
(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
gmapQr :: forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Type -> r
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> Type -> [u]
gmapQ :: forall u. (forall d. Data d => d -> u) -> Type -> [u]
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Type -> u
gmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Type -> u
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Type -> m Type
gmapM :: forall (m :: * -> *).
Monad m =>
(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
gmapMp :: forall (m :: * -> *).
MonadPlus m =>
(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
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Type -> m Type
Data.Data
instance Outputable Type where
ppr :: Type -> SDoc
ppr = Type -> 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 -> Type
mkTyVarTy TyVar
v = Bool -> SDoc -> Type -> Type
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
<+> Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr (TyVar -> Type
tyVarKind TyVar
v)) (Type -> Type) -> Type -> Type
forall a b. (a -> b) -> a -> b
$
TyVar -> Type
TyVarTy TyVar
v
mkTyVarTys :: [TyVar] -> [Type]
mkTyVarTys :: [TyVar] -> [Type]
mkTyVarTys = (TyVar -> Type) -> [TyVar] -> [Type]
forall a b. (a -> b) -> [a] -> [b]
map TyVar -> Type
mkTyVarTy
mkTyCoVarTy :: TyCoVar -> Type
mkTyCoVarTy :: TyVar -> Type
mkTyCoVarTy TyVar
v
| TyVar -> Bool
isTyVar TyVar
v
= TyVar -> Type
TyVarTy TyVar
v
| Bool
otherwise
= KindCoercion -> Type
CoercionTy (TyVar -> KindCoercion
CoVarCo TyVar
v)
mkTyCoVarTys :: [TyCoVar] -> [Type]
mkTyCoVarTys :: [TyVar] -> [Type]
mkTyCoVarTys = (TyVar -> Type) -> [TyVar] -> [Type]
forall a b. (a -> b) -> [a] -> [b]
map TyVar -> Type
mkTyCoVarTy
infixr 3 `mkFunTy`, `mkInvisFunTy`, `mkVisFunTyMany`
mkNakedFunTy :: FunTyFlag -> Kind -> Kind -> Kind
mkNakedFunTy :: FunTyFlag -> Type -> Type -> Type
mkNakedFunTy FunTyFlag
af Type
arg Type
res
= FunTy { ft_af :: FunTyFlag
ft_af = FunTyFlag
af, ft_mult :: Type
ft_mult = Type
manyDataConTy
, ft_arg :: Type
ft_arg = Type
arg, ft_res :: Type
ft_res = Type
res }
mkFunTy :: HasDebugCallStack => FunTyFlag -> Mult -> Type -> Type -> Type
mkFunTy :: HasDebugCallStack => FunTyFlag -> Type -> Type -> Type -> Type
mkFunTy FunTyFlag
af Type
mult Type
arg Type
res
= Bool -> SDoc -> Type -> Type
forall a. HasCallStack => Bool -> SDoc -> a -> a
assertPpr (FunTyFlag
af FunTyFlag -> FunTyFlag -> Bool
forall a. Eq a => a -> a -> Bool
== HasDebugCallStack => Type -> Type -> FunTyFlag
Type -> Type -> FunTyFlag
chooseFunTyFlag Type
arg Type
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 (HasDebugCallStack => Type -> Type -> FunTyFlag
Type -> Type -> FunTyFlag
chooseFunTyFlag Type
arg Type
res)
, String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"arg" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
arg SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> SDoc
dcolon SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr (HasDebugCallStack => Type -> Type
Type -> Type
typeKind Type
arg)
, String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"res" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
res SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> SDoc
dcolon SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr (HasDebugCallStack => Type -> Type
Type -> Type
typeKind Type
res) ]) (Type -> Type) -> Type -> Type
forall a b. (a -> b) -> a -> b
$
FunTy { ft_af :: FunTyFlag
ft_af = FunTyFlag
af
, ft_mult :: Type
ft_mult = Type
mult
, ft_arg :: Type
ft_arg = Type
arg
, ft_res :: Type
ft_res = Type
res }
mkInvisFunTy :: HasDebugCallStack => Type -> Type -> Type
mkInvisFunTy :: HasDebugCallStack => Type -> Type -> Type
mkInvisFunTy Type
arg Type
res
= HasDebugCallStack => FunTyFlag -> Type -> Type -> Type -> Type
FunTyFlag -> Type -> Type -> Type -> Type
mkFunTy (TypeOrConstraint -> FunTyFlag
invisArg (HasDebugCallStack => Type -> TypeOrConstraint
Type -> TypeOrConstraint
typeTypeOrConstraint Type
res)) Type
manyDataConTy Type
arg Type
res
mkInvisFunTys :: HasDebugCallStack => [Type] -> Type -> Type
mkInvisFunTys :: HasDebugCallStack => [Type] -> Type -> Type
mkInvisFunTys [Type]
args Type
res
= (Type -> Type -> Type) -> Type -> [Type] -> Type
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (HasDebugCallStack => FunTyFlag -> Type -> Type -> Type -> Type
FunTyFlag -> Type -> Type -> Type -> Type
mkFunTy FunTyFlag
af Type
manyDataConTy) Type
res [Type]
args
where
af :: FunTyFlag
af = TypeOrConstraint -> FunTyFlag
invisArg (HasDebugCallStack => Type -> TypeOrConstraint
Type -> TypeOrConstraint
typeTypeOrConstraint Type
res)
mkVisFunTy :: HasDebugCallStack => Mult -> Type -> Type -> Type
mkVisFunTy :: HasDebugCallStack => Type -> Type -> Type -> Type
mkVisFunTy = HasDebugCallStack => FunTyFlag -> Type -> Type -> Type -> Type
FunTyFlag -> Type -> Type -> Type -> Type
mkFunTy FunTyFlag
visArgTypeLike
mkVisFunTyMany :: HasDebugCallStack => Type -> Type -> Type
mkVisFunTyMany :: HasDebugCallStack => Type -> Type -> Type
mkVisFunTyMany = HasDebugCallStack => Type -> Type -> Type -> Type
Type -> Type -> Type -> Type
mkVisFunTy Type
manyDataConTy
mkVisFunTysMany :: [Type] -> Type -> Type
mkVisFunTysMany :: [Type] -> Type -> Type
mkVisFunTysMany [Type]
tys Type
ty = (Type -> Type -> Type) -> Type -> [Type] -> Type
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr HasDebugCallStack => Type -> Type -> Type
Type -> Type -> Type
mkVisFunTyMany Type
ty [Type]
tys
mkScaledFunTy :: HasDebugCallStack => FunTyFlag -> Scaled Type -> Type -> Type
mkScaledFunTy :: HasDebugCallStack => FunTyFlag -> Scaled Type -> Type -> Type
mkScaledFunTy FunTyFlag
af (Scaled Type
mult Type
arg) Type
res = HasDebugCallStack => FunTyFlag -> Type -> Type -> Type -> Type
FunTyFlag -> Type -> Type -> Type -> Type
mkFunTy FunTyFlag
af Type
mult Type
arg Type
res
mkScaledFunTys :: HasDebugCallStack => [Scaled Type] -> Type -> Type
mkScaledFunTys :: HasDebugCallStack => [Scaled Type] -> Type -> Type
mkScaledFunTys [Scaled Type]
tys Type
ty = (Scaled Type -> Type -> Type) -> Type -> [Scaled Type] -> Type
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (HasDebugCallStack => FunTyFlag -> Scaled Type -> Type -> Type
FunTyFlag -> Scaled Type -> Type -> Type
mkScaledFunTy FunTyFlag
af) Type
ty [Scaled Type]
tys
where
af :: FunTyFlag
af = TypeOrConstraint -> FunTyFlag
visArg (HasDebugCallStack => Type -> TypeOrConstraint
Type -> TypeOrConstraint
typeTypeOrConstraint Type
ty)
mkForAllTy :: ForAllTyBinder -> Type -> Type
mkForAllTy :: ForAllTyBinder -> Type -> Type
mkForAllTy ForAllTyBinder
bndr Type
body
= Bool -> SDoc -> Type -> Type
forall a. HasCallStack => Bool -> SDoc -> a -> a
assertPpr (ForAllTyBinder -> Bool
good_bndr ForAllTyBinder
bndr) (ForAllTyBinder -> SDoc
forall a. Outputable a => a -> SDoc
ppr ForAllTyBinder
bndr SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
body) (Type -> Type) -> Type -> Type
forall a b. (a -> b) -> a -> b
$
ForAllTyBinder -> Type -> Type
ForAllTy ForAllTyBinder
bndr Type
body
where
good_bndr :: ForAllTyBinder -> Bool
good_bndr (Bndr TyVar
cv ForAllTyFlag
vis)
| TyVar -> Bool
isCoVar TyVar
cv = ForAllTyFlag
vis ForAllTyFlag -> ForAllTyFlag -> Bool
forall a. Eq a => a -> a -> Bool
== ForAllTyFlag
coreTyLamForAllTyFlag
Bool -> Bool -> Bool
&& (TyVar
cv TyVar -> VarSet -> Bool
`elemVarSet` Type -> VarSet
tyCoVarsOfType Type
body)
| Bool
otherwise = Bool
True
mkForAllTys :: [ForAllTyBinder] -> Type -> Type
mkForAllTys :: [ForAllTyBinder] -> Type -> Type
mkForAllTys [ForAllTyBinder]
tyvars Type
ty = (ForAllTyBinder -> Type -> Type)
-> Type -> [ForAllTyBinder] -> Type
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr ForAllTyBinder -> Type -> Type
ForAllTy Type
ty [ForAllTyBinder]
tyvars
mkInvisForAllTys :: [InvisTVBinder] -> Type -> Type
mkInvisForAllTys :: [InvisTVBinder] -> Type -> Type
mkInvisForAllTys [InvisTVBinder]
tyvars = [ForAllTyBinder] -> Type -> Type
mkForAllTys ([InvisTVBinder] -> [ForAllTyBinder]
forall a. [VarBndr a Specificity] -> [VarBndr a ForAllTyFlag]
tyVarSpecToBinders [InvisTVBinder]
tyvars)
mkPiTy :: HasDebugCallStack => PiTyBinder -> Type -> Type
mkPiTy :: HasDebugCallStack => PiTyBinder -> Type -> Type
mkPiTy (Anon Scaled Type
ty1 FunTyFlag
af) Type
ty2 = HasDebugCallStack => FunTyFlag -> Scaled Type -> Type -> Type
FunTyFlag -> Scaled Type -> Type -> Type
mkScaledFunTy FunTyFlag
af Scaled Type
ty1 Type
ty2
mkPiTy (Named ForAllTyBinder
bndr) Type
ty = ForAllTyBinder -> Type -> Type
mkForAllTy ForAllTyBinder
bndr Type
ty
mkPiTys :: HasDebugCallStack => [PiTyBinder] -> Type -> Type
mkPiTys :: HasDebugCallStack => [PiTyBinder] -> Type -> Type
mkPiTys [PiTyBinder]
tbs Type
ty = (PiTyBinder -> Type -> Type) -> Type -> [PiTyBinder] -> Type
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr HasDebugCallStack => PiTyBinder -> Type -> Type
PiTyBinder -> Type -> Type
mkPiTy Type
ty [PiTyBinder]
tbs
mkNakedTyConTy :: TyCon -> Type
mkNakedTyConTy :: TyCon -> Type
mkNakedTyConTy TyCon
tycon = TyCon -> [Type] -> Type
TyConApp TyCon
tycon []
tcMkVisFunTy :: Mult -> Type -> Type -> Type
tcMkVisFunTy :: Type -> Type -> Type -> Type
tcMkVisFunTy Type
mult Type
arg Type
res
= FunTy { ft_af :: FunTyFlag
ft_af = FunTyFlag
visArgTypeLike, ft_mult :: Type
ft_mult = Type
mult
, ft_arg :: Type
ft_arg = Type
arg, ft_res :: Type
ft_res = Type
res }
tcMkInvisFunTy :: TypeOrConstraint -> Type -> Type -> Type
tcMkInvisFunTy :: TypeOrConstraint -> Type -> Type -> Type
tcMkInvisFunTy TypeOrConstraint
res_torc Type
arg Type
res
= FunTy { ft_af :: FunTyFlag
ft_af = TypeOrConstraint -> FunTyFlag
invisArg TypeOrConstraint
res_torc, ft_mult :: Type
ft_mult = Type
manyDataConTy
, ft_arg :: Type
ft_arg = Type
arg, ft_res :: Type
ft_res = Type
res }
tcMkScaledFunTys :: [Scaled Type] -> Type -> Type
tcMkScaledFunTys :: [Scaled Type] -> Type -> Type
tcMkScaledFunTys [Scaled Type]
tys Type
ty = (Scaled Type -> Type -> Type) -> Type -> [Scaled Type] -> Type
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr Scaled Type -> Type -> Type
tcMkScaledFunTy Type
ty [Scaled Type]
tys
tcMkScaledFunTy :: Scaled Type -> Type -> Type
tcMkScaledFunTy :: Scaled Type -> Type -> Type
tcMkScaledFunTy (Scaled Type
mult Type
arg) Type
res = Type -> Type -> Type -> Type
tcMkVisFunTy Type
mult Type
arg Type
res
data Coercion
=
Refl Type
| GRefl Role Type MCoercionN
| TyConAppCo Role TyCon [Coercion]
| AppCo Coercion CoercionN
| ForAllCo
{ KindCoercion -> TyVar
fco_tcv :: TyCoVar
, KindCoercion -> ForAllTyFlag
fco_visL :: !ForAllTyFlag
, KindCoercion -> ForAllTyFlag
fco_visR :: !ForAllTyFlag
, KindCoercion -> KindCoercion
fco_kind :: KindCoercion
, KindCoercion -> KindCoercion
fco_body :: 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
| AxiomCo CoAxiomRule [Coercion]
| UnivCo
{ KindCoercion -> UnivCoProvenance
uco_prov :: UnivCoProvenance
, KindCoercion -> Role
uco_role :: Role
, KindCoercion -> Type
uco_lty, KindCoercion -> Type
uco_rty :: Type
, KindCoercion -> [KindCoercion]
uco_deps :: [Coercion]
}
| 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, Eq CoSel
Eq CoSel =>
(CoSel -> CoSel -> Ordering)
-> (CoSel -> CoSel -> Bool)
-> (CoSel -> CoSel -> Bool)
-> (CoSel -> CoSel -> Bool)
-> (CoSel -> CoSel -> Bool)
-> (CoSel -> CoSel -> CoSel)
-> (CoSel -> CoSel -> CoSel)
-> Ord CoSel
CoSel -> CoSel -> Bool
CoSel -> CoSel -> Ordering
CoSel -> CoSel -> CoSel
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
$ccompare :: CoSel -> CoSel -> Ordering
compare :: CoSel -> CoSel -> Ordering
$c< :: CoSel -> CoSel -> Bool
< :: CoSel -> CoSel -> Bool
$c<= :: CoSel -> CoSel -> Bool
<= :: CoSel -> CoSel -> Bool
$c> :: CoSel -> CoSel -> Bool
> :: CoSel -> CoSel -> Bool
$c>= :: CoSel -> CoSel -> Bool
>= :: CoSel -> CoSel -> Bool
$cmax :: CoSel -> CoSel -> CoSel
max :: CoSel -> CoSel -> CoSel
$cmin :: CoSel -> CoSel -> CoSel
min :: CoSel -> CoSel -> CoSel
Ord )
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, Eq FunSel
Eq FunSel =>
(FunSel -> FunSel -> Ordering)
-> (FunSel -> FunSel -> Bool)
-> (FunSel -> FunSel -> Bool)
-> (FunSel -> FunSel -> Bool)
-> (FunSel -> FunSel -> Bool)
-> (FunSel -> FunSel -> FunSel)
-> (FunSel -> FunSel -> FunSel)
-> Ord FunSel
FunSel -> FunSel -> Bool
FunSel -> FunSel -> Ordering
FunSel -> FunSel -> FunSel
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
$ccompare :: FunSel -> FunSel -> Ordering
compare :: FunSel -> FunSel -> Ordering
$c< :: FunSel -> FunSel -> Bool
< :: FunSel -> FunSel -> Bool
$c<= :: FunSel -> FunSel -> Bool
<= :: FunSel -> FunSel -> Bool
$c> :: FunSel -> FunSel -> Bool
> :: FunSel -> FunSel -> Bool
$c>= :: FunSel -> FunSel -> Bool
>= :: FunSel -> FunSel -> Bool
$cmax :: FunSel -> FunSel -> FunSel
max :: FunSel -> FunSel -> FunSel
$cmin :: FunSel -> FunSel -> FunSel
min :: FunSel -> FunSel -> FunSel
Ord )
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 SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<> SDoc
forall doc. IsLine doc => doc
comma SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<> Role -> SDoc
pprOneCharRole Role
r)
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)
pprOneCharRole :: Role -> SDoc
pprOneCharRole :: Role -> SDoc
pprOneCharRole Role
Nominal = Char -> SDoc
forall doc. IsLine doc => Char -> doc
char Char
'N'
pprOneCharRole Role
Representational = Char -> SDoc
forall doc. IsLine doc => Char -> doc
char Char
'R'
pprOneCharRole Role
Phantom = Char -> SDoc
forall doc. IsLine doc => Char -> doc
char Char
'P'
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_ :: WriteBinHandle -> CoSel -> IO ()
put_ WriteBinHandle
bh (SelTyCon Int
n Role
r) = do { WriteBinHandle -> Word8 -> IO ()
putByte WriteBinHandle
bh Word8
0; WriteBinHandle -> Int -> IO ()
forall a. Binary a => WriteBinHandle -> a -> IO ()
put_ WriteBinHandle
bh Int
n; WriteBinHandle -> Role -> IO ()
forall a. Binary a => WriteBinHandle -> a -> IO ()
put_ WriteBinHandle
bh Role
r }
put_ WriteBinHandle
bh CoSel
SelForAll = WriteBinHandle -> Word8 -> IO ()
putByte WriteBinHandle
bh Word8
1
put_ WriteBinHandle
bh (SelFun FunSel
SelMult) = WriteBinHandle -> Word8 -> IO ()
putByte WriteBinHandle
bh Word8
2
put_ WriteBinHandle
bh (SelFun FunSel
SelArg) = WriteBinHandle -> Word8 -> IO ()
putByte WriteBinHandle
bh Word8
3
put_ WriteBinHandle
bh (SelFun FunSel
SelRes) = WriteBinHandle -> Word8 -> IO ()
putByte WriteBinHandle
bh Word8
4
get :: ReadBinHandle -> IO CoSel
get ReadBinHandle
bh = do { h <- ReadBinHandle -> IO Word8
getByte ReadBinHandle
bh
; case h of
Word8
0 -> do { n <- ReadBinHandle -> IO Int
forall a. Binary a => ReadBinHandle -> IO a
get ReadBinHandle
bh; r <- get bh; return (SelTyCon n 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
| ProofIrrelProv
| PluginProv String
deriving (UnivCoProvenance -> UnivCoProvenance -> Bool
(UnivCoProvenance -> UnivCoProvenance -> Bool)
-> (UnivCoProvenance -> UnivCoProvenance -> Bool)
-> Eq UnivCoProvenance
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: UnivCoProvenance -> UnivCoProvenance -> Bool
== :: UnivCoProvenance -> UnivCoProvenance -> Bool
$c/= :: UnivCoProvenance -> UnivCoProvenance -> Bool
/= :: UnivCoProvenance -> UnivCoProvenance -> Bool
Eq, Eq UnivCoProvenance
Eq UnivCoProvenance =>
(UnivCoProvenance -> UnivCoProvenance -> Ordering)
-> (UnivCoProvenance -> UnivCoProvenance -> Bool)
-> (UnivCoProvenance -> UnivCoProvenance -> Bool)
-> (UnivCoProvenance -> UnivCoProvenance -> Bool)
-> (UnivCoProvenance -> UnivCoProvenance -> Bool)
-> (UnivCoProvenance -> UnivCoProvenance -> UnivCoProvenance)
-> (UnivCoProvenance -> UnivCoProvenance -> UnivCoProvenance)
-> Ord UnivCoProvenance
UnivCoProvenance -> UnivCoProvenance -> Bool
UnivCoProvenance -> UnivCoProvenance -> Ordering
UnivCoProvenance -> UnivCoProvenance -> UnivCoProvenance
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
$ccompare :: UnivCoProvenance -> UnivCoProvenance -> Ordering
compare :: UnivCoProvenance -> UnivCoProvenance -> Ordering
$c< :: UnivCoProvenance -> UnivCoProvenance -> Bool
< :: UnivCoProvenance -> UnivCoProvenance -> Bool
$c<= :: UnivCoProvenance -> UnivCoProvenance -> Bool
<= :: UnivCoProvenance -> UnivCoProvenance -> Bool
$c> :: UnivCoProvenance -> UnivCoProvenance -> Bool
> :: UnivCoProvenance -> UnivCoProvenance -> Bool
$c>= :: UnivCoProvenance -> UnivCoProvenance -> Bool
>= :: UnivCoProvenance -> UnivCoProvenance -> Bool
$cmax :: UnivCoProvenance -> UnivCoProvenance -> UnivCoProvenance
max :: UnivCoProvenance -> UnivCoProvenance -> UnivCoProvenance
$cmin :: UnivCoProvenance -> UnivCoProvenance -> UnivCoProvenance
min :: UnivCoProvenance -> UnivCoProvenance -> UnivCoProvenance
Ord, 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 UnivCoProvenance
PhantomProv = String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"(phantom)"
ppr UnivCoProvenance
ProofIrrelProv = 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))
instance NFData UnivCoProvenance where
rnf :: UnivCoProvenance -> ()
rnf UnivCoProvenance
p = UnivCoProvenance
p UnivCoProvenance -> () -> ()
forall a b. a -> b -> b
`seq` ()
instance Binary UnivCoProvenance where
put_ :: WriteBinHandle -> UnivCoProvenance -> IO ()
put_ WriteBinHandle
bh UnivCoProvenance
PhantomProv = WriteBinHandle -> Word8 -> IO ()
putByte WriteBinHandle
bh Word8
1
put_ WriteBinHandle
bh UnivCoProvenance
ProofIrrelProv = WriteBinHandle -> Word8 -> IO ()
putByte WriteBinHandle
bh Word8
2
put_ WriteBinHandle
bh (PluginProv String
a) = WriteBinHandle -> Word8 -> IO ()
putByte WriteBinHandle
bh Word8
3 IO () -> IO () -> IO ()
forall a b. IO a -> IO b -> IO b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> WriteBinHandle -> String -> IO ()
forall a. Binary a => WriteBinHandle -> a -> IO ()
put_ WriteBinHandle
bh String
a
get :: ReadBinHandle -> IO UnivCoProvenance
get ReadBinHandle
bh = do
tag <- ReadBinHandle -> IO Word8
getByte ReadBinHandle
bh
case tag of
Word8
1 -> UnivCoProvenance -> IO UnivCoProvenance
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return UnivCoProvenance
PhantomProv
Word8
2 -> UnivCoProvenance -> IO UnivCoProvenance
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return UnivCoProvenance
ProofIrrelProv
Word8
3 -> do a <- ReadBinHandle -> IO String
forall a. Binary a => ReadBinHandle -> IO a
get ReadBinHandle
bh
return $ PluginProv a
Word8
_ -> String -> IO UnivCoProvenance
forall a. HasCallStack => String -> a
panic (String
"get UnivCoProvenance " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Word8 -> String
forall a. Show a => a -> String
show Word8
tag)
data CoercionHole
= CoercionHole { CoercionHole -> TyVar
ch_co_var :: CoVar
, CoercionHole -> IORef (Maybe KindCoercion)
ch_ref :: IORef (Maybe Coercion)
, CoercionHole -> Bool
ch_hetero_kind :: Bool
}
coHoleCoVar :: CoercionHole -> CoVar
coHoleCoVar :: CoercionHole -> TyVar
coHoleCoVar = CoercionHole -> TyVar
ch_co_var
isHeteroKindCoHole :: CoercionHole -> Bool
isHeteroKindCoHole :: CoercionHole -> Bool
isHeteroKindCoHole = CoercionHole -> Bool
ch_hetero_kind
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, ch_hetero_kind :: CoercionHole -> Bool
ch_hetero_kind = Bool
hk })
= SDoc -> SDoc
forall doc. IsLine doc => doc -> doc
braces (TyVar -> SDoc
forall a. Outputable a => a -> SDoc
ppr TyVar
cv SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<> Bool -> SDoc -> SDoc
forall doc. IsOutput doc => Bool -> doc -> doc
ppWhen Bool
hk (String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"[hk]"))
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 -> Type -> Maybe Type
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
-> (Type -> a, [Type] -> a, KindCoercion -> a, [KindCoercion] -> a)
foldTyCo (TyCoFolder { tcf_view :: forall env a. TyCoFolder env a -> Type -> Maybe Type
tcf_view = Type -> Maybe Type
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 -> Type -> a
go_ty env
env, env -> [Type] -> a
go_tys env
env, env -> KindCoercion -> a
go_co env
env, env -> [KindCoercion] -> a
go_cos env
env)
where
go_ty :: env -> Type -> a
go_ty env
env Type
ty | Just Type
ty' <- Type -> Maybe Type
view Type
ty = env -> Type -> a
go_ty env
env Type
ty'
go_ty env
env (TyVarTy TyVar
tv) = env -> TyVar -> a
tyvar env
env TyVar
tv
go_ty env
env (AppTy Type
t1 Type
t2) = env -> Type -> a
go_ty env
env Type
t1 a -> a -> a
forall a. Monoid a => a -> a -> a
`mappend` env -> Type -> a
go_ty env
env Type
t2
go_ty env
_ (LitTy {}) = a
forall a. Monoid a => a
mempty
go_ty env
env (CastTy Type
ty KindCoercion
co) = env -> Type -> a
go_ty env
env Type
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
_ Type
w Type
arg Type
res) = env -> Type -> a
go_ty env
env Type
w a -> a -> a
forall a. Monoid a => a -> a -> a
`mappend` env -> Type -> a
go_ty env
env Type
arg a -> a -> a
forall a. Monoid a => a -> a -> a
`mappend` env -> Type -> a
go_ty env
env Type
res
go_ty env
env (TyConApp TyCon
_ [Type]
tys) = env -> [Type] -> a
go_tys env
env [Type]
tys
go_ty env
env (ForAllTy (Bndr TyVar
tv ForAllTyFlag
vis) Type
inner)
= let !env' :: env
env' = env -> TyVar -> ForAllTyFlag -> env
tycobinder env
env TyVar
tv ForAllTyFlag
vis
in env -> Type -> a
go_ty env
env (TyVar -> Type
varType TyVar
tv) a -> a -> a
forall a. Monoid a => a -> a -> a
`mappend` env -> Type -> a
go_ty env
env' Type
inner
go_tys :: env -> [Type] -> a
go_tys env
_ [] = a
forall a. Monoid a => a
mempty
go_tys env
env (Type
t:[Type]
ts) = env -> Type -> a
go_ty env
env Type
t a -> a -> a
forall a. Monoid a => a -> a -> a
`mappend` env -> [Type] -> a
go_tys env
env [Type]
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 Type
ty) = env -> Type -> a
go_ty env
env Type
ty
go_co env
env (GRefl Role
_ Type
ty MCoercionN
MRefl) = env -> Type -> a
go_ty env
env Type
ty
go_co env
env (GRefl Role
_ Type
ty (MCo KindCoercion
co)) = env -> Type -> a
go_ty env
env Type
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 (AxiomCo CoAxiomRule
_ [KindCoercion]
cos) = env -> [KindCoercion] -> a
go_cos env
env [KindCoercion]
cos
go_co env
env (HoleCo CoercionHole
hole) = env -> CoercionHole -> a
cohole env
env CoercionHole
hole
go_co env
env (UnivCo { uco_lty :: KindCoercion -> Type
uco_lty = Type
t1, uco_rty :: KindCoercion -> Type
uco_rty = Type
t2, uco_deps :: KindCoercion -> [KindCoercion]
uco_deps = [KindCoercion]
deps })
= env -> Type -> a
go_ty env
env Type
t1 a -> a -> a
forall a. Monoid a => a -> a -> a
`mappend` env -> Type -> a
go_ty env
env Type
t2
a -> a -> a
forall a. Monoid a => a -> a -> a
`mappend` env -> [KindCoercion] -> a
go_cos env
env [KindCoercion]
deps
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 (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 ForAllTyFlag
_vis1 ForAllTyFlag
_vis2 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 -> Type -> a
go_ty env
env (TyVar -> Type
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
noView :: Type -> Maybe Type
noView :: Type -> Maybe Type
noView Type
_ = Maybe Type
forall a. Maybe a
Nothing
typeSize :: Type -> Int
typeSize :: Type -> Int
typeSize (LitTy {}) = Int
1
typeSize (TyVarTy {}) = Int
1
typeSize (AppTy Type
t1 Type
t2) = Type -> Int
typeSize Type
t1 Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Type -> Int
typeSize Type
t2
typeSize (FunTy FunTyFlag
_ Type
_ Type
t1 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 TyVar
tv ForAllTyFlag
_) Type
t) = Type -> Int
typeSize (TyVar -> Type
varType TyVar
tv) Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Type -> Int
typeSize Type
t
typeSize (TyConApp TyCon
_ [Type]
ts) = Int
1 Int -> Int -> Int
forall a. Num a => a -> a -> a
+ [Type] -> Int
typesSize [Type]
ts
typeSize (CastTy Type
ty KindCoercion
co) = Type -> Int
typeSize Type
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
typesSize :: [Type] -> Int
typesSize :: [Type] -> Int
typesSize [Type]
tys = (Type -> Int -> Int) -> Int -> [Type] -> Int
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (Int -> Int -> Int
forall a. Num a => a -> a -> a
(+) (Int -> Int -> Int) -> (Type -> Int) -> Type -> Int -> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Type -> Int
typeSize) Int
0 [Type]
tys
coercionSize :: Coercion -> Int
coercionSize :: KindCoercion -> Int
coercionSize (Refl Type
ty) = Type -> Int
typeSize Type
ty
coercionSize (GRefl Role
_ Type
ty MCoercionN
MRefl) = Type -> Int
typeSize Type
ty
coercionSize (GRefl Role
_ Type
ty (MCo KindCoercion
co)) = Int
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
+ 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 { fco_kind :: KindCoercion -> KindCoercion
fco_kind = KindCoercion
h, fco_body :: KindCoercion -> KindCoercion
fco_body = 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 (AxiomCo 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)
coercionSize (UnivCo { uco_lty :: KindCoercion -> Type
uco_lty = Type
t1, uco_rty :: KindCoercion -> Type
uco_rty = Type
t2 }) = Int
1 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 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
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 Type
_cnt a
t) = a -> SDoc
forall a. Outputable a => a -> SDoc
ppr a
t
scaledMult :: Scaled a -> Mult
scaledMult :: forall a. Scaled a -> Type
scaledMult (Scaled Type
m a
_) = Type
m
scaledThing :: Scaled a -> a
scaledThing :: forall a. Scaled a -> a
scaledThing (Scaled Type
_ a
t) = a
t
mapScaledType :: (Type -> Type) -> Scaled Type -> Scaled Type
mapScaledType :: (Type -> Type) -> Scaled Type -> Scaled Type
mapScaledType Type -> Type
f (Scaled Type
m Type
t) = Type -> Type -> Scaled Type
forall a. Type -> a -> Scaled a
Scaled (Type -> Type
f Type
m) (Type -> Type
f Type
t)
type Mult = Type