how to limit a parameter to only one variant of a variant type

Question

Suppose I have two types, Vector2D and Vector3D and they are tagged (that's the correct term, right?), and I want to write a function that operates ONLY on Vector2D (or is vector(two) more correct here?), like this:

type two;
type three;
type vector('a) = 
  | Vector2D(float, float): vector(two)
  | Vector3D(float, float, float): vector(three);

let first = (a: vector(two)) => {
  switch(a) {
    | (x, y) => x +. y
  }
}

let second = (Vector2D(x, y)) => {
  x +. y
}

let third = ((x, y): vector(two)) => {
  x +.y
}

The first and second functions prohibit passing a Vector3D, just as I want but they raise a warning "This pattern matching is not exhaustive".

For first I'd like to know why this is not exhaustive, have I not limited the possible options to Vector2D here? For second I guess the reason is the same as for first, but how would it even be possible to solve the issue with this syntax?

As for third, this one does not compile because "This pattern matches ('a, 'b) but vector(two) was expected". Why does the compiler expect any tuple here? Is it not possible to use destructuring in function parameters?

EDIT:
Turns out there's an even simpler problem to demonstrate what I want

type state = Solid | Liquid
let splash = (object) => {
  switch(object) {
    | Liquid => "splashing sounds. I guess."
    | Solid => "" // this should not even be possible in the context of this function, and I want to compiler to enforce this
}

Answer 1

Concerning the GADT part, the issue here is that you are using bucklescript and its ancient 4.02.3 compiler version. For instance, the following code works perfectly fine in OCaml ≥ 4.03 :

type two = Two ; 
type three = Three ;
/* Never define abstract types when you want to use them as type level tags,
  your code will only works inside the module defining them, and then
  fail due to injectivity problems.
*/

type vector('a) = 
  | Vector2D(float, float): vector(two)
  | Vector3D(float, float, float): vector(three);

let sum_2 = (Vector2D(x,y)) => x +. y
let sum_3 = (Vector3D(x,y,z)) => x +. y +. z 
let sum_any = (type a, x: vector(a) ) => switch (x) {
  | Vector2D(x,y) => x +. y;
  | Vector3D(x,y,z) => x +. y +. z
}

But it will fail on 4.02.3 with an exhaustiveness warning(which should be treated as an error), because exhaustiveness check for GADTs with refutation clauses was only added in 4.03 .