Skip to content

Commit

Permalink
Disable smart elaboration of negation in guards
Browse files Browse the repository at this point in the history
Summary:
As title, do not narrow types under negations. The issue is that, currently, `not (V == a)` is refined identically to `(V == a)`, as the negation is not "propagated".

Occurrence typing is still able to soundly refine types under negations, this is thus only a limitation for functions where occ typing is disabled.

Reviewed By: ilya-klyuchnikov

Differential Revision: D58184266

fbshipit-source-id: 4f71dd99971a7ce0dd73e61b0ebda435952fa4a1
  • Loading branch information
VLanvin authored and facebook-github-bot committed Jun 6, 2024
1 parent 2d26851 commit 0a6767c
Showing 1 changed file with 4 additions and 1 deletion.
Original file line number Diff line number Diff line change
Expand Up @@ -264,7 +264,10 @@ final class ElabGuard(pipelineContext: PipelineContext) {
val TestUnOp(op, arg) = unOp
op match {
case "not" =>
(booleanType, elabTestT(arg, booleanType, env))
arg match {
case TestVar(_) => (booleanType, elabTestT(arg, booleanType, env))
case _ => (booleanType, env)
}
case "bnot" | "+" | "-" =>
(NumberType, elabTestT(arg, NumberType, env))
case _ =>
Expand Down

0 comments on commit 0a6767c

Please sign in to comment.