OCaml GADTs - pattern matching matches wrong type of argument

Question

I have to implement a perfectly balanced binary tree (or PBT for short) using generalized algebraic data types. I have understood how GADTs work in general and the (somewhat ugly) syntax that I have to use in order for it to work in OCaml. Then I have to implement some functions that work with it. Right now, I am having a problem with a function that takes two PBTs that have integers stored in their nodes and returns a PBT which stores in its nodes the sum of each of its corresponding nodes. Ok. Sounds easy enough. This is the code that I have written for the PBT data type:

(*Important in order to define the index of the level of our perfectly 
balanced tree*)
(*Natural numbers, Peano style (now with GADTs)*)
type zero = Zero
type _ succ = Succ : 'natural -> 'natural succ

(*Implementing the perfectly balanced binary tree - or PBTree - with GADTs*)
(*'a -> type of tree | _ -> index of level*)

type ('a, _) pbtree =
(*Base case: empty tree - level 0, rock-bottom*)
EmptyTree : ('a, zero) pbtree
(*Inductive case: regular PBTree - tree on the left, value, tree on the 
right*)          
| PBTree : ('a, 'natural) pbtree * 'a * ('a, 'natural) pbtree -> ('a, 
'natural succ) pbtree

It worked so far. The type compiles and I even managed to do a flip function (return the mirror image of a PBT). Now the real issue comes from this little brat:

let rec add : type int natural. 
(int, natural) pbtree -> (int, natural) pbtree -> (int, natural) pbtree =
function
| EmptyTree, EmptyTree -> EmptyTree
| PBTree(left1, value1, right1), PBTree(left2, value2, right2) -> 
PBTree((add left1 left2), value1 + value2, (add right1, right2))

Right where I do the pattern matching for the empty tree, it gives me the following error:

| EmptyTree, EmptyTree -> EmptyTree

Error: This pattern matches values of type 'a*'b
       but a pattern was expected which matches values of type
         (int, natural) pbtree

I can solve this if I make the function take a pair of trees. It would end up with the inductive case slightly changed and the function would look like this:

let rec add : type int natural. (int, natural) pbtree * (int, natural)         
pbtree -> (int, natural) pbtree =
function
| EmptyTree, EmptyTree -> EmptyTree
| PBTree(left1, value1, right1), PBTree(left2, value2, right2) -> 
PBTree((add (left1, left2)), value1 + value2, (add (right1, right2)))

However, this is not what I am supposed to do. My function needs to take two arguments. Even with this modification that solves the pair type conundrum, it will give the following error:

Error: This pattern matches values of type int/1805
        but an expression was expected of type int/1

So the first approach I took is the best I can do. My question is: why the pattern matching detects a pair when it is clearly not there? Why can it not detect two arguments like it normally should? Is it the way I wrote the function to detect that pattern?

If I, hypothetically, used the second approach in creating the function (the one where it took a pair of PBTs as an argument instead of two arguments - two PBTs), then why does it not recognise the integer value I am trying to give it to calculate? Is it maybe because it is too instrumented to work with?

I cannot understand what went wrong here and if I tried to modify the type to ease up on this syntactic restriction, then I risk creating a PBT that violates its own definition simply because of the type allowing branches which are unequal in size.

So again, I ask: why does pattern-matching fail to recognise the proper value types that I am giving it in the cases I presented?

Answer 1

The last error you're getting:

Error: This pattern matches values of type int/1805
       but an expression was expected of type int/1

is saying that there are two different int types that are not compatible, and gives you their internal ids so you can differentiate them. This error occurs because type int natural. creates two new locally abstract types scoped to the function, which will shadow any other types with those names within that scope. Resolving this error is simply done by not creating a locally abstract type named int. It will then constrain the type variable to the actual int type, as intended.

The other error:

Error: This pattern matches values of type 'a*'b
       but a pattern was expected which matches values of type
         (int, natural) pbtree

occurs because EmptyTree, EmptyTree actually is a pattern that matches a pair. In OCaml, tuples don't require parenthesis if they are delimited in other ways. So this, for example, is a valid (and extremely confusing) literal of type (int * int) list: [1, 2; 3, 4; 5, 6].

function is also restricted to only one argument, so in order to match on multiple arguments you need to use fun a b -> match a, b with.... Or you could just have add take a tuple directly.

Then finally you'll get an error because you use a comma to delimit function arguments in add right1, right2 which, again, will be interpreted as a tuple instead. It should be add right1 right2.

The final working (or at least compiling) add function is then:

let rec add : type natural. 
(int, natural) pbtree -> (int, natural) pbtree -> (int, natural) pbtree =
fun a b -> match a, b with
| EmptyTree, EmptyTree -> EmptyTree
| PBTree(left1, value1, right1), PBTree(left2, value2, right2) -> 
PBTree((add left1 left2), value1 + value2, (add right1 right2))