GADT exhaustiveness

Learning
1

Hello !

I’ve got some warnings when using pattern matching with gadt : the compiler does not seems able to detect the exhaustiveness when the type is private.

Here is a minimal example :

module Num = struct
  type t
end


type _ dataFormat =
  | Date:   Num.t dataFormat
  | Number: Num.t dataFormat
  | String: string dataFormat
  | Bool:   bool dataFormat

let test: Num.t dataFormat -> unit = function
| Number -> ()
| Date -> ()
| _ -> .

The compilation fail with the message

Error: This match case could not be refuted.
Here is an example of a value that would reach it: String

Is there a known workaround for ensuring that the pattern is exhaustive without make the type public ?

Thanks a lot !

1 Like
2

There is no workaround : nothing prevents the type Num.t to be the type string. Hence the case String cannot be refuted, when Num.t is abstract.

3

It’s sad !

I thought that an abstract type will be considered as a new type, and different for any other existing types, as said in the documentation :

Names that are defined as abstract types in a signature can be implemented in a matching structure by any kind of type definition (provided it has the same number of type parameters). The exact implementation of the type will be hidden to the users of the structure. In particular, if the type is implemented as a variant type or record type, the associated constructors and fields will not be accessible to the users; if the type is implemented as an abbreviation, the type equality between the type name and the right-hand side of the abbreviation will be hidden from the users of the structure. Users of the structure consider that type as incompatible with any other type: a fresh type has been generated.

4

So, this is a case where the typechecker is not as clever as it could be, and for rather good reasons.

If you remove the submodule, i.e, replace Num.t by

type num

then it will do what you expect. This is because the type num is both fresh and abstract, and thus the typechecker can prove that it is different than any other type.

However, when the type comes from a module, the typechecker will simply consider that the type is abstract, but not fresh, as if it was provided by a module like this:

module Num : sig type t end = struct 
  type t = .....
end

Here, the type Num.t might be equal to any type, even if the definition is not exposed.

To demonstrate that a type is different than any other type, the only way is to show what it is, for example with a private type.

module Num : sig type t = private ... end = struct
  type t = ...
end
2 Likes
5

To give an example where a similar pattern matching is really not exhaustive, it is possible to hide equality between types using a module signature, while still making it possible to reveal this equality at a later date. For instance:

type (_,_) eq = Eq: ('a,'a) eq
module Num: sig
  type t
  val eq: (t,string) eq
end =
struct
  type t = string
   let  eq = Eq
end

The the pattern matching in test is then not exhaustive
because the following expression is well-typed:

let () = match Num.eq with Eq -> test String
1 Like
6

Hello,

Thanks everybody for your answers and explanations. I’m not a type guru, and do not understand very well how the compiler infer the type with gadts : this seems conterintuitve to check the type once it have been hiden in the signature.

@Drup :

Here, the type Num.t might be equal to any type, even if the definition is not exposed.

On an other side, we could expect Num.t to be different to any other type, even if the definition declare the type as an alias to another one.

@octachron: the example you give with the Eq constructor make sense at first sight, but it does not give more information to the type itself : replacing string by float still does not compile the pattern exhaustiveness. Again, here, I could argue that the langage could, by default, consider an abstract type as completely opaque, and give a way to reveal it type with a trick like you describe.

Anyway, I’m not here to complain about the language : I would be happy to completely hide a type and still ensure that the code I write is valid, but I can live without. I understand the error given by the compiler as a choice in the langage design, and I’m not here for rewriting OCaml !

7

When you have an abstract type, it is existentially quantified: you could read it as “there is a type t such that M.t = t and …”. The only things you know about t are contained in the module signature, but with GADT you can sometime deduce (as in @octachron example) in some context that your abstract type is in fact equal to another type (in this case string). Therefore the fact that Num.t is abstract is not a sufficient condition to conclude that it is never equal to string. The type checker must prove that in any context Num.t is distinct from string, but it cannot prove this from the premise that Num.t is abstract.

type (_,_) eq = Eq : ('a, 'a) eq

module M : sig
  type t
  val eq : (t, string) eq
end = struct
  type t = string
  let eq = Eq
end

type _ data = A : M.t data | B : string data

let test : M.t data -> char = function
  | A -> 'a'
  | B -> 'b'

here M.t is abstract, but in some context (as illustrated below) we can prove that M.t = string.

(* ill-typed expression *)
test B;;
Error: This expression has type string data
       but an expression was expected of type M.t data
       Type string is not compatible with type M.t

(* well-typed expression *)
match M.eq with Eq -> test B;;
- : char = 'b'

By the way, without GADT, I think we can never prove that an abstract type is equal to another type. Therefore It may be interesting to improve the refutation algorithm in such a way that (as in your example) if the module signature doesn’t contain a GADT type (which should be a common situation in an OCaml. code base), then the abstract type can never be compatible with any other type.

Maybe you can open an issue on Mantis to have a confirmation from OCaml type system experts that my criterion is correct.

8

Functors can also hide temporarily type equalities:

module F(X : sig type t end) =
struct
    type _ t = A : string t | B : X.t t
    let unsafe: string t -> _ = function A -> ()
end
module M = F(struct type t = string end);;
M.unsafe B;;
1 Like
9

Your example is interesting but I don’t think this is exactly the same situation. In this case X is a functor parameter but not a value (even if in OCaml modules are not really first class values). Here the functor signature say that the module type of X must be a subtype of sig type t end and therefore the type checker complains that the pattern matching is not exhaustive because we can have X.t = string (sig type t = string end <: sig type t end).

In your example, when we instantiate the functor F with X = struct type t = string we know that M.B : string t, so M.unsafe B is well-typed and M.unsafe is really unsafe. But if we put constraint signature on the functor, it can become safe:

module F(X : sig type t end) : sig 
  type _ t 
  val unsafe : string t -> unit
  val a : string t
end  = struct
    type _ t = A : string t | B : X.t t
    let unsafe: string t -> _ = function A -> ()
    let a = A
end

module M = F(struct type t = string end);;
module M : sig type _ t val unsafe : string t -> unit val a : string t end

Functors do not really hide type equalities because a parameter is not a real module (it’s just a variable name as in any function definition), but there is a bounded universal quantification over module signatures (for all module whose signature is less than sig type t end) and when we instantiate the functor we can reveal a concrete type.

10

Another example with neither functors nor GADTs:

module rec M: sig
  type t
  val exfiltrate: unit -> string N.t
end = struct
  type t = string
  let exfiltrate () = N.B
end
and N: sig
  type _ t = A: string t | B: M.t t
  val unsafe: string t -> unit
end = struct
  type _ t = A: string t | B: M.t t
  let unsafe: string t -> unit = function A -> ()
end
let fail = N.unsafe (M.exfiltrate ())
11

Hum, I think that N.t is a GADT :wink: That was already the case with your previous example, the type _ t defined by your functor was a GADT.

I realise that my argumentation was a bit confuse. In both situations, Chimrod one and yours, the type checker complained that the pattern matching over a GADT is not exhaustive.

In the Chimrod case the abstract type was existentially quantified, and I conjectured that if there was no GADT in the module signature then it would not be possible to unify the abstract type with a concrete one (namely string in the examples). Note, I’m not very sure I was right, so that’s why I said it should be asked to type system experts.

In your functor example, the abstract type was universally quantified and so the two problems are not formally equivalent and this criterion can not be applied to it. Indeed, at unsafe definition site the type checker can not prove that the functor will never be instantiated with X.t = string.

In your present case, there is effectively an existential quantification on M.t (M is a path) but in module M signature we find the type unit -> string N.t and N.t is a GADT, and so the criterion I proposed doesn’t apply.

12

It is also possible to export type equalities with functors rather than a GADT:

module M: sig 
   type t
   module F: functor(X: sig type 'a x val x: string x end) -> sig val x: t X.x end
end =
struct
  type t = string
  module F(X: sig type 'a x val x: string x end ): sig val x: t X.x end = 
  struct 
    let x = X.x
   end
end

type _ t = A: string t | B: M.t t

let unsafe: M.t t -> unit = function B -> ()
let a = let module K = M.F(struct type 'a x = 'a t let x = A end) in K.x

let () = unsafe a
1 Like
13

Your right and your example contradicts my criterion. In fact the problem here is that there is a universal quantification over a parametric type (namely 'a x) with functor M.F and when you instantiate with the GADT it exports the type equality.

Maybe the criterion can be refined : since there is a universal quantification over a parametric type, there may be a GADT and so the pattern matching must be considered non exhaustive.

Do you know other patterns that can export type equality? Or, even better, do you know if the problem is undecidable?

14

It would be undecidable in general: type inhabitation for GADTs is undecidable, and it is perfectly possible to write a functor that only export a type equality if a specific type is inhabited.

15

Do you have an example in mind?

The intuition behind my conjecture was that the essence of GADT is the equality GADT you wrote (as described on section 8.2 of these lecture notes). As @yallop and @lpw25 said, we can encode all GADTs using the equality GADT and regular ADTs.

type (_, _) eql = Refl : ('a, 'a) eql

type 'a adt =
  | S of ('a, string) eql
  | F of ('a, float) eql

type 'a gadt =
  | Sg : string gadt
  | Fg : float gadt

(* these two type are indeed isomorphic *)
let adt_to_gadt : type a. a adt -> a gadt = function
  | S eql -> (match eql with Refl -> Sg)
  | F eql -> (match eql with Refl -> Fg)

let gadt_to_adt : type a. a gadt -> a adt = function
  | Sg -> S Refl
  | Fg -> F Refl

Therefore, my intuition is that if we remove GADT from the type system the concrete type of an abstract type can never leak outside of its module. GADT is the only way to work with proofs and type equalities as first-class objects. So if a module doesn’t use the GADT functionalities, it cannot leak the concrete types of its abstract types. But, as you illustrate, if it defines functor which abstract over parametric type then it may leak the concrete types of its abstract ones.

I played a little bit with your last example, and it was funny. When we look at the signature of your module, we can prove (in the spirit of Wadler’s theorems for free) that its type t is necessarily equal to string. Without GADTs this proof is metalinguistic, but with them we can write it in the language itself. :slight_smile:

module type S = sig
  type t
  module F :
    functor (X : sig type 'a x val x : string x end) -> sig val x : t X.x end
end

(* the proof is straightforward, this is mostly the one you wrote *)
let leak_S_t (type a) (module M : S with type t = a) =
  let module K = M.F(struct type 'a x = ('a, string) eql let x = Refl end) in
  K.x;;
val leak_S_t : (module S with type t = 'a) -> ('a, string) eql = <fun>

(* the type of `leak_S_t' clearly say that any module which implements
   the signature S,  must have a type `t' equal to `string' *)

(* as shown if we apply it to your module implementation *)
leak_S_t (module M);;
- : (M.t, string) eql = Refl

We can go further with a variation of your example:

module type S = sig
  type t
  module F :
    functor (X : sig type 'a x val x : string x val y : float x end) ->
      sig val x : t X.x end
end

Here we can statically prove that for a module M : S the concrete type of M.t is string or float, and we can find dynamically which one it is.

(* here for the proof I use the previously defined 'a gadt type *)
let leak_S_t (type a) (module M : S with type t = a) =
  let module K = M.F(struct type 'a x = 'a gadt let x = Sg let y = Fg end) in
  K.x;;
val leak_S_t : (module S with type t = 'a) -> 'a gadt = <fun>

(* and with two examples *)
leak_S_t (module M);;
- : M.t gadt = Fg (* M.t = float *)

leak_S_t (module N);;
- : N.t gadt = Sg (* N.t = string *)

By the way, it may still be possible to improve the refutation algorithm (using a more refined criterion than the one I gave first) in such a way that for @Chimrod example, the type checker can prove that the pattern matching is exhaustive. Maybe @yallop or @lpw25 can enlighten us on this point?

2 Likes
16

I only skimmed what you wrote but I suspect that this would be of interest. In particular, Jeremy’s talk at ML 2010: “First-class modules: hidden power and tantalizing promises to GADTs and beyond”

1 Like