Scope safe lambda calculus using type level programming in Haskell

TypeLevelScopeSafety.hs

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE OverloadedLabels #-}

import GHC.TypeLits
import Data.Kind
import GHC.OverloadedLabels
import Data.Function ((&))

type family Equal x y where
  Equal x x = True
  Equal x y = False

class Elem s ss
instance ElemB (Equal s s') s s' ss => Elem s (s' : ss)

class ElemB b s s' ss
instance ElemB True s s ss
instance Elem s ss => ElemB False s s' ss

type Lam :: [Symbol] -> Type
data Lam fvs where
  Var :: (Elem s ss) => SSymbol s -> Lam ss
  Abs :: SSymbol s -> Lam (s : ss) -> Lam ss
  App :: Lam ss -> Lam ss -> Lam ss
  LetRec :: Bindings ss1 ss3 -> Lam ss3 -> Lam ss1
deriving instance Show (Lam fvs)

data Bindings ss1 ss2 where
  Module :: Bindings ss ss
  (:=) :: SSymbol s -> Lam ss2 -> Bindings (s : ss1) ss2 -> Bindings ss1 ss2
deriving instance Show (Bindings ss1 ss2)

instance forall s s'. (KnownSymbol s', s ~ s') => IsLabel s (SSymbol s') where
  fromLabel = SSymbol @s

prelude
  = Module
  & #id    := Abs #x (Var #x)
  & #const := Abs #x (Abs #y (Var #x))
  & #x1    := Var #x2
  & #x2    := Var #x1