Why does this declaration use `sorry`?

Stream: lean4

[James E Hanson]

I'm trying to understand how some of the internals of the elaborator work and I can't figure out why declarations like this end up involving sorry when the corresponding native_decide proof doesn't.

@[implemented_by true]
def true' : Bool := true

/-- warning: declaration uses `sorry` -/
#guard_msgs in
theorem sorry? : Lean.reduceBool true' = true := rfl

/-- info: 'sorry?' depends on axioms: [sorryAx, Lean.trustCompiler] -/
#guard_msgs in
#print axioms sorry?

-- The proof of `sorry?` is actually just a `sorry` term.
/-- info: sorry -/
#guard_msgs in
#reduce (proofs := true) sorry?

theorem notSorry : true' = true := by native_decide

/-- info: 'notSorry' depends on axioms: [Lean.ofReduceBool, Lean.trustCompiler] -/
#guard_msgs in
#print axioms notSorry

Perhaps relatedly, the #check here just silently fails, producing no message or error.

@[implemented_by true]
def true' : Bool := true

#check (rfl : Lean.reduceBool true' = true)

I know that the behavior of native_decide is probably going to change eventually, but I just want to understand where this sorry is coming from.

[Aaron Liu]

uhoh

[Aaron Liu]

is there not an error on the rfl?

[Aaron Liu]

like "type mismatch" or something

[James E Hanson]

I believe you get an error if you try to compile it, but you don't in the editor.

[James E Hanson]

The thing is that I think Lean.reduceBool true' is supposed to be definitionally equal to true (because of how Lean.reduceBool has special treatment in the kernel), and it would be if true' was defined in an import instead of in the same file.

[Robin Arnez]

It doesn't work because Bool.true is a constructor and thus doesn't have an executable IR declaration associated to it

[Robin Arnez]

but the lack of error is weird

[James E Hanson]

Robin Arnez said:

It doesn't work because Bool.true is a constructor and thus doesn't have an executable IR declaration associated to it

Why does it behave differently than this example then?

/-- error: (interpreter) unknown declaration 'Bool.true' -/
#guard_msgs in
example : Lean.reduceBool true = true := rfl