unsound interaction of -rectypes and GADTs

[vicuna]

Original bug ID: 6405
Reporter: @gasche
Assigned to: @garrigue
Status: closed (set by @xavierleroy on 2015-12-11T18:26:54Z)
Resolution: fixed
Priority: normal
Severity: minor
Fixed in version: 4.02.0+dev
Category: typing
Child of: #5998

Bug 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.

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 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.

[vicuna]

Comment author: @gasche

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.

[vicuna]

Comment author: @garrigue

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 .

[vicuna]

Comment author: @garrigue

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.

[vicuna]

Comment author: @gasche

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 =

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.

[vicuna]

Comment author: @garrigue

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.