The bidirectionally typed lambda calculus in OCaml using structural types

bidirectional-structural.ml

(* A bidirectionally-typed λ-calculus looks like:

  types  A,B ∷= base | A → B
  terms  M ∷= E | λx.M
  exprs  E ∷= x | E M | (M : A)

This is an exploration of how to encode this in OCaml using _structural_
typing (polymorphic variants & equirecursive types), rather than _nominal_
typing. *)

type var = string
type tp = Base | Fn of tp * tp
type ctx = (var * tp) list

(* I'd like to be able to write THIS:

  type expr = [ `Var of var | `App of expr * term | `Asc of tp * term ]
  and term = [ expr | `Lam of var * term ]

But this produces the error message:

  Error: The type constructor expr is not yet completely defined.

So instead, I need to tie the knot explicitly: *)
type ('t,'e) exprF = [ `Var of var | `App of 'e * 't | `Asc of tp * 't ]
type ('t,'e) termF = [ ('t,'e) exprF | `Lam of var * 't ]
type term = (term,expr) termF
and  expr = (term,expr) exprF

(* This works! Now, let's write a pair of mutually recursive functions over
terms and exprs - say, a bidirectional typechecker:

val infer: ctx -> expr -> tp
val check: ctx -> tp -> term -> unit *)
exception TypeError
let rec infer (ctx: ctx): expr -> tp = function
  | `Var x -> List.assoc x ctx
  | `App (e,m) -> (match infer ctx e with
                   | Fn(a,b) -> check ctx b m; a
                   | _ -> raise TypeError)
  | `Asc (a,m) -> check ctx a m; a

and check (ctx: ctx) (tp: tp) (term: term): unit =
  match tp, term with
  | Fn(a,b), `Lam(x,m) -> check ((x,a)::ctx) b m
  | _, `Lam _ -> raise TypeError
  (* I've now handled all the terms that aren't also exprs, so `e` must be an
   * expr. But to convince OCaml's typechecker of this, we need a slightly
   * obscure (to me) feature of OCaml patterns: polymorphic variant abbreviation
   * patterns. If foo is a polymorphic variant type, then #foo matches any value
   * of that type. See https://caml.inria.fr/pub/docs/manual-ocaml/patterns.html
   *)
  | expected, (#expr as e) ->
     let inferred = infer ctx e in
     if inferred = expected then () else raise TypeError