Mantis Bug Tracker

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0006437OCamlOCaml typingpublic2014-05-21 20:472015-06-15 23:06
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 Filesdiff file icon type_pat_cps.diff [^] (35,978 bytes) 2015-05-07 09:47 [Show Content]
diff file icon type_pat_cps2.diff [^] (39,997 bytes) 2015-05-08 07:16 [Show Content]
diff file icon type_pat_cps3.diff [^] (45,336 bytes) 2015-05-18 06:04 [Show Content]

- Relationships
related to 0006403acknowledgedgarrigue another broken GADT exhaustiveness check 
parent of 0006220assignedgarrigue GADT type information is not used to detect unused match cases 
related to 0006801confirmed Exhaustiveness messages for GADTs suggest patterns that will not type check 
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.
garrigue (manager)
2015-04-30 06:44

After looking more carefully, this case is really interesting.
To prove that (Nil, _) doesn't accept any value, we need to do a case analysis on the right part, using its type. However, we cannot use the type coming from the other patterns, as it depends on the left part.

The solution seems to be to do the splitting when typing the pattern (to prove that it cannot be typed). The tricky part is that we need to do backtracking in the typing function Typecore.type_pat.
garrigue (manager)
2015-04-30 14:01

The patch type_pat_cps.diff implements a new approach, which can fully exploit typing information.
The idea is to rewrite Typecore.type_pat in continuation passing style, so that it becomes possible to backtrack, looking for a counter-example.
This is rather heavy-weight, and potentially brittle, but I think this is the only way to have accurate warnings. Looking at the testsuite, it indeed removes a number of false positives.
garrigue (manager)
2015-04-30 14:16

Brittle indeed: this doesn't bootstrap yet, due to an interaction with objects.
garrigue (manager)
2015-05-07 09:51

Updated patch. Now it bootstraps.
I see no slowdown when compiling ocamlc, so I'm thinking of merging this patch to trunk.
This fixes both this example, the one in PR#6403, and one in typing-gadts/
Tell me if you see problems.
garrigue (manager)
2015-05-08 07:17

Cleaner patch. Could simplify parmatch more, as there seems to be no need to do 2 passes.
garrigue (manager)
2015-05-10 03:57

type_pat_cps3.diff additionally simplifies parmatch, merging the two passes.
Also changed the logic, so that the warning will preferably show ground patterns (they are checked first).
Note that all these patches change the output of exhaustiveness warnings, as or-patterns do not appear in the output (they are always exploded into their components, and only one of them is shown).
garrigue (manager)
2015-05-20 01:15

Created a branch in the subversion server.
The code can be checked out with
  svn checkout [^]

- 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
2015-04-30 06:44 garrigue Note Added: 0013767
2015-04-30 13:57 garrigue File Added: type_pat_cps.diff
2015-04-30 14:01 garrigue Note Added: 0013768
2015-04-30 14:16 garrigue Note Added: 0013770
2015-05-07 09:46 garrigue File Deleted: type_pat_cps.diff
2015-05-07 09:47 garrigue File Added: type_pat_cps.diff
2015-05-07 09:51 garrigue Note Added: 0013859
2015-05-08 07:16 garrigue File Added: type_pat_cps2.diff
2015-05-08 07:17 garrigue Note Added: 0013871
2015-05-10 03:52 garrigue File Added: type_pat_cps3.diff
2015-05-10 03:57 garrigue Note Added: 0013884
2015-05-18 04:29 garrigue Relationship added related to 0006801
2015-05-18 05:40 garrigue File Deleted: type_pat_cps3.diff
2015-05-18 05:40 garrigue File Added: type_pat_cps3.diff
2015-05-18 06:04 garrigue File Deleted: type_pat_cps3.diff
2015-05-18 06:04 garrigue File Added: type_pat_cps3.diff
2015-05-20 01:15 garrigue Note Added: 0013951

Copyright © 2000 - 2011 MantisBT Group
Powered by Mantis Bugtracker