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 expression =
      | Var of variable
      | Layer of layer
 
    and state =
      | Fresh of int * int
      | Solved of expression
 
    and variable = state ref
 
    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 rec 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+IHVuaXQKICBlbmQKCm1vZHVsZSBQb2x5IChMIDogTEFZRVIpID0KICBzdHJ1Y3QKICAgIHR5cGUgZXhwcmVzc2lvbiA9CiAgICAgIHwgVmFyIG9mIHZhcmlhYmxlCiAgICAgIHwgTGF5ZXIgb2YgbGF5ZXIKICAgIAogICAgYW5kIHN0YXRlID0KICAgICAgfCBGcmVzaCBvZiBpbnQgKiBpbnQKICAgICAgfCBTb2x2ZWQgb2YgZXhwcmVzc2lvbgogICAgCiAgICBhbmQgdmFyaWFibGUgPSBzdGF0ZSByZWYKICAgIAogICAgYW5kIGxheWVyID0gZXhwcmVzc2lvbiBMLmxheWVyCiAgICAKICAgIHR5cGUgY29udGV4dCA9IGV4cHJlc3Npb24gTC5jb250ZXh0CiAgICAKICAgIGxldCBmcmVzaCA9CiAgICAgIGxldCBpZCA9IHJlZiAwIGluCiAgICAgICAgZnVuIGxldmVsIC0+IHJlZiAoRnJlc2ggKCFpZCwgbGV2ZWwpKQogICAgCiAgICBsZXQgcmVjIHJlYWQgdiA9CiAgICAgIG1hdGNoICF2IHdpdGgKICAgICAgfCBGcmVzaCBfIC0+IFZhciB2CiAgICAgIHwgU29sdmVkIChMYXllciBfIGFzIGUpIC0+IGUKICAgICAgfCBTb2x2ZWQgKFZhciB3KSAtPgogICAgICAgICBsZXQgZSA9IHJlYWQgdyBpbgogICAgICAgICB2IDo9IFNvbHZlZCBlIDsgZQogICAgCiAgICBsZXQgc2ltcGxpZnkgPSBmdW5jdGlvbgogICAgICB8IFZhciB2IC0+IHJlYWQgdgogICAgICB8IGUgLT4gZQogICAgCiAgICBsZXQgdGFncyB2ID0KICAgICAgbWF0Y2ggIXYgd2l0aAogICAgICB8IEZyZXNoIChpZCwgbHZsKSAtPiBpZCwgbHZsCiAgICAgIHwgXyAtPiBmYWlsd2l0aCAidmFyaWFibGUgbm90IGZyZXNoIgogICAgCiAgICBsZXQgb2NjdXJzIGN0eCB2ID0KICAgICAgbGV0IGlkLCBsdmwgPSB0YWdzIHYgaW4KICAgICAgbGV0IHJlYyBsb29wIGUgPQogICAgICAgIG1hdGNoIHNpbXBsaWZ5IGUgd2l0aAogICAgICAgIHwgTGF5ZXIgbCAtPiBMaXN0Lml0ZXIgbG9vcCAoTC5zbWFsbGVyIGN0eCBsKQogICAgICAgIHwgVmFyIHYgLT4KICAgICAgICAgICBsZXQgaWQnLCBsdmwnID0gdGFncyB2IGluCiAgICAgICAgICAgaWYgaWQgPSBpZCcgdGhlbgogICAgICAgICAgICAgZmFpbHdpdGggImluZmluaXRlIHJlY3Vyc2lvbiIKICAgICAgICAgICBlbHNlIGlmIGx2bCA8IGx2bCcgdGhlbgogICAgICAgICAgICAgdiA6PSBGcmVzaCAoaWQnLCBsdmwpCiAgICAgIGluIGxvb3AKICAgIAogICAgbGV0IHVuaWZ5IGN0eCA9CiAgICAgIGxldCByZWMgbG9vcCAoZTEsIGUyKSA9CiAgICAgICAgbWF0Y2ggc2ltcGxpZnkgZTEsIHNpbXBsaWZ5IGUyIHdpdGgKICAgICAgICB8IFZhciB2MSwgVmFyIHYyIC0+CiAgICAgICAgICAgbGV0IF8sIGx2bDEgPSB0YWdzIHYxIGluCiAgICAgICAgICAgbGV0IF8sIGx2bDIgPSB0YWdzIHYyIGluCiAgICAgICAgICAgaWYgbHZsMSA8IGx2bDIgdGhlbgogICAgICAgICAgICAgdjIgOj0gU29sdmVkIChWYXIgdjEpCiAgICAgICAgICAgZWxzZQogICAgICAgICAgICAgdjEgOj0gU29sdmVkIChWYXIgdjIpCiAgICAgICAgfCBWYXIgdiwgZSB8IGUsIFZhciB2IC0+CiAgICAgICAgICAgb2NjdXJzIGN0eCB2IGU7CiAgICAgICAgICAgdiA6PSBTb2x2ZWQgZQogICAgICAgIHwgTGF5ZXIgbDEsIExheWVyIGwyIC0+CiAgICAgICAgICAgbWF0Y2ggTC5nZW5lcmF0ZSBjdHggKGwxLCBsMikgd2l0aAogICAgICAgICAgIHwgU29tZSBlcXMgLT4gTGlzdC5pdGVyIGxvb3AgZXFzCiAgICAgICAgICAgfCBOb25lIC0+IGZhaWx3aXRoICJjYW5ub3QgdW5pZnkiCiAgICAgIGluIGxvb3AKICBlbmQK