{-# LANGUAGE ConstraintKinds #-}
+{-# LANGUAGE EmptyCase #-}
{-# LANGUAGE InstanceSigs #-}
{-# LANGUAGE QuantifiedConstraints #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE UndecidableInstances #-}
+{-# OPTIONS_GHC -Wno-partial-fields #-}
module Symantic.Compiler.Term where
import Data.Function ((.))
import Data.Function qualified as Fun
import Data.Functor (Functor (..))
-import Data.Int (Int)
import GHC.Types (Constraint, Type)
import Symantic.Syntaxes.Classes (Unabstractable (..))
+import Text.Show (Show (..))
import Unsafe.Coerce (unsafeCoerce)
import Symantic.Typer.Type (Ty)
type Semantic = Type -> Type
type Syntax = Semantic -> Constraint
+-- * Type 'PerSyntax'
+data PerSyntax :: [Syntax] -> (Syntax -> Type) -> Type where
+ PerSyntaxZ :: a syn -> PerSyntax (syn ': syns) a
+ PerSyntaxS :: PerSyntax syns a -> PerSyntax (not_s ': syns) a
+
+instance Show (PerSyntax '[] a) where
+ showsPrec _p = \case {}
+instance
+ ( Show (a syn)
+ , Show (PerSyntax syns a)
+ ) =>
+ Show (PerSyntax (syn ': syns) a)
+ where
+ showsPrec p = \case
+ PerSyntaxZ a -> showsPrec p a
+ PerSyntaxS s -> showsPrec p s
+
+-- ** Class 'PerSyntaxable'
+class PerSyntaxable (syns :: [Syntax]) (syn :: Syntax) where
+ perSyntax :: a syn -> PerSyntax syns a
+instance {-# OVERLAPS #-} PerSyntaxable (syn ': syns) syn where
+ perSyntax = PerSyntaxZ
+instance PerSyntaxable syns syn => PerSyntaxable (not_syn ': syns) syn where
+ perSyntax = PerSyntaxS . perSyntax
+
-- | Merge syntax 'Constraint's into a single 'Constraint'.
type family Syntaxes (syns :: [(Type -> Type) -> Constraint]) (sem :: Type -> Type) :: Constraint where
Syntaxes '[] sem = (() :: Constraint)
{-# LANGUAGE RankNTypes #-}
+{-# OPTIONS_GHC -Wno-partial-fields #-}
module Symantic.Parser where
( -- MT.State (TokenTerm meta a)
forall vs.
CtxTy meta vs Void ->
- Either ErrMsg (TermVT syns meta vs)
+ Either (PerSyntax syns (ErrorParser meta)) (TermVT syns meta vs)
)
}
type ErrMsg = String
+-- * Data family 'ErrorParser'
+data family ErrorParser meta (syn :: Syntax)
+
+---- * Type 'SomeParsingError'
+-- data SomeParsingError
+-- = forall syn.
+-- (
+-- -- Derivable (SomeParsingError syn sem),
+-- Typeable syn
+-- ) =>
+-- SomeParsingError (SomeParsingError syn)
+--
+----type instance Derived (SomeParsingError sem) = sem
+----instance Derivable (SomeParsingError sem) where
+---- derive (SomeParsingError x) = derive x
+--
+---- ** Type 'SomeParsingError'
+--
+---- TODO: neither data families nor data instances
+---- can have phantom roles with GHC-9's RoleAnnotations,
+---- hence 'SomeParsingError.Coerce.coerce' cannot be used on them for now.
+---- https://gitlab.haskell.org/ghc/ghc/-/issues/8177
+---- https://gitlab.haskell.org/ghc/ghc/-/wikis/roles#proposal-roles-for-type-families
+-- data family SomeParsingError (syn :: Syntax) :: Semantic -> Semantic
+----type instance Derived (SomeParsingError syn sem) = sem
+--
+---- | Convenient utility to pattern-match a 'SomeParsingError'.
+----pattern SomeParsingError :: Typeable syn => SomeParsingError syn sem a -> SomeParsingError sem a
+----pattern SomeParsingError x <- (unSomeParsingError -> Maybe.Just x)
+--
+---- | @(unSomeParsingError sd :: 'Maybe' ('SomeParsingError' syn sem a))@
+---- extract the data-constructor from the given 'SomeParsingError' @(sd)@
+---- iif. it belongs to the @('SomeParsingError' syn sem a)@ data-instance.
+-- unSomeParsingError ::
+-- forall syn sem a.
+-- Typeable syn =>
+-- SomeParsingError sem a ->
+-- Maybe (SomeParsingError syn sem a)
+-- unSomeParsingError (SomeParsingError (constr :: SomeParsingError actualSyn sem a)) =
+-- case typeRep @syn `eqTypeRep` typeRep @actualSyn of
+-- Maybe.Just HRefl -> Maybe.Just constr
+-- Maybe.Nothing -> Maybe.Nothing
+
data TermVT syns meta vs = forall a vs'.
TermVT
{ termVTType :: Ty meta vs' a
module Symantic.Printer where
-import Control.Applicative (Applicative (..))
-import Control.Monad (Monad (..))
-import Control.Monad.Trans.Except qualified as MT
-import Control.Monad.Trans.Reader qualified as MT
-import Control.Monad.Trans.State qualified as MT
-import Data.Bool (otherwise)
-import Data.Either (Either (..))
-import Data.Eq (Eq (..))
-import Data.Function (id, ($), (.))
-import Data.Functor (Functor (..), (<$>))
-import Data.Functor.Constant (Constant (..))
-import Data.Int (Int)
-import Data.Kind (Constraint, Type)
-import Data.Maybe (Maybe (..), isJust)
-import Data.Proxy (Proxy (..))
-import Data.Semigroup (Semigroup (..))
+import Data.Function (($))
import Data.String (String)
-import GHC.Types
-import Text.Read (Read (..), reads)
-import Text.Show (Show (..))
-import Unsafe.Coerce (unsafeCoerce)
-import Prelude (error)
-import Prelude qualified
-import Symantic.Compiler
import Symantic.Parser
-- TODO: var num
{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE EmptyDataDeriving #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE QuantifiedConstraints #-}
{-# LANGUAGE RankNTypes #-}
import Control.Arrow (left)
import Data.Either (Either (..))
import Data.Eq (Eq (..))
-import Data.Function (fix, ($))
+import Data.Function (fix, ($), (.))
import Data.Int (Int)
+import Data.Kind (Type)
import Data.Maybe (Maybe (..))
import Data.Monoid (Monoid (..))
-import Data.Semigroup (Semigroup (..))
import Data.Void (Void)
import Symantic.Syntaxes.Classes (Unabstractable (..))
import Text.Show (Show (..))
-import Type.Reflection (eqTypeRep, typeRep, (:~~:) (..))
+import Type.Reflection (Typeable, eqTypeRep, typeRep, (:~~:) (..))
import Prelude (error)
import Symantic
Syntaxes finalSyns (ForallSemantic finalSyns) =>
Parsers finalSyns finalSyns meta =>
TermAST meta ->
- Either ErrMsg (TermVT finalSyns meta '[])
-parse ast = unParser (fix parsersA ast) CtxTyZ
+ Either (PerSyntax finalSyns (ErrorParser meta)) (TermVT finalSyns meta '[])
+parse ast = unParser (fix openParser ast) CtxTyZ
where
-- Unabstractable and Constable are always required.
- parsersA final (BinTree2 fT aT) = Parser $ \ctx -> do
+ openParser final (BinTree2 fT aT) = Parser $ \ctx -> do
let Parser fE = final fT
- TermVT fTy (f :: OpenTerm finalSyns fVS a2b) <- fE ctx
let Parser aE = final aT
+ TermVT fTy (f :: OpenTerm finalSyns fVS a2b) <- fE ctx
TermVT aTy (a :: OpenTerm finalSyns aVS a) <- aE ctx
- let (fTy', aTy') = appendVars fTy aTy
- case fTy' of
+ case fTy of
-- FUN faTy bTy -> do
TyApp
{ tyAppFun =
}
, tyAppArg = bTy
} -> do
- mgu <- show `left` unifyType mempty faTy aTy'
- let faTy' = subst @Ty mgu faTy
+ let (faTy', aTy') = appendVars faTy aTy
+ mgu <- (perSyntax . ErrorParserUnabstractableUnify) `left` unifyType mempty faTy' aTy'
+ let faTy'' = subst @Ty mgu faTy'
let aTy'' = subst @Ty mgu aTy'
- case eqTy faTy' aTy'' of
- Nothing ->
- Left $
- "TypeError: Unabstractable: eqTy: "
- <> "\n faTy'="
- <> show faTy
- <> "\n aTy'="
- <> show aTy''
+ case eqTy faTy'' aTy'' of
+ Nothing -> Left $ perSyntax $ ErrorParserUnabstractableArgumentMismatch (TyVT faTy'') (TyVT aTy'')
Just HRefl -> Right $ TermVT bTy $ f .@ a
- _ -> Left "TypeError: Unabstractable: fTy is not a function"
- parsersA final (BinTree0 e) = parsers @finalSyns @finalSyns @meta final e
+ _ -> Left $ perSyntax $ ErrorParserUnabstractableNotAFunction (TyVT fTy)
+ openParser final (BinTree0 e) = parsers @finalSyns @finalSyns @meta final e
+data instance ErrorParser meta Unabstractable
+ = ErrorParserUnabstractableArgumentMismatch (TyVT meta) (TyVT meta)
+ | ErrorParserUnabstractableNotAFunction (TyVT meta)
+ | ErrorParserUnabstractableUnify (ErrorUnify meta)
+ deriving (Show)
+
+data instance ErrorParser meta Constable
+ = ErrorParserConstableInvalid (TokenTerm meta)
+ deriving (Show)
-- * Class 'Parsers'
class Parsers syns finalSyns meta where
parsers :: OpenParser finalSyns meta
-instance Parsers '[] finalSyns meta where
- parsers _final ast = Parser $ \_ctx -> Left $ "Invalid tree: " <> show ast
+instance PerSyntaxable finalSyns Constable => Parsers '[] finalSyns meta where
+ parsers _final tok = Parser $ \_ctx ->
+ Left $ perSyntax $ ErrorParserConstableInvalid tok
instance
( TokenParser syn finalSyns meta
, Parsers syns finalSyns meta
Parser syns meta
-- ** Class 'TokenParser'
-class TokenParser syn finalSyn meta where
+class TokenParser syn finalSyns meta where
tokenParser ::
- {-next-} (TokenTerm meta -> Parser finalSyn meta) ->
- OpenParser finalSyn meta
+ {-next-} (TokenTerm meta -> Parser finalSyns meta) ->
+ OpenParser finalSyns meta
instance
- ( Syntaxes finalSyn (ForallSemantic finalSyn)
+ ( Syntaxes finalSyns (ForallSemantic finalSyns)
) =>
- TokenParser Unabstractable finalSyn meta
+ TokenParser Unabstractable finalSyns meta
where
tokenParser next _final = next
+data instance ErrorParser meta (Abstractable meta)
+ = ErrorParserAbstractableUnknown Name
+ | ErrorParserAbstractableNotAType (TyVT meta)
+ deriving (Show)
instance
- ( Syntaxes finalSyn (ForallSemantic finalSyn)
- , forall sem. Syntaxes finalSyn sem => Constable sem
- , forall sem. Syntaxes finalSyn sem => Unabstractable sem
+ ( Syntaxes finalSyns (ForallSemantic finalSyns)
+ , forall sem. Syntaxes finalSyns sem => Constable sem
+ , forall sem. Syntaxes finalSyns sem => Unabstractable sem
+ , PerSyntaxable finalSyns (Abstractable meta)
) =>
- TokenParser (Abstractable meta) finalSyn meta
+ TokenParser (Abstractable meta) finalSyns meta
where
tokenParser _next _final (TokenTermVar vN) = Parser go
where
- go :: forall vs. CtxTy meta vs Void -> Either ErrMsg (TermVT finalSyn meta vs)
- go CtxTyZ = Left $ "Error_Term_unknown: " <> vN
+ go :: forall vs. CtxTy meta vs Void -> Either (PerSyntax finalSyns (ErrorParser meta)) (TermVT finalSyns meta vs)
+ go CtxTyZ = Left $ perSyntax $ ErrorParserAbstractableUnknown vN
go (CtxTyS n ty _) | n == vN = Right $ TermVT ty $ V
go (CtxTyS _n _typ tys) = do
TermVT ty ot <- go tys
Right $ TermVT ty $ W ot
tokenParser _next final (TokenTermAbst argName (TyT (aTy :: Ty meta '[] a)) bT) =
Parser $ \ctx ->
- case eqTy (typeTy @meta) (kindOf aTy) of
- Nothing -> Left "TypeError: Abstractable: TokenTermAbst"
+ case eqTy (monoTy @Type @meta) (kindOf aTy) of
+ Nothing -> Left $ perSyntax $ ErrorParserAbstractableNotAType (TyVT aTy)
Just HRefl -> do
let Parser bE = final bT
TermVT bTy (b :: OpenTerm syn bVS b) <- bE (CtxTyS argName aTy ctx)
N e -> e
tokenParser next _final e = next e
instance
- ( Syntaxes finalSyn (ForallSemantic finalSyn)
- , forall sem. Syntaxes finalSyn sem => Addable sem
+ ( Syntaxes finalSyns (ForallSemantic finalSyns)
+ , forall sem. Syntaxes finalSyns sem => Addable sem
) =>
- TokenParser Addable finalSyn meta
+ TokenParser Addable finalSyns meta
where
tokenParser next _final = \case
TokenTermAtom s
| Right (i :: Int) <- safeRead s ->
- Parser $ \ctx -> Right $ TermVT (inferTy @_ @Int (mempty :: meta) (lenVar ctx)) $ E $ ForallSemantic @_ @Int $ lit i
+ Parser $ \ctx ->
+ Right
+ $ TermVT
+ (tyOfTypeRep mempty (lenVar ctx) (typeRep @Int))
+ $ E
+ $ ForallSemantic @_ @Int
+ $ lit i
TokenTermAtom "neg" -> Parser $ \_ctx ->
- Right $ TermVT (intTy ~> intTy) $ E neg
+ Right $ TermVT (monoTy @Int ~> monoTy @Int) $ E neg
TokenTermAtom "add" -> Parser $ \_ctx ->
- Right $ TermVT (intTy ~> intTy ~> intTy) $ E add
+ Right $ TermVT (monoTy @Int ~> monoTy @Int ~> monoTy @Int) $ E add
ast -> next ast
instance
( Syntaxes syns (ForallSemantic syns)
(a ~> a)
$ E constI
where
- a = TyVar{tyVar = VarZ{varZKind = typeTy, varZNext = LenZ, varZMeta = (mempty :: meta)}, tyVarName = "a"}
+ a = TyVar{tyVar = VarZ{varZKind = monoTy @Type, varZNext = LenZ, varZMeta = (mempty :: meta)}, tyVarName = "a"}
TokenTermAtom "(<*>)" -> Parser $ \_ctx ->
Right
$ TermVT
((a ~> b ~> c) ~> (a ~> b) ~> a ~> c)
$ E constS
where
- a = TyVar{tyVar = VarZ{varZKind = typeTy, varZNext = LenS $ LenS $ LenZ, varZMeta = (mempty :: meta)}, tyVarName = "a"}
- b = TyVar{tyVar = VarS $ VarZ{varZKind = typeTy, varZNext = LenS $ LenZ, varZMeta = (mempty :: meta)}, tyVarName = "b"}
- c = TyVar{tyVar = VarS $ VarS $ VarZ{varZKind = typeTy, varZNext = LenZ, varZMeta = (mempty :: meta)}, tyVarName = "c"}
+ a = TyVar{tyVar = VarZ{varZKind = monoTy @Type, varZNext = LenS $ LenS $ LenZ, varZMeta = (mempty :: meta)}, tyVarName = "a"}
+ b = TyVar{tyVar = VarS $ VarZ{varZKind = monoTy @Type, varZNext = LenS $ LenZ, varZMeta = (mempty :: meta)}, tyVarName = "b"}
+ c = TyVar{tyVar = VarS $ VarS $ VarZ{varZKind = monoTy @Type, varZNext = LenZ, varZMeta = (mempty :: meta)}, tyVarName = "c"}
tok -> next tok
-intTy :: Monoid meta => Ty meta '[] Int
-intTy = TyConst{tyConst = Const{constType = typeRep @Int, constMeta = mempty}, tyConstLen = LenZ}
-
+-- * Class 'Addable'
class Addable sem where
lit :: Int -> sem Int
neg :: sem (Int -> Int)
add :: sem (Int -> Int -> Int)
+data instance ErrorParser meta Addable
+ deriving (Show)
+-- * Class 'Mulable'
class Mulable sem where
mul :: sem Int -> sem Int -> sem Int
instance (forall sem. Syntaxes syn sem => Addable sem) => Addable (ForallSemantic syn) where
-- tree0 = lit 0
tree0 = add .@ lit 8 .@ (neg .@ (add .@ lit 1 .@ lit 2))
+fun ::
+ Abstractable () sem =>
+ Typeable a =>
+ (sem a -> sem b) ->
+ sem (a -> b)
+fun = lam (monoTy @_ @())
+
-- tree1 = mul (add (lit 8) (neg (add (lit 1) (lit 2)))) (lit 2)
-tree2 = lam (typeOf @()) (\(x :: sem Int) -> add .@ x .@ lit 0)
-tree3 = lam (typeOf @()) (\(x :: sem Int) -> add .@ x .@ x)
+tree2 = fun (\x -> add .@ x .@ lit 0)
+tree3 = fun (\x -> add .@ x .@ x)
tree4 = constS .@ add .@ constI
tree0Print = print tree0
tree0ParsePrint :: TermAST ()
tree0ParsePrint = case parse @(FinalSyntaxes ()) @() tree0Print of
- Left e -> error e
+ Left e -> error $ show e
Right (TermVT _ty (runOpenTerm -> ForallSemantic sem)) -> print sem
-- tree1ParsePrint :: TermAST ()
tree2ParsePrint :: TermAST ()
tree2ParsePrint = case parse @(FinalSyntaxes ()) @() tree2Print of
- Left e -> error e
+ Left e -> error $ show e
Right (TermVT _ty (runOpenTerm -> ForallSemantic sem)) -> print sem
tree3ParsePrint :: TermAST ()
tree3ParsePrint = case parse @(FinalSyntaxes ()) @() tree3Print of
- Left e -> error e
+ Left e -> error $ show e
Right (TermVT _ty (runOpenTerm -> ForallSemantic sem)) -> print sem
tree3ParsePrint' :: TermAST ()
tree3ParsePrint' = case parse @(FinalSyntaxes ()) @() tree3ParsePrint of
- Left e -> error e
+ Left e -> error $ show e
Right (TermVT _ty (runOpenTerm -> ForallSemantic sem)) -> print sem
tree4ParsePrint :: TermAST ()
tree4ParsePrint = case parse @(FinalSyntaxes ()) @() tree4Print of
- Left e -> error e
+ Left e -> error $ show e
Right (TermVT _ty (runOpenTerm -> ForallSemantic sem)) -> print sem
import Data.Kind (Type)
import Data.Maybe (Maybe (..))
+import GHC.Stack (HasCallStack)
import Type.Reflection ((:~~:) (..))
class EqTy (x :: xK -> Type) (y :: yK -> Type) where
-- | /Heterogeneous type equality/:
-- return two proofs when two types are equals:
-- one for the type and one for the kind.
- eqTy :: x (xT :: xK) -> y (yT :: yK) -> Maybe (xT :~~: yT)
+ eqTy :: HasCallStack => x (xT :: xK) -> y (yT :: yK) -> Maybe (xT :~~: yT)
-- import GHC.Stack (HasCallStack)
import GHC.Types
import Text.Show (Show (..))
-import Type.Reflection (TypeRep, Typeable, eqTypeRep, typeRep, (:~~:) (..))
+import Type.Reflection (TypeRep, Typeable, eqTypeRep, typeRep, typeRepKind, (:~~:) (..), pattern App)
import Prelude (error)
import Prelude qualified
import Symantic.Typer.Eq
import Symantic.Typer.List
-data Const meta (a :: aK) = InferTyable aK =>
+data Const meta (a :: aK) =
+ -- InferTyable aK =>
Const
{ constType :: TypeRep a
- , -- , constKind :: Kind meta aK
- constMeta :: meta
+ , constMeta :: meta
}
-- deriving (Show)
TyApp :: {tyAppFun :: Ty meta vs f, tyAppArg :: Ty meta vs a} -> Ty meta vs (f a)
infixl 9 `TyApp`
--- ** Class 'InferTyable'
-class InferTyable (a :: aK) where
- inferTy :: meta -> Len vs -> Ty meta vs a
-instance (InferTyable a, InferTyable b) => InferTyable (a b) where
- inferTy meta vs = TyApp (inferTy @_ @a meta vs) (inferTy @_ @b meta vs)
+tyOfTypeRep :: meta -> Len vs -> TypeRep a -> Ty meta vs a
+tyOfTypeRep meta len ty = case ty of
+ App f x -> TyApp{tyAppFun = tyOfTypeRep meta len f, tyAppArg = tyOfTypeRep meta len x}
+ constType -> TyConst{tyConst = Const{constType, constMeta = meta}, tyConstLen = len}
--- instance {-# OVERLAPS #-} InferTyable Type where
--- inferTy meta vs = TyConst{tyConst = Const{constType = typeRep, constMeta = meta}, tyConstLen = vs}
-instance {-# OVERLAPPABLE #-} (Typeable a, Typeable aK) => InferTyable (a :: aK) where
- inferTy meta vs = TyConst{tyConst = Const{constType = typeRep, constMeta = meta}, tyConstLen = vs}
-
-typeOf :: Monoid meta => InferTyable a => Ty meta '[] a
-typeOf = inferTy mempty LenZ
+-- | Monomorphic 'Ty' from a 'Typeable'.
+monoTy :: forall {aK} (a :: aK) meta. Typeable a => Monoid meta => Ty meta '[] a
+monoTy = tyOfTypeRep mempty LenZ typeRep
pattern FUN ::
-- CReq
TyApp
{ tyAppFun =
TyApp
- { tyAppFun -- inferTy @(->) mempty (lenVar arg)
- =
+ { tyAppFun =
TyConst{tyConst = Const{constType = typeRep, constMeta = mempty}, tyConstLen = (lenVar arg)}
, tyAppArg = arg
}
}
infixr 0 ~>
-typeTy :: Monoid meta => Ty meta '[] Type
--- typeTy = TyConst{tyConst = Const{constType = typeRep @Type, constMeta = mempty}, tyConstLen = LenZ}
-typeTy = inferTy mempty LenZ
-
deriving instance Show meta => Show (Ty meta vs a)
-- type instance SourceOf (Ty vs src t) = src
-- instance (Monoid src) => EqTy (MT.Writer src) (MT.Writer src) where
-- eqTy x y = eqTy (unSourced x) (unSourced y)
instance EqTy (Ty meta vs) (Ty meta vs) where
- eqTy TyConst{tyConst = x} TyConst{tyConst = y} = eqTy x y
- eqTy TyVar{tyVar = x} TyVar{tyVar = y} = eqTy x y
- eqTy TyApp{tyAppFun = xF, tyAppArg = xA} TyApp{tyAppFun = yF, tyAppArg = yA}
- | Just HRefl <- eqTy xF yF
- , Just HRefl <- eqTy xA yA =
- Just HRefl
- eqTy _x _y = Nothing
+ eqTy = go
+ where
+ go :: forall xK xT yK yT. Ty meta vs (xT :: xK) -> Ty meta vs (yT :: yK) -> Maybe (xT :~~: yT)
+ go TyConst{tyConst = x} TyConst{tyConst = y} = eqTy x y
+ go TyVar{tyVar = x} TyVar{tyVar = y} = eqTy x y
+ go TyApp{tyAppFun = xF, tyAppArg = xA} TyApp{tyAppFun = yF, tyAppArg = yA}
+ | Just HRefl <- go xF yF
+ , Just HRefl <- go xA yA =
+ Just HRefl
+ go _x _y = Nothing
-- eqTy (TyFam _ _lx xF xA) (TyFam _ _ly yF yA)
-- | Just HRefl <- eqTypeRep xF yF
Maybe (c :~~: u)
proj_ConstKi = eqTypeRep (typeRep @c) . constType
--- HRefl <- eqTy ku kc -- $ kindInjP @(Ty_of_Type kc) ()
--- HRefl :: u:~~:c <- eqT
--- Just HRefl
-
-- ** Type @(#>)@
-- | /Type constant/ to qualify a 'Type'.
instance KindOf Var where
kindOf Var{varKind} = varKind
instance KindOf Ty where
- kindOf TyConst{tyConst = Const{constMeta} :: Const meta (a :: aK)} =
- -- withTypeable (typeRepKind constType) $
- inferTy @_ @aK constMeta LenZ
+ kindOf TyConst{tyConst = Const{..} :: Const meta (a :: aK)} =
+ tyOfTypeRep constMeta LenZ (typeRepKind constType)
kindOf TyApp{tyAppFun = f} = case kindOf f of
- FUN _ kf -> kf
+ TyApp
+ { tyAppFun =
+ TyApp
+ { tyAppFun = TyConst{tyConst = Const{constType = eqTypeRep (typeRep @(->)) -> Just HRefl}}
+ }
+ , tyAppArg = k
+ } -> k
t -> error $ "here: " <> show t
kindOf TyVar{tyVar = Var{varKind, varMeta}} = varKind