Writing type inference algorithms in OCaml

Learning
10

Alright, I’ve been messing around some more with the code from Oleg’s site, but I seem to have run into a bug with the code on the site.

In particular, with the unify function:

     let rec unify : typ -> typ -> unit = fun t1 t2 ->
       if t1 == t2 then ()                   (* t1 and t2 are physically the same *)
       else match (t1,t2) with
       | (TVar ({contents = Unbound _} as tv),t') | (t',TVar ({contents = Unbound _} as tv)) -> 
           occurs tv t'; tv := Link t'
       | (TVar {contents = Link t1},t2) | (t1,TVar {contents = Link t2}) -> 
           unify t1 t2
       | (TArrow (tyl1,tyl2), TArrow (tyr1,tyr2)) ->
           unify tyl1 tyr1;
           unify tyl2 tyr2

Shouldn’t the case for handling links occur before the case for unbound type variables?

For example in the case where you have arguments as:

let t = fresh_var () in
(t, Tvar { contents = Link t })

i.e (the two arguments are semantically equal modulo a irrelevant Link, but because the link case is second, the code would run an occurs check and cause a failure)

1 Like