Syntax matching error message

Stream: lean4

[Damiano Testa]

I was confused by these errors:

open Lean

example : Syntax → Syntax
  | `($s) => .missing
  | `(tactic| intro) => default  -- typeclass instance problem is stuck

-- let's try passing `.missing` instead
example : Syntax → Syntax
  | `($s) => .missing
  | `(tactic| intro) => .missing  -- invalid dotted identifier

-- let's tell Lean that `.missing` is `Syntax.missing`
example : Syntax → Syntax
  | `($s) => Syntax.missing  --  failed to infer binder type
  | `(tactic| intro) => Syntax.missing  -- there you go

-- would it be possible to have a `redundant alternative` error instead?
example : Syntax → Syntax
  | s => .missing
  | .node .. => .missing -- redundant alternative

[Thomas Murrills]

Ah, weird; it looks like this is something to do with how matches on syntax quotations are actually elaborated in terms of lets and such. Check out

variable (stx : Syntax)
#check show Syntax from match stx with | `($s) => .missing | `(tactic|intro) => .missing

which logs

let_fun this :=
  let_fun __discr := stx;
  let rhs := fun x => ?m.883 __discr x;
  let_fun s := { raw := __discr };
  Syntax.missing;
this : Syntax

It seems like the expected type is not passed through in these matches. "Failed to infer binder type" is also a weird error message (and could possibly be fixed in the same way)!

I wonder if there are some technical limitations/awkwardnesses when passing the expected types, or if passing them along is doable and would resolve these errors.

[Damiano Testa]

Thanks for the diagnosis! I don't really follow the log that you mention, but if a better error message is possible, I would be happy! In my use case, it took me a while to debug what was going on, especially since I had started with a match on a natural number and a syntax and the initial error was on the natural number 0!

[Thomas Murrills]

Oh, weird! You mean something like | n => … | `($s) => …?

[Damiano Testa]

More like match n, stx with | 0, `($s) => .missing | _, _ => .missing
(I'm on mobile and have switched off the computer for the day, so I don't guarantee that this errors in the right way!)

[Thomas Murrills]

Ah, I see!