From f33e08d27702bae9339fe99905e44e6607192e27 Mon Sep 17 00:00:00 2001
From: Julien Moutinho <julm@sourcephile.fr>
Date: Sat, 5 Aug 2023 13:48:46 +0200
Subject: [PATCH] init

---
 .gitignore                    |  21 ++
 .reuse/dep5                   |  10 +-
 flake.nix                     |   2 +-
 src/ForallSem.hs              | 547 ----------------------------------
 src/Symantic/Compiler.hs      |   5 +
 src/Symantic/Compiler/Term.hs |  72 +++++
 src/Symantic/Parser.hs        |  83 ++++++
 src/Symantic/Parser/Error.hs  |  23 ++
 src/Symantic/Parser/Source.hs |  89 ++++++
 src/Symantic/Printer.hs       |  34 +++
 src/Symantic/Syntaxes.hs      | 226 ++++++++++++++
 src/Symantic/Typer.hs         |  11 +
 src/Symantic/Typer/Eq.hs      |  14 +
 src/Symantic/Typer/List.hs    |  47 +++
 src/Symantic/Typer/Type.hs    | 467 +++++++++++++++++++++++++++++
 src/Symantic/Typer/Unify.hs   | 269 +++++++++++++++++
 symantic.cabal                | 206 ++-----------
 17 files changed, 1396 insertions(+), 730 deletions(-)
 create mode 100644 .gitignore
 delete mode 100644 src/ForallSem.hs
 create mode 100644 src/Symantic/Compiler.hs
 create mode 100644 src/Symantic/Compiler/Term.hs
 create mode 100644 src/Symantic/Parser.hs
 create mode 100644 src/Symantic/Parser/Error.hs
 create mode 100644 src/Symantic/Parser/Source.hs
 create mode 100644 src/Symantic/Printer.hs
 create mode 100644 src/Symantic/Syntaxes.hs
 create mode 100644 src/Symantic/Typer.hs
 create mode 100644 src/Symantic/Typer/Eq.hs
 create mode 100644 src/Symantic/Typer/List.hs
 create mode 100644 src/Symantic/Typer/Type.hs
 create mode 100644 src/Symantic/Typer/Unify.hs

diff --git a/.gitignore b/.gitignore
new file mode 100644
index 0000000..2f00fe6
--- /dev/null
+++ b/.gitignore
@@ -0,0 +1,21 @@
+*.actual.*
+*.eventlog
+*.eventlog.html
+*.eventlog.json
+*.hi
+*.hp
+*.o
+*.orig
+*.prof
+*.root
+*~
+.direnv/
+.ghc.environment.*
+.shake
+.stack-work/
+/.direnv
+/.pre-commit-config.yaml
+dist-newstyle/
+dump-core/
+hlint.html
+result*
diff --git a/.reuse/dep5 b/.reuse/dep5
index 4db55a9..e110498 100644
--- a/.reuse/dep5
+++ b/.reuse/dep5
@@ -1,13 +1,13 @@
 Format: https://www.debian.org/doc/packaging-manuals/copyright-format/1.0/
-Upstream-Name: literate-web
-Upstream-Contact: Julien Moutinho <julm+literate-web@sourcephile.fr>
-Source: https://git.sourcephile.fr/haskell/literate-web
+Upstream-Name: symantic
+Upstream-Contact: Julien Moutinho <julm+symantic@sourcephile.fr>
+Source: https://git.sourcephile.fr/haskell/symantic
 
 Files: *.lock cabal.project* *.cabal *.md .chglog/* .envrc
  .gitignore .gitmodules .git-blame-ignore-revs *.yaml
-Copyright: Julien Moutinho <julm+literate-web@sourcephile.fr>
+Copyright: Julien Moutinho <julm+symantic@sourcephile.fr>
 License: CC0-1.0
 
 Files: src/* tests/* Makefile *.nix
-Copyright: Julien Moutinho <julm+literate-web@sourcephile.fr>
+Copyright: Julien Moutinho <julm+symantic@sourcephile.fr>
 License: AGPL-3.0-or-later
diff --git a/flake.nix b/flake.nix
index 6fbe0ea..da7bddd 100644
--- a/flake.nix
+++ b/flake.nix
@@ -13,7 +13,7 @@
       forAllSystems = f: lib.genAttrs lib.systems.flakeExposed (system: f rec {
         inherit system;
         pkgs = inputs.nixpkgs.legacyPackages.${system};
-        haskellPackages = pkgs.haskellPackages.extend (with pkgs.haskell.lib; hfinal: hsuper: {
+        haskellPackages = pkgs.haskell.packages.ghc92.extend (with pkgs.haskell.lib; hfinal: hsuper: {
           ${pkg} = doBenchmark (buildFromSdist (hfinal.callCabal2nix pkg ./. { }));
           symantic-base = buildFromSdist (hfinal.callCabal2nix "symantic-base" inputs.symantic-base { });
         });
diff --git a/src/ForallSem.hs b/src/ForallSem.hs
deleted file mode 100644
index 342f22b..0000000
--- a/src/ForallSem.hs
+++ /dev/null
@@ -1,547 +0,0 @@
-{-# LANGUAGE ConstraintKinds #-}
-{-# LANGUAGE DataKinds #-}
-{-# LANGUAGE DeriveFunctor #-}
-{-# LANGUAGE AllowAmbiguousTypes #-}
-{-# LANGUAGE NoImplicitPrelude #-}
-{-# LANGUAGE NoMonomorphismRestriction #-}
-{-# LANGUAGE QuantifiedConstraints #-}
-{-# LANGUAGE RankNTypes #-}
-{-# LANGUAGE ScopedTypeVariables #-}
-{-# LANGUAGE StandaloneDeriving #-}
-{-# LANGUAGE TypeFamilies #-}
-{-# LANGUAGE UndecidableInstances #-}
-{-# LANGUAGE UndecidableSuperClasses #-}
-{-# LANGUAGE ImportQualifiedPost #-}
-{-# LANGUAGE PatternSynonyms #-}
-{-# LANGUAGE StandaloneKindSignatures #-}
-{-# LANGUAGE PolyKinds #-}
-{-# LANGUAGE DataKinds #-}
-{-# LANGUAGE ViewPatterns #-}
-
-module ForallSem where
-
-import Data.Functor (Functor(..), (<$>))
-import Data.Functor.Constant (Constant(..))
-import Control.Applicative (Applicative(..))
-import Control.Monad (Monad(..))
-import Data.Kind (Type, Constraint)
-import Data.Function (($), (.), id)
-import Data.String (String)
-import Data.Semigroup (Semigroup(..))
-import Data.Maybe (Maybe(..), isJust)
-import Text.Read (Read(..), reads)
-import Data.Bool (otherwise)
-import Text.Show (Show(..))
-import Data.Eq (Eq(..))
-import Data.Either (Either(..))
-import Data.Int (Int)
-import Prelude (error)
-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 Type.Reflection
-import Unsafe.Coerce (unsafeCoerce)
-import Data.Proxy (Proxy(..))
-import Prelude qualified
-import GHC.Types
-
-type Semantic = Type -> Type
-type Syntax = Semantic -> Constraint
-class Syn0 (sem::Semantic) where
-  syn0 :: sem ()
-class Syn1 (sem::Semantic) where
-  syn1 :: sem ()
-class Syn2 (sem::Semantic) where
-  syn2 :: sem () -> sem () -> sem ()
-
-p0 :: (forall sem. syn sem => Syn0 sem) => ForallSem syn ()
-p0 = ForallSem syn0
-
-p1 :: (forall sem. syn sem => Syn1 sem) => ForallSem syn ()
-p1 = ForallSem syn1
-
-p3 :: forall syn.
-      ( forall sem. syn sem => Syn0 sem
-      , forall sem. syn sem => Syn1 sem
-      , forall sem. syn sem => Syn2 sem
-      ) => ForallSem syn ()
-p3 = ForallSem $ syn2 (unForallSem @syn p0) (unForallSem @syn p1)
-
-
-
-
-
-
-
-data ForallSem (syn::Syntax) (a::Type)
-   = ForallSem { unForallSem :: forall sem. syn sem => sem a }
-
-instance ( forall sem. syn sem => Functor sem
-         ) => Functor (ForallSem syn) where
-  fmap f (ForallSem sem) = ForallSem (fmap f sem)
-  a <$ (ForallSem sem) = ForallSem (a <$ sem)
-instance ( forall sem. syn sem => Applicative sem
-         , Functor (ForallSem syn)
-         ) => Applicative (ForallSem syn) where
-  pure a = ForallSem (pure a)
-  liftA2 f (ForallSem a) (ForallSem b) = ForallSem (liftA2 f a b)
-  (<*>) (ForallSem f) (ForallSem a) = ForallSem ((<*>) f a)
-  (<*) (ForallSem f) (ForallSem a) = ForallSem ((<*) f a)
-  (*>) (ForallSem f) (ForallSem a) = ForallSem ((*>) f a)
-instance ( forall sem. syn sem => Monad sem
-         , Applicative (ForallSem syn)
-         ) => Monad (ForallSem syn) where
-  (>>=) (ForallSem sa) f = ForallSem (sa >>= \a -> case f a of ForallSem sb -> sb)
-  return = pure
-  (>>) = (*>)
-
--- * Interpreter 'Parser'
-data TermVT syn = forall vs a. TermVT
-  { typeTermVT :: Ty vs a
-  , unTermVT  :: ForallSem syn a
-  }
-
--- instance Eq (TyVT) where
---   TyVT x == TyVT y =
---     let (x', y') = appendVars x y in
---     isJust $ eqTypeKi x' y'
-
--- * Type family @(++)@
-type family (++) xs ys where
-  '[] ++ ys  = ys
-  -- xs  ++ '[] = xs
-  (x ': xs) ++ ys = x ': xs ++ ys
-infixr 5 ++
-
--- * Type 'Len'
-data Len (xs::[k]) where
-  LenZ :: Len '[]
-  LenS :: Len xs -> Len (x ': xs)
-
-instance Show (Len vs) where
-  showsPrec _p = showsPrec 10 . intLen
-
-addLen :: Len a -> Len b -> Len (a ++ b)
-addLen LenZ     b = b
-addLen (LenS a) b = LenS $ addLen a b
-
-shiftLen :: forall t b a.  Len a -> Len (a ++      b) -> Len (a ++ t ': b)
-shiftLen LenZ b = LenS b
-shiftLen (LenS a) (LenS b) = LenS $ shiftLen @t @b a b
-
-intLen :: Len xs -> Int
-intLen = go 0
-  where
-  go :: Int -> Len xs -> Int
-  go i LenZ     = i
-  go i (LenS l) = go (1 Prelude.+ i) l
-
--- ** Class 'LenInj'
-class LenInj (vs::[k]) where
-  lenInj :: Len vs
-instance LenInj '[] where
-  lenInj = LenZ
-instance LenInj as => LenInj (a ': as) where
-  lenInj = LenS lenInj
-
-type Name = String
--- Use a CUSK, because it's a polymorphically recursive type,
--- See https://ryanglscott.github.io/2020/01/05/five-benefits-to-using-standalonekindsignatures/
-data Ty :: forall aK. [Type] -> aK -> Type where
-  TyConst :: Len vs -> TypeRep a -> Ty vs a
-  TyVar :: Name -> Var vs a -> Ty vs a
-  TyApp :: Ty vs f -> Ty vs a -> Ty vs (f a)
-infixl 9 `TyApp`
-deriving instance Show (Ty vs a)
-instance AllocVars Ty where
-  allocVarsL len (TyConst l c)  = TyConst (addLen len l) c
-  allocVarsL len (TyApp f a)    = TyApp (allocVarsL len f) (allocVarsL len a)
-  allocVarsL len (TyVar n v)    = TyVar n (allocVarsL len v)
-  --allocVarsL len (TyFam l f as) = TyFam (addLen len l) f $ allocVarsL len `mapTys` as
-  
-  allocVarsR len (TyConst l c)  = TyConst (addLen l len) c
-  allocVarsR len (TyApp f a)    = TyApp (allocVarsR len f) (allocVarsR len a)
-  allocVarsR len (TyVar n v)    = TyVar n (allocVarsR len v)
-  --allocVarsR len (TyFam l f as) = TyFam (addLen l len) f $ allocVarsR len `mapTys` as
-
-data TyVT = forall vs a. TyVT (Ty vs a)
-deriving instance Show TyVT
-instance Eq TyVT where
-  TyVT x == TyVT y = isJust (eqTyKi x' y')
-    where (x', y') = appendVars x y
-
--- | /Heterogeneous type equality/:
--- return two proofs when two 'Type's are equals:
--- one for the type and one for the kind.
-eqTyKi :: Ty vs (x::xK) -> Ty vs (y::yK) -> Maybe (x:~~:y)
-eqTyKi (TyConst _lx x) (TyConst _ly y) = eqTypeRep x y
-eqTyKi (TyVar   _nx x) (TyVar   _ny y) = eqVarKi   x y
-eqTyKi (TyApp fx ax) (TyApp fy ay)
- | Just HRefl <- eqTyKi fx fy
- , Just HRefl <- eqTyKi ax ay
- = Just HRefl
--- eqTyKi (TyFam _ _lx fx ax) (TyFam _ _ly fy ay)
---  | Just HRefl <- eqTypeRep fx fy
---  , Just HRefl <- eqTypes ax ay
---  = Just HRefl
--- -- NOTE: 'TyFam' is expanded as much as possible.
--- eqTyKi x@TyFam{} y = eqTyKi (expandFam x) y
--- eqTyKi x y@TyFam{} = eqTyKi x (expandFam y)
-eqTyKi _x _y = Nothing
-
--- data Some :: (Type -> Type) -> Type where
---   Some :: TypeRep a -> t a -> Some t
--- 
--- mapSome :: (forall a. s a -> t a) -> Some s -> Some t
--- mapSome f (Some a t) = Some a (f t)
--- 
--- type SomeTy = Some (Constant ())
-
--- pattern SomeTy :: TypeRep a -> SomeTy
--- pattern SomeTy a = Some a (Constant ())
--- {-# COMPLETE SomeTy #-}
-
--- someType :: TypeRep a -> SomeTy
--- someType a = Some a (Constant ())
-
---infer :: Vars vs -> TermVT syn -> Maybe (TermVT syn)
---infer ctx te = case te of
---Lit i -> return $ Some TTyInt (embed (CInt i))
-
-
-data Parser syn = Parser
-  { unParser ::
-      --MT.State (TokenTerm a)
-        (Either ErrMsg (TermVT syn))
-  }
-
-{-
-instance ( forall sem. syn sem => Functor sem
-         ) => Functor (Parser syn) where
-  fmap f (Parser esa) = Parser $
-    case esa of
-      Left e -> Left e
-      Right (ForallSem sem) -> Right (ForallSem (f <$> sem))
-  a <$ Parser esa = Parser $
-    case esa of
-      Left e -> Left e
-      Right (ForallSem sem) -> Right (ForallSem (a <$ sem))
-instance ( forall sem. syn sem => Applicative sem
-         , Applicative (ForallSem syn)
-         , forall err. syn (Either err)
-         , syn (Parser syn) -- FIXME: what constraint is still missing to still require that?
-         ) => Applicative (Parser syn) where
-  pure a = Parser (Right (ForallSem (pure a)))
-  liftA2 f (Parser a) (Parser b) = Parser (liftA2 (liftA2 f) a b)
-  (<*>) (Parser f) (Parser a) = Parser (liftA2 (<*>) f a)
-  (*>) (Parser f) (Parser a) = Parser (liftA2 (*>) f a)
-  (<*) (Parser f) (Parser a) = Parser (liftA2 (<*) f a)
-instance ( forall sem. syn sem => Monad sem
-         , forall err. syn (Either err)
-         , syn (Parser syn) -- FIXME: what constraint is still missing to still require that?
-         ) => Monad (Parser syn) where
-  (>>=) (Parser efsa) f = Parser (efsa >>= \(ForallSem sa) -> sa >>= unParser . f)
--}
-
--- * Type 'BinTree'
--- | /Binary Tree/.
-data BinTree a
- =   BinTree0 a
- |   BinTree2 (BinTree a) (BinTree a)
- deriving (Eq, Show)
-
-type TermAST = BinTree TokenTerm
-data TokenTerm
-   = TokenTermAtom String
-   | TokenTermAbst String TyVT TermAST
-   deriving (Show)
-
-tree0 = add (lit 8) (neg (add (lit 1) (lit 2)))
-tree1 = mul (add (lit 8) (neg (add (lit 1) (lit 2)))) (lit 2)
-tree2 = lam (\(x::sem Int) -> mul (lit 0) (add (lit 1) (lit 2)))
-tree0Print = print tree0
-tree1Print = print tree1
-tree2Print = print tree2
-
-type ErrMsg = String
-
-safeRead :: Read a => String -> Either ErrMsg a
-safeRead s = case reads s of
-               [(x,"")] -> Right x
-               _        -> Left $ "Read error: " <> s
-
-instance (forall sem. syn sem => Addable sem) => Addable (ForallSem syn) where
-  lit n = ForallSem (lit n)
-  neg (ForallSem a) = ForallSem (neg a)
-  add (ForallSem a) (ForallSem b) = ForallSem (add a b)
-instance (forall sem. syn sem => Mulable sem) => Mulable (ForallSem syn) where
-  mul (ForallSem a) (ForallSem b) = ForallSem (mul a b)
-instance ( forall sem. syn sem => Abstractable sem
-         --, forall sem. syn sem => Typeable sem -- user instance not accepted
-         --, forall s1 s2. (syn s1, syn s2) => s1 ~ s2 -- crazy...
-         ) => Abstractable (ForallSem syn) where
-  ForallSem a2b .@ ForallSem a = ForallSem (a2b .@ a)
-  lam f = ForallSem (lam (\a -> let ForallSem b = f (forallSem a) in b))
-    where
-    -- Safe here because a :: sem a and b :: sem b share the same 'sem'.
-    forallSem :: sem a -> ForallSem syn a
-    forallSem a = ForallSem (unsafeCoerce a)
-
-
-
-parseAddable ::
- ( forall sem. syn sem => Addable sem
- , syn (ForallSem syn)
- ) =>
- (TermAST -> Parser syn) -> TermAST -> Parser syn
-parseAddable _final (BinTree0 (TokenTermAtom s))
-  | Right (i::Int) <- safeRead s
-  = Parser $ Right $ TermVT (TyConst LenZ typeRep) $ ForallSem @_ @Int $ lit i
-parseAddable final (BinTree2 (BinTree0 (TokenTermAtom "Neg")) aT) = Parser $
-  case final aT of
-    Parser aE -> do
-      TermVT aTy (ForallSem a :: ForallSem syn a) <- aE
-      case eqTyKi aTy (TyConst (lenVars aTy) (typeRep @Int)) of
-        Nothing -> Left "TypeError"
-        Just HRefl -> do
-          Right $ TermVT aTy $ neg a
-parseAddable final (BinTree2 (BinTree2 (BinTree0 (TokenTermAtom "Add")) aT) bT) =
-  Parser $ do
-    TermVT aTy (ForallSem a :: ForallSem syn a) <- unParser (final aT)
-    case eqTyKi aTy (TyConst (lenVars aTy) (typeRep @Int)) of
-      Nothing -> Left "TypeError"
-      Just HRefl -> do
-        TermVT bTy (ForallSem b :: ForallSem syn b) <- unParser (final bT)
-        case eqTyKi bTy (TyConst (lenVars bTy) (typeRep @Int)) of
-          Nothing -> Left "TypeError"
-          Just HRefl -> do
-            Right $ TermVT aTy $ ForallSem @_ @Int $ add a b
-parseAddable _final e = Parser $ Left $ "Invalid tree: " <> show e
-
---tree0Parser :: (forall sem. syn sem => Addable sem, syn (ForallSem syn)) => Either ErrMsg (ForallSem syn Int)
---tree0Parser = unParser $ parse tree0Print
-
-class    (Addable sem, Mulable sem, Abstractable sem) => FinalSyntaxes sem
-instance (Addable sem, Mulable sem, Abstractable sem) => FinalSyntaxes sem
-
-parseMulable ::
-  ( forall sem. syn sem => Mulable sem
-  , forall sem. syn sem => Addable sem
-  , syn (ForallSem syn)
-  ) =>
-  (TermAST -> Parser syn) -> TermAST -> Parser syn
-parseMulable final (BinTree2 (BinTree2 (BinTree0 (TokenTermAtom "Mul")) aT) bT) =
-  Parser $ do
-    case (final aT, final bT) of
-      (Parser aE, Parser bE) -> do
-        TermVT aTy (ForallSem a :: ForallSem syn a) <- aE
-        case eqTyKi aTy (TyConst (lenVars aTy) (typeRep @Int)) of
-          Nothing -> Left "TypeError"
-          Just HRefl -> do
-            TermVT bTy (ForallSem b :: ForallSem syn b) <- bE
-            case eqTyKi bTy (TyConst (lenVars bTy) (typeRep @Int)) of
-              Nothing -> Left "TypeError"
-              Just HRefl -> do
-                    Right $ TermVT aTy (ForallSem @_ @a $ mul a b)
-parseMulable final t = parseAddable final t
-
-parseAbstractable ::
-  ( forall sem. syn sem => Mulable sem
-  , forall sem. syn sem => Addable sem
-  , forall sem. syn sem => Abstractable sem
-  , syn (ForallSem syn)
-  ) =>
-  a ~ Int =>
-  (TermAST -> Parser syn) -> TermAST -> Parser syn
--- TODO: parse variables
-parseAbstractable final (BinTree0 (TokenTermAbst n (TyVT (aTy::Ty vs a)) bT)) =
-  Parser $
-    case final bT of
-      Parser bE -> do
-            TermVT abTy (abF :: ForallSem syn ab) <- bE
-            case eqTyKi (TyConst (lenVars aTy) (typeRep @Type)) aTy of
-              Nothing -> Left "TypeError"
-              Just HRefl -> do
-                case abTy of
-                  FUN iTy bTy ->
-                    case eqTyKi (TyConst (lenVars bTy) (typeRep @Type)) bTy of
-                      Nothing -> Left "TypeError"
-                      Just HRefl -> do
-                        -- FIXME: appendVars
-                        case eqTyKi aTy iTy of
-                          Nothing -> Left "TypeError"
-                          Just HRefl -> do
-                            case abF of
-                              ForallSem ab ->
-                                Right $ TermVT abTy $ ForallSem @_ @ab $
-                                  -- FIXME: Tyable
-                                  lam (ab .@)
-                  _ -> Left "TypeError"
-parseAbstractable final t = parseMulable final t
-
-pattern FUN :: forall k (fun :: k) vs. ()
-            => forall (r1 :: RuntimeRep) (r2 :: RuntimeRep)
-                      (arg :: TYPE r1) (res :: TYPE r2).
-               (k ~ Type, fun ~~ (arg -> res))
-            => Ty vs arg
-            -> Ty vs res
-            -> Ty vs fun
-pattern FUN arg res <- (TyConst _len (eqTypeRep (typeRep @(->)) -> Just HRefl) `TyApp` arg) `TyApp` res
-  where FUN arg res = (TyConst (lenVars arg) (typeRep @(->)) `TyApp` arg) `TyApp` res
-
--- * Class 'LenVars'
--- | Return the 'Len' of the 'Var' context.
-class LenVars a where
-  lenVars :: a -> Len (VarsOf a)
-
-type instance VarsOf (Ty vs a) = vs
-instance LenVars (Ty vs a) where
-  lenVars (TyConst len _c) = len
-  lenVars (TyApp f _a)     = lenVars f
-  lenVars (TyVar _n v)     = lenVars v
-  -- lenVars (TyFam l _f _as) = l
-
--- * Type family 'VarsOf'
--- | Return the 'Var' context of something.
-type family   VarsOf a :: [Type]
-type instance VarsOf (Var vs v) = vs
---type instance VarsOf (UsedVars src vs vs') = vs'
-
-
-
--- * Class 'AllocVars'
--- | Allocate 'Var's in a 'Var' context,
--- either to the left or to the right.
-class AllocVars (a::[Type] -> k -> Type) where
-  allocVarsL :: Len len -> a vs x -> a (len ++ vs) x
-  allocVarsR :: Len len -> a vs x -> a (vs ++ len) x
-
-appendVars ::
- AllocVars a =>
- AllocVars b =>
- LenVars (a vs_x x) =>
- LenVars (b vs_y y) =>
- VarsOf (a vs_x x) ~ vs_x =>
- VarsOf (b vs_y y) ~ vs_y =>
- a vs_x (x::kx) ->
- b vs_y (y::ky) ->
- ( a (vs_x ++ vs_y) x
- , b (vs_x ++ vs_y) y )
-appendVars x y =
-  ( allocVarsR (lenVars y) x
-  , allocVarsL (lenVars x) y
-  )
-
-
-
--- Var
-data Var (vs::[Type]) (v::vK) :: Type where
-  VarZ :: TypeRep vk -> Len (Proxy (v::vK) ': vs) -> Var (Proxy (v::vK) ': vs) v
-  VarS :: Var vs v -> Var (not_v ': vs) v
-instance AllocVars Var where
-  allocVarsL LenZ v       = v
-  allocVarsL (LenS len) v = VarS (allocVarsL len v)
-
-  allocVarsR len (VarZ k l) = VarZ k (addLen l len)
-  allocVarsR len (VarS v)   = VarS (allocVarsR len v)
-
-data VarV vs = forall v. VarV (Var vs v)
-instance LenVars (Var vs v) where
-  lenVars (VarZ _k l) = l
-  lenVars (VarS v)    = LenS (lenVars v)
-
-deriving instance Show (Var vs v)
-
-eqVarKi :: Var vs x -> Var vs y -> Maybe ((x::kx) :~~: (y::ky))
-eqVarKi VarZ{} VarZ{}     = Just HRefl
-eqVarKi (VarS x) (VarS y) = eqVarKi x y
-eqVarKi _ _               = Nothing
-
--- Vars
-data Vars (vs::[Type]) :: Type where
-  -- VarsZ represents an empty context.
-  VarsZ :: Vars '[]
-  -- A cons stores a variable name and its type,
-  -- and then the rest of the context.
-  VarsS :: String -> TypeRep vK -> Vars vs -> Vars (Proxy (v::vK) ': vs)
-type instance VarsOf (Vars vs) = vs
-instance LenVars (Vars vs) where
-  lenVars VarsZ = LenZ
-  lenVars (VarsS _n _kv vs) = LenS $ lenVars vs
-
-
--- Vars
-data Env :: [Type] -> Type where
-  ENil :: Env '[]
-  ECons :: v -> Env vs -> Env (v ': vs)
-
--- (!) :: Env vs -> Var vs v -> v
--- (ECons x _) ! VarZ = x
--- (ECons _ e) ! (VarS x) = e ! x
--- ENil ! _ = error "GHC can't tell this is impossible"
-
-lookupVars :: String -> Vars vs -> Maybe (VarV vs)
-lookupVars _ VarsZ = Nothing
-lookupVars n (VarsS vN vK vs)
-  | n == vN = Just (VarV (VarZ vK (LenS (lenVars vs))))
-  | otherwise = (\(VarV v) -> VarV (VarS v)) <$> lookupVars n vs
-
-
-fix :: (a -> a) -> a
-fix f = f (fix f)
-
-parse ::
-  ( forall sem. syn sem => Addable sem
-  , forall sem. syn sem => Mulable sem
-  , forall sem. syn sem => Abstractable sem
-  , syn (ForallSem syn)
-  ) =>
-  TermAST -> Parser syn
-parse = fix parseAbstractable
-
-tree0ParsePrint :: TermAST
-tree0ParsePrint = case parse @FinalSyntaxes tree0Print of
-  Parser (Left e) -> error e
-  Parser (Right (TermVT _ty (ForallSem sem))) -> print sem
-
-tree1ParsePrint :: TermAST
-tree1ParsePrint = case parse @FinalSyntaxes tree1Print of
-  Parser (Left e) -> error e
-  Parser (Right (TermVT _ty (ForallSem sem))) -> print sem
-
-tree2ParsePrint :: TermAST
-tree2ParsePrint = case parse @FinalSyntaxes tree2Print of
-  Parser (Left e) -> error e
-  Parser (Right (TermVT _ty (ForallSem sem))) -> print sem
-
-class Addable sem where
-  lit :: Int -> sem Int
-  neg :: sem Int -> sem Int
-  add :: sem Int -> sem Int -> sem Int
-class Mulable sem where
-  mul :: sem Int -> sem Int -> sem Int
-class Abstractable sem where
-  -- | Lambda term abstraction, in HOAS (Higher-Order Abstract Syntax) style.
-  lam :: Typeable a => (sem a -> sem b) -> sem (a -> b)
-  -- | Application, aka. unabstract.
-  (.@) :: sem (a -> b) -> sem a -> sem b
-
-
--- * Interpreter 'Printer'
-newtype Printer a = Printer { unPrinter :: TermAST }
-print :: Printer a -> TermAST
-print = unPrinter
-print2 :: String -> Printer a1 -> Printer a2 -> Printer a3
-print2 n (Printer aT) (Printer bT) = Printer $ BinTree2 (BinTree2 (BinTree0 (TokenTermAtom n)) aT) bT
-instance Addable Printer where
-  lit n = Printer $ BinTree0 (TokenTermAtom (show n))
-  neg (Printer aT) = Printer $ BinTree2 (BinTree0 (TokenTermAtom "Neg")) aT
-  add = print2 "Add"
-instance Mulable Printer where
-  mul = print2 "Mul"
-instance Abstractable Printer where
-  Printer f .@ Printer a = Printer $ BinTree2 f a
-  lam (f::Printer a -> Printer b) = Printer $
-                                  -- FIXME: Tyable? instead of Typeable?
-      BinTree0 (TokenTermAbst "x" (TyVT (TyConst (lenInj @_ @'[]) (typeRep @a)))
-                                  (unPrinter (f (Printer (BinTree0 (TokenTermAtom "x"))))))
diff --git a/src/Symantic/Compiler.hs b/src/Symantic/Compiler.hs
new file mode 100644
index 0000000..2fea388
--- /dev/null
+++ b/src/Symantic/Compiler.hs
@@ -0,0 +1,5 @@
+module Symantic.Compiler (
+  module Symantic.Compiler.Term,
+) where
+
+import Symantic.Compiler.Term
diff --git a/src/Symantic/Compiler/Term.hs b/src/Symantic/Compiler/Term.hs
new file mode 100644
index 0000000..42307ea
--- /dev/null
+++ b/src/Symantic/Compiler/Term.hs
@@ -0,0 +1,72 @@
+{-# LANGUAGE ConstraintKinds #-}
+{-# LANGUAGE QuantifiedConstraints #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE UndecidableInstances #-}
+
+module Symantic.Compiler.Term 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.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.Typer
+
+type Semantic = Type -> Type
+type Syntax = Semantic -> Constraint
+
+data ForallSem (syn :: Syntax) (a :: Type) = ForallSem {unForallSem :: forall sem. syn sem => sem a}
+
+instance
+  ( forall sem. syn sem => Functor sem
+  ) =>
+  Functor (ForallSem syn)
+  where
+  fmap f (ForallSem sem) = ForallSem (fmap f sem)
+  a <$ (ForallSem sem) = ForallSem (a <$ sem)
+instance
+  ( forall sem. syn sem => Applicative sem
+  , Functor (ForallSem syn)
+  ) =>
+  Applicative (ForallSem syn)
+  where
+  pure a = ForallSem (pure a)
+  liftA2 f (ForallSem a) (ForallSem b) = ForallSem (liftA2 f a b)
+  (<*>) (ForallSem f) (ForallSem a) = ForallSem ((<*>) f a)
+  (<*) (ForallSem f) (ForallSem a) = ForallSem ((<*) f a)
+  (*>) (ForallSem f) (ForallSem a) = ForallSem ((*>) f a)
+instance
+  ( forall sem. syn sem => Monad sem
+  , Applicative (ForallSem syn)
+  ) =>
+  Monad (ForallSem syn)
+  where
+  (>>=) (ForallSem sa) f = ForallSem (sa >>= \a -> case f a of ForallSem sb -> sb)
+  return = pure
+  (>>) = (*>)
+
+-- * Interpreter 'Parser'
+data TermVT syn = forall vs a.
+  TermVT
+  { typeTermVT :: Ty () vs a
+  , unTermVT :: ForallSem syn a
+  }
diff --git a/src/Symantic/Parser.hs b/src/Symantic/Parser.hs
new file mode 100644
index 0000000..d031073
--- /dev/null
+++ b/src/Symantic/Parser.hs
@@ -0,0 +1,83 @@
+module Symantic.Parser 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.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.Typer
+
+-- * Type 'Parser'
+data Parser syn = Parser
+  { unParser ::
+      ( -- MT.State (TokenTerm a)
+        Either ErrMsg (TermVT syn)
+      )
+  }
+type ErrMsg = String
+-- * Type 'BinTree'
+
+-- | /Binary Tree/.
+data BinTree a
+  = BinTree0 a
+  | BinTree2 (BinTree a) (BinTree a)
+  deriving (Eq, Show)
+
+type TermAST = BinTree TokenTerm
+data TokenTerm
+  = TokenTermAtom String
+  | TokenTermAbst String (TyVT ()) TermAST
+  deriving (Show)
+
+safeRead :: Read a => String -> Either ErrMsg a
+safeRead s = case reads s of
+  [(x, "")] -> Right x
+  _ -> Left $ "Read error: " <> s
+
+{-
+instance ( forall sem. syn sem => Functor sem
+         ) => Functor (Parser syn) where
+  fmap f (Parser esa) = Parser $
+    case esa of
+      Left e -> Left e
+      Right (ForallSem sem) -> Right (ForallSem (f <$> sem))
+  a <$ Parser esa = Parser $
+    case esa of
+      Left e -> Left e
+      Right (ForallSem sem) -> Right (ForallSem (a <$ sem))
+instance ( forall sem. syn sem => Applicative sem
+         , Applicative (ForallSem syn)
+         , forall err. syn (Either err)
+         , syn (Parser syn) -- FIXME: what constraint is still missing to still require that?
+         ) => Applicative (Parser syn) where
+  pure a = Parser (Right (ForallSem (pure a)))
+  liftA2 f (Parser a) (Parser b) = Parser (liftA2 (liftA2 f) a b)
+  (<*>) (Parser f) (Parser a) = Parser (liftA2 (<*>) f a)
+  (*>) (Parser f) (Parser a) = Parser (liftA2 (*>) f a)
+  (<*) (Parser f) (Parser a) = Parser (liftA2 (<*) f a)
+instance ( forall sem. syn sem => Monad sem
+         , forall err. syn (Either err)
+         , syn (Parser syn) -- FIXME: what constraint is still missing to still require that?
+         ) => Monad (Parser syn) where
+  (>>=) (Parser efsa) f = Parser (efsa >>= \(ForallSem sa) -> sa >>= unParser . f)
+-}
diff --git a/src/Symantic/Parser/Error.hs b/src/Symantic/Parser/Error.hs
new file mode 100644
index 0000000..ed697bc
--- /dev/null
+++ b/src/Symantic/Parser/Error.hs
@@ -0,0 +1,23 @@
+{-# LANGUAGE TypeApplications #-}
+
+module Symantic.Parser.Error where
+
+import Data.Either (Either (..))
+import Data.Function (($), (.))
+import Data.Proxy (Proxy)
+
+-- * Class 'ErrorInj'
+class ErrorInj a b where
+  errorInj :: a -> b
+instance ErrorInj err e => ErrorInj err (Either e a) where
+  errorInj = Left . errorInj
+
+liftError ::
+  forall e0 err e1 a.
+  ErrorInj e0 e1 =>
+  ErrorInj e1 err =>
+  Proxy e1 ->
+  Either e0 a ->
+  Either err a
+liftError _e1 (Right a) = Right a
+liftError _e1 (Left e) = Left $ errorInj @e1 @err $ errorInj @e0 @e1 e
diff --git a/src/Symantic/Parser/Source.hs b/src/Symantic/Parser/Source.hs
new file mode 100644
index 0000000..a2c5e72
--- /dev/null
+++ b/src/Symantic/Parser/Source.hs
@@ -0,0 +1,89 @@
+{-# LANGUAGE ConstraintKinds #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE UndecidableInstances #-}
+-- {-# LANGUAGE PolyKinds #-}
+{-# OPTIONS_GHC -Wno-orphans #-}
+
+module Symantic.Parser.Source where
+
+import Control.Applicative (Applicative (..))
+import Control.Monad (Monad (..))
+import Control.Monad.Classes qualified as MC
+import Control.Monad.Trans.Writer.CPS qualified as MT
+import Data.Bool (Bool (..))
+import Data.Eq (Eq)
+import Data.Function ((.))
+import Data.Functor (Functor)
+import Data.Functor.Classes (Show1 (..), liftShowList2, liftShowsPrec2, showsPrec1, showsUnaryWith)
+import Data.Kind (Type)
+import Data.Monoid (Monoid (..))
+import Data.Ord (Ord)
+import Data.Semigroup (Semigroup (..))
+import Data.Tuple (fst)
+import Data.Typeable (Typeable)
+import Text.Show (Show (..))
+
+-- * Class 'Source'
+class Monoid src => Source src
+instance Source ()
+
+-- ** Class 'SourceInj'
+class Source src => SourceInj a src where
+  sourceInj :: a -> src
+instance SourceInj a () where
+  sourceInj _ = ()
+
+-- ** Type family 'SourceOf'
+type family SourceOf a
+
+-- ** Type 'Sourceable'
+class Source (SourceOf a) => Sourceable a where
+  sourceOf :: a -> SourceOf a
+  setSource :: a -> SourceOf a -> a
+infixl 5 `setSource`
+
+withSource :: SourceInj src (SourceOf a) => Sourceable a => a -> src -> a
+withSource a src = a `setSource` sourceInj src
+
+-- ** Type 'Source_Input'
+type family Source_Input (src :: Type) :: Type
+type instance Source_Input () = ()
+
+-- ** Type 'Span'
+data Span src = Span
+  { spanBegin :: !src
+  , spanEnd :: !src
+  }
+  deriving (Eq, Ord, Show, Typeable)
+
+type Sourced src a = MT.Writer src a
+unSourced :: Monoid src => Sourced src a -> a
+unSourced = fst . MT.runWriter
+
+instance (Show w, Monoid w, Show1 m, Show a) => Show (MT.WriterT w m a) where
+  showsPrec = showsPrec1
+
+instance (Show w, Monoid w, Show1 m) => Show1 (MT.WriterT w m) where
+  liftShowsPrec sp sl d m =
+    showsUnaryWith (liftShowsPrec sp' sl') "WriterT" d (MT.runWriterT m)
+    where
+      sp' = liftShowsPrec2 sp sl showsPrec showList
+      sl' = liftShowList2 sp sl showsPrec showList
+
+appendSource :: MC.MonadWriter src m => m a -> src -> m a
+appendSource m src = do
+  a <- m
+  MC.tell src
+  return a
+
+-- class MC.MonadWriter w m => Provenanceable w (m::Type -> Type)
+-- instance MC.MonadWriter w m => Provenanceable w m
+-- type Provenanceable w m = MC.MonadWriter w m
+
+type instance MC.CanDo (MT.WriterT w m) eff = WriterCanDo w eff
+type family WriterCanDo w eff where
+  WriterCanDo w (MC.EffWriter w) = 'True
+  WriterCanDo w eff = 'False
+
+class Provenanceable prov sem where
+  provenance :: prov -> sem prov
diff --git a/src/Symantic/Printer.hs b/src/Symantic/Printer.hs
new file mode 100644
index 0000000..484d9ea
--- /dev/null
+++ b/src/Symantic/Printer.hs
@@ -0,0 +1,34 @@
+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.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
+
+newtype Printer a = Printer {unPrinter :: TermAST}
+print :: Printer a -> TermAST
+print = unPrinter
+print2 :: String -> Printer a1 -> Printer a2 -> Printer a3
+print2 n (Printer aT) (Printer bT) = Printer $ BinTree2 (BinTree2 (BinTree0 (TokenTermAtom n)) aT) bT
diff --git a/src/Symantic/Syntaxes.hs b/src/Symantic/Syntaxes.hs
new file mode 100644
index 0000000..c2f987f
--- /dev/null
+++ b/src/Symantic/Syntaxes.hs
@@ -0,0 +1,226 @@
+{-# LANGUAGE ConstraintKinds #-}
+{-# LANGUAGE QuantifiedConstraints #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE UndecidableInstances #-}
+
+module Symantic.Syntaxes 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.String (String)
+import GHC.Types
+import Text.Read (Read (..), reads)
+import Text.Show (Show (..))
+import Type.Reflection (TypeRep, Typeable, eqTypeRep, typeRep, (:~~:) (..))
+import Unsafe.Coerce (unsafeCoerce)
+import Prelude (error)
+import Prelude qualified
+
+import Symantic
+import Symantic.Typer
+
+class Addable sem where
+  lit :: Int -> sem Int
+  neg :: sem Int -> sem Int
+  add :: sem Int -> sem Int -> sem Int
+class Mulable sem where
+  mul :: sem Int -> sem Int -> sem Int
+class Abstractable sem where
+  -- | Lambda term abstraction, in HOAS (Higher-Order Abstract Syntax) style.
+  lam :: Typeable a => (sem a -> sem b) -> sem (a -> b)
+
+  -- | Application, aka. unabstract.
+  (.@) :: sem (a -> b) -> sem a -> sem b
+
+instance (forall sem. syn sem => Addable sem) => Addable (ForallSem syn) where
+  lit n = ForallSem (lit n)
+  neg (ForallSem a) = ForallSem (neg a)
+  add (ForallSem a) (ForallSem b) = ForallSem (add a b)
+instance (forall sem. syn sem => Mulable sem) => Mulable (ForallSem syn) where
+  mul (ForallSem a) (ForallSem b) = ForallSem (mul a b)
+instance
+  ( forall sem. syn sem => Abstractable sem
+  -- , forall sem. syn sem => Typeable sem -- user instance not accepted
+  -- , forall s1 s2. (syn s1, syn s2) => s1 ~ s2 -- crazy...
+  ) =>
+  Abstractable (ForallSem syn)
+  where
+  ForallSem a2b .@ ForallSem a = ForallSem (a2b .@ a)
+  lam f = ForallSem (lam (\a -> let ForallSem b = f (forallSem a) in b))
+    where
+      -- Safe here because a :: sem a and b :: sem b share the same 'sem'.
+      forallSem :: sem a -> ForallSem syn a
+      forallSem a = ForallSem (unsafeCoerce a)
+
+--
+-- Parsing
+--
+
+parseAddable ::
+  ( forall sem. syn sem => Addable sem
+  , syn (ForallSem syn)
+  ) =>
+  (TermAST -> Parser syn) ->
+  TermAST ->
+  Parser syn
+parseAddable _final (BinTree0 (TokenTermAtom s))
+  | Right (i :: Int) <- safeRead s =
+      Parser $ Right $ TermVT TyConst{tyConst = Const{constType = typeRep, constMeta = ()}, tyConstLen = LenZ} $ ForallSem @_ @Int $ lit i
+parseAddable final (BinTree2 (BinTree0 (TokenTermAtom "Neg")) aT) = Parser $
+  case final aT of
+    Parser aE -> do
+      TermVT aTy (ForallSem a :: ForallSem syn a) <- aE
+      case eqTy aTy TyConst{tyConst = Const{constType = typeRep @Int, constMeta = ()}, tyConstLen = lenVar aTy} of
+        Nothing -> Left "TypeError"
+        Just HRefl -> do
+          Right $ TermVT aTy $ neg a
+parseAddable final (BinTree2 (BinTree2 (BinTree0 (TokenTermAtom "Add")) aT) bT) =
+  Parser $ do
+    TermVT aTy (ForallSem a :: ForallSem syn a) <- unParser (final aT)
+    case eqTy aTy TyConst{tyConst = Const{constType = typeRep @Int, constMeta = ()}, tyConstLen = lenVar aTy} of
+      Nothing -> Left "TypeError"
+      Just HRefl -> do
+        TermVT bTy (ForallSem b :: ForallSem syn b) <- unParser (final bT)
+        case eqTy bTy TyConst{tyConst = Const{constType = typeRep @Int, constMeta = ()}, tyConstLen = lenVar bTy} of
+          Nothing -> Left "TypeError"
+          Just HRefl -> do
+            Right $ TermVT aTy $ ForallSem @_ @Int $ add a b
+parseAddable _final e = Parser $ Left $ "Invalid tree: " <> show e
+
+-- tree0Parser :: (forall sem. syn sem => Addable sem, syn (ForallSem syn)) => Either ErrMsg (ForallSem syn Int)
+-- tree0Parser = unParser $ parse tree0Print
+
+parseMulable ::
+  ( forall sem. syn sem => Mulable sem
+  , forall sem. syn sem => Addable sem
+  , syn (ForallSem syn)
+  ) =>
+  (TermAST -> Parser syn) ->
+  TermAST ->
+  Parser syn
+parseMulable final (BinTree2 (BinTree2 (BinTree0 (TokenTermAtom "Mul")) aT) bT) =
+  Parser $ do
+    case (final aT, final bT) of
+      (Parser aE, Parser bE) -> do
+        TermVT aTy (ForallSem a :: ForallSem syn a) <- aE
+        case eqTy aTy TyConst{tyConst = Const{constType = typeRep @Int, constMeta = ()}, tyConstLen = lenVar aTy} of
+          Nothing -> Left "TypeError"
+          Just HRefl -> do
+            TermVT bTy (ForallSem b :: ForallSem syn b) <- bE
+            case eqTy bTy TyConst{tyConst = Const{constType = typeRep @Int, constMeta = ()}, tyConstLen = lenVar bTy} of
+              Nothing -> Left "TypeError"
+              Just HRefl -> do
+                Right $ TermVT aTy (ForallSem @_ @a $ mul a b)
+parseMulable final t = parseAddable final t
+
+parseAbstractable ::
+  ( forall sem. syn sem => Mulable sem
+  , forall sem. syn sem => Addable sem
+  , forall sem. syn sem => Abstractable sem
+  , syn (ForallSem syn)
+  ) =>
+  a ~ Int =>
+  (TermAST -> Parser syn) ->
+  TermAST ->
+  Parser syn
+-- TODO: parse variables
+parseAbstractable final (BinTree0 (TokenTermAbst n (TyVT (aTy :: Ty meta vs a)) bT)) =
+  Parser $
+    case final bT of
+      Parser bE -> do
+        TermVT abTy (abF :: ForallSem syn ab) <- bE
+        case eqTy TyConst{tyConst = Const{constType = typeRep @Type, constMeta = ()}, tyConstLen = lenVar aTy} aTy of
+          Nothing -> Left "TypeError"
+          Just HRefl -> do
+            case abTy of
+              FUN iTy bTy ->
+                case eqTy TyConst{tyConst = Const{constType = typeRep @Type, constMeta = ()}, tyConstLen = lenVar bTy} bTy of
+                  Nothing -> Left "TypeError"
+                  Just HRefl -> do
+                    let (aTy', iTy') = appendVars aTy iTy
+                    case eqTy aTy' iTy' of
+                      Nothing -> Left "TypeError"
+                      Just HRefl -> do
+                        case abF of
+                          ForallSem ab ->
+                            Right $
+                              TermVT abTy $
+                                ForallSem @_ @ab $
+                                  -- FIXME: Tyable
+                                  lam (ab .@)
+              _ -> Left "TypeError"
+parseAbstractable final t = parseMulable final t
+
+--
+-- Printing
+--
+
+instance Addable Printer where
+  lit n = Printer $ BinTree0 (TokenTermAtom (show n))
+  neg (Printer aT) = Printer $ BinTree2 (BinTree0 (TokenTermAtom "Neg")) aT
+  add = print2 "Add"
+instance Mulable Printer where
+  mul = print2 "Mul"
+instance Abstractable Printer where
+  Printer f .@ Printer a = Printer $ BinTree2 f a
+  lam (f :: Printer a -> Printer b) =
+    Printer $
+      -- FIXME: Tyable? instead of Typeable?
+      BinTree0
+        ( TokenTermAbst
+            "x"
+            (TyVT TyConst{tyConst = Const{constType = typeRep @a, constMeta = ()}, tyConstLen = LenZ})
+            (unPrinter (f (Printer (BinTree0 (TokenTermAtom "x")))))
+        )
+
+class (Addable sem, Mulable sem, Abstractable sem) => FinalSyntaxes sem
+instance (Addable sem, Mulable sem, Abstractable sem) => FinalSyntaxes sem
+
+fix :: (a -> a) -> a
+fix f = f (fix f)
+
+parse ::
+  ( forall sem. syn sem => Addable sem
+  , forall sem. syn sem => Mulable sem
+  , forall sem. syn sem => Abstractable sem
+  , syn (ForallSem syn)
+  ) =>
+  TermAST ->
+  Parser syn
+parse = fix parseAbstractable
+
+tree0 = add (lit 8) (neg (add (lit 1) (lit 2)))
+tree1 = mul (add (lit 8) (neg (add (lit 1) (lit 2)))) (lit 2)
+tree2 = lam (\(x :: sem Int) -> mul (lit 0) (add (lit 1) (lit 2)))
+tree0Print = print tree0
+tree1Print = print tree1
+tree2Print = print tree2
+
+tree0ParsePrint :: TermAST
+tree0ParsePrint = case parse @FinalSyntaxes tree0Print of
+  Parser (Left e) -> error e
+  Parser (Right (TermVT _ty (ForallSem sem))) -> print sem
+
+tree1ParsePrint :: TermAST
+tree1ParsePrint = case parse @FinalSyntaxes tree1Print of
+  Parser (Left e) -> error e
+  Parser (Right (TermVT _ty (ForallSem sem))) -> print sem
+
+tree2ParsePrint :: TermAST
+tree2ParsePrint = case parse @FinalSyntaxes tree2Print of
+  Parser (Left e) -> error e
+  Parser (Right (TermVT _ty (ForallSem sem))) -> print sem
diff --git a/src/Symantic/Typer.hs b/src/Symantic/Typer.hs
new file mode 100644
index 0000000..1a2a16d
--- /dev/null
+++ b/src/Symantic/Typer.hs
@@ -0,0 +1,11 @@
+module Symantic.Typer (
+  module Symantic.Typer.Type,
+  module Symantic.Typer.List,
+  module Symantic.Typer.Unify,
+  module Symantic.Typer.Eq,
+) where
+
+import Symantic.Typer.Eq
+import Symantic.Typer.List
+import Symantic.Typer.Type
+import Symantic.Typer.Unify
diff --git a/src/Symantic/Typer/Eq.hs b/src/Symantic/Typer/Eq.hs
new file mode 100644
index 0000000..b2cc9ba
--- /dev/null
+++ b/src/Symantic/Typer/Eq.hs
@@ -0,0 +1,14 @@
+{-# LANGUAGE AllowAmbiguousTypes #-}
+{-# LANGUAGE PolyKinds #-}
+
+module Symantic.Typer.Eq where
+
+import Data.Kind (Type)
+import Data.Maybe (Maybe (..))
+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)
diff --git a/src/Symantic/Typer/List.hs b/src/Symantic/Typer/List.hs
new file mode 100644
index 0000000..9ac5b7c
--- /dev/null
+++ b/src/Symantic/Typer/List.hs
@@ -0,0 +1,47 @@
+{-# LANGUAGE AllowAmbiguousTypes #-}
+{-# LANGUAGE PolyKinds #-}
+
+module Symantic.Typer.List where
+
+import Data.Function (($), (.))
+import Data.Int (Int)
+import Text.Show (Show (..))
+import Prelude qualified
+
+-- * Type family @(++)@
+type family (++) xs ys where
+  '[] ++ ys = ys
+  -- xs  ++ '[] = xs
+  (x ': xs) ++ ys = x ': xs ++ ys
+infixr 5 ++
+
+-- * Type 'Len'
+data Len (xs :: [k]) where
+  LenZ :: Len '[]
+  LenS :: Len xs -> Len (x ': xs)
+
+instance Show (Len vs) where
+  showsPrec _p = showsPrec 10 . intLen
+
+addLen :: Len a -> Len b -> Len (a ++ b)
+addLen LenZ b = b
+addLen (LenS a) b = LenS $ addLen a b
+
+shiftLen :: forall t b a. Len a -> Len (a ++ b) -> Len (a ++ t ': b)
+shiftLen LenZ b = LenS b
+shiftLen (LenS a) (LenS b) = LenS $ shiftLen @t @b a b
+
+intLen :: Len xs -> Int
+intLen = go 0
+  where
+    go :: Int -> Len xs -> Int
+    go i LenZ = i
+    go i (LenS l) = go (1 Prelude.+ i) l
+
+-- ** Class 'LenInj'
+class LenInj (vs :: [k]) where
+  lenInj :: Len vs
+instance LenInj '[] where
+  lenInj = LenZ
+instance LenInj as => LenInj (a ': as) where
+  lenInj = LenS lenInj
diff --git a/src/Symantic/Typer/Type.hs b/src/Symantic/Typer/Type.hs
new file mode 100644
index 0000000..68e2754
--- /dev/null
+++ b/src/Symantic/Typer/Type.hs
@@ -0,0 +1,467 @@
+{-# LANGUAGE ConstraintKinds #-}
+{-# LANGUAGE PatternSynonyms #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE StandaloneDeriving #-}
+{-# LANGUAGE UndecidableSuperClasses #-}
+{-# LANGUAGE ViewPatterns #-}
+{-# OPTIONS_GHC -Wno-partial-fields #-}
+
+module Symantic.Typer.Type where
+
+import Control.Applicative (Applicative (..), liftA3)
+import Control.Monad (Monad (..), sequence)
+import Control.Monad.Classes as MC ()
+import Control.Monad.Classes.Run as MC ()
+import Control.Monad.Trans.Except qualified as MT
+import Control.Monad.Trans.Identity (IdentityT (..))
+import Control.Monad.Trans.Reader qualified as MT
+import Control.Monad.Trans.State qualified as MT
+import Control.Monad.Trans.Writer.CPS qualified as MT
+import Data.Bool (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.Map.Strict qualified as Map
+import Data.Maybe (Maybe (..), isJust)
+import Data.Monoid (Monoid (..))
+import Data.Proxy (Proxy (..))
+import Data.Semigroup (Semigroup (..))
+import Data.Set qualified as Set
+import Data.String (String)
+import GHC.Types
+import Text.Read (Read (..), reads)
+import Text.Show (Show (..))
+import Type.Reflection (TypeRep, Typeable, eqTypeRep, typeRep, typeRepKind, (:~~:) (..))
+import Unsafe.Coerce (unsafeCoerce)
+import Prelude (error)
+import Prelude qualified
+
+import Symantic.Parser.Source
+import Symantic.Typer.Eq
+import Symantic.Typer.List
+
+data Const meta a = Const
+  { constType :: TypeRep a
+  , constMeta :: meta
+  }
+  deriving (Show)
+instance EqTy (Const meta) (Const meta) where
+  eqTy Const{constType = x} Const{constType = y} = eqTypeRep x y
+
+type Name = String
+
+-- * Type 'Var'
+data Var :: forall vK. Type -> [Type] -> vK -> Type where
+  VarZ ::
+    { varZKind :: Kind meta vK
+    , varZNext :: Len ws
+    , varZMeta :: meta
+    } ->
+    Var meta (Proxy (v :: vK) ': ws) (v :: vK)
+  VarS :: Var meta vs v -> Var meta (not_v ': vs) v
+deriving instance Show meta => Show (Var meta vs v)
+
+pattern Var :: () => () => Kind meta vK -> Len ws -> meta -> Var meta vs' (v :: vK)
+pattern Var{varKind, varNext, varMeta} <- (var -> VarVS VarZ{varZKind = varKind, varZNext = varNext, varZMeta = varMeta})
+{-# COMPLETE Var #-}
+
+-- -- * Type 'VarVS'
+data VarVS meta (v :: vK) = forall vs. VarVS (Var meta vs v)
+var :: Var meta vs (v :: vK) -> VarVS meta (v :: vK)
+var v@VarZ{} = VarVS v
+var (VarS v) = var v
+
+instance EqTy (Var meta vs) (Var meta vs) where
+  eqTy VarZ{} VarZ{} = Just HRefl
+  eqTy (VarS x) (VarS y) = eqTy x y
+  eqTy _ _ = Nothing
+
+type VarSem = Type -> [Type] -> Type -> Type
+
+-- data VarV (var::VarSem) vs = forall vK (v::vK). VarVSem (var vs v)
+data VarV meta vs = forall v. VarV (Var meta vs v)
+
+class LenVar var where
+  lenVar :: var meta vs a -> Len vs
+instance LenVar Var where
+  lenVar VarZ{varZNext} = LenS varZNext
+  lenVar (VarS v) = LenS (lenVar v)
+
+class LenVar var => AllocVars var where
+  allocVarsL :: Len len -> var meta vs x -> var meta (len ++ vs) x
+  allocVarsR :: Len len -> var meta vs x -> var meta (vs ++ len) x
+instance AllocVars Var where
+  allocVarsL LenZ v = v
+  allocVarsL (LenS len) v = VarS (allocVarsL len v)
+
+  allocVarsR len VarZ{..} = VarZ{varZNext = addLen varZNext len, ..}
+  allocVarsR len (VarS v) = VarS (allocVarsR len v)
+
+appendVars ::
+  AllocVars xVar =>
+  AllocVars yVar =>
+  xVar meta xVS (x :: xK) ->
+  yVar meta yVS (y :: yK) ->
+  ( xVar meta (xVS ++ yVS) x
+  , yVar meta (xVS ++ yVS) y
+  )
+appendVars x y =
+  ( allocVarsR (lenVar y) x
+  , allocVarsL (lenVar x) y
+  )
+
+-- ** Type 'IndexVar'
+
+-- | Index of a 'Var'.
+type IndexVar = Int
+
+indexVar :: Var meta vs v -> Int
+indexVar VarZ{} = 0
+indexVar (VarS v) = 1 Prelude.+ indexVar v
+
+-- instance KindOf (Var meta vs) where
+--   kindOf = fmap go
+--     where
+--     go :: forall vs2 aK a. Var meta vs2 (Proxy (a::aK)) -> TypeRep aK
+--     go VarZ{varKind} = varKind
+--     go (VarS v) = go v
+
+-- * Type 'Vars'
+type Vars meta vs = Map.Map Name (VarV meta vs)
+
+lookupVar :: Name -> Vars meta vs -> Maybe (VarV meta vs)
+lookupVar = Map.lookup
+
+insertVar :: Name -> VarV meta vs -> Vars meta vs -> Vars meta vs
+insertVar = Map.insert
+
+-- * Type 'UsedVars'
+
+-- | List of 'Var's, used to change the context of a 'Var'
+-- when removing unused 'Var's.
+data UsedVars oldVS meta newVS a where
+  UsedVarsZ :: UsedVars oldVS meta '[] a
+  UsedVarsS ::
+    Var meta oldVS (v :: vK) ->
+    UsedVars oldVS meta newVS a ->
+    UsedVars oldVS meta (Proxy (v :: vK) ': newVS) a
+
+instance LenVar (UsedVars oldVS) where
+  lenVar UsedVarsZ = LenZ
+  lenVar (UsedVarsS _v oldVS) = LenS $ lenVar oldVS
+
+lookupUsedVars ::
+  Var meta oldVS (v :: vK) ->
+  UsedVars oldVS meta newVS a ->
+  Maybe (Var meta newVS (v :: vK))
+lookupUsedVars _v UsedVarsZ = Nothing
+lookupUsedVars v (UsedVarsS v' us) = do
+  case v `eqTy` v' of
+    Just HRefl ->
+      case v' of
+        Var{varKind, varMeta} ->
+          Just
+            VarZ
+              { varZNext = lenVar us
+              , varZKind = varKind
+              , varZMeta = varMeta
+              }
+    Nothing -> VarS Data.Functor.<$> lookupUsedVars v us
+
+insertUsedVars ::
+  Var meta vs v ->
+  UsedVars vs meta us a ->
+  Maybe (UsedVars vs meta (Proxy v ': us) a)
+insertUsedVars v vs =
+  case lookupUsedVars v vs of
+    Just{} -> Nothing
+    Nothing -> Just (UsedVarsS v vs)
+
+-- * Class 'VarOccursIn'
+
+-- | Test whether a given 'Var' occurs within @(t)@.
+class VarOccursIn (t :: Type -> [Type] -> aK -> Type) where
+  varOccursIn :: Var meta vs v -> t meta vs a -> Bool
+
+-- * Class 'UsedVarsOf'
+class UsedVarsOf t where
+  usedVarsOf ::
+    UsedVars vs meta oldVS a ->
+    t meta vs b ->
+    (forall newVS. UsedVars vs meta newVS a -> ret) ->
+    ret
+
+-- * Type 'Ty'
+
+-- Use a CUSK, because it's a polymorphically recursive type,
+-- See https://ryanglscott.github.io/2020/01/05/five-benefits-to-using-standalonekindsignatures/
+data Ty :: forall aK. Type -> [Type] -> aK -> Type where
+  TyConst :: {tyConst :: Const meta a, tyConstLen :: Len vs} -> Ty meta vs a
+  TyVar :: {tyVar :: Var meta vs a, tyVarName :: Name} -> Ty meta vs a
+  TyApp :: {tyAppFun :: Ty meta vs f, tyAppArg :: Ty meta vs a} -> Ty meta vs (f a)
+infixl 9 `TyApp`
+
+pattern FUN ::
+  -- CReq
+  forall k (fun :: k) meta vs.
+  () =>
+  {-Monoid meta-}
+  -- CProv
+  forall
+    (r1 :: RuntimeRep)
+    (r2 :: RuntimeRep)
+    (arg :: TYPE r1)
+    (res :: TYPE r2).
+  ( k ~ Type
+  , fun ~~ (arg -> res)
+  -- , r1 ~ LiftedRep
+  -- , r2 ~ LiftedRep {- fixme: remove those 2 constraints -}
+  ) =>
+  Ty meta vs arg ->
+  Ty meta vs res ->
+  Ty meta vs fun
+pattern FUN arg res <-
+  TyApp
+    { tyAppFun =
+      TyApp
+        { tyAppFun = TyConst{tyConst = Const{constType = eqTypeRep (typeRep @(->)) -> Just HRefl}}
+        , tyAppArg = arg
+        }
+    , tyAppArg = res
+    }
+
+-- where FUN arg res =
+--        TyApp
+--          { tyAppFun = TyApp
+--              { tyAppFun = TyConst
+--                             { tyConstLen=lenVar arg
+--                             , tyConst=Const{ constType=typeRep @(->)
+--                                            , constMeta=(mempty::meta)}
+--                             }
+--              , tyAppArg = arg
+--              }
+--          , tyAppArg = res
+--          }
+
+deriving instance Show meta => Show (Ty meta vs a)
+
+-- type instance SourceOf (Ty vs src t) = src
+instance LenVar Ty where
+  lenVar TyConst{tyConstLen} = tyConstLen
+  lenVar TyApp{tyAppFun} = lenVar tyAppFun
+  lenVar TyVar{tyVar} = lenVar tyVar
+
+-- lenVars (TyFam l _f _as) = l
+instance AllocVars Ty where
+  allocVarsL len ty@TyConst{..} = ty{tyConstLen = addLen len tyConstLen}
+  allocVarsL len TyApp{..} = TyApp{tyAppFun = allocVarsL len tyAppFun, tyAppArg = allocVarsL len tyAppArg}
+  allocVarsL len ty@TyVar{..} = ty{tyVar = allocVarsL len tyVar}
+
+  -- allocVarsL len (TyFam l f as) = TyFam (addLen len l) f $ allocVarsL len `mapTys` as
+
+  allocVarsR len ty@TyConst{..} = ty{tyConstLen = addLen tyConstLen len}
+  allocVarsR len TyApp{..} = TyApp{tyAppFun = allocVarsR len tyAppFun, tyAppArg = allocVarsR len tyAppArg, ..}
+  allocVarsR len ty@TyVar{..} = ty{tyVar = allocVarsR len tyVar}
+
+-- allocVarsR len (TyFam l f as) = TyFam (addLen l len) f $ allocVarsR len `mapTys` as
+instance VarOccursIn Ty where
+  varOccursIn v TyVar{tyVar = v'} | Just{} <- v `eqTy` v' = False
+  varOccursIn _v TyVar{} = False
+  varOccursIn _v TyConst{} = False
+  varOccursIn v TyApp{tyAppFun = f, tyAppArg = a} = varOccursIn v f Prelude.|| varOccursIn v a
+
+-- varOccursIn v (TyFam _src _len _fam as) = varOccursIn v as
+instance UsedVarsOf Ty where
+  usedVarsOf vs TyConst{} k = k vs
+  usedVarsOf vs TyApp{tyAppFun = f, tyAppArg = a} k =
+    usedVarsOf vs f $ \vs' ->
+      usedVarsOf vs' a k
+  usedVarsOf vs TyVar{tyVar = v} k =
+    case insertUsedVars v vs of
+      Nothing -> k vs
+      Just vs' -> k vs'
+
+-- usedVarsOf vs (TyFam _src _len _fam as) k = usedVarsOf vs as k
+
+-- ** Type 'TyT'
+
+-- | Existential for 'Type'.
+data TyT meta vs = forall a. TyT (Ty meta vs a)
+
+-- type instance SourceOf (TyT vs src) = src
+instance Eq (TyT meta vs) where
+  TyT x == TyT y = isJust $ eqTy x y
+instance Show meta => Show (TyT meta vs) where
+  showsPrec p (TyT x) = showsPrec p x
+
+-- * Type 'Kind'
+type Kind meta a = Ty meta '[] a
+
+-- ** Type 'KindK'
+type KindK meta = TyT meta '[]
+
+-- ** Type 'TyVT'
+data TyVT meta = forall vs a. TyVT (Ty meta vs a)
+
+deriving instance Show meta => Show (TyVT meta)
+instance Eq (TyVT m) where
+  TyVT x == TyVT y = isJust (eqTy x' y')
+    where
+      (x', y') = appendVars x y
+
+-- 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 (TyFam _ _lx xF xA) (TyFam _ _ly yF yA)
+--  | Just HRefl <- eqTypeRep xF yF
+--  , Just HRefl <- eqTys xA yA
+--  = Just HRefl
+-- -- NOTE: 'TyFam' is expanded as much as possible.
+-- eqTy x@TyFam{} y = eqTy (expandFam x) y
+-- eqTy x y@TyFam{} = eqTy x (expandFam y)
+
+-- * Type 'Tys'
+data Tys (as :: [Type]) meta vs (a :: aK) where
+  TysZ :: Tys '[] meta vs a
+  TysS :: Ty meta vs a -> Tys as meta vs b -> Tys (Proxy a ': as) meta vs b
+infixr 5 `TysS`
+
+-- type instance SourceOf (Tys vs src ts) = src
+-- instance ConstsOf (Tys meta vs ts) where
+--  constsOf TysZ = Set.empty
+--  constsOf (TysS t ts) = constsOf t `Set.union` constsOf ts
+instance UsedVarsOf (Tys as) where
+  usedVarsOf vs TysZ k = k vs
+  usedVarsOf vs (TysS t ts) k =
+    usedVarsOf vs t $ \vs' ->
+      usedVarsOf vs' ts k
+instance VarOccursIn (Tys as) where
+  varOccursIn _v TysZ = False
+  varOccursIn v (TysS t ts) = varOccursIn v t Prelude.|| varOccursIn v ts
+
+-- ** Type family 'FunArg'
+type family FunArg (fun :: Type) :: Type where
+  FunArg (q #> f) = FunArg f
+  FunArg (a -> b) = a
+
+-- ** Type family 'FunRes'
+type family FunRes (fun :: Type) :: Type where
+  FunRes (q #> f) = FunRes f
+  FunRes (a -> b) = b
+
+-- -- | Return, when the given 'Type' is a function,
+-- -- the argument of that function.
+-- unTyFun ::
+--  forall t src tys.
+--  SourceInj (TyVT src) src =>
+--  --Constable (->) =>
+--  Type src tys t ->
+--  Maybe ( Type src tys (FunArg t)
+--        , Type src tys (FunRes t) )
+-- unTyFun ty_ini = go ty_ini
+--   where
+--   go ::
+--    Type src tys x ->
+--    Maybe ( Type src tys (FunArg x)
+--          , Type src tys (FunRes x) )
+--   go (TyApp _ (TyApp _ (TyConst _ _ f) a) b)
+--    | Just HRefl <- proj_ConstKi @(K (->)) @(->) f
+--    = Just ((a `withSource` TyVT ty_ini), (b `withSource` TyVT ty_ini))
+--   go (TyApp _ (TyApp _ (TyConst _ _ f) _a) b)
+--    | Just HRefl <- proj_ConstKi @(K (#>)) @(#>) f
+--    = go b
+--   go TyApp{}   = Nothing
+--   go TyConst{} = Nothing
+--   go TyVar{}   = Nothing
+--   go TyFam{}   = Nothing
+
+proj_ConstKi ::
+  forall kc (c :: kc) u meta.
+  Typeable c =>
+  -- (kc ~ Type_of_Ty (Ty_of_Type kc)) =>
+  -- KindInjP (Ty_of_Type kc) =>
+  Const meta u ->
+  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'.
+newtype (#>) (q :: Constraint) (a :: Type) = Qual (q => a)
+
+-- | Qualify a 'Type'.
+(#>) :: Monoid meta => Ty meta vs q -> Ty meta vs t -> Ty meta vs (q #> t)
+(#>) q t =
+  -- (tyConstLen @(K (#>)) @(#>) (lenVars q) `tyApp` q) `tyApp` t
+  TyApp
+    { tyAppFun =
+        TyApp
+          { tyAppFun = TyConst{tyConst = Const{constType = typeRep @(#>), constMeta = mempty}, tyConstLen = lenVar q}
+          , tyAppArg = q
+          }
+    , tyAppArg = t
+    }
+
+infixr 0 #>
+
+-- NOTE: should actually be (-1)
+-- to compose well with @infixr 0 (->)@
+-- but this is not allowed by GHC.
+
+-- ** Class @(#)@
+
+-- | 'Constraint' union.
+class ((x, y) :: Constraint) => x # y
+
+instance ((x, y) :: Constraint) => x # y
+
+-- | Unify two 'K.Constraint's.
+(#) :: Monoid meta => Ty meta vs qx -> Ty meta vs qy -> Ty meta vs (qx # qy)
+(#) a b =
+  -- (tyConstLen @(K (#)) @(#) (lenVars a) `tyApp` a) `tyApp` b
+  TyApp
+    { tyAppFun =
+        TyApp
+          { tyAppFun = TyConst{tyConst = Const{constType = typeRep @(#), constMeta = mempty}, tyConstLen = lenVar a}
+          , tyAppArg = a
+          }
+    , tyAppArg = b
+    }
+
+infixr 2 #
+
+-- * Class 'KindOf'
+class KindOf (ty :: Type -> [Type] -> aK -> Type) where
+  -- | Return the kind of the given 'Var'.
+  kindOf ::
+    -- Provenanceable (ProvenanceKindOf t) m =>
+    -- MC.MonadWriter (ProvenanceKindOf t) m =>
+    ty meta vs (a :: aK) ->
+    Kind meta aK
+
+instance KindOf Var where
+  kindOf Var{varKind} = varKind
+instance KindOf Ty where
+  kindOf TyConst{tyConst = c} = TyConst{tyConst = c{constType = typeRepKind (constType c)}, tyConstLen = LenZ}
+  kindOf TyApp{tyAppFun = f} = case kindOf f of
+    FUN _ kf -> kf
+  kindOf TyVar{tyVar = Var{varKind, varMeta}} = varKind
+
+-- kindOf (TyFam _src _len fam _as) = kindOfConst fam
diff --git a/src/Symantic/Typer/Unify.hs b/src/Symantic/Typer/Unify.hs
new file mode 100644
index 0000000..0cf58c9
--- /dev/null
+++ b/src/Symantic/Typer/Unify.hs
@@ -0,0 +1,269 @@
+{-# LANGUAGE ExistentialQuantification #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE StandaloneDeriving #-}
+{-# LANGUAGE UndecidableInstances #-}
+{-# OPTIONS_GHC -fno-warn-orphans #-}
+
+module Symantic.Typer.Unify where
+
+import Control.Monad (Monad (..))
+import Control.Monad.Classes as MC (MonadExcept, throw)
+import Control.Monad.Classes.Run as MC ()
+import Data.Bool (otherwise)
+import Data.Eq (Eq (..))
+import Data.Function (id, ($))
+import Data.Functor ((<$>))
+import Data.Map.Strict (Map)
+import Data.Map.Strict qualified as Map
+import Data.Maybe (Maybe (..))
+import Data.Monoid (Monoid (..))
+import Data.Semigroup (Semigroup (..))
+import Text.Show (Show)
+import Type.Reflection ((:~~:) (..))
+import Unsafe.Coerce (unsafeCoerce)
+import Prelude qualified
+
+-- import Symantic.Grammar
+import Symantic.Typer.Variable ()
+
+-- import Symantic.Typer.Kind
+
+import Symantic.Parser.Error (ErrorInj (..))
+import Symantic.Parser.Source (Source, SourceInj)
+import Symantic.Typer.Eq (EqTy (eqTy))
+import Symantic.Typer.Type (
+  IndexVar,
+  KindK,
+  KindOf (kindOf),
+  Ty (TyApp, TyConst, TyVar, tyConst, tyVar),
+  TyT (..),
+  TyVT (..),
+  Tys (..),
+  Var,
+  VarOccursIn (..),
+  indexVar,
+  proj_ConstKi,
+  type (#>),
+ )
+
+-- import Symantic.Typer.Show ()
+
+-- * Type 'Subst'
+
+-- | /Type variable substitution/.
+--
+-- WARNING: a 'Subst' MUST be without loops, and fully expanded.
+newtype Subst meta vs
+  = Subst (Map IndexVar (VT meta vs))
+
+deriving instance (Show meta, Monoid meta) => Show (Subst meta vs)
+instance Monoid meta => Semigroup (Subst meta vs) where
+  (<>) = unionSubst
+instance Monoid meta => Monoid (Subst meta vs) where
+  mempty = Subst Map.empty
+  mappend = (<>)
+
+-- | Unify two 'Subst's.
+--
+-- NOTE: the union is left-biased: in case of duplicate 'Var's,
+-- it keeps the one from the first 'Subst' given.
+--
+-- NOTE: the first 'Subst' given is applied to the second (with 'subst'),
+-- this way each 'Var' directly maps to an expanded 'Type',
+-- so that, when using the resulting 'Subst',
+-- there is no need to apply it multiple times
+-- until there is no more substitution to be done.
+unionSubst :: Subst meta vs -> Subst meta vs -> Subst meta vs
+unionSubst sx@(Subst x) (Subst y) = Subst $ x `Map.union` ((\(VT v r) -> VT v $ subst sx r) Data.Functor.<$> y)
+
+-- * Type 'VT'
+
+-- | A 'Var' and a 'Type' existentialized over their type index.
+data VT meta vs = forall t. VT (Var meta vs t) (Ty meta vs t)
+
+deriving instance (Show meta, Monoid meta) => Show (VT meta vs)
+
+insertSubst :: Monoid meta => Var meta vs v -> Ty meta vs v -> Subst meta vs -> Subst meta vs
+insertSubst v t (Subst s) = Subst $ Map.insert (indexVar v) (VT v t) s
+
+lookupSubst :: Monoid meta => Var meta vs v -> Subst meta vs -> Maybe (Ty meta vs v)
+lookupSubst v (Subst s)
+  | Just (VT v' t) <- Map.lookup (indexVar v) s
+  , Just Type.Reflection.HRefl <- v `eqTy` v' =
+      Just t
+lookupSubst _v _m = Nothing
+
+-- * Class 'Substable'
+class Substable t where
+  -- | Like 'substVar', but without the /occurence check/.
+  substVarUnsafe ::
+    Var meta vs v -> Ty meta vs v -> t meta vs a -> t meta vs a
+
+  -- | Substitute all the 'Var's which have a match in given 'Subst'.
+  subst ::
+    Subst meta vs -> t meta vs a -> t meta vs a
+instance Substable Ty where
+  substVarUnsafe _v _r t@TyConst{} = t
+  substVarUnsafe v r (TyApp f a) =
+    TyApp
+      (substVarUnsafe v r f)
+      (substVarUnsafe v r a)
+  substVarUnsafe v r t@TyVar{tyVar = tv} =
+    case v `eqTy` tv of
+      Just Type.Reflection.HRefl -> r
+      Nothing -> t
+
+  -- substVarUnsafe v r (TyFam meta len fam as) =
+  --  TyFam meta len fam $ substVarUnsafe v r as
+
+  subst _s t@TyConst{} = t
+  subst s (TyApp f a) = TyApp (subst s f) (subst s a)
+  subst (Subst s) t@TyVar{tyVar = tv} =
+    case Map.lookup (indexVar tv) s of
+      Nothing -> t
+      Just (VT vr r) ->
+        case tv `eqTy` vr of
+          Nothing -> Prelude.error "[BUG] subst: kind mismatch"
+          Just Type.Reflection.HRefl -> r
+
+-- subst s (TyFam meta len fam as) = TyFam meta len fam $ subst s as
+instance Substable (Tys as) where
+  substVarUnsafe _v _r TysZ = TysZ
+  substVarUnsafe v r (TysS t ts) =
+    substVarUnsafe v r t
+      `TysS` substVarUnsafe v r ts
+  subst _s TysZ = TysZ
+  subst s (TysS t ts) = subst s t `TysS` subst s ts
+
+-- | Substitute the given 'Var' by the given 'Type',
+-- returning 'Nothing' if this 'Type' contains
+-- the 'Var' (occurence check).
+substVar ::
+  VarOccursIn t =>
+  Substable t =>
+  Var meta vs v ->
+  Ty meta vs v ->
+  t meta vs a ->
+  Maybe (t meta vs a)
+substVar v r t =
+  if v `varOccursIn` r
+    then Nothing -- NOTE: occurence check
+    else Just $ substVarUnsafe v r t
+
+-- ** Type 'ErrorUnify'
+
+-- | Reasons why two 'Type's cannot be unified.
+data ErrorUnify meta
+  = -- | /occurence check/: a 'Var' is unified with a 'Type'
+    --   which contains this same 'Var'.
+    ErrorUnifyVarLoop IndexVar (TyVT meta)
+  | -- | Two 'TyConst's should be the same, but are different.
+    ErrorUnifyConst (TyVT meta) (TyVT meta)
+  | -- | Two 'Kind's should be the same, but are different.
+    ErrorUnifyKind (KindK meta) (KindK meta)
+  | -- | Cannot unify those two 'Type's.
+    ErrorUnifyType (TyVT meta) (TyVT meta)
+
+deriving instance Monoid meta => Eq (ErrorUnify meta)
+deriving instance (Show meta, Monoid meta) => Show (ErrorUnify meta)
+
+instance ErrorInj (ErrorUnify meta) (ErrorUnify meta) where
+  errorInj = id
+
+data SourceTypeArg meta
+  = SourceTypeArg (TyVT meta)
+
+-- | Return the left spine of a 'Ty':
+-- the root 'Ty' and its 'Ty' parameters,
+-- from the left to the right.
+spineTy ::
+  forall meta vs t.
+  -- MC.MonadWriter (SourceTypeArg meta) (Sourced meta) =>
+  Source meta =>
+  SourceInj (TyVT meta) meta =>
+  Ty meta vs t ->
+  (TyT meta vs, [TyT meta vs])
+spineTy = go []
+  where
+    go :: forall kx (x :: kx). [TyT meta vs] -> Ty meta vs x -> (TyT meta vs, [TyT meta vs])
+    -- Skip the constraint @q@.
+    go ctx (TyApp (TyApp (TyConst{tyConst = c}) _q) t)
+      | Just Type.Reflection.HRefl <- proj_ConstKi @_ @(#>) c =
+          go ctx t
+    -- Add a type to the spine.
+    go ctx (TyApp f a) = go (TyT a {-(SourceTypeArg (TyVT ty)-} : ctx) f
+    -- Add the root.
+    go ctx t = (TyT t {-SourceTypeArg (TyVT ty)-}, ctx)
+
+{-
+spineTy
+ :: Ty meta ctx ss cs (t::k)
+ -> (forall kx (x::kx) xs. Ty meta ctx ss cs x -> Tys meta ctx ss cs xs -> ret)
+ -> ret
+spineTy = go TysZ
+  where
+  go :: Tys meta ctx ss cs hs
+     -> Ty meta ctx ss cs (t::k)
+     -> (forall kx (x::kx) xs. Ty meta ctx ss cs x -> Tys meta ctx ss cs xs -> ret)
+     -> ret
+  go ctx (TyApp  _src f a) k = go (a `TysS` ctx) f k
+  go ctx (Term x _te)    k = go ctx x k
+  go ctx (TyAny x)       k = go ctx x k
+  go ctx t k = k t ctx
+-}
+
+-- | Return the /most general unification/ of two 'Type's, when it exists.
+unifyType ::
+  forall ki (x :: ki) (y :: ki) vs meta m.
+  SourceInj (TyVT meta) meta =>
+  -- ErrorInj (Con_Kind meta) (ErrorUnify meta) =>
+  MC.MonadExcept (ErrorUnify meta) m =>
+  Subst meta vs ->
+  Ty meta vs (x :: ki) ->
+  Ty meta vs (y :: ki) ->
+  m (Subst meta vs)
+unifyType vs x y =
+  let k = kindOf x
+   in case (spineTy x, spineTy y) of
+        ((TyT xRootTy, px), (TyT yRootTy, py)) ->
+          case (xRootTy, yRootTy) of
+            (TyVar{tyVar = vx}, _) | Just Type.Reflection.HRefl <- k `eqTy` kindOf vx -> goVar vs vx y
+            (_, TyVar{tyVar = vy}) | Just Type.Reflection.HRefl <- k `eqTy` kindOf vy -> goVar vs vy x
+            (TyConst{tyConst = cx}, TyConst{tyConst = cy})
+              | Just Type.Reflection.HRefl <- cx `eqTy` cy -> goZip vs px py
+              | otherwise -> MC.throw $ ErrorUnifyConst (TyVT xRootTy) (TyVT yRootTy)
+            _ ->
+              case (x, y) of
+                (TyApp fx ax, TyApp fy ay) -> goZip vs [TyT fx, TyT ax] [TyT fy, TyT ay]
+                _ -> MC.throw $ ErrorUnifyType (TyVT x) (TyVT y)
+  where
+    goVar ::
+      forall k (a :: k) (b :: k) vs'.
+      Subst meta vs' ->
+      Var meta vs' a ->
+      Ty meta vs' b ->
+      m (Subst meta vs')
+    goVar vs' va b =
+      case va `lookupSubst` vs' of
+        Just a -> unifyType vs' b a
+        Nothing ->
+          case vs' `subst` b of
+            TyVar{tyVar = vb} | Just Type.Reflection.HRefl <- va `eqTy` vb -> return vs'
+            b'
+              | va `varOccursIn` b' -> MC.throw $ ErrorUnifyVarLoop (indexVar va) (TyVT b')
+              | Type.Reflection.HRefl :: a Type.Reflection.:~~: b <- unsafeCoerce Type.Reflection.HRefl ->
+                  return $ insertSubst va b' mempty <> vs'
+    goZip ::
+      forall vs'.
+      Subst meta vs' ->
+      [TyT meta vs'] ->
+      [TyT meta vs'] ->
+      m (Subst meta vs')
+    goZip vs' [] [] = return vs'
+    goZip vs' (TyT a : as) (TyT b : bs) =
+      let xK = kindOf a
+       in let yK = kindOf b
+           in case xK `eqTy` yK of
+                Nothing -> MC.throw $ ErrorUnifyKind (TyT xK) (TyT yK)
+                Just Type.Reflection.HRefl -> unifyType vs' a b >>= \vs'' -> goZip vs'' as bs
+    goZip _vs _a _b = Prelude.error "[BUG] unifyType: kinds mismatch"
diff --git a/symantic.cabal b/symantic.cabal
index 4c0004d..8b59ff2 100644
--- a/symantic.cabal
+++ b/symantic.cabal
@@ -1,35 +1,26 @@
 cabal-version:      3.0
-name:               literate-web
-maintainer:         mailto:literate-web@sourcephile.fr
-bug-reports:        https://mails.sourcephile.fr/inbox/literate-web
-homepage:           https://git.sourcephile.fr/literate-web.git
-author:             Julien Moutinho <julm+literate-web@sourcephile.fr>
-copyright:          Julien Moutinho <julm+literate-web@sourcephile.fr>
+name:               symantic
+maintainer:         mailto:symantic@sourcephile.fr
+bug-reports:        https://mails.sourcephile.fr/inbox/symantic
+homepage:           https://git.sourcephile.fr/symantic.git
+author:             Julien Moutinho <julm+symantic@sourcephile.fr>
+copyright:          Julien Moutinho <julm+symantic@sourcephile.fr>
 license:            AGPL-3.0-or-later
 license-file:       LICENSES/AGPL-3.0-or-later.txt
 
 --             PVP: +-+------- breaking API changes
 --                  | | +----- non-breaking API additions
 --                  | | | +--- code changes with no API change
-version:            0.0.0.20221117
+version:            0.0.0.20230723
 stability:          experimental
-category:           Web
+category:           Language
 synopsis:           Haskell-website compiler
 description:
-  Exploring the design space of compile-time website generator
-  by using a domain-specific language (DSL)
-  embedded into the Haskell language.
-  .
-  Alternatives:
-  .
-  * <https://hackage.haskell.org/package/ema ema>
-
 build-type:         Simple
 tested-with:        GHC ==9.2.4
 extra-doc-files:    ChangeLog.md
 extra-source-files:
   .envrc
-  cabal.project
   flake.lock
   flake.nix
 
@@ -37,7 +28,7 @@ extra-tmp-files:
 
 source-repository head
   type:     git
-  location: git://git.sourcephile.fr/haskell/literate-web.git
+  location: git://git.sourcephile.fr/haskell/symantic.git
 
 common boilerplate
   default-language:   Haskell2010
@@ -70,6 +61,8 @@ common boilerplate
     -Wmonomorphism-restriction -Wpartial-fields
     -fprint-potential-instances
 
+-- -fprint-explicit-kinds
+
 -- -dshow-passes
 -- -ddump-to-file
 -- -ddump-simpl
@@ -81,169 +74,28 @@ common boilerplate
 
 common library-deps
   build-depends:
-    , async                  >=2.2
-    , base                   >=4.6  && <5
-    , bytestring             >=0.10
-    , containers             >=0.5
-    , directory              >=1.3
-    , filepath               >=1.4
-    , filepattern            >=0.1
-    , hashable
-    , http-client            >=0.6
-    , http-media             >=0.7
+    , base           >=4.6 && <5
+    , containers     >=0.5
+    , ghc-prim
     , monad-classes
-    , peano
-    , reflection
-    , symantic-base          >=0.5
-    , template-haskell
+    , symantic-base  >=0.5
     , text
-    , transformers           >=0.5
-    , unicode-transforms     >=0.2
-    , unordered-containers
-    , uri-encode             >=1.5
-    , wai
-    , wai-middleware-static
-    , wai-websockets
-    , warp
-    , websockets             >=0.12
-    , pipes
-    , pipes-safe
-    , pipes-concurrency
-    , pipes-parse
-    , pipes-group
-    , mvc
-    , mvc-updates
-    , ghc-prim
+    , transformers
+    , vector
 
 library
   import:          boilerplate, library-deps
   hs-source-dirs:  src
   exposed-modules:
-    ForallSem
-    Literate.Web
-    Literate.Web.Semantics.Compiler
-    Literate.Web.Semantics.Addresser
-    Literate.Web.Syntaxes
-    Literate.Web.Types.MIME
-    Literate.Web.Types.URL
-
-library relactive
-  import:          boilerplate, library-deps
-  hs-source-dirs:  src
-  build-depends:
-    , async
-    , contravariant  >=1.5
-    , stm
-    , monad-classes
-
-  exposed-modules:
-    Control.Reactive
-    Control.Reactive.IORef
-    Control.Reactive.MVar
-    Control.Reactive.Relation
-    Control.Reactive.STRef
-    Control.Reactive.TVar
-    Control.Reactive.Value
-
--- Literate.Web.Semantics.Server
--- Literate.Web.Semantics.Client
---Literate.Web.Decoder
---Literate.Web.Encoder
---Literate.Web.Generator
---Literate.Web.MIME
-
---Literate.Web.Decoder
-test-suite literate-web-tests
-  -- library-deps is only to have ghcid reloaded on changes in src
-  import:          boilerplate, library-deps
-  type:            exitcode-stdio-1.0
-  hs-source-dirs:  tests
-  main-is:         Main.hs
-  other-modules:
-    Examples.Ex01
-    Examples.Ex02
-    Examples.Ex03
-    Examples.Ex04
-    Examples.Ex05
-    Goldens
-    Paths_literate_web
-    Utils
-  autogen-modules: Paths_literate_web
-  build-depends:
-    , base           >=4.6  && <5
-    , containers     >=0.5
-    , literate-web
-    , monad-classes
-    , relude
-    , symantic-base  >=0.5
-    , tasty          >=0.11
-    , tasty-golden   >=2.3
-    , tasty-hunit    >=0.9
-    , text           >=1.2
-    , transformers   >=0.5
-    , relactive
-
--- , relude         >=1    && <2
-benchmark time
-  import:         boilerplate, library-deps
-  type:           exitcode-stdio-1.0
-  hs-source-dirs: benchmarks/time
-  main-is:        Main.hs
-  build-depends:
-    , base         >=4.6 && <5
-    , relactive
-    , tasty
-    , tasty-bench
-
-  -- , relude >= 1
-  -- Set a larger allocation area (nursery)
-  -- to remove some noisiness of the garbage collection.
-  ghc-options:    -with-rtsopts=-A32m
-
-benchmark weigh
-  import:         boilerplate, library-deps
-  type:           exitcode-stdio-1.0
-  hs-source-dirs: benchmarks/weigh src
-  build-depends:
-    , async
-    , contravariant  >=1.5
-    , stm
-
-  main-is:        Main.hs
-  build-depends:
-    , base    >=4.6 && <5
-    , relude  >=1
-    , weigh
-
---, relactive
-executable async
-  import:         boilerplate, library-deps
-  hs-source-dirs: executables/async
-  main-is:        Main.hs
-  build-depends:
-    , async
-    , base           >=4.6 && <5
-    , relactive
-    , relude
-    , symantic-base
-    , tasty
-    , tasty-bench
-
--- , relude >= 1
-
-executable fsnotify
-  import:         boilerplate, library-deps
-  hs-source-dirs: executables/fsnotify
-  main-is:        Main.hs
-  build-depends:
-    , async
-    , base           >=4.6 && <5
-    , directory
-    , filepath
-    , fsnotify
-    , relactive
-    , relude         >=1
-    , symantic-base
-    , tasty
-    , tasty-bench
-    , time
+    Symantic.Compiler
+    Symantic.Compiler.Term
+    Symantic.Parser
+    Symantic.Parser.Error
+    Symantic.Parser.Source
+    Symantic.Printer
+    Symantic.Syntaxes
+    Symantic.Typer
+    Symantic.Typer.Eq
+    Symantic.Typer.List
+    Symantic.Typer.Type
+    Symantic.Typer.Unify
-- 
2.47.2