val same_shape : 'a tree -> 'a tree -> bool = <fun>

The problem is when I try to compare an int tree with a string tree, I get the following error

Error: This expression has type string but an expression was expected of type
int

I’m pretty sure that this is because the function is compiled as 'a tree -> 'a tree -> bool, but I do not want the node value to matter. So my question is, how can I write my function as a 'a tree -> 'b tree -> bool function?

Hi, OCaml infers types according to the implementation. In this case it unified the 'a and the 'b types into a single type because it saw that the implementation is treating them as the same type.

This means you have a bug in your implementation. Check this: same_shape y2 y2

Just to be clear, the annotationsof (t1 : 'a tree) (t2 : 'b tree) were actually ignored during the typechecking process. If you want annotations that will actually cause a type error, use an interface (either a file or a signature). E.g.,

module M : sig
val same_shape : _ tree -> _ tree -> bool
end = struct
let rec same_shape t1 t2 = match t1, t2 with
| Leaf, Node (_, _, _) | Node (_, _, _), Leaf -> false
| Node (_, x1, y1), Node (_, x2, y2) -> same_shape x1 x2 && same_shape y1 y2
| Leaf, Leaf -> true
end

I wondered, reading your explanation, if that was all there was to it. So …

# let rec same_shape : 'a 'b .'a tree -> 'b tree -> bool = fun t1 t2 ->
match t1, t2 with
| Leaf, Node(_, _, _) | Node(_, _, _), Leaf -> false
| Node(_, x1, y1), Node(_, x2, y2) -> same_shape x1 x2 && same_shape y2 y2
| Leaf, Leaf -> true;;
val same_shape : 'a tree -> 'b tree -> bool = <fun>

The only change was to put the type-constraint on the recursive function definition directly. So even if one intended the bug you found, you could still get the indifference to the node-type.

Obviously this isn’t the right way to do it, and the natural way is the one that will expose the bug.

The annotation is not ignored during typechecking, it is just perfectly valid to infer that 'a = 'b from the call to

same_shape y1 y2

It is the issue with unification type variables which have a semantics that is not well adapted for debugging purpose.
Locally abstract types are a better fit than unification variables for such purpose. For instance,

let same_shape (type a b) =
let rec same_shape (t1 : a tree) (t2 : b tree) =
match t1, t2 with
| Leaf, Node(_, _, _) | Node(_, _, _), Leaf -> false
| Node(_, x1, y1), Node(_, x2, y2) -> same_shape x1 x2 && same_shape y2 y2
| Leaf, Leaf -> true
in
same_shape

fails with

6 | | Node(_, x1, y1), Node(_, x2, y2) -> same_shape x1 x2 && same_shape y2 y2
^^
Error: This expression has type b tree but an expression was expected of type
a tree
Type b is not compatible with type a