Unable to refute impossible GADT pattern when phantom types belong to a module

Community
1

I have the following code, which complies successfully:

type foo
type bar

type _ kind =
  | Foo : foo kind
  | Bar : bar kind

type _ t =
  | With_kind : 'a kind -> 'a t
  | Foo2 : foo t

let what_is_it (t : foo t) =
  match t with
  | With_kind Foo -> "this is a foo"
  | Foo2 -> "this is a foo too"
  | _ -> .

Nothing surprising here: the only valid ways to construct a foo t are via Foo2 or With_kind with a foo kind, which can only be constructed with Foo.

However, if I replace the phantom type declarations with an included module, like so:

module Phantom = struct
  type foo
  type bar
end

include Phantom

I am met with the following bizarre compilation error:

24 |   | _ -> .
         ^
Error: This match case could not be refuted.
       Here is an example of a value that would reach it: With_kind Bar

What’s more, trying to call this function with the unmatched pattern leads to an additional, contradictory error:

26 | let _ = what_is_it (With_kind Bar)      
                                   ^^^       
Error: This expression has type bar kind     
       but an expression was expected of type foo kind                                    
       Type bar is not compatible with type foo

Any insight as to what’s happening here? I’d like to avoid using assert false or failwith to handle this case, and my understanding (along with the compiler’s on line 26) is that this case really is impossible.

1 Like
2

Change

module Phantom = struct
  type foo
  type bar
end

to this:

module Phantom = struct
  type foo = Foo
  type bar = Bar
end

and it will work.

You can see this issue for more info: When pattern matching on GADTs, abstract (phantom) types are not considered structurally different from concrete ones · Issue #7360 · ocaml/ocaml · GitHub

3 Likes