Hindley-Milner type inference in Lean 4. (WIP)

HindleyMilner.lean

import Lean.Data.AssocList
import Lean.Data.HashMap

abbrev Name := String

inductive Literal : Type
| LInt : Int -> Literal
| LBool : Bool -> Literal
deriving Repr, Inhabited, DecidableEq, Ord

inductive BinOp : Type
| Add | Sub | Mul | Eql
deriving Repr, Inhabited, DecidableEq, Ord

inductive Expr : Type
| Var : Name -> Expr
| App : Expr -> Expr -> Expr
| Lam : Name -> Expr -> Expr
| Let : Name -> Expr -> Expr -> Expr
| Lit : Literal -> Expr
| If : Expr -> Expr -> Expr -> Expr
| Fix : Expr -> Expr
| Op : BinOp -> Expr -> Expr -> Expr
deriving Repr, Inhabited, DecidableEq, Ord

abbrev Decls := Lean.AssocList Name Expr

structure Program where
  env : Decls
  expr : Expr

inductive TVar : Type
| TV : String -> TVar
deriving Repr, DecidableEq, Ord

inductive Typ : Type
| TVar : TVar -> Typ
| TCon : String -> Typ
| TArr : Typ -> Typ -> Typ
deriving Repr, DecidableEq, Ord

def typeInt : Typ := Typ.TCon "Int"
def typeBool : Typ := Typ.TCon "Bool"

inductive Scheme : Type
| Forall : List TVar -> Typ -> Scheme

abbrev TypeEnv := Lean.HashMap Name Scheme