Mantis Bug Tracker

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0006405OCamlOCaml typingpublic2014-05-08 18:452014-05-11 10:51
Reportergasche 
Assigned Togarrigue 
PrioritynormalSeverityminorReproducibilityalways
StatusresolvedResolutionfixed 
PlatformOSOS Version
Product Version 
Target VersionFixed in Version4.02.0+dev 
Summary0006405: unsound interaction of -rectypes and GADTs
DescriptionGADT type-checking currently accepts to consider as different types that become unifiable in presence of -rectypes. When linking modules that use -rectypes and other that do not, this allows to break typing soundness.

In blah.ml:

  type ('a, 'b, 'c) eqtest =
  | Refl : ('a, 'a, float) eqtest
  | Diff : ('a, 'b, int) eqtest
  
  let test : type a b . (unit -> a, a, b) eqtest -> b = function
    | Diff -> 42

In bluh.ml:

  let () =
    print_float Blah.(test (Refl : (unit -> 'a as 'a, 'a, _) eqtest))

To test:

  ocamlc -c blah.ml && \
  ocamlc -rectypes -c bluh.ml && \
  ocamlc blah.cmo bluh.cmo -o bang && \
  ./bang

Result:

  Segmentation fault


Reproduced under 4.01 and trunk.
Additional InformationA good share of the credit for this bug goes to BenoƮt Vaugon, for
trying to show me that surely the format6 type I expected for "%(%)%d"
was unsound, as -rectypes would allow to perform
a seemingly-impossible unification.
TagsNo tags attached.
Attached Files

- Relationships
child of 0005998assignedgarrigue GADT typing and exhaustiveness bugs 

-  Notes
(0011408)
gasche (developer)
2014-05-08 19:34
edited on: 2014-05-08 22:57

Note that if the GADT unification check itself (blah.ml in my example) is compiled with -rectypes, it warns about non-exhaustiveness *and* compiles the pattern-matching in suh a way that running the complete program correctly fails with a Match_failure.

This means that disabling the optimization of non-conditional access when the GADT type is restrictive enough would probably be enough to restore type soundness. People are not going to like that, though.

The other option would be to forbid -rectypes-compiled compilation unit *implementations* (not just signatures) to be linked with others without -rectypes, but in practice that means forbidding use of -rectypes entirely.

PS: in fact the exhaustiveness optimizations just need to be disabled for pattern-matchings whose dead-ness depends on the occur check, so that should not affect most GADT code in practice and would be a reasonable choice.

(0011413)
garrigue (manager)
2014-05-09 08:14

Fixed in trunk at revision 14769.
The fix allows to add recursive equations to locally abstract types.
So in some way it allows recursive local definitions even without
-rectypes, but they cannot escape their scope, so I suppose this is
fine.
Note that this changes some error messages when using gadts.

Memo: probably local_non_recursive_abbrev could be discarded, because
it actually does nothing, since its parameters are already normalized: no
recursive call can ever happen, and p' is always different from p.
Note that on the other hand occurs is needed even with -rectypes,
because it is called on non-normalized types .
(0011420)
garrigue (manager)
2014-05-11 09:50

Commented out local_non_recursive_abbrev, since it is useless as explained by the above Memo.

Note that, while this change effectively allows pattern-matching branches to introduce recursive types even without -rectypes, these branches can only be reached by providing a witness of this recursion, which can only be produced using -rectypes.
(0011423)
gasche (developer)
2014-05-11 10:05
edited on: 2014-05-11 10:06

If I understand correctly, the implication of your change is that anyone reasoning on exhaustiveness of GADT branches should consider that -rectypes is implicitly enabled for safety. For example, I just checked that the following produces an exhaustivity warning, while it previously did not:

# type (_, _) eq = Refl : ('a, 'a) eq | Diff : ('a, 'b) eq;;
# let test : type a . (a, a -> int) eq -> unit = function Diff -> ();;
Warning 8: this pattern-matching is not exhaustive.
Here is an example of a value that is not matched:
Refl
val test : ('a, 'a -> int) eq -> unit = <fun>

Would it be possible to instead produce a warning only when -rectypes is enabled, but nonetheless compile the pattern-matching safely (so that it fails with a Match_failure if a consumer uses -rectypes to craft unplanned-for values)?

I'm not sure that would be a strictly better design. But I find it a bit unpleasant to think that all GADT reasoning would have to happen in that rather exotic mode that is quite rarely used in practice.

(0011426)
garrigue (manager)
2014-05-11 10:51

The rule for the exhaustiveness check is that it should be sound, and that whenever an exhaustiveness warning is generated, the extra pattern should be accepted by the typechecker.
Completeness is not required, and this is important because at least from a semantic point of view you cannot get it.
So the fact some seemingly impossible patterns are output as counter-examples of exhaustiveness is not a big deal: you just have to add the patterns as impossible ones (assert false or whatever).

You suggestion is interesting, but it would require more work, having two notions of exhaustiveness, one for the warnings, and one for the code generated. Doing this correctly could be tricky, like for variance.
Also, there is something a bit strange in having no warning, seemingly implying that this case is superfluous, and still being able to add a case that can be really triggered in practice, even if this is in a convoluted way.

- Issue History
Date Modified Username Field Change
2014-05-08 18:45 gasche New Issue
2014-05-08 19:34 gasche Note Added: 0011408
2014-05-08 19:35 gasche Note Edited: 0011408 View Revisions
2014-05-08 22:57 gasche Note Edited: 0011408 View Revisions
2014-05-09 08:14 garrigue Note Added: 0011413
2014-05-09 08:14 garrigue Status new => resolved
2014-05-09 08:14 garrigue Fixed in Version => 4.02.0+dev
2014-05-09 08:14 garrigue Resolution open => fixed
2014-05-09 08:14 garrigue Assigned To => garrigue
2014-05-11 09:50 garrigue Note Added: 0011420
2014-05-11 09:56 garrigue Relationship added child of 0005998
2014-05-11 10:05 gasche Note Added: 0011423
2014-05-11 10:06 gasche Note Edited: 0011423 View Revisions
2014-05-11 10:51 garrigue Note Added: 0011426


Copyright © 2000 - 2011 MantisBT Group
Powered by Mantis Bugtracker