The other day I read the article: "Recursive Subtyping revealed". A Functional Pearl by Gapeyev, Levin and Pierce. This is a bit of code I wrote to convince myself of the algorithm described in the paper.
You can get the article here
<code> 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