Regression in implicit argument inference

Stream: lean4

[Mario Carneiro]

This fails on today's nightly but not yesterday's:

inductive sublist : List α → List α → Prop
  | slnil : sublist [] []
  | cons l₁ l₂ a : sublist l₁ l₂ → sublist l₁ (a :: l₂)
  | cons2 l₁ l₂ a : sublist l₁ l₂ → sublist (a :: l₁) (a :: l₂)

The issue appears to be that the type parameter of sublist cannot be inferred from these uses. In fact, each use of the sublist variable is inferred separately, so all these annotations are needed:

inductive sublist : List α → List α → Prop
  | slnil : @sublist α [] []
  | cons l₁ l₂ a : @sublist α l₁ l₂ → sublist l₁ (a :: l₂)
  | cons2 l₁ l₂ a : @sublist α l₁ l₂ → sublist (a :: l₁) (a :: l₂)

From one perspective, this makes sense, the use sublist [] [] does not give away what type alpha is. But it is especially frustrating in this case since it is a parameter to the inductive type (and these are often implicit type arguments like here). Is this deliberate? (Looking at the RSS does not reveal any commits that look like they are supposed to affect this, so perhaps it is a bug.)

[Sebastian Ullrich]

since it is a parameter to the inductive type

I think that's the problem: it isn't inferred as such anymore https://github.com/leanprover/lean4-nightly/releases/tag/nightly-2022-03-07

[Mario Carneiro]

Hm, that seems... undesirable. I would much rather have indices be required to be written explicitly, since they have such an important effect on the inductive spec. The fact that auto-bounds are also usually placed before all other arguments suggests that they would end up before the colon, and I guess even in an inductive type we can get auto-bounds to be parameters if they are mentioned in another parameter.

[Leonardo de Moura]

The change was motivated by this example: https://github.com/leanprover/lean4/blob/master/tests/lean/run/interp.lean
We have experienced a similar regression in the Lean4 repo ourselves: https://github.com/leanprover/lean4/commit/b105c006a57438d76bc72733a47c9552bd0cae03
I want both instances to work without providing the implicit arguments.
I am planning to analyze the shape of the constructor to decide what should be an index or not.

[Leonardo de Moura]

In the meantime, we can write sublist as

inductive sublist {α} : List α → List α → Prop
  | slnil : sublist [] []
  | cons l₁ l₂ a : sublist l₁ l₂ → sublist l₁ (a :: l₂)
  | cons2 l₁ l₂ a : sublist l₁ l₂ → sublist (a :: l₁) (a :: l₂)

[Mario Carneiro]

@Leonardo de Moura I saw the example, but I think that even if lean did magic to figure this out, it is not clear code and should be discouraged. Like here:

inductive Expr : Vector Ty n → Ty → Type where
  | var   : HasType i ctx ty → Expr ctx ty
  | val   : Int → Expr ctx Ty.int
  | lam   : Expr (a :: ctx) ty → Expr ctx (Ty.fn a ty)
  | app   : Expr ctx (Ty.fn a ty) → Expr ctx a → Expr ctx ty
  | op    : (a.interp → b.interp → c.interp) → Expr ctx a → Expr ctx b → Expr ctx c
  | ife   : Expr ctx Ty.bool → Expr ctx a → Expr ctx a → Expr ctx a
  | delay : (Unit → Expr ctx a) → Expr ctx a

It isn't obvious whether this is supposed to be a collection of types with fixed context depth n, or of various depths, and I have to go hunting for a constructor that requires a different context before I can tell. That should really be made explicit in the type signature of Expr.

[Leonardo de Moura]

@Mario Carneiro This is example is from the Idris manual. It looks very elegant and compact. And it is also now compact in Lean 4. It is a simple example, and it should look simple. In Lean 3, this example is super messy.
Note that, you can still make everything explicit if you want and even disable the auto implicit feature. It is up to you, but I suspect many Idris users would prefer the compact version.

[Mario Carneiro]

The delta on the example is also small, you just add Expr : \forall {n}, Vector Ty n → Ty → Type and nothing else changes. Idris doesn't have a distinction between parameters and indices, but in lean this is important information for the reader so I don't think it should be elided.

[Mario Carneiro]

the rule "auto-bound arguments are always parameters" is easy to learn and can prevent mistakes

[Leonardo de Moura]

This is a simple example, it can get much more complicated if one makes heavy use of inductive families as they do in Idris and Agda.
Forcing them to add the \forall {n}, looks like a bug, and most users will be confused by the error message if they forget the \forall {n},.

[Mario Carneiro]

Also, at least in mathlib these kinds of examples are essentially nonexistent, because we avoid inductive type families like Vector, so the current behavior is going to get the wrong answer in most mathlib examples

[Mario Carneiro]

because making the \alpha an index is a silent bug that I didn't even notice while upgrading until sebastian pointed out the change

[Mario Carneiro]

If sublist had proper type ascriptions in it, it wouldn't even have broken, it would just silently have different behavior

[Leonardo de Moura]

Mario Carneiro said:

Also, at least in mathlib these kinds of examples are essentially nonexistent, because we avoid inductive type families like Vector, so the current behavior is going to get the wrong answer in most mathlib examples

Sure, I agree mathlib does not make heavy use of this feature, but there will be other users.

[Mario Carneiro]

I think that we should always default to making as few things indices as possible. That is an explicit part of the design of the inductive and deserves to be called out. If you can do magic to fix the idris example, okay, but without the magic I think that defaulting to indices will pull in all sorts of weird things that the user will not easily be able to see

[Leonardo de Moura]

Mario Carneiro said:

because making the \alpha an index is a silent bug that I didn't even notice while upgrading until sebastian pointed out the change

Sure, I understand, but we are trying to make the system better and this kind of thing will happen.
This may be annoying now, but I suspect after you get used to the new feature, you will not even remember the old behavior.

[Leonardo de Moura]

Mario Carneiro said:

I think that we should always default to making as few things indices as possible. That is an explicit part of the design of the inductive and deserves to be called out. If you can do magic to fix the idris example, okay, but without the magic I think that defaulting to indices will pull in all sorts of weird things that the user will not easily be able to see

I am adding a new feature that will promote fixed indices to parameters. I hope it will address the concerns in this thread.

[Mario Carneiro]

That is a good idea (especially if you can somehow fix the inference issue in the original example), although if it works also on variables to the right of the colon then it will make certain inductive types inexpressible. In my experience there is no need to ever have an index that doesn't vary and making it a parameter is always better, but perhaps an option should be able to turn it off for the odd case where you actually want such an inductive for didactic purposes or something.