Unsoundness with GADTs and let rec

[vicuna]

Original bug ID: 7215
Reporter: @stedolan
Assigned to: @yallop
Status: resolved (set by @yallop on 2017-09-25T14:14:16Z)
Resolution: fixed
Priority: normal
Severity: crash
Version: 4.03.0+dev / +beta1
Target version: 4.06.0 +dev/beta1/beta2/rc1
Category: typing
Related to: #6738 #7231
Monitored by: braibant @gasche @diml

Bug description

The following program segfaults, on at least 4.02.1, 4.03.0+beta1 and trunk:

type (,) eq = Refl : ('a, 'a) eq
let cast (type a) (type b) (Refl : (a, b) eq) (x : a) = (x : b)

let is_int (type a) =
let rec (p : (int, a) eq) = match p with Refl -> Refl in
p

let bang = print_string (cast (is_int : (int, string) eq) 42)

[vicuna]

Comment author: @gasche

This is the kind of situation that makes me think that we should properly account, in the intermediate languages and their optimization passes, for the fact that abstraction over potentially-inconsistent equalities should block reduction.

[vicuna]

Comment author: @garrigue

I tend to think that the problem here is that the check for recursive values is too liberal.
It is rather strange that one would be able to pattern-match on the value itself when building it.
The reason is that the check is on the lambda code, after pattern-matching has been compiled, so that actually there the value is not used. But this makes impossible to make any sound reasoning.

This may be what gasche meant: we could keep note of informative matchings in the intermediate language.
Or we could move the check from lambda to typedtree. Would it be that difficult?

[vicuna]

Comment author: @yallop

Or we could move the check from lambda to typedtree. Would it be that difficult?

I think it wouldn't be particularly hard, and there are other reasons to move the check out of Translcore. For example, it's good to have as strong a guarantee as possible that code that passes type checking will be successfully compiled, so that tools (such as Merlin) that call the type checker in isolation can give useful feedback to the user. Furthermore, it's better for the well-formedness criterion to be defined in terms of the source language rather than the intermediate language, so that it can be described in the manual without getting into the details of translation into internal representations.

I actually have a mostly-finished patch that moves the check to the type-checking phase. I'll try to find time to finish it off and submit it.

[vicuna]

Comment author: @stedolan

we should properly account, in the intermediate languages and their optimization passes, for the fact that abstraction over potentially-inconsistent equalities should block reduction.

Essentially, we already do through non-termination. In OCaml, unlike many languages, it is actually unsound to optimise an infinite loop to a no-op, since the infinite loop may claim to produce a witness to lies. As long as non-termination is preserved through optimisations, reduction under falsehoods is delayed until after an infinite amount of work.

Or we could move the check from lambda to typedtree

This makes sense to me: the bug, as far as I understand it, is that the check for whether the right-hand side of let rec makes sense is delayed until OCaml has forgotten the difference between "let rec p = match p with Refl -> Refl" and "let rec p = 0".

[vicuna]

Comment author: @garrigue

Jeremy,
Just too be sure it's clear: this is a soundness bug, so it has to be fixed in 4.03.
I think your approach (moving to typedtree) is correct.
Can you do it in the next days?
Otherwise I can do it myself.
This is rather mechanical, but one has to be careful of allowing as many programs as possible, as we are certainly going to break some.

[vicuna]

Comment author: @yallop

Jacques: that's a good point.

I'll try to finish off the patch in the next couple of days, and let you know if things don't look promising then. The change is indeed fairly mechanical, but typedtree is much bigger than lambda, and there are a few subtleties.

[vicuna]

Comment author: @gasche

I can try to review the patch, I looked closely at the recursive value definition when working on the letrec+floats segfault a few years ago; and Damien knows it even better.

We should have a testsuite to exercise valid and invalid recursive value definitions.

[vicuna]

Comment author: @garrigue

How do we stand on this one?
It would be nice to fix it for 4.04.
Note that there is an open pull request for it, GPR 556.
#556

[vicuna]

Comment author: @yallop

I agree that it would be good to fix it for 4.04.

[vicuna]

Comment author: @yallop

This is fixed in 4.06, now that GPR 556 is merged:

type (,) eq = Refl : ('a, 'a) eq;;

type (_, _) eq = Refl : ('a, 'a) eq

let cast (type a) (type b) (Refl : (a, b) eq) (x : a) = (x : b);;

val cast : ('a, 'b) eq -> 'a -> 'b =

let is_int (type a) =

 let rec (p : (int, a) eq) = match p with Refl -> Refl in
 p;;
   Characters 52-77:
   let rec (p : (int, a) eq) = match p with Refl -> Refl in
                               ^^^^^^^^^^^^^^^^^^^^^^^^^

Error: This kind of expression is not allowed as right-hand side of `let rec'