Various type inference designs/sketches

0README.md

Type Inference: Various Designs

I'm exploring the right data types for writing a type inference with higher kinds and poly types.

Putting more things in the type system can force you to think about more things, but it also can make it harder and more verbose to write and read algorithms.

• This one implements a fairly good type inferer, with a free monad, but kinds are not enforced, and forall/schemes are not considered atll.
• This one pushes kinds and generic vars into the type system with a nested tuples approach
• This one borrows from Oleg's typed eval, but doesn't actually implement any hard things yet.
• This one pushes kinds into the type system and also generic vars.

infer-untyped.hs

-- This one implements a fairly good type inferer, with a free monad, 
-- but kinds are not enforced, and forall/schemes are not considered atll.

{-# LANGUAGE TupleSections #-}
{-# LANGUAGE NamedFieldPuns #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE ApplicativeDo #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE DeriveFunctor #-}
{-# LANGUAGE LambdaCase #-}

-- |
--
-- 1. Produce skeletons for structure (-> for lambdas, int, etc.)
-- 3. Equality constraints t~t' are given as leftovers.

-- 2. Unknown types--type variables--are returned, too.
-- 3. Class constraints are bubbled up around each expression.

-- 4. Finally, we unify all the constraints.
-- 5. We resolve instances that are complete.
-- 6. We complain about class constraints that aren't filled in.
-- 7. Make sure that you can't define: id :: a -> a; id x = 6
-- <https://gitlab.haskell.org/ghc/ghc/issues/4499>

-- Note
--
-- It seems clear below that unknown and p0 can be unified (one-way;
-- rigids are like constants); i.e. all p0's become unknown's, same
-- for out/r2.
--
-- Elaboration would let me explicitly state this, as a kind of elab
-- :: [constraint] -> [constraint] that would yield further
-- constraints based on what we see here.
--
-- Furthermore, rigids are only relevant when checking the definition
-- of a toplevel or let with an explicit type signature. Otherwise;
-- they may also be relevant for using a name "read-only" without
-- changing its type-variables in-place to match our use; instead we
-- copy them. So f Int or f Char works fine.
--
--
-- Constraints:
--                                  p0 -> r3   ≡   p1
--                                 Int -> r2   ≡   r3
-- unknown -> (unknown -> Int -> out) -> out   ≡   p0 -> p1 -> r2
--
-- unknown -> (unknown -> Int -> out) -> out -- from expression

module Duet.Infer2 where

import Control.Applicative.Free
import Control.Monad.Free
import Control.Monad.State
import Data.List
import Text.Printf

--------------------------------------------------------------------------------
-- Types

data T
  = VT String -- variable
  | CT String -- constant
  | FT T T     -- func
  deriving (Eq)

instance Show T where
  show = go False
    where
      go o =
        \case
          VT v -> v

          CT s -> s
          FT a b -> opt "(" ++ go True a ++ " -> " ++ go False b ++ opt ")"
            where opt str =
                    if o
                      then str
                      else ""

--------------------------------------------------------------------------------
-- Expression

data E s
  = CE T
  | LE (SType s) String (E s)
  | VE (SType s) String
  | AE (SType s) (E s) (E s)

--------------------------------------------------------------------------------
-- Stages

data Stage = PreInfer | PostInfer

type family SType s where
  SType 'PreInfer = Maybe T
  SType 'PostInfer = T

--------------------------------------------------------------------------------
-- Inferer

inferE :: E 'PreInfer -> Infer (E 'PostInfer)
inferE = go
  where
    go =
      \case
        CE t -> pure (CE t)
        LE msig p e -> do
          pt <- liftStep (NewVT "p")
          liftStep (BindTV p pt)
          e' <- go e
          let lt = FT pt (eType e')
          lt' <-
            case msig of
              Nothing -> pure lt
              Just t -> do
                liftStep (Equiv t lt)
                pure t
          pure (LE lt' p e')
        VE msig p -> do
          mt <- liftStep (LookupP p)
          case mt of
            Nothing -> liftStep (MissingP p)
            Just t ->
              case msig of
                Nothing -> pure (VE t p)
                Just sigt -> do
                  liftStep (Equiv sigt t)
                  pure (VE sigt p)
        AE msig f x -> do
          rt <- liftStep (NewVT "r")
          case msig of
            Nothing -> pure ()
            Just t -> liftStep (Equiv t rt)
          f' <- go f
          x' <- go x
          let ft_expected = FT (eType x') rt
          liftStep (Equiv ft_expected (eType f'))
          pure (AE rt f' x')

--------------------------------------------------------------------------------
-- Infer monad

data InferStep a where
  NewVT :: String -> InferStep T
  BindTV :: String -> T -> InferStep ()
  LookupP :: String -> InferStep (Maybe T)
  MissingP :: String -> InferStep a
  Equiv :: T -> T -> InferStep ()

newtype Infer a = Infer
  { unInfer :: Free (Ap InferStep) a
  } deriving (Functor, Applicative, Monad)
liftStep :: InferStep a -> Infer a
liftStep = Infer . liftF . liftAp

data S = S
  { idents :: Int
  , constraints :: [(T, T)]
  , env :: [(String, T)]
  , vars :: [T]
  }

runInfer :: Infer (E 'PostInfer) -> (E 'PostInfer, S)
runInfer m =
  runState
    (foldFree (runAp reify) (unInfer m))
    (S {idents = 0, constraints = [], env = [], vars = []})
  where
    reify :: InferStep a -> State S a
    reify =
      \case
        NewVT prefix -> do
          i <- gets idents
          let t = (VT (prefix ++ show i))
          modify (\s -> s {idents = i + 1, vars = vars s ++ [t]})
          pure t
        BindTV p t -> modify (\s -> s {env = (p, t) : (env s)})
        LookupP p -> gets env >>= pure . lookup p
        MissingP i -> error ("Missing parameter " ++ i)
        Equiv x y ->
          modify (\s -> s {constraints = (constraints s) ++ [(x, y)]})

--------------------------------------------------------------------------------
-- Debug

instance Show S where
  show S {idents, constraints, env, vars} =
    unlines
      [ "Identifier counter: " ++ show idents
      , "Environment:"
      , unlines (map (\(p, t) -> p ++ " :: " ++ show t) env)
      , unlines (map show vars)
      , "Constraints:"
      , tablize
          (map
             (\(t, t') -> [(False, show t), (False, " ≡ "), (True, show t')])
             constraints)
      ]

debug example =
  let (t, state) = runInfer (inferE example)
   in do print t
         print state
         putStrLn (show (eType t) ++ " -- from expression")
         {-putStrLn
           (graph
              (Left (eType t) :
               map Left (vars state) ++ map Right (constraints state)))-}

graph :: [Either T (T,T)] -> String
graph cs = unlines ["strict digraph {", unlines (map go cs), "}"]
  where
    go (Left e) = unlines [show (show e) ++ ";", splice e]
    go (Right (x, y)) =
      unlines
        [ unlines
            [ unlines
              [ show (show yt) ++ "->" ++ show (show xt) ++ " [dir=none, color=\"black:invis:black\"];"

              ]
            | xt <- [x]
            , yt <- [y]
            ]
        , splice x
        , splice y
        ]
    splice x =
      unlines
        [show (show t) ++ "->" ++ show (show x) ++ ";" | t <- tVars x, t /= x]

tVars :: T -> [T]
tVars =
  \case
    FT x y -> concatMap tVars [x, y]
    t -> [t]

-- | Make a table out of a list of rows.
tablize :: [[(Bool,String)]] -> String
tablize xs =
  intercalate "\n"
              (map (intercalate "  " . map fill . zip [0 ..]) xs)
  where fill (x',(left',text')) = printf ("%" ++ direction ++ show width ++ "s") text'
          where direction = if left'
                               then "-"
                               else ""
                width = maximum (map (length . snd . (!! x')) xs)

instance Show (E 'PreInfer) where
  show = \case
            CE t -> "(_ :: " ++ show t ++ ")"
            LE t p e -> "(\\" ++ p ++ " -> " ++ show e ++ ")"
            VE t v -> v
            AE t f x -> "(" ++ show f ++ " " ++ show x ++ ")"
instance Show (E 'PostInfer) where
  show = \case
            CE t -> "(_ :: " ++ show t ++ ")"
            LE t p e -> "((\\" ++ p ++ " -> " ++ show e ++ ") :: " ++ show t ++ ")"
            VE t v -> "(" ++ v ++ " :: " ++ show t ++ ")"
            AE t f x -> "((" ++ show f ++ " " ++ show x ++ ") :: " ++ show t ++ ")"

eType :: E 'PostInfer -> T
eType =
  \case
    CE t -> t
    LE t _ _ -> t
    VE t _ -> t
    AE t _ _ -> t

example0 :: E 'PreInfer
example0 =
  LE Nothing "f" (AE Nothing (VE Nothing "f") (CE (CT "Int")))

example1 :: E 'PreInfer
example1 =
  LE
    (Just
       (FT
          (RT "unknown")
          (FT (FT (RT "unknown") (FT (CT "Int") (RT "out"))) (RT "out"))))
    "x"
    (LE
       Nothing
       "f"
       (AE
          Nothing
          (AE Nothing (VE Nothing "f") (VE Nothing "x"))
          (CE (CT "Int"))))

example2_wrong :: E 'PreInfer
example2_wrong =
  LE Nothing "f" (AE Nothing (VE Nothing "f") (VE Nothing "f"))

splitting-kind-from-val.hs

-- This one separates the kind from the return @a@ value.

{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE LambdaCase, StandaloneDeriving, GADTs #-}

data Type env k a where
 -- Regular types

  -- A constant type.
  C :: Show k => k -> Type env k ()
  -- A free variable.
  Free :: Show k => k -> Type env k ()
  -- App.
  Ap :: Type env (i :-> k) () -> Type env i () -> Type env k ()

  -- Schemes

  -- This correponds to a rigid.
  V :: Var env k t -> Type env k t
  -- This corresponds to forall a. ... a ...
  L :: Type (a,env) o b -> Type env (Forall i o) (a -> b)
  -- This wouldn't be writable by a user.
  A :: Type env (Forall k o) (a -> b) -> Type env k a -> Type env o b
deriving instance Show (Type env k a)

data Forall k o = Forall k o deriving (Show)
data TypeK = TypeK deriving (Show)
data a :-> k = a :-> k deriving (Show)

data Var env k t where
  VZ :: Var (t, env) k t
  VS :: Var env k t -> Var (a, env) k t
deriving instance Show (Var env k t)

eval :: env -> Type env k t -> t
eval _ Ap {}          = ()
eval _ Free{}         = ()
eval env (V v)        = lookp v env
eval _   C{}          = ()
eval env (L e)        = \x -> eval (x, env) e
eval env (A e1 e2)    = (eval env e1) (eval env e2)

lookp :: Var env k t -> env -> t
lookp VZ (x,_)        = x
lookp (VS v) (_, env) = lookp v env

{-

Example:

> eval () (A (L (V VZ)) (C 'a'))
'a'

-- const
> eval () (A (A (L (L (V (VS VZ)))) (C 'a')) (C 123))
'a'

-}

super-typed.hs

-- This one pushes kinds and generic vars into the type system with a nested tuples approach.

{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE NamedFieldPuns #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeOperators, LambdaCase, StandaloneDeriving, GADTs #-}

module StructuredInfer where

import Control.Applicative.Free
import Control.Monad.Free
import Control.Monad.State
import Data.List
import Data.Typeable
import Numeric.Natural
import Text.Printf

--------------------------------------------------------------------------------
-- Types

data Type env kind where
  -- A constant type. Add kinds?
  -- Maybe, (), Int, Either, (->), etc.
  Constructor :: String -> kind -> Type env kind
  -- A free variable.
  -- a
  FreeVariable :: Natural -> kind -> Type env kind
  -- Type application.
  -- Maybe a
  Application :: (Show ki, Show ko) => Type env (ki -> ko) -> Type env ki -> Type env ko
  -- A generic variable used in a forall scheme.
  -- Rigid variables that will not unify with free variables.
  GenericVariable :: (env ~ (t, env')) => Var env kind -> Type env kind
  -- Forall scheme:
  -- forall. a -> ... a ...
  -- Forall :: (Show b, env' ~ (a,env)) => Type (x,env') b -> Type env' b
  -- -- This wouldn't be writable by a user.
  -- -- E.g. Show a => a -> String
  -- -- Instantiate with: Int
  -- -- Int -> String
  -- InstantiateForall :: Type env (Forall a b) -> Type env a -> Type env b
  -- -- Class qualification
  -- -- E.g. Show a => a -> String
  -- Qualify :: c -> Var env x -> Type env o -> Type env ((c, x) :=> o)
  -- -- Row types.
  -- -- E.g. { a :: Int, b :: String }
  -- Row :: Row env -> Type env RowKind

data SchemeOrType env kind where
  SchemeType :: SchemeOrType (a, env) kind -> SchemeOrType env kind
  TypeType :: Type env kind -> SchemeOrType env kind
instance Show (SchemeOrType e k) where show _ = "s"

functionCons :: Type e (() -> () -> ())
functionCons = undefined {-Constructor "(->)" (TypeK :*-> (TypeK :*-> TypeK))-}

functionType :: Type e TypeK -> Type e TypeK -> Type e TypeK
functionType i o = undefined {-Application (Application functionCons i) o-}

instance Show (Type e k) where
  show t0 = go 0 t0
    where
      go ::
           forall e k. Int
        -> Type e k
        -> String
      go nesting =
        \case
          Constructor str kind -> "" ++ str ++ "" -- " :: " ++ show kind ++
          FreeVariable nat kind -> "v" ++ show nat ++ "" -- ++ " :: " ++ show kind
          Application (Application (Constructor "(->)" _) x) y ->
            "(" ++ go nesting x ++ " -> " ++ go nesting y ++ ")"
          Application typeF typeX ->
            "(" ++ show typeF ++ " " ++ indent (show typeX) ++ ")"
          -- Forall t ->
          --   "(forall _" ++ show nesting ++ ". " ++ go (nesting + 1) t ++ ")"
          GenericVariable var -> "_" ++ show (varnesting var)

varnesting :: Var env t -> Int
varnesting =
  \case
     VZ -> 0
     VS v -> 1 + varnesting v

indent :: String -> String
indent = intercalate "\n" . map ("  " ++) . lines

--------------------------------------------------------------------------------
-- Kinds

data Kind a where
  TypeK :: Kind ()
  (:*->) :: Kind a -> Kind b -> Kind (a -> b)
instance Show (Kind a) where show _ = "Kind"
type TypeK = Kind ()

--------------------------------------------------------------------------------
-- Vars
data Var env t where
  VZ :: Var (t, env) t
  VS :: Var env t -> Var (a, env) t
deriving instance Show (Var env t)

--------------------------------------------------------------------------------
-- Expression

data E s
  = CE (SomeKindedType TypeK) -- this needs to be an arbitrary thing
  | LE (SType s (Type () TypeK)) Natural (E  s)
  | VE (SType s (Type () TypeK)) Natural
  | AE (SType s (Type () TypeK)) (E  s) (E  s)

eType :: E 'PostInfer -> SomeKindedType TypeK
eType =
  \case
    CE t -> t
    LE t _ _ -> SomeKindedType (TypeType t)
    VE t _ -> SomeKindedType (TypeType  t)
    AE t _ _ -> SomeKindedType (TypeType  t)

instance Show (E  'PreInfer) where
  show = \case
            CE t -> "(_ :: " ++ show t ++ ")"
            LE t p e -> "(\\p" ++ show p ++ " -> " ++ show e ++ ")"
            VE t v -> "p"++ show v
            AE t f x -> "(" ++ show f ++ " " ++ show x ++ ")"
instance Show (E  'PostInfer) where
  show = \case
            CE t -> "(_ :: " ++ show t ++ ")"
            LE t p e -> "((\\p" ++ show p ++ " -> " ++ show e ++ ") :: " ++ show t ++ ")"
            VE t v -> "(p" ++ show v ++ " :: " ++ show t ++ ")"
            AE t f x -> "((" ++ show f ++ " " ++ show x ++ ") :: " ++ show t ++ ")"

--------------------------------------------------------------------------------
-- Stages

data Stage = PreInfer | PostInfer

type family SType s t where
  SType 'PreInfer t = Maybe t
  SType 'PostInfer t = t

--------------------------------------------------------------------------------
-- Infer algebra

data InferStep a where
  NewVT :: (Typeable env, Typeable k, Show k) => k -> InferStep (Type env k)
  BindTV :: (Typeable env) => Natural -> Type env TypeK -> InferStep ()
  LookupP :: Natural -> InferStep (SomeKindedType TypeK)
  Equiv :: (Show k) => Type env k -> Type env k -> InferStep ()
deriving instance Show (InferStep a)

data SomeKindedType k =
  forall env. (Typeable env) =>
                SomeKindedType (SchemeOrType env k)
deriving instance Show k => Show (SomeKindedType k)

--------------------------------------------------------------------------------
-- Inferer

-- TODO:
--
-- We need to distinguish between
--
-- * /Defining/ an expression whose type is forall'd (make sure types are polymorphic)
-- * /Using/ a variable whose type is forall'd (instantiate scheme with fresh variables)
--
-- And make sure that this situation makes sense (this is a case of /using/):
--
--                     (Int -> v3)   ≡   v0 <--- this is a lambda parameter,
--                    (Char -> v4)   ≡   v0 <--- presenty we don't know its type because
                                             --- we don't provide a sig for the param,
                                             --- nor do we figure it out based on the
                                             --- lambda's type (we could)
--                      (v4 -> v1)   ≡   v2
--                      (v3 -> v2)   ≡   (forall _0. (_0 -> (forall _1. (_1 -> ()))))
-- ((forall _0. (_0 -> _0)) -> ())   ≡   (v0 -> v1)

inferE :: E  'PreInfer -> Infer (E  'PostInfer)
inferE = go
  where
    go =
      \case
        CE t -> pure (CE t)
        LE msig p e -> do
          pt <- liftStep (NewVT TypeK)
          liftStep (BindTV p pt)
          e' <- go e
          let lt = functionType pt (undefined (eType e'))
          lt' <-
            case msig of
              Nothing -> pure lt
              Just t -> do
                liftStep (Equiv t lt)
                pure t
          pure (LE lt' p e')
        VE msig p -> do
          sky <- liftStep (LookupP p)
          t <- instantiate sky
          case msig of
            Nothing -> pure (VE t p)
            Just sigt -> do
              liftStep (Equiv sigt t)
              pure (VE sigt p)
        AE msig f x -> do
          rt <- liftStep (NewVT TypeK)
          case msig of
            Nothing -> pure ()
            Just t -> liftStep (Equiv t rt)
          f' <- go f
          x' <- go x
          let ft_expected = functionType (undefined (eType x')) rt
          liftStep (Equiv ft_expected (undefined (eType f')))
          pure (AE rt f' x')

instantiate :: SomeKindedType TypeK -> Infer (Type () TypeK)
instantiate (SomeKindedType schemeOrType) = go schemeOrType
  where go =
          \case
             SchemeType t -> undefined

eval :: e -> Type e k -> k
eval e =
  \case
    Constructor s k ->  k
    FreeVariable s k -> k
    Application s k -> (eval e s) (eval e k)
    -- Forall inner -> pure (\x -> eval (x, e) inner)
    GenericVariable var -> (lookp var e)

lookp :: Var env t -> env -> t
lookp VZ (x,_)        = x
lookp (VS v) (_, env) = lookp v env

--------------------------------------------------------------------------------
-- Infer monad

newtype Infer a = Infer
  { unInfer :: Free (Ap InferStep) a
  } deriving (Functor, Applicative, Monad)
liftStep :: InferStep a -> Infer a
liftStep = Infer . liftF . liftAp

--------------------------------------------------------------------------------
-- Infer monad runner

data SomeEquivalence =
  forall env k. (Show k) =>
                SomeEquivalence (Type env k, Type env k)

data SomeType =
  forall env k. (Typeable k, Typeable env, Show k) =>
                SomeType (Type env k)
deriving instance Show SomeType

data S = S
  { idents :: !Natural
  , constraints :: ![SomeEquivalence]
  , env :: ![(Natural, SomeKindedType TypeK)]
  , vars :: ![SomeType]
  }

runInfer :: Infer (E  'PostInfer) -> IO (E  'PostInfer, S)
runInfer m =
  runStateT
    (foldFree (runAp (printit >=> reify)) (unInfer m))
    (S {idents = 0, constraints = [], env = [], vars = []})
  where
    printit x = x <$ lift (print x)
    reify :: InferStep a -> StateT S IO a
    reify =
      \case
        NewVT kind -> do
          nat <- gets idents
          let t = (FreeVariable nat kind)
          modify (\s -> s {idents = nat + 1, vars = vars s ++ [SomeType t]})
          pure t
        BindTV p t -> modify (\s -> s {env = (p, SomeKindedType (TypeType t)) : (env s)})
        LookupP p -> do
          r <- gets env >>= pure . lookup p
          case r of
            Nothing -> error "variable not in scope!"
            Just yes -> pure yes
        Equiv x y ->
          modify
            (\s -> s {constraints = (constraints s) ++ [SomeEquivalence (x, y)]})

instance Show S where
  show S {idents, constraints, env, vars} =
    unlines
      [ "Identifier counter: " ++ show idents
      , "Environment:"
      , unlines (map (\(p, t) -> show p ++ " :: " ++ show t) env)
      , unlines (map show vars)
      , "Constraints:"
      , tablize
          (map
             (\(SomeEquivalence (t, t')) -> [(False, show t), (False, " ≡ "), (True, show t')])
             constraints)
      ]

debug :: (Show (E  'PostInfer)) => E  'PreInfer -> IO ()
debug example = do
  (t, s) <- runInfer (inferE example)
  print example
  putStrLn "=>"
  print t
  print s
  putStrLn (show (eType t) ++ " -- from expression")


tablize :: (Foldable t, PrintfArg (t a)) => [[(Bool, t a)]] -> [Char]
tablize xs =
  intercalate "\n"
              (map (intercalate "  " . map fill . zip [0 ..]) xs)
  where fill (x',(left',text')) = printf ("%" ++ direction ++ show width ++ "s") text'
          where direction = if left'
                               then "-"
                               else ""
                width = maximum (map (length . snd . (!! x')) xs)


example0 :: E  'PreInfer
example0 =
  LE Nothing 0 (AE Nothing (VE Nothing 0) (CE (SomeKindedType(TypeType (Constructor "Int" TypeK :: Type () TypeK)))))

example1_err :: E  'PreInfer
example1_err =
  LE Nothing 0 (AE Nothing (CE (SomeKindedType(TypeType(Constructor "Int" TypeK :: Type () TypeK)))) (VE Nothing 0))

example2_err :: E  'PreInfer
example2_err =
  LE
    Nothing {-(Just (functionType (GenericVariable VZ) (GenericVariable VZ)))-}
    0
    (AE Nothing (CE (SomeKindedType(TypeType(Constructor "Int" TypeK :: Type () TypeK)))) (VE Nothing 0))

example3_correct :: E  'PreInfer
example3_correct =
  LE
    Nothing
    {-(Just (Forall (functionType (functionType (Constructor "Int" TypeK) (GenericVariable VZ)) (GenericVariable VZ))))-}
    0
    (AE Nothing (VE Nothing 0) (CE (SomeKindedType(TypeType(Constructor "Int" TypeK :: Type () TypeK)))))

example3_err :: E  'PreInfer
example3_err =
  LE
    Nothing{-(Just (Forall (functionType (functionType (GenericVariable VZ) (GenericVariable VZ)) (GenericVariable VZ))))-}
    0
    (AE Nothing (VE Nothing 0) (CE (SomeKindedType(TypeType(Constructor "Int" TypeK :: Type () TypeK)))))

example4_ok :: E  'PreInfer
example4_ok =
  LE
    Nothing
    {-(Just
       (functionType
          (Forall (functionType (GenericVariable VZ) (GenericVariable VZ)))
          (Constructor "()" TypeK)))-}
    0
    (AE
       Nothing
       (AE
          Nothing
          (CE
             (SomeKindedType @(TypeK) @(TypeK, (TypeK, ()))
                (SchemeType
                   (SchemeType
                      (TypeType
                         (functionType
                            (GenericVariable VZ)
                            (functionType
                               (GenericVariable (VS VZ))
                               (Constructor "()" TypeK))))))))
          (AE
             Nothing
             (VE Nothing 0)
             (CE
                (SomeKindedType
                   (TypeType (Constructor "Int" TypeK :: Type () TypeK))))))
       (AE
          Nothing
          (VE Nothing 0)
          (CE
             (SomeKindedType
                (TypeType (Constructor "Char" TypeK :: Type () TypeK))))))

total-eval-type.hs

-- This one borrows from Oleg's typed eval, but doesn't actually implement any hard things yet.

{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE LambdaCase, StandaloneDeriving, GADTs #-}

data a :-> b = a :-> b
data a :=> b = a :=> b

data Type env t where
  -- A constant type. Add kinds?
  C :: a -> Type env a
  -- This correponds to a rigid.
  V :: Var env t -> Type env t
  -- This corresponds to forall. a -> ... a ...
  L :: Type (a,env) b -> Type env (a-> b)
  -- This wouldn't be writable by a user.
  A :: Type env (a-> b) -> Type env a -> Type env b
  -- A free variable.
  Free :: Type env ()
  -- An a -> b type.
  Fun :: Type env a -> Type env b -> Type env (a :-> b)
  -- Class qualification: C x => a
  Qual :: c -> Var env x -> Type env o -> Type env ((c, x) :=> o)

data Var env t where
  VZ :: Var (t, env) t
  VS :: Var env t -> Var (a, env) t
deriving instance Show (Var env t)

eval :: env -> Type env t -> t
eval env (Qual c v t) = (c, lookp v env) :=> eval env t
eval _ Free           = ()
eval env (V v)        = lookp v env
eval _   (C c)        = c
eval env (L e)        = \x -> eval (x, env) e
eval env (A e1 e2)    = (eval env e1) (eval env e2)
eval env (Fun x y)    = eval env x :-> eval env y

lookp :: Var env t -> env -> t
lookp VZ (x,_)        = x
lookp (VS v) (_, env) = lookp v env

{-

Example:

> eval () (A (L (V VZ)) (C 'a'))
'a'

-- const
> eval () (A (A (L (L (V (VS VZ)))) (C 'a')) (C 123))
'a'

-}

typed-poly-kinds.hs

-- This one pushes kinds into the type system and also generic vars.

{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE GADTs #-}

module InferV3 where

import Data.Finite
import GHC.TypeLits

data Monomorphic
data Polymorphic (n :: Nat)

data a :-> b = a :-> b deriving Show; infixr 2 :->

data Type s k where
  Var :: Integer -> k -> Type s k
  Con :: String -> k -> Type s k
  App :: Type s (i :-> o) -> Type s i -> Type s o
  -- We use a @Finite@ to ensure that any @Gen@ instance is always
  -- within the bounds of the @forall x y z. ...@ -- this is a
  -- Polymorphic 3.
  --
  -- We could even go as far as to use @Polymorphic 0@ to mean "not
  -- polymorphic", but I'm not sure how I feel about that.
  Gen :: Finite n -> k -> Type (Polymorphic n) k

-- If the @Finite@ and Nat in the @Polymorphic@ doesn't work out, we
-- can just drop it.
data SomePolyType k =
  forall n. KnownNat n =>
            SomePolyType (Type (Polymorphic n) k)

-- | Convert a polymorphic type to a monomorphic type.
--
-- In other words, replace all the @Gen@ with @Var@.
mono :: SomePolyType k -> (Type Monomorphic k)
mono (SomePolyType t) = go t
  where go :: Type (Polymorphic n) k -> Type Monomorphic k
        go =
          \case
             -- Here we lookup, or if missing, generate. The function
             -- @genToVar idx k@ should always be idempotent. It should also
             -- check that the returned lookup variable has the same kind;
             -- else that's an error.
             Gen idx k -> undefined
             --
             Var idx k -> Var idx k
             Con s k -> Con s k
             App f x -> App (go f) (go x)

-- | Generalize a monomorphic type to a polymorphic type.
poly :: Type Monomorphic k -> SomePolyType k
poly = undefined