New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Unsoundness with GADTs and let rec #7215
Comments
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. |
Comment author: @garrigue I tend to think that the problem here is that the check for recursive values is too liberal. This may be what gasche meant: we could keep note of informative matchings in the intermediate language. |
Comment author: @yallop
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. |
Comment author: @stedolan
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.
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". |
Comment author: @garrigue Jeremy, |
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. |
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. |
Comment author: @yallop I agree that it would be good to fix it for 4.04. |
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) =
Error: This kind of expression is not allowed as right-hand side of `let rec' |
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)
The text was updated successfully, but these errors were encountered: