Original bug ID: 7028
Reporter: @alainfrisch
Status: acknowledged (set by @xavierleroy on 2015-11-15T17:17:53Z)
Resolution: open
Priority: normal
Severity: feature
Target version: later
Category: typing
Has duplicate: #7360
Monitored by: @gasche @yallop @hcarty

Bug description

It is well known that GADT and abstract types don't interact well w.r.t. exhaustiveness checking. A typical example:

module X : sig
  type abstr
end = struct
  type abstr = ...
end

type _ t =
  | Int: int t
  | Float: float t
  | Abstr: X.abstr t

let f Int = ()

Since the type checker has no way to know that X.t (which could come from an external unit) is different from int in all contexts, it cannot prove that the pattern matching is exhaustive.

This seriously limits the usefulness of GADT. Possible workarounds: (i) break abstraction; (ii) add impossible pattern matching cases. Note that (i) does not work for instance when the type is really implemented as an abstract type (to represent external data structures). I'd like to propose a pragmatic solution based on a softer version of abstraction breaking. Instead of exposing the concrete definition of the type, one could allow to attach an arbitrary string (or identifier) to any type definition without a manifest type (i.e. "fresh" concrete or abstract types, not re-exported types or pure abbreviations). This string could be forgotten in the interface but not changed or added. This provides the guarantee that if two types have such an attached string, and the two strings are different, it is safe to assume that the two types are non-compatible (i.e. different in any context). Built-in types would come with such internal strings.

I don't have a concrete proposal for the syntax, but conceptually, this would give:

module X : sig
  type abstr "blabla"
end = struct
  type abstr "blabla"
end

type _ t =
  | Int: int t
  | Float: float t
  | Abstr: X.abstr t

let f Int = ()  (* type checker can now prove exhaustivity *)

The programmer would be responsible to use unique enough strings if they need to. Using the same string for two types does not break safety, it only prevents the type-checker from proving exhaustivity of some GADT patterns.

A functor could even specify that some abstract types in its argument must have a specific string, allowing to use a GADT as above in the body of the functor (exposing the concrete structure is not an option here).