ML can't unify 'a with int

Question

The exercise is to code a function in ML that deletes an element from a binary search tree. Here's the code:

datatype 'a tree = Lf | Br of 'a * 'a tree * 'a tree;

fun deleteTop (Br(_, Lf, t2)) = t2
  | deleteTop (Br(_, t1, Lf)) = t1
  | deleteTop (Br(_, Br(v, u1, u2), t2)) =
    Br(v, deleteTop (Br(v, u1, u2)), t2);

fun delete (Lf, k : string) = Lf
  | delete (Br((a,b),t1,t2), k) =
    if a=k then deleteTop(Br((a,b),t1,t2))
    else if k<a then Br((a,b),delete(t1,k),t2)
            else Br((a,b),t1,delete(t2,k));

When I load this into Poly/ML it warns me of incomplete pattern matching in deleteTop but that doesn't matter because delete only ever passes deleteTop a branch.

val deleteTop = fn: 'a tree -> 'a tree
val delete = fn: (string * 'a) tree * string -> (string * 'a) tree

I created a (string * int) tree and ran

> delete(a,"they");
Error-Type error in function application.
   Function: delete : (string * 'a) tree * string -> (string * 'a) tree
   Argument: (a, "they") : (string * int) tree * string
   Reason:
      Can't unify (string * 'a) tree with (string * int) tree
      (Different type constructors)
Found near delete (a, "they")
Static Errors

Let me re-iterate one of those lines:

Can't unify (string * 'a) tree with (string * int) tree

Why can't ML unify 'a with int?

Answer 1

You can get a message like that if you have redefined tree and delete at the top level since you defined a. It's complaining that the tree in a is not the same as the tree in delete.

For example

> datatype 'a t = T of 'a;
datatype 'a t = T of 'a
> val x = T 1;
val x = T 1: int t
> datatype 'a t = T of 'a;
datatype 'a t = T of 'a
> val T y = x;
Pattern and expression have incompatible types.
   Pattern: T y : 'a t
   Expression: x : int t
   Reason: Can't unify 'a t with int t (Different type constructors)
Found near val T y = x
Static Errors
>