|Anonymous | Login | Signup for a new account||2017-10-23 08:18 CEST|
|Main | My View | View Issues | Change Log | Roadmap|
|View Issue Details|
|ID||Project||Category||View Status||Date Submitted||Last Update|
|0006405||OCaml||typing||public||2014-05-08 18:45||2015-12-11 19:26|
|Target Version||Fixed in Version||4.02.0+dev|
|Summary||0006405: unsound interaction of -rectypes and GADTs|
|Description||GADT 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.|
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
let () =
print_float Blah.(test (Refl : (unit -> 'a as 'a, 'a, _) eqtest))
ocamlc -c blah.ml && \
ocamlc -rectypes -c bluh.ml && \
ocamlc blah.cmo bluh.cmo -o bang && \
Reproduced under 4.01 and trunk.
|Additional Information||A 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.
|Tags||No tags attached.|
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.
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
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 .
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.
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:
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.
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.
|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|
|2015-12-11 19:26||xleroy||Status||resolved => closed|
|2017-02-23 16:45||doligez||Category||OCaml typing => typing|
|Copyright © 2000 - 2011 MantisBT Group|