Pattern matching on a GADT fails

Question

I was playing around a bit more with ReasonML and found pattern matching on type t from the following example to not be working with the error

Error: This pattern matches values of type t(float) but a pattern was expected which matches values of type t(int) Type float is not compatible with type int

  type t('a) =
    | One: t(int)
    | Two: t(float);

  let x =
    fun
    | One => None
    | Two => None;

Now on some level this makes sense to me if this was about the return type of a function.

I found an answer (I think) to an equivalent question. For the second section the answer seems to be to kinda ignore the bound type of the constructor. Is the same possible in ReasonML?

P.s.: please correct me pedantically on terminology, I'm still learning what's what.

P.p.s.: I know I could work around the original problem by explicitly typing x but I really like the fun syntax because it's fun.

octachron octachron · Accepted Answer · 2019-11-21T12:06:55

The brief answer is that GADTs make the type system too expressive to be fully inferred. For instance, in your case, the following functions are both total (aka they handle all possible values of their input

let one = (One) => None
let two = (Two) => None

You can check that they are total by adding an explicit refutation clause in OCaml syntax (Reason syntax has not yet be updated to include those):

let one = function
| One -> None
| _ -> .

Here the dot . means that the pattern described on the left-hand side of the clause is syntactically valid, but does not refer to any actual value due to some type constraints.

Consequently, you need to tell the type checker that you intend to match of a value of type t(a) for any a, this needs to be done with locally abstract types:

let x (type a, (x:t(a))) = switch(x){
| One => None
| Two => None
}

With this locally abstract annotation, the type checker knows that it is not supposed to replace this variable a by a concrete type globally (aka it should consider that locally a is some unknown abstract type), but it can refine it locally when matching a GADT.

Strictly speaking, the annotation is only needed on the pattern, thus you can write

let x (type a) = fun
| (One:t(a)) => None
| Two => None

Note that for recursive functions with GADTs, you may need to go for the full explictly polymorphic locally abstract type notations:

type t(_) =
| Int(int): t(int)
| Equal(t('a),t('a)):t(bool)

let rec eval: type any. t(any) => any = fun
| Int(n) => n
| Equal(x,y) => eval(x) = eval(y)

where the difference is that eval is recursively polymorphic. See https://caml.inria.fr/pub/docs/manual-ocaml-4.09/polymorphism.html#sec60 .

EDIT: Annotating the return type

Another annotation that is often needed to avoid the dreaded "this type would escape its scope" is to add an annotation when leaving a pattern matching. A typical example would be the function:

let zero (type a, (x:t(a)) = switch (x){
| One => 0
| Two => 0.
}

There is an ambiguity here because inside the branch One, the typechecker knows that int=a but when leaving this context, it needs to choose one side of the equation or the other. (In this specific case, left at its own device the typechecker decides that (0: int) is the more logical conclusion because 0 is an integer and this type has not been in contact in any way with the locally abstract type a .)

This ambiguity can be avoided by using an explicit annotation, either locally

let zero (type a, (x:t(a))) = switch (x){
| One => ( 0 : a )
| Two => ( 0. : a )
}

or on the whole function

let zero (type a): t(a) => a = fun
| One => 0
| Two => 0.

Pattern matching on a GADT fails

2 Answers