module type LAYER =
  sig
    type 'a layer
    type 'a context
 
    val smaller : 'a context -> 'a layer -> 'a list
    val generate : 'a context -> 'a layer * 'a layer -> ('a * 'a) list option
  end
 
module type POLY =
  sig
    type layer
    type context
    type variable
 
    type expression =
      | Var of variable
      | Layer of layer
 
    val fresh : int -> variable
    val read : variable -> expression
    val occurs : variable -> expression -> unit
    val unify : context -> expression * expression -> unit
  end
 
module Poly (L : LAYER) =
  struct
    type variable = private
      [ `Fresh of int * int
      | `Solved of expression
      ] ref
 
    and expression =
      | Var of variable
      | Layer of layer
 
    and layer = expression L.layer
 
    type context = expression L.context
 
    let fresh =
      let id = ref 0 in
        fun level -> ref (`Fresh (!id, level))
 
    let rec read v =
      match !v with
      | `Fresh _ -> Var v
      | `Solved (Layer _ as e) -> e
      | `Solved (Var w) ->
         let e = read w in
         v := Solved e ; e
 
    let simplify = function
      | Var v -> read v
      | e -> e
 
    let tags v =
      match !v with
      | `Fresh (id, lvl) -> id, lvl
      | _ -> failwith "variable not fresh"
 
    let occurs ctx v =
      let id, lvl = tags v in
      let loop e =
        match simplify e with
        | Layer l -> List.iter loop (L.smaller ctx l)
        | Var v ->
           let id', lvl' = tags v in
           if id = id' then
             failwith "infinite recursion"
           else if lvl < lvl' then
             v := Fresh (id', lvl)
      in loop
 
    let unify ctx =
      let rec loop (e1, e2) =
        match simplify e1, simplify e2 with
        | Var v1, Var v2 ->
           let _, lvl1 = tags v1 in
           let _, lvl2 = tags v2 in
           if lvl1 < lvl2 then
             v2 := Solved (Var v1)
           else
             v1 := Solved (Var v2)
        | Var v, e | e, Var v ->
           occurs ctx v e;
           v := Solved e
        | Layer l1, Layer l2 ->
           match L.generate ctx (l1, l2) with
           | Some eqs -> List.iter loop eqs
           | None -> failwith "cannot unify"
      in loop
  end
 

bW9kdWxlIHR5cGUgTEFZRVIgPQogIHNpZwogICAgdHlwZSAnYSBsYXllcgogICAgdHlwZSAnYSBjb250ZXh0CiAgICAKICAgIHZhbCBzbWFsbGVyIDogJ2EgY29udGV4dCAtPiAnYSBsYXllciAtPiAnYSBsaXN0CiAgICB2YWwgZ2VuZXJhdGUgOiAnYSBjb250ZXh0IC0+ICdhIGxheWVyICogJ2EgbGF5ZXIgLT4gKCdhICogJ2EpIGxpc3Qgb3B0aW9uCiAgZW5kCgptb2R1bGUgdHlwZSBQT0xZID0KICBzaWcKICAgIHR5cGUgbGF5ZXIKICAgIHR5cGUgY29udGV4dAogICAgdHlwZSB2YXJpYWJsZQogICAgCiAgICB0eXBlIGV4cHJlc3Npb24gPQogICAgICB8IFZhciBvZiB2YXJpYWJsZQogICAgICB8IExheWVyIG9mIGxheWVyCiAgICAKICAgIHZhbCBmcmVzaCA6IGludCAtPiB2YXJpYWJsZQogICAgdmFsIHJlYWQgOiB2YXJpYWJsZSAtPiBleHByZXNzaW9uCiAgICB2YWwgb2NjdXJzIDogdmFyaWFibGUgLT4gZXhwcmVzc2lvbiAtPiB1bml0CiAgICB2YWwgdW5pZnkgOiBjb250ZXh0IC0+IGV4cHJlc3Npb24gKiBleHByZXNzaW9uIC0+IHVuaXQKICBlbmQKCm1vZHVsZSBQb2x5IChMIDogTEFZRVIpID0KICBzdHJ1Y3QKICAgIHR5cGUgdmFyaWFibGUgPSBwcml2YXRlCiAgICAgIFsgYEZyZXNoIG9mIGludCAqIGludAogICAgICB8IGBTb2x2ZWQgb2YgZXhwcmVzc2lvbgogICAgICBdIHJlZgogICAgCiAgICBhbmQgZXhwcmVzc2lvbiA9CiAgICAgIHwgVmFyIG9mIHZhcmlhYmxlCiAgICAgIHwgTGF5ZXIgb2YgbGF5ZXIKICAgIAogICAgYW5kIGxheWVyID0gZXhwcmVzc2lvbiBMLmxheWVyCiAgICAKICAgIHR5cGUgY29udGV4dCA9IGV4cHJlc3Npb24gTC5jb250ZXh0CiAgICAKICAgIGxldCBmcmVzaCA9CiAgICAgIGxldCBpZCA9IHJlZiAwIGluCiAgICAgICAgZnVuIGxldmVsIC0+IHJlZiAoYEZyZXNoICghaWQsIGxldmVsKSkKICAgIAogICAgbGV0IHJlYyByZWFkIHYgPQogICAgICBtYXRjaCAhdiB3aXRoCiAgICAgIHwgYEZyZXNoIF8gLT4gVmFyIHYKICAgICAgfCBgU29sdmVkIChMYXllciBfIGFzIGUpIC0+IGUKICAgICAgfCBgU29sdmVkIChWYXIgdykgLT4KICAgICAgICAgbGV0IGUgPSByZWFkIHcgaW4KICAgICAgICAgdiA6PSBTb2x2ZWQgZSA7IGUKICAgIAogICAgbGV0IHNpbXBsaWZ5ID0gZnVuY3Rpb24KICAgICAgfCBWYXIgdiAtPiByZWFkIHYKICAgICAgfCBlIC0+IGUKICAgIAogICAgbGV0IHRhZ3MgdiA9CiAgICAgIG1hdGNoICF2IHdpdGgKICAgICAgfCBgRnJlc2ggKGlkLCBsdmwpIC0+IGlkLCBsdmwKICAgICAgfCBfIC0+IGZhaWx3aXRoICJ2YXJpYWJsZSBub3QgZnJlc2giCiAgICAKICAgIGxldCBvY2N1cnMgY3R4IHYgPQogICAgICBsZXQgaWQsIGx2bCA9IHRhZ3MgdiBpbgogICAgICBsZXQgbG9vcCBlID0KICAgICAgICBtYXRjaCBzaW1wbGlmeSBlIHdpdGgKICAgICAgICB8IExheWVyIGwgLT4gTGlzdC5pdGVyIGxvb3AgKEwuc21hbGxlciBjdHggbCkKICAgICAgICB8IFZhciB2IC0+CiAgICAgICAgICAgbGV0IGlkJywgbHZsJyA9IHRhZ3MgdiBpbgogICAgICAgICAgIGlmIGlkID0gaWQnIHRoZW4KICAgICAgICAgICAgIGZhaWx3aXRoICJpbmZpbml0ZSByZWN1cnNpb24iCiAgICAgICAgICAgZWxzZSBpZiBsdmwgPCBsdmwnIHRoZW4KICAgICAgICAgICAgIHYgOj0gRnJlc2ggKGlkJywgbHZsKQogICAgICBpbiBsb29wCiAgICAKICAgIGxldCB1bmlmeSBjdHggPQogICAgICBsZXQgcmVjIGxvb3AgKGUxLCBlMikgPQogICAgICAgIG1hdGNoIHNpbXBsaWZ5IGUxLCBzaW1wbGlmeSBlMiB3aXRoCiAgICAgICAgfCBWYXIgdjEsIFZhciB2MiAtPgogICAgICAgICAgIGxldCBfLCBsdmwxID0gdGFncyB2MSBpbgogICAgICAgICAgIGxldCBfLCBsdmwyID0gdGFncyB2MiBpbgogICAgICAgICAgIGlmIGx2bDEgPCBsdmwyIHRoZW4KICAgICAgICAgICAgIHYyIDo9IFNvbHZlZCAoVmFyIHYxKQogICAgICAgICAgIGVsc2UKICAgICAgICAgICAgIHYxIDo9IFNvbHZlZCAoVmFyIHYyKQogICAgICAgIHwgVmFyIHYsIGUgfCBlLCBWYXIgdiAtPgogICAgICAgICAgIG9jY3VycyBjdHggdiBlOwogICAgICAgICAgIHYgOj0gU29sdmVkIGUKICAgICAgICB8IExheWVyIGwxLCBMYXllciBsMiAtPgogICAgICAgICAgIG1hdGNoIEwuZ2VuZXJhdGUgY3R4IChsMSwgbDIpIHdpdGgKICAgICAgICAgICB8IFNvbWUgZXFzIC0+IExpc3QuaXRlciBsb29wIGVxcwogICAgICAgICAgIHwgTm9uZSAtPiBmYWlsd2l0aCAiY2Fubm90IHVuaWZ5IgogICAgICBpbiBsb29wCiAgZW5kCg==