Kernel error on declaring inductive type

Stream: lean4

[Siddharth Bhat]

Consider the MWE inductive declaration:

abbrev Kind := Unit
abbrev ExprKind :=  Unit
inductive OpKind : Kind → Kind → Type
| const : OpKind () ()

inductive Expr : ExprKind → Type where
| ops: Expr () → Expr () → Expr () -- op ;; ops.

inductive ExprEval {kindMotive : Kind → Type}
  (opFold: {i o: Kind} → OpKind i o → kindMotive i → kindMotive o) : Expr ek  → Type where
  | ops (EVAL_OPS: ExprEval opFold ops) : ExprEval opFold (Expr.ops op ops)

which fails with an error:

(kernel) arg #9 of 'ExprEval.ops' contains a non valid occurrence of the datatypes being declared

Lean nightly:

~/work/new/ssa/ssa lean --version
Lean (version 4.0.0-nightly-2023-03-01, commit 0da281fab48d, Release)

I am unsure what's going wrong. The current example looks far too artificial, the code arises from writing an inductive type that represents derivation rules for stepping through the evaluation of an intrinsically well-typed AST.

[Marcus Rossel]

Superficially this looks like it could be related to a change in the last nightly - though I don't understand how:
https://github.com/leanprover/lean4-nightly/commit/0da281fab48d353e9da080d81dc7d736836f84b6

[Gabriel Ebner]

I get the same error with older nightlies, so it doesn't seem to be related to lean4#2125

[Gabriel Ebner]

Fixed:

abbrev Kind := Unit
abbrev ExprKind :=  Unit
inductive OpKind : Kind → Kind → Type
| const : OpKind () ()

inductive Expr : ExprKind → Type where
| ops: Expr () → Expr () → Expr () -- op ;; ops.

inductive ExprEval {kindMotive : Kind → Type}
  (opFold: {i o: Kind} → OpKind i o → kindMotive i → kindMotive o) : Expr ek  → Type where
  | ops (EVAL_OPS: @ExprEval kindMotive @opFold ek ops) : ExprEval opFold (Expr.ops op ops)

[Henrik Böving]

Is this just a wrong guess of the unification algorithm then?

[Gabriel Ebner]

It's a combination of the inductive module being overly pedantic, and the unifier being overly sloppy. The inductive module wants the parameters (kindMotive, opFold, and ek) to match exactly (i.e., be free variables). While the unifier creates a lambda for opFold and thinks that's good enough because it's defeq.

[Siddharth Bhat]

Is this an issue I should file?

[Gabriel Ebner]

I don't think there's anything broken here. The error message could of course be better.

[Gabriel Ebner]

If you can easily work around it, I would just lay low for now.