Original bug ID: 6598
Reporter: @gasche
Assigned to: @garrigue
Status: closed (set by @xavierleroy on 2017-02-16T14:14:45Z)
Resolution: fixed
Priority: normal
Severity: feature
Target version: 4.03.0+dev / +beta1
Fixed in version: 4.03.0+dev / +beta1
Category: ~DO NOT USE (was: OCaml general)
Related to: #5998 #6403
Monitored by: jpdeplaix

Bug description

Assuming the usual declaration of GADT equality:

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

the function of type ((int, bool) eq -> float) with no branches cannot be written.

This is a purely syntactic limitation, as using the revised syntax makes the following program type-check:

type eq 'a 'b = [ Refl : eq 'a 'a ];
value f : eq int bool -> float = fun [ ];

It would be nice to have a way to express this in regular OCaml syntax.