Subsingleton.elim in a def

Stream: lean4

[Kyle Miller]

I was having an issue where Subsingleton.elim is more powerful than you expect in a def/instance than a theorem:

def foo (β : Sort _) (x y : β) : x = y :=
  Subsingleton.elim _ _

[Kyle Miller]

What rule is allowing this to go through?

[Yaël Dillies]

Can you #print the resulting declaration? I suspect it found Subsingleton Prop and unified the universe variable with 0. All that because the body of defs is inspected for unification.

[Kyle Miller]

(I was thinking of leaving it as a puzzle why this isn't totally broken, but the spoiler for that is that Sort _ unifies with Prop. If you change it to Type _ it doesn't use the Subsingleton Prop instance.)

[Anne Baanen]

docs4#instSubsingleton

[Kyle Miller]

Yes, I know it's instSubsingleton that it's finding. The question is why it's ok with using this instance even though beta is a Sort ?u

[Kyle Miller]

This is bad for finite instances, since it can make Sort variables collapse to Prop without you realizing it.

[Kyle Miller]

I think it's also not very good how you can't protect against it when there's automation inside proofs inside definitions. Like, imagine that apply Subsingleton.elim is done using a mathlib3-style congr' tactic:

def foo (β : Sort _) (x y : β) : {z // x = z} :=
  ⟨y, by apply Subsingleton.elim⟩

[Eric Wieser]

I think in general a lot of places where we'd write Sort _ in lean3 need to become Sort u in Lean 4

[Eric Wieser]

In Lean 4, the universe metavariables in variables lines are now bound per lemma, rather than globally to a free universe variable

[Eric Wieser]

Which means you can write variables {I : Sort _}, and still end up with all the lemmas in the file begin about I : Type u without realizing it

[Kyle Miller]

Ok, that's a good hint for how to resolve some subtle bugs I ran into when I was modifying convert to use Subsingleton.elim.

There were some instances that weren't being picked up anymore despite nothing seeming to involve convert (spooky action at a distance). Eventually I traced through to find the instance that didn't work, and it took too long to realize that β here specialized to Prop:

instance Equiv.finite_right {α β : Sort _} [Finite β] : Finite (α ≃ β) :=
  Finite.of_injective Equiv.toEmbedding fun e₁ e₂ h => Equiv.ext <| by convert FunLike.congr_fun h

[Kyle Miller]

Is there any case where you would want a Sort _ variable to specialize to Prop?

[Eric Wieser]

I think in general we almost never want universe variable unification of any kind before the colon

[Kyle Miller]

It seems like having Sort _ or Type _ specialize to Sort n or Type n with a constant n is never what you want. But I haven't really thought about it.

[Eric Wieser]

And in mathlib we just use it as lazy declaration of free universe variables

[Eric Wieser]

Having Type _ unify to Type (max u v) is a problem we ran into a bunch in mathlib3, and we have a linter against it (more specifically, against things which use only (max u v) and not either universe variable separately)

[Reid Barton]

Eric Wieser said:

And in mathlib we just use it as lazy declaration of free universe variables

Yes, IMO this was always a bad practice.

[Reid Barton]

Does Lean 4 have implicit declaration of universe variables?

[Kyle Miller]

Yes, autoimplicits applies to universe variables too.

[Kyle Miller]

I made use of it in the fix for the issue I was having that led to this thread.

[Kyle Miller]

though it doesn't create fresh universe variables for types introduces via autoimplicits. Using the tactic from the linked PR, this unfortunately works:

def foo (x y : α) : x = y := by
  congr!

(but thankfully changing def -> theorem keeps it from working)

[Eric Wieser]

I think the problem is that people much prefer writing {R M N P Q : Type _} to {R : Type u} {M : Type v} {N : Type w} {P : Type x} {Q : Type y}

[Eric Wieser]

It's not {a : Type _} vs {a : Type u} that is the problem

[Reid Barton]

Well it's (potentially) a problem if you write Type _ when you mean Type u, but I agree it's not a problem if you know not to do that

[Eric Wieser]

Maybe Lean 4 could repurpose Type* as syntax for "generate new universe variables (not metavariables) for everything in this group"?

[Eric Wieser]

Is that easy to write as a syntax extension?

[Kyle Miller]

Just going back to this last foo example, note that α was introduced using autoimplicits, and apparently this is indistinguishable from doing (α : Sort _).

[Reid Barton]

(Unfortunately?) I think this is actually correct/desirable behavior, since it would be pretty annoying if you couldn't use autoimplicit types in combination with e.g. docs4#IO

[Kyle Miller]

Yeah, it also lets you introduce propositions:

example : p → q → p := Function.const _

The unfortunate part is just that something like Type* doesn't help with autoimplicit arguments, which have been seeming like a way to get around certain issues with variables. I'm not sure I've seen an example yet of these issues impacting types introduced via variable though, since you can't do induction/cases on them so tactics shouldn't touch them.

[Floris van Doorn]

Eric Wieser said:

Maybe Lean 4 could repurpose Type* as syntax for "generate new universe variables (not metavariables) for everything in this group"?

It's a bit limiting. I think we have plenty of cases in mathlib where we write Type _ for a bunch of types, and some of the universe variables are equal to each other. One example: you're using a category theory hom between types (potentially with extra structure).

[Kyle Miller]

Here's another funny example of this:

import Mathlib.Logic.Basic
theorem hmm (a b : α) : decide (a = b) = true := by simp

[Yaël Dillies]

Floris, I think the plenty of cases you mention are still not many. Often you only have one type, and almost everywhere away from category theory everything is fully universe-polymorphic.