Comment author: @garrigue

This one is a long-term goal.
To do that, one would need to know that the branches are equivalent,
but in the current implementation of GADTs there is no way to check that.
That is, we end up with two environments, we need to compare them,
and worse, we need to drop one of the two and still be safe for that branch...
Maybe we could use the summary, but this is still going to be difficult,
particularly if we are creating fresh skolem variables in both patterns.

Comment author: @xavierleroy

Moving to "later" based on @garrigue's comment.

It would be handy to be able to combine the branches for GADT constructors that refer to the same types.

This has been implemented in #2110, and the first version of the type_of_gadt function is now accepted as written, so I'm closing this.

This hasn't quite been implemented: after #2110 you don't have the information that t = float outside the or-pattern.
We still hope to be able to do that in the future, but more work is required.

But I agree that the example given here is now accepted by the compiler indeed.

I see --- so the following example is not yet allowed:

let zero : type t. t gadt -> t = function
  | Float _ | Float2 _ -> 0.0
  | Int _ -> 0

@trefis: feel free to reopen if you think this is the best place to track that work.

Will it ever be possible to pattern match by the type rather than the constructor? eg in pseudo-OCaml:

let zero : type t. t gadt -> t = function
  | _ when t = float -> 0.0
  | Int _ -> 0

Your syntax is confusing.
I suppose that you mean something like

let zero : type t. t gadt -> t = function
  | (_ : float gadt) -> 0.0
  | Int _ -> 0

expecting that it would automatically expand _ into all the cases compatible with float gadt.
That's an interesting idea, a bit related to the #-patterns for polymorphic variants.
However this would need a more precise definition (using only a type annotation seems brittle).
Maybe (#gadt : float gadt), insisting on the similarity.

If I follow, your idea is that #foo would expand to all the constructors of the datatype foo that are well-typed in the current context. However, I don't like the fact that this gives a non-modular semantics for type annotations: it feels wrong that (#foo : float foo) would be accepted in a place where (_ : float foo) or (x : float foo) are rejected.

(Note: we already have logic in place to explode wildcard patterns in situations that are different but related -- when checking refutation clauses.)

I've longed for such a feature several time. Simple syntax proposition: extend #<t> to any simple type expression, and expand when it's a sum type/gadt/polymorphic variant, as proposed above. It's consistent with the current version, which only accepts an identifier. When it's composed, we can simply use parens: #(float t).