|Anonymous | Login | Signup for a new account||2014-11-21 03:25 CET|
|Main | My View | View Issues | Change Log | Roadmap|
|View Issue Details|
|ID||Project||Category||View Status||Date Submitted||Last Update|
|0006437||OCaml||OCaml typing||public||2014-05-21 20:47||2014-07-16 17:38|
|Target Version||4.03.0+dev||Fixed in Version|
|Summary||0006437: GADT exhaustiveness check incompleteness|
type ('a, 'b) ctx =
| Nil : (unit, unit) ctx
| Cons : ('a, 'b) ctx -> ('a * unit, 'b * unit) ctx
type 'a var =
| O : ('a * unit) var
| S : 'a var -> ('a * unit) var
let rec f : type g1 g2. (g1, g2) ctx * g1 var -> g2 var = function
| Cons g, O -> O
| Cons g, S n -> S (f (g, n))
(* | Nil, _ -> (assert false) *)
reports a warning for non-exhaustive pattern-matching, whereas (I think) it should not, since the last commented case is impossible.
Or am I missing something?
|Tags||No tags attached.|
A more concise version of the same bug (I guess):
type 'a t = T1 : ('a * 'b) t | T2 : 'a t -> ('a * 'b) t
type 'a u = U1 : unit u | U2 : ('a * 'b) u
let bug : type a. a t * a u -> unit = function
| t, U2 -> ()
(* | T1, U2 -> () *)
(* | T2 _, U2 -> () *)
(* | _, U1 -> () *) (* impossible *)
reports a warning for non-exhaustive pattern-matching; but whatever the value of t is, the second argument cannot be U1 (this branch 4 is impossible). Note that eta-expanding the first argument (ie. uncommenting branches 2 and 3) the warning disappears.
Hope it helps.
This is a well known limitation of the way the exhaustiveness check works for GADTs requires a constructor to "seed" counterexamples. Doing it on the basis of the type alone could cause infinite loops.
We should eventually do something about that, but this is not high-priority.
By the way, this is not a bug, since we know that the exhaustiveness check cannot be complete, and do not provide any specification for it other than it should be sound (i.e. detect all non-exhaustive cases).
|Hello Jacques. Is the first piece of code (in the bug report, not in the comment) of the same kind? I don't see how it could be helped by "seeding" counterexamples.|
Indeed the example in the bug report is a simpler case.
The warning can be avoided by reversing the order in the tuple:
let rec f : type g1 g2. g1 var * (g1,g2) ctx -> g2 var = function
| O, Cons g -> O
| S n, Cons g -> S(f (n,g));;
But the cause of the warning is the same: using the original order,
one tries to build a pattern for the Nil context, but then the var part
is not seeded, and the exhaustiveness checked does not try to split
the var into O and S. The O and S of the Cons case do no propagate
to the Nil (and they should not, since GADT matching being left to
right, they might actually not be valid there).
Progress report: I've tried to solve these problem (including 6220)
by using typing information to split a wildcard pattern when checking
exhaustiveness. However, there is a big problem: the current
of exhaustiveness checking does not keep types... Keeping them is
going to be a lot of work, and we should be extremely careful about
not propagating wrong typing information in presence of GADTs.
Compared to these risks, a few false positives does not seem to be
a big problem, particularly since you can really add the reported
pattern to remove the warning.
|2014-05-21 20:47||mqtthiqs||New Issue|
|2014-05-21 22:10||gasche||Relationship added||child of 0005998|
|2014-05-23 21:53||mqtthiqs||Note Added: 0011560|
|2014-05-24 09:06||garrigue||Note Added: 0011561|
|2014-05-30 14:02||shinwell||Assigned To||=> garrigue|
|2014-05-30 14:02||shinwell||Status||new => confirmed|
|2014-05-30 17:05||mqtthiqs||Note Added: 0011609|
|2014-05-31 15:33||garrigue||Relationship added||parent of 0006220|
|2014-05-31 15:46||garrigue||Note Added: 0011610|
|2014-07-16 17:38||doligez||Target Version||=> 4.03.0+dev|
|Copyright © 2000 - 2011 MantisBT Group|