native_decide: "(kernel) declaration has free variables "

Stream: new members

[Alex Meiburg]

When I try

import Mathlib
theorem stupid : IsLeast {s | true} 0 := by
  have : Decidable (IsLeast {s | true} 0 ) := by
    apply isTrue
    simp
  native_decide

I get the fairly inscrutable message

(kernel) declaration has free variables 'stupid._nativeDecide_1'

Any idea what this means / how to fix it?

[Alex Meiburg]

Best I can find is that it comes from declHasFVars in the kernel, which comes from a declaration_has_free_vars_exception in C, which comes from check_no_metavar_no_fvar (which is only caller of check_no_fvar).

[Mario Carneiro]

Lean can't evaluate your decidable instance because it is a local variable in that context. If you lift it to a separate definition then it should work

[Alex Meiburg]

Oh, huh. Is this related to the fact that theorems are opaque? Like somehow native_decide doesn't "pass on" the relevant details to the kernel?

[Mario Carneiro]

native_decide only works when (inferInstance : Decidable <your_goal>) results in a proof with no free variables

[Mario Carneiro]

which can therefore be sent to the compiler

[Mario Carneiro]

it's the same reason that

variable (a : Nat)
#eval a

doesn't work

[Alex Meiburg]

Interesting. Alright! Maybe worth mentioning in the docstring for native_decide (or a clearer error message?) I was banging my head on this for fifteen minutes and wouldn't have guessed that :)

Thanks!

[Mario Carneiro]

yeah no that's a really bad error message, you should report it

[Mario Carneiro]

Normally this is a point where I would point out that you've used have where you really should have used let, but in this case I think that won't be good enough because the code in question is not smart enough to unfold let variables before the free variable check

[Alex Meiburg]

Yeah,

theorem stupid : IsLeast {s | true} 0 := by
  let inst : Decidable (IsLeast {s | true} 0 ) := by
    apply isTrue
    simp
  native_decide

has the same message