Error: unknown free variable '_uniq.402'

Stream: lean4

[François G. Dorais]

I'm not sure this should work, but the error message does not explain much: unknown free variable '_uniq.402'

structure Pos where
  protected succ ::
  protected pred : Nat

protected def Pos.add : Pos → Pos → Pos
| Pos.succ x, Pos.succ y => Pos.succ (x + y).succ
instance : Add Pos := ⟨Pos.add⟩

instance (x : Nat) : OfNat Pos x.succ := ⟨Pos.succ x⟩

def f : Pos → Pos
| 1 => 1
| x+1 => f x + x + 1

Should this work? If not, what is the actual error?

[Mario Carneiro]

this is a bug that happens when a tactic handles expressions from a goal without opening the metavariable context first

[Marcus Rossel]

@Mario Carneiro: And the tactic that is causing the problem in this case is part of Lean's attempt to show termination of f?

[Henrik Böving]

What does that funky colon syntax for succ do?

[Henrik Böving]

Ohhhh its a custom constructor but weirdly typed out, dont mind me

[Leonardo de Moura]

The weird error message is due to a missing check in the new pattern elaboration code. We have redesigned it last week to be able to support overloaded notation in patterns and issue https://github.com/leanprover/lean4/issues/944
I pushed a fix for this. https://github.com/leanprover/lean4/commit/05a2778b0db14fda956f1ff3fff9525217a5ab1e
It now produces the error

invalidPatternIssue.lean:13:0-13:20: error: invalid patterns, `x` is an explicit pattern variable, but it only occurs in positions that are inaccessible to pattern matching
  { pred := Nat.succ .(x.1) }

The x+1 pattern in f, is interpreted as { pred := Nat.succ .(x.1) }. Recall that .( .. ) is the notation for inaccessible patterns, and x.1 is x.pred.

[Leonardo de Moura]

BTW, I added a new test that uses "views" to pattern match in types such as Pos. The termination proof is a bit manual, but it will be more automated in the future.
https://github.com/leanprover/lean4/blob/68154a6c690f22d195906b9ae6563dea3f2b5f0e/tests/lean/run/posView.lean