Mantis Bug Tracker

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0006437OCamlOCaml typingpublic2014-05-21 20:472015-04-27 12:22
Assigned Togarrigue 
PlatformOSOS Version
Product Version4.01.0 
Target Version4.03.0+devFixed in Version 
Summary0006437: GADT exhaustiveness check incompleteness
DescriptionThis code:

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?
TagsNo tags attached.
Attached Files

- Relationships
related to 0006403acknowledgedgarrigue another broken GADT exhaustiveness check 
parent of 0006220assignedgarrigue GADT type information is not used to detect unused match cases 
child of 0005998assignedgarrigue GADT typing and exhaustiveness bugs 
Not all the children of this issue are yet resolved or closed.

-  Notes
mqtthiqs (reporter)
2014-05-23 21:53

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.
garrigue (manager)
2014-05-24 09:06

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).
mqtthiqs (reporter)
2014-05-30 17:05

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.
garrigue (manager)
2014-05-31 15:46

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.
garrigue (manager)
2015-04-27 12:22

The patch attached to 6403 does not solve this case: not clear where to hook the expansion here.

- Issue History
Date Modified Username Field Change
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
2015-04-27 12:21 garrigue Relationship added related to 0006403
2015-04-27 12:22 garrigue Note Added: 0013739

Copyright © 2000 - 2011 MantisBT Group
Powered by Mantis Bugtracker