Inferred logic qualifier results in inconsistent qualifier annotations error

[s-zanella]

The code below yields Inconsistent qualifier annotations on foo; Expected { }, got {logic }

val foo: int -> GTot Type0
let foo n = True \/ True

The qualifier logic is undocumented in the wiki. https://github.com/FStarLang/FStar/wiki/Qualifiers-for-definitions-and-declarations#logic
According to @nikswamy, it serves as a way to trigger an optimization in the SMT encoding by translating a term shallowly to SMT, rather than the default deep embedding. F* usually infers when to add this qualifier.

In this case, it inferred logic for the let but complains that what it inferred didn't match what was written for the val ...which it really shouldn't complain about. It should just use its inferred qualifier and enable the optimization.

The idea is to make it invalid for a programmer to write logic explicitly, and make it so that F* doesn't complain about missing logic annotations.

[s-zanella]

I keep hitting this issue.
Easy to work around (just don't write a val), but frustrating anyway.

[jkzinzindohoue]

Nikhil gave me a workaround for it, you need an inner let binding like:

val foo: int -> GTot Type0
let foo n =
 let _ = () in True \/ True

It is not very pretty but it works. It is useful in case your val is in a .fsti for instance.

[catalin-hritcu]

One idea behind prop (#1048) was that we could also get rid of the logic qualifier.

[aseemr]

This is fixed in master now. The logic qualifier is deprecated and F* has a better inference for encoding terms using the shallow encoding, adding the testcase to regressions.