the danger of sorried instances

Stream: lean4

[Kenny Lau]

set_option autoImplicit false

universe u

variable (G : Type u) [Add G]

instance : Subsingleton G := sorry

Let's say you have a very long proof of the theorem "any additive magma is subsingleton", so you'd want to sorry it first and then move on, but to your horror you notice that everything afterwards pass, and then as you inspect what was happening to the sorried instance, you discover to your horror:

image.png

[Kenny Lau]

yep, Lean automatically removed the unused [Add G] for you

[Kenny Lau]

now obviously mathlib does not allow sorries, but sorries are commonplace in downstream repos, and if you aren't careful you might end up proving something very strong :melt:

[Kenny Lau]

This is a public call to all downstream repo projects, really, check your sorried instances!

[Kyle Miller]

Another fun issue with using sorry for instances is if you have multiple universe level parameters and some are supposed to be determined by the instance (you see this happen in category theory, where the parameter for the size of the hom sets is determined by the instance). This can lead to some overly general instances as well, but the risk here doesn't seem to be correctness, just that you start getting into impossible-to-figure-out situations.

[Kim Morrison]

Another interpretation of this behaviour is that you should be careful of relying on variable for def and instance!

I think it generally helps readability to explicitly write out all the explicit arguments for every def and instance.

[Jason Reed]

I'm confused now about how variable is meant to work, orthogonal to any occurrence of sorry. Consider :

variable (G : Type u) [Add G]

def foo1 : (g : G) → g = g := fun _g => rfl
def foo2 : (g : G) → g + g = g + g := fun _g => rfl

/-- info: foo1.{u} (G : Type u) (g : G) : g = g -/
#guard_msgs in
#check foo1
/-- info: foo2.{u} (G : Type u) [Add G] (g : G) : g + g = g + g -/
#guard_msgs in
#check foo2

I read in the language reference that

When the name of a section variable is encountered in a non-theorem declaration, it is added as a parameter. Any instance implicit section variables that mention the variable are also added.

This would make me think that [Add G] should be added whenever G is mentioned. Specifically, I would have expected foo would have had [Add G]. Am I misreading the spec?

(the behavior I seem to be seeing --- that instance implicits are added if they're actually used --- doesn't seem to be an unreasonable or undesirable behavior, though)

[Aaron Liu]

Jason Reed said:

I read in the language reference that

When the name of a section variable is encountered in a non-theorem declaration, it is added as a parameter. Any instance implicit section variables that mention the variable are also added.

This would make me think that [Add G] should be added whenever G is mentioned. Am I misreading the spec?

(the behavior I seem to be seeing --- that instance implicits are added if they're actually used --- doesn't seem to be an unreasonable or undesirable behavior, though)

It's added but then it wasn't used so at the end it's removed

[Jason Reed]

Huh, ok. Removed by what process?

[Aaron Liu]

There are some places you can include a variable

• when elaborating the theorem statement
• when elaborating the theorem body
• when adding the theorem to the environment

In the first case, it is always included
In the second case, Lean uses those criteria from the language reference you showed
In the third case, it's only the used section variables that are included I think

[Jason Reed]

Hmmm. All of your three bullet points involve theorems, and my example contained a non-theorem def declaration, so I thought I could take the passage I cited at face value. If I'm getting hung up on a distinction that doesn't matter, let me know...

[Jason Reed]

If there's some other process that removes unused instance implicit arguments later on in the elaboration process, I'd love to know about it.

[Jason Reed]

But if theorems and defs are treated differently, then I think I do perceive the relevance of @Kim Morrison 's "you should be careful of relying on variable for def and instance!" above :slight_smile:

[Jason Reed]

I'm still scratching my head over the exact language of the reference manual versus the behavior I see though.

[Jason Reed]

I do note different behavior if I rewrite def to theorem:

variable (G : Type u) [Add G]

theorem foo1 : (g : G) → g = g := fun _g => rfl
theorem foo2 : (g : G) → g + g = g + g := fun _g => rfl

/-- info: foo1.{u} (G : Type u) [Add G] (g : G) : g = g -/
#guard_msgs in
#check foo1
/-- info: foo2.{u} (G : Type u) [Add G] (g : G) : g + g = g + g -/
#guard_msgs in
#check foo2

[Jason Reed]

I get a warning at the definition of foo1 that [Add G] is unused.

[Aaron Liu]

oh for definitions it's different

[Aaron Liu]

for definitions I think when elaborating the statement and body everything is included and when adding it to the environment only used things are included

[Aaron Liu]

Jason Reed said:

I get a warning at the definition of foo1 that [Add G] is unused.

I guess then I was wrong with what I said about only including the used variables

[Robin Arnez]

I believe for () and {} it includes when used but for [] it includes when all of the stuff it depends on is included.