Decidable of Exists changes `if` macro semantics

Stream: lean4

[Yakov Pechersky]

The presence of a Decidable instance for Exists changes how the if macro is used to make definitions. It results in specialization of an argument from Sort _ to Prop, and wraps the definition in a .proof_1. Relying on @dite does not have this happen.

namespace Debug

scoped instance exists_prop_decidable {p} (P : p → Prop)
  [Decidable p] [∀ h, Decidable (P h)] : Decidable (∃ h, P h) :=
if h : p then
  decidable_of_decidable_of_iff ⟨fun h2 => ⟨h, h2⟩, fun ⟨_, h2⟩ => h2⟩
else isFalse fun ⟨h', _⟩ => h h'

end Debug

@[reducible]
protected noncomputable def Classical.arbitrary (α) [h : Nonempty α] : α :=
  Classical.choice h

noncomputable section Extend

attribute [local instance] Classical.propDecidable

noncomputable def invFun [Nonempty α] (f : α → β) : β → α :=
  fun y => if h : (∃ x, f x = y) then (Classical.choose h) else Classical.arbitrary α

noncomputable def invFun' [Nonempty α] (f : α → β) : β → α :=
  fun y => @dite α (∃ x, f x = y) (Classical.propDecidable _)
    Classical.choose (fun _ => Classical.arbitrary _)

#check @invFun -- Sort, Sort
#check @invFun' -- Sort, Sort
#print invFun
#print invFun'

attribute [local instance] Debug.exists_prop_decidable

noncomputable def invFun_variant [Nonempty α] (f : α → β) : β → α :=
  fun y => if h : (∃ x, f x = y) then (Classical.choose h) else Classical.arbitrary α

noncomputable def invFun_variant' [Nonempty α] (f : α → β) : β → α :=
  fun y => @dite α (∃ x, f x = y) (Classical.propDecidable _)
    Classical.choose (fun _ => Classical.arbitrary _)

#check @invFun_variant -- Prop, Sort
#check @invFun_variant' -- Sort, Sort
#print invFun_variant.proof_1
#print invFun_variant'

[Sebastian Ullrich]

At a glance it looks like things are working as expected. Typeclass resolution is allowed to assign undetermined universe levels.

[Yakov Pechersky]

What's the right way to write the definition using the if then else macro, if we'd like to retain the Sort _ generalized?

[Mario Carneiro]

@Sebastian Ullrich The part that seems suspicious here is that the universe levels should have already been turned into variables by the point you get to that instance

[Mario Carneiro]

Like, I thought that changing the body of a definition can't change its type? That sort of thing is pretty valuable for incremental compilation and such

[Mario Carneiro]

what I'm hearing here is that this is only true up to universe metavariables, which are not yet determined by the time the type is elaborated since apparently the value can refine them

[Sebastian Ullrich]

Correct, universe levels are considered more of an implementation detail than part of the formal signature by the elaborator

[Yakov Pechersky]

@Mario Carneiro , should we tag exists_prop_decidable with (priority := low)?

[Mario Carneiro]

I don't think this is exists_prop_decidable's fault. Assuming the lean 4 behavior doesn't change, I would blame invFun for not specifying that it wants alpha to be a Sort u

[Yakov Pechersky]

So switching from Sort _ to Sort u should be sufficient, correct?

[Mario Carneiro]

yes

[Mario Carneiro]

I'm thinking of making a linter similar to the suspicious_universes linter which will warn if universe metavariables are refined in the definition. I think that will 90% of the time be a bug

[Yakov Pechersky]

How would you check that in this case?

[Yakov Pechersky]

If you only see the definition after it's been specialized to Sort 0

[Mario Carneiro]

You can re-elaborate the type, generalize the universes and see if you get the same thing as the final result

[Mario Carneiro]

I really think that this should just be fixed on the lean 4 side, that's a lot simpler: you just up the universe metavariable context depth when elaborating the value of the definition, to ensure that the metavariables can't be instantiated by the value

[Mario Carneiro]

(you can't immediately promote the metavariables to variables, because you don't yet know what variables are included)

[Scott Morrison]

I've run into this issue recently as well, and needed to workaround by changing Sort _ to Sort u. It would be nice not to have this gotcha.

[Mario Carneiro]

On the other hand, I think that my proposal will increase the probability of universe mismatch errors, which are definitely an un-fun experience for beginners. Enabling it on the lean core repo will probably already find some cases where they are relying on this behavior for something like List.foldl : (α → β → α) → α → List β → α inferring α to be a Sort (from the signature) instead of a Type (from the definition)

[Gabriel Ebner]

This particular example should be fine since α can be generalized to Sort here. :smile:

[Mario Carneiro]

That was the point of the example. If you look at the type, you will think that alpha can be a Sort, but if it is defined using specialization of foldlM to Id in the definition then alpha must be a Type. That's a universe constraint that happens only in the value, not the type, so with the current approach that would silently infer alpha to be a Type and under the proposal it would be a universe error