Recursive subtyping revealed

type at =
    |Top |Nat |Bool |Even | Odd
    |Times of ( at * at )
    |Arrow of ( at * at )
    |Mu of ( string * at )
    |Var of string

module S = SortedList.Make(
    struct
        type t = (at * at)
        let compare = compare
        let hash = Hashtbl.hash
        let equal (t1,t2) (s1,s2)  =
          ((compare t1 s1) = 0) && ((compare t2 s2) = 0)
    end
    )

module B = SortedList.Make(
    struct
        type t = string
        let compare = compare
        let hash = Hashtbl.hash
        let equal t s  = (compare t s) = 0
    end
    )

(* canonical substitution *)
let rec sub x t = function
    |Var s when s = x -> t
    |Times(t1,t2) -> Times(sub x t t1,sub x t t2)
    |Arrow(t1,t2) -> Arrow(sub x t t1,sub x t t2)
    |_ as t -> t

(* free variables *)
let rec fv = function
    |Var t -> B.add t B.empty
    |Times(t1,t2) -> B.cup (fv t1) (fv t2)
    |Arrow(t1,t2) -> B.cup (fv t1) (fv t2)
    |_ -> B.empty

exception Undef of (at * at)

let rec subtype (a,s,t) =
    if s = t then S.add (s,t) a
    else if List.mem (s,t) a then a
    else
        let a0 = S.add (s,t) a in
        match (s,t) with
        |_,Top -> a0
        |Mu(x,s1),_ ->
                subtype(a0,sub x s s1,t)
        |_,Mu(x,t1) ->
                subtype(a0,s,sub x t t1)
        |Times(s1,s2),Times(t1,t2) ->
                let a1 = subtype(a0,s1,t1) in
                subtype(a1,s2,t2)
        |Arrow(s1,s2),Arrow(t1,t2) ->
                let a1 = subtype(a0,t1,s1) in
                subtype(a1,s2,t2)
        |_ -> raise (Undef (s,t))

let (<:) t s = subtype([],t,s);;

(* ------------- parser -------------------*)
open Camlp4.PreCast
module TypeGram = MakeGram(Lexer)

let expression = TypeGram.Entry.mk "expression"

EXTEND TypeGram
  GLOBAL: expression;

  expression: [
      "arrow" [ e1 = SELF; "->"; e2 = SELF -> Arrow(e1, e2) ]
    | "prod"  [ e1 = SELF; "x";  e2 = SELF -> Times(e1, e2) ]
    | "var" [
          "Nat" -> Nat
        | "Even" -> Even
        | "Odd" -> Odd
        | "Bool" -> Bool
        | "T" -> Top
        | "mu"; `UIDENT x ; "." ; e = SELF -> Mu(x,e)
        | `UIDENT x -> Var x
        | "("; e = SELF; ")" -> e
    ]
  ];

END

let p s = TypeGram.parse_string expression (Loc.mk "<string>") s
(* ------------- parser -------------------*)

(* Examples *)
let a = p "mu X . ( Nat -> (Nat x X))" ;;
let b = p "Nat -> (Nat x (mu X . (Nat -> (Nat x X))))" ;;

let d = p "mu X . ( Nat -> (Even x X))" ;;
let e = p "mu X . ( Even -> (Nat x X))" ;;

(* suppose Even is subtype of Nat *)
let (<::) t s = subtype([Even,Nat],t,s);;
d <:: e;;