intrinsic deep system F syntax in Haskell

SysF.hs

{-# language
  TypeInType, GADTs, RankNTypes, TypeFamilies,
  TypeOperators, TypeApplications,
  UnicodeSyntax, UndecidableInstances
#-}

import Data.Kind
import Data.Proxy

data Nat = Z | S Nat

data Fin n where
  FZ ∷ Fin (S n)
  FS ∷ Fin n → Fin (S n)

data OPE n m where
  ZZ   ∷ OPE Z Z
  Keep ∷ OPE n m → OPE (S n) (S m)
  Drop ∷ OPE n m → OPE (S n) m

type family FinE (σ ∷ OPE n m) (x ∷ Fin m) ∷ Fin n where
  FinE ZZ       x      = x
  FinE (Drop σ) x      = FS (FinE σ x)
  FinE (Keep σ) FZ     = FZ
  FinE (Keep σ) (FS x) = FS (FinE σ x)

data Ty (n ∷ Nat) where
  TyVar ∷ Fin n → Ty n
  (:=>) ∷ Ty n → Ty n → Ty n
  All   ∷ Ty (S n) → Ty n
infixr 4 :=>

type family TyE (σ ∷ OPE n m) (a ∷ Ty m) ∷ Ty n where
  TyE σ (TyVar x) = TyVar (FinE σ x)
  TyE σ (a :=> b) = TyE σ a :=> TyE σ b
  TyE σ (All b)   = All (TyE (Keep σ) b)

type family Id n ∷ OPE n n where
  Id Z     = ZZ
  Id (S n) = Keep (Id n)

type family WkTy (a ∷ Ty n) ∷ Ty (S n) where
  WkTy (a ∷ Ty n) = TyE (Drop (Id n)) a

data Sub n m where
  SNil  ∷ Sub n Z
  SSnoc ∷ Sub n m → Ty n → Sub n (S m)

type family CompSE (σ ∷ Sub m k)(δ ∷ OPE n m) ∷ Sub n k where
  CompSE SNil        δ = SNil
  CompSE (SSnoc σ a) δ = SSnoc (CompSE σ δ) (TyE δ a)

type family DropS (σ ∷ Sub n m) ∷ Sub (S n) m where
  DropS (σ ∷ Sub n m) = CompSE σ (Drop (Id n))

type family KeepS (σ ∷ Sub n m) ∷ Sub (S n) (S m) where
  KeepS (σ ∷ Sub n m) = SSnoc (DropS σ) (TyVar FZ)

type family IdS n ∷ Sub n n where
  IdS Z     = SNil
  IdS (S n) = KeepS (IdS n)

type family FinS (σ ∷ Sub n m)(x ∷ Fin m) ∷ Ty n where
  FinS (SSnoc σ a) FZ     = a
  FinS (SSnoc σ a) (FS x) = FinS σ x

type family TyS (σ ∷ Sub n m)(a ∷ Ty m) ∷ Ty n where
  TyS σ (TyVar x) = FinS σ x
  TyS σ (a :=> b) = TyS σ a :=> TyS σ b
  TyS σ (All b)   = All (TyS (KeepS σ) b)

data Con n where
  Nil     ∷ Con Z
  (:>)   ∷ Con n → Ty n → Con n
  SnocSt ∷ Con n → Con (S n)
infixl 4 :>

data Var ∷ ∀ n. Con n → Ty n → Type where
  VZ  ∷ Var (γ :> a) a
  VS  ∷ Var γ a → Var (γ :> b) a
  VS' ∷ ∀ n (γ ∷ Con n) a. Var γ a → Var (SnocSt γ) (WkTy a)

data Tm ∷ ∀ n. Con n → Ty n → Type where
  Var  ∷ Var γ a → Tm γ a
  Lam  ∷ Tm (γ :> a) b → Tm γ (a :=> b)
  App  ∷ Tm γ (a :=> b) → Tm γ a → Tm γ b
  Lam' ∷ Tm (SnocSt γ) b → Tm γ (All b)
  -- replace Proxy with singletons if you want
  App' ∷ Tm (γ ∷ Con n) (All b) → Proxy (a ∷ Ty n) → Tm γ (TyS (SSnoc (IdS n) a) b)

--------------------------------------------------------------------------------

type Ty0 = TyVar FZ
type Ty1 = TyVar (FS FZ)
type Ty2 = TyVar (FS (FS FZ))

v0 = Var VZ
v1 = Var (VS VZ)
v2 = Var (VS (VS VZ))

id' ∷ Tm Nil (All (Ty0 :=> Ty0))
id' = Lam' (Lam (Var VZ))

const' ∷ Tm Nil (All (All (Ty1 :=> Ty0 :=> Ty1)))
const' = Lam' (Lam' (Lam (Lam v1)))

apply ∷ Tm Nil (All (All ((Ty1 :=> Ty0) :=> Ty1 :=> Ty0)))
apply = Lam' (Lam' (Lam (Lam (App v1 v0))))

idApply ∷ Tm Nil (All (Ty0 :=> Ty0) :=> All (Ty0 :=> Ty0))
idApply = Lam (Lam' (Lam (App (App' (Var (VS (VS' VZ))) (Proxy @Ty0)) v0)))