Compiler warning for non-exhaustive cases with GADT type arguments

1

I am trying to implement a GADT in ReScript, which has been working great so far. However, I keep getting this strange compiler warning for a specific case where the generic types that I want to use for my GADT do not seem to be matched correctly in a function that instantiates just one of them.

Here is a simplified example of my setup:

See in Playground

module Foo = {
  type one
  type two
}

module Bar = {

  type rec t<'a> =
  |	A(int): t<Foo.one>
  | B(string): t<Foo.two>
  
  let fun = (x: t<Foo.one>) => switch x {
  | A(_) => "a"
  }
}

As you can see, module Bar generalizes over Foo.one and Foo.two and fun() requires just t<Foo.one> for the pattern match but I still get the compiler warning “You forgot to handle a possible case here, for example: B _” – and B is of type t<Foo.two>. Why does the compiler want both types to be matched?

This is especially strange since I can define types ‘one’ and ‘two’ without a separate module in the parent scope or inside the Bar module and don’t get any compiler warnings:

See in Playground

type one
type two

module Bar = {

  type rec t<'a> =
  |	A(int): t<one>
  | B(string): t<two>
  
  let fun = (x: t<one>) => switch x {
  | A(_) => "a"
  }
}

Does anyone have an explanation for this warning? I am still new to ReScript and haven’t had much experience with type theory and GADTs yet, I just used to experiment with them for a prototype in Haskell that I am now trying to implement in ReScript.

If you are wondering why I want to use a separate module for the generic types in the first place: I use two GADTs in different files that both use the same types for their variant constructors.

2

This is caused by GADT pattern exhaustiveness checking and abstract types · Issue #7028 · ocaml/ocaml · GitHub . Fix is easy, just make the types concrete:

module Foo = {
  type one = One
  type two = Two
}
3

Thanks, the solution works fine! Have to read through the issue more closely, seems quite complicated, but good to know I wasn’t missing something in my code.

I am also going to look through the OCaml manual now in hope to better understand how GADTs are implemented in this type system: OCaml - Language extensions (in case someone needs this link)

1 Like