large vs small elimination

Stream: general

[Reid Barton]

For each inductive type or structure Lean has to decide whether to generate large or small eliminators (eliminating to a type in an arbitrary universe, or only to a proposition). As I understand it, the algorithm is something like this.

• If the target universe of the inductive type is a Type (Sort u for u >= 1), then always generate a large eliminator.
• If the target universe is Prop, then only generate a large eliminator if there's at most one constructor and all of its fields are Props.

However, with universe polymorphism, the target universe might be Prop for some values of the universe parameters but not others. Currently Lean just rejects such definitions. That means you cannot define a structure like

universe u
structure a (x : Sort u) : Sort u := (f : x)

You have to use a target universe of Sort (max u 1) or similar. This causes some minor issues in #824 where we want to replace Type by Sort in category theory.

Would it be possible/sound for Lean to instead do the following?

• Solve for the universe variable substitutions which cause the target universe to become Prop = Sort 0, if possible. (This can be done in a simple syntax-directed way: max u v = 0 iff u = 0 and v = 0; imax u v = 0 iff v = 0; u+1 is never 0; etc.)
• If there are such substitutions, then apply them before doing the large eliminator check for Props.

In the example, a large eliminator would be generated for a, because when the target universe is Prop, the field f is also a Prop.

Are there other reasons that Lean needs to know whether or not the target universe is a Prop?

[Mario Carneiro]

This would obviously require a modification to lean's kernel, but I can confirm soundness against the paper proof.

[Mario Carneiro]

I think lean will accept inductive types in Sort u under some circumstances; there are weird consequences in general, but it should be fine for large eliminating inductives

[Mario Carneiro]

In particular, lean seems to have no trouble with the structure you gave, if you use an inductive instead:

inductive {u} foo (α : Sort u) : Sort u
| mk : α → foo

[Reid Barton]

Oh interesting

[Reid Barton]

It only generates a small eliminator, though

[Mario Carneiro]

ah yes, that's the weird consequence

[Mario Carneiro]

that's why the structure won't work, of course