title: OCaml GADTs - pattern matching matches wrong type of argument
body: <p>I have to implement <strong>a perfectly balanced binary tree</strong> (or PBT for short) using <strong>generalized algebraic data types</strong>. 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:</p>
  
  <pre><code>(*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 -&gt; 'natural succ
  
  (*Implementing the perfectly balanced binary tree - or PBTree - with GADTs*)
  (*'a -&gt; type of tree | _ -&gt; 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 -&gt; ('a, 
  'natural succ) pbtree
  </code></pre>
  
  <p>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:</p>
  
  <pre><code>let rec add : type int natural. 
  (int, natural) pbtree -&gt; (int, natural) pbtree -&gt; (int, natural) pbtree =
  function
  | EmptyTree, EmptyTree -&gt; EmptyTree
  | PBTree(left1, value1, right1), PBTree(left2, value2, right2) -&gt; 
  PBTree((add left1 left2), value1 + value2, (add right1, right2))
  </code></pre>
  
  <p>Right where I do the pattern matching for the empty tree, it gives me the following error:</p>
  
  <pre><code>| EmptyTree, EmptyTree -&gt; EmptyTree
  
  Error: This pattern matches values of type 'a*'b
         but a pattern was expected which matches values of type
           (int, natural) pbtree
  </code></pre>
  
  <p>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:</p>
  
  <pre><code>let rec add : type int natural. (int, natural) pbtree * (int, natural)         
  pbtree -&gt; (int, natural) pbtree =
  function
  | EmptyTree, EmptyTree -&gt; EmptyTree
  | PBTree(left1, value1, right1), PBTree(left2, value2, right2) -&gt; 
  PBTree((add (left1, left2)), value1 + value2, (add (right1, right2)))
  </code></pre>
  
  <p>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:</p>
  
  <pre><code>Error: This pattern matches values of type int/1805
          but an expression was expected of type int/1
  </code></pre>
  
  <p>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?</p>
  
  <p>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?</p>
  
  <p>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.</p>
  
  <p>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?</p>