init
authorJulien Moutinho <julm@sourcephile.fr>
Tue, 29 Aug 2023 20:39:25 +0000 (22:39 +0200)
committerJulien Moutinho <julm@sourcephile.fr>
Tue, 29 Aug 2023 20:39:25 +0000 (22:39 +0200)
src/Symantic/Compiler/Term.hs
src/Symantic/Parser.hs
src/Symantic/Printer.hs
src/Symantic/Syntaxes.hs
src/Symantic/Typer/Eq.hs
src/Symantic/Typer/Type.hs

index 0f38ec4de617cd4e7a4c65f754f6f4c2c282b92b..be746436abf2d56e300fdfaf02caa4a6863f0683 100644 (file)
@@ -1,8 +1,10 @@
 {-# LANGUAGE ConstraintKinds #-}
+{-# LANGUAGE EmptyCase #-}
 {-# LANGUAGE InstanceSigs #-}
 {-# LANGUAGE QuantifiedConstraints #-}
 {-# LANGUAGE RankNTypes #-}
 {-# LANGUAGE UndecidableInstances #-}
+{-# OPTIONS_GHC -Wno-partial-fields #-}
 
 module Symantic.Compiler.Term where
 
@@ -11,9 +13,9 @@ import Control.Monad (Monad (..))
 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)
@@ -21,6 +23,31 @@ 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)
index c8d8a3a48768e3db1d0b232ef6b5c2b539df642b..d6e66d7dd6aba169266b53ae0e702dda67c1490e 100644 (file)
@@ -1,4 +1,5 @@
 {-# LANGUAGE RankNTypes #-}
+{-# OPTIONS_GHC -Wno-partial-fields #-}
 
 module Symantic.Parser where
 
@@ -21,11 +22,54 @@ data Parser syns meta = Parser
       ( -- 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
index ca55eff2cd0cf2babb1745067381f572df82b5b8..17e6885022359250af978665ddcd2c276970ae90 100644 (file)
@@ -3,31 +3,9 @@
 
 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
index e19b85f97434501afe76cd2c79126b6b9819cd19..6038851e6738113f12b2e43c4bab54388a7cd0a4 100644 (file)
@@ -1,6 +1,7 @@
 {-# LANGUAGE AllowAmbiguousTypes #-}
 {-# LANGUAGE ConstraintKinds #-}
 {-# LANGUAGE DataKinds #-}
+{-# LANGUAGE EmptyDataDeriving #-}
 {-# LANGUAGE PolyKinds #-}
 {-# LANGUAGE QuantifiedConstraints #-}
 {-# LANGUAGE RankNTypes #-}
@@ -18,15 +19,15 @@ module Symantic.Syntaxes where
 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
@@ -40,17 +41,16 @@ parse ::
   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 =
@@ -60,26 +60,31 @@ parse ast = unParser (fix parsersA ast) CtxTyZ
               }
           , 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
@@ -97,35 +102,40 @@ type OpenParser syns 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)
@@ -139,19 +149,25 @@ instance
                 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)
@@ -166,26 +182,27 @@ instance
           (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
@@ -263,9 +280,16 @@ type FinalSyntaxes meta = '[Abstractable meta, Addable]
 -- 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
 
@@ -276,7 +300,7 @@ tree4Print = print tree4
 
 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 ()
@@ -286,20 +310,20 @@ tree0ParsePrint = case parse @(FinalSyntaxes ()) @() tree0Print of
 
 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
index b2cc9bae30a56f0bcf3d9c58cea20d667d51e943..3929dc7f10f3fcdafb4a1f570a9d8019ab48a048 100644 (file)
@@ -5,10 +5,11 @@ module Symantic.Typer.Eq where
 
 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)
index 1825ca46ad257ab83c3dce24a5f288ce2f4a082f..5825a6f4215d39de877dc6a7d93633d969fe8ae0 100644 (file)
@@ -25,18 +25,18 @@ import Data.String (String)
 -- 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)
@@ -197,19 +197,14 @@ data Ty :: forall aK. Type -> [Type] -> aK -> Type where
   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
@@ -245,8 +240,7 @@ pattern FUN arg res <-
   TyApp
     { tyAppFun =
         TyApp
-          { tyAppFun -- inferTy @(->) mempty (lenVar arg)
-            =
+          { tyAppFun =
               TyConst{tyConst = Const{constType = typeRep, constMeta = mempty}, tyConstLen = (lenVar arg)}
           , tyAppArg = arg
           }
@@ -254,10 +248,6 @@ pattern FUN arg res <-
     }
 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
@@ -327,13 +317,16 @@ instance Eq (TyVT m) where
 -- 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
@@ -407,10 +400,6 @@ proj_ConstKi ::
   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'.
@@ -469,11 +458,16 @@ class KindOf (ty :: Type -> [Type] -> aK -> Type) where
 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