relative_unify.ml

module Unify = struct
  type typ =
    | T_var of int
    | T_hole of hole ref
    | T_forall of typ
    | T_arrow of typ * typ

  and hole = H_open of int | H_link of typ * int
  
  let rec occurs h_off h in_off in_ =
    let occurs in_off in_ = occurs h_off h in_off in_ in
    match in_ with
    | T_var off -> (
        let off = in_off + off in
        match off < h_off with true -> failwith "escape check" | false -> ())
    | T_hole in_ -> (
        match !in_ with
        | H_open off -> (
            let diff = h_off - (in_off + off) in
            match diff > 0 with
            | true ->
                let off = off + diff in
                in_ := H_open off
            | false -> ())
        | H_link (in_, off) ->
            let in_off = in_off + off in
            occurs in_off in_)
    | T_forall return -> occurs in_off return
    | T_arrow (param, return) ->
        occurs in_off param;
        occurs in_off return

  let rec unify a_off a b_off b =
    match (a, b) with
    | T_var a, T_var b -> (
        let a = a_off + a in
        let b = b_off + b in
        match a = b with true -> () | false -> failwith "var clash")
    | T_hole a, b -> (
        match !a with
        | H_open off ->
            let a_off = a_off + off in
            unify_hole a_off a b_off b
        | H_link (a, off) ->
            let a_off = a_off + off in
            unify a_off a b_off b)
    | a, T_hole b -> (
        match !b with
        | H_open off ->
            let b_off = b_off + off in
            unify_hole b_off b a_off a
        | H_link (b, off) ->
            let b_off = b_off + off in
            unify a_off a b_off b)
    | T_forall a, T_forall b -> unify a_off a b_off b
    | T_arrow (a1, a2), T_arrow (b1, b2) ->
        unify a_off a1 b_off b1;
        unify a_off a2 b_off b2
    | _ -> failwith "type clash"

  and unify_hole h_off h in_off in_ =
    occurs h_off h in_off in_;
    h := H_link (in_, in_off - h_off)
end
(* example:
a : (A : Type) -> _C@0 -> (A@2 -> A@3) -> _C@0\2;
b : (X : Type) -> _D@0 ->         _B@0 -> _B@0\1;

a : (A : Type) -> _C@0   -> (A@2 -> A@3) -> _C@0\2;
b : (X : Type) -> _C@0\0 ->         _B@0 -> _B@0\1;

a : (A : Type) -> _C@0   -> (A@2 -> A@3)   ->           _C@0\2;
b : (X : Type) -> _C@0\0 -> (A@2 -> A@3)\0 -> (A@2 -> A@3)\0\1;

// the fancy step
a : 0 : _C@0\2
b : 0 : (A@2 -> A@3)\0\1
a : 2 : _C@0
b : 0 : (A@2 -> A@3)\0\1
_C := (A@2 -> A@3)\0\1\(in_off - h_off)
_C := (A@2 -> A@3)\0\1\-2

// done
a : (A : Type) -> (A@2 -> A@3)\0\1\-2   -> (A@2 -> A@3)   -> (A@2 -> A@3)\0\1\-2\2;
b : (X : Type) -> (A@2 -> A@3)\0\1\-2\0 -> (A@2 -> A@3)\0 -> (A@2 -> A@3)\0\1;


// meta step, just solve the offsets
a : (A : Type) -> (A@2 -> A@3)\-1 -> (A@2 -> A@3)   -> (A@2 -> A@3)\1;
b : (X : Type) -> (A@2 -> A@3)\-1 -> (A@2 -> A@3)\0 -> (A@2 -> A@3)\1;

// meta step, just expand the types
a : (A : Type) -> (A@1 -> A@2) -> (A@2 -> A@3) -> (A@3 -> A@4);
b : (X : Type) -> (A@1 -> A@2) -> (A@2 -> A@3) -> (A@3 -> A@4);

// meta step, just fix the names
a : (A : Type) -> (A@1 -> A@2) -> (A@2 -> A@3) -> (A@3 -> A@4);
b : (X : Type) -> (X@1 -> X@2) -> (X@2 -> X@3) -> (X@3 -> X@4);
*)