Unabstracted variables in indices of inductive types in mutual block

[arthur-adjedj]

Prerequisites

• Put an X between the brackets on this line if you have done all of the following:
  • Check that your issue is not already filed.
  • Reduce the issue to a minimal, self-contained, reproducible test case. Avoid dependencies to mathlib4 or std4.

Description

In certain cases, when elaborating inductive types, Lean fails to abstract some loose free variables in the signature of inductive types (more particularly on indices) in a mutual block, leading to an error.

Context

Discovered initially here. The issue can be avoided by using variable

Steps to Reproduce

mutual

inductive R (F: α → α → Prop) (a : α) : α → Prop where
| ind : ∀ (f: Nat → α) b, (∀ n, And₂ F a b f n) → R F a b

inductive And₂ (F: α → α → Prop) (a : α) : α → (Nat → α) → Nat → Prop where
  | mk (b : α) (f : Nat → α) (n : Nat): R F a (f n) → F (f n) b → And₂ F a b f n

end

Expected behavior: No error

Actual behavior: Error (kernel) declaration has free variables 'And₂'

Versions

4.5.0
Web Browser

Additional Information

The signature type of And₂ here is: {α : Sort u_1} → (α → α → Prop) → α → _uniq.21 → (Nat → _uniq.21) → Nat → Prop.

The issue can be circumvented by using variable, the following code works:

variable {α : Type _}

mutual

inductive R (F: α → α → Prop) (a : α) : α → Prop where
  | base : R F a a
  | ind : ∀ (f: Nat → α) b, (∀ n, And₂ F a b f n) → R F a b

inductive And₂ (F: α → α → Prop) (a : α) : α → (Nat → α) → Nat → Prop where
  | mk (b : α) (f : Nat → α) (n : Nat): R F a (f n) → F (f n) b → And₂ F a b f n

end

Impact

Add 👍 to issues you consider important. If others are impacted by this issue, please ask them to add 👍 to it.

[arthur-adjedj]

Further minimization:

mutual
inductive A (α : Type) : α → Type where

inductive B (α : Type) : α → Type where
end
/-unknown free variable '_uniq.7'-/

[mik-jozef]

I believe I found another instance of this problem that still reproduces in 4.8.0-rc1 (and the web compiler, as of writing):

structure Salg (n: Nat) where
  D: Type

mutual
inductive Ins (salg: Salg n) : salg.D → Prop
inductive Out (salg: Salg n) : salg.D → Prop
end

The error I'm getting is (kernel) declaration has free variables 'Out'. As above, variable {n: Nat} fixes the error.

[arthur-adjedj]

I'll take a look, thanks for the reporting.

[arthur-adjedj]

It appears the that issue comes from unification/metavariables. When the term is elaborated, there is still an mvar that needs to be elaborated (the n argument of Salg in salg.D. I'm guessing the metavar is resolved before that step, but is not correctly instantiated at that point. Because of this, the instantiation done here doesn't replace the expected free variables, since they do not appear in the term before the instantiation.
At first glance, it seems like replacing

        let type  := r.type |>.abstract r.params |>.instantiateRev params

with

        let type ← instantiateMVars r.type
        let type  := type |>.abstract r.params |>.instantiateRev params

Seems to resolve the issue, but I am anything but skilled when it comes to working with unification, and fear this might have some unexpected consequences. A second opinion would be greatly appreciated.