invalid pattern, dependent elimination failure

Stream: lean4

[Max Nowak 🐉]

I have minimized my problem into the following, where I get a very short and not very insightful "invalid pattern ?m.1234 u" error.

inductive Ty : Type 1
| U : Ty
| Pi : (Nat -> Ty) -> Ty

inductive Tm : Ty -> Type 1
| app : Tm (Ty.Pi A) -> Tm (A 0)

def foo {A : Ty} : Tm A -> Nat
| .app t => 0 -- invalid pattern ?m.1234 0`

And with the following, slightly less minimal example, I get "dependent elimination failed"

-- Same Ty

/-- Typed terms. -/
inductive Tm : Ty -> Type 1
/-- A term `t` can have function type `Nat -> A`, then `t arg` has type `A arg`. -/
| app :
  Tm (Ty.Pi A) -> -- Given "⊢ t : (u : Nat) -> A u"
  (arg : Nat) -> -- Given "arg : Nat"
  Tm (A arg) -- Conclude "⊢ t arg : A arg"

def foo {A : Ty} : Tm A -> Nat
| .app t u => 0 -- here

Gives the error:

dependent elimination failed, type mismatch when solving alternative with type
  motive (Tm.app _uniq.45254 arg✝)
but expected
  motive (Tm.app a✝ arg✝)

I have been staring at these errors and have no clue how to start debugging them, other than maybe try finding a manual invocation of Tm.rec with my own motive.

For some context, foo is supposed to be this.

[Mario Carneiro]

you need to move the {A : Ty} into the pattern match

[Mario Carneiro]

oh no, you need Tm.app instead of .app in the first example

[Max Nowak 🐉]

Oh! huh

[Mario Carneiro]

adding .app (A := A) fixes both examples

[Max Nowak 🐉]

...that also solves my non-minimized problem. I actually genuinely have no idea why the .app (A := A) t u works, whereas Tm.app _ _ A t u does not. I thought those would desugar to the same.

[Mario Carneiro]

Did you forget a @?

[Mario Carneiro]

@Tm.app A t u works on the (second) minimized example

[Max Nowak 🐉]

Yes sorry I forgot to write the @ in chat here.

[Mario Carneiro]

(I assume the _ _ are additional parameters not in the MWE?)

[Max Nowak 🐉]

Yeah my original problem has more implicit parameters, hence the _.

[Mario Carneiro]

but moving the {A : Ty} into the match can also help, like this:

def foo : {A : Ty} → Tm A -> Nat
| _, @Tm.app A t u => 0 -- here

[Mario Carneiro]

lean will sometimes infer that it needs to do this but it's not 100%

[Mario Carneiro]

whenever you are pattern matching an inductive family, you always need to pattern match the indices at the same time

[Mario Carneiro]

and you shouldn't provide a value either, or it can mess things up. There is only one thing you can put there and it is an "inaccessible pattern" .(_). In theory you should be able to put the type there as in .(A u), but inaccessible patterns are used so rarely that support for them seems to be broken

[Max Nowak 🐉]

Nevermind, the original problem also works by doing | _, @Tm.app _ _ A t u => .... I think my thinko was that I was trying to do something like | SPi _, Tm.app t u => ... instead and that doesn't really make sense.

[Max Nowak 🐉]

I can't do | .(A u), ... since the u is bound only on the second parameter.

[Mario Carneiro]

I know, the syntax is weird

[Mario Carneiro]

an inaccessible pattern is not really a pattern

[Mario Carneiro]

it's more like a type ascription

[Mario Carneiro]

and it can use pattern variables in later arguments (actually it pretty much has to)

[Max Nowak 🐉]

Oh! That's really weird

[Mario Carneiro]

But _ also works as an inaccessible pattern and that's the most commonly used method

[Max Nowak 🐉]

Yeah, if it works. If not then it might still be useful to know how inaccessible patterns work for debugging purposes. But now I at least have a starting point for the next time I encounter a problem like this. You helped greatly, thank you :).

[Mario Carneiro]

in particular, variables used in an inaccessible pattern are not introduced like regular pattern variables, they are references to existing variables

[Mario Carneiro]

You might need to consult lean 3 to find out how they work because I suspect they are untested in lean 4

[Max Nowak 🐉]

I now have stumbled upon a related problem. Here is a MWE:

inductive Ty : Type 1
| U : Ty
| Pi : (Nat -> Ty) -> Ty

/-- Typed terms. -/
inductive Tm : Ty -> Type 1
/-- A term `t` can have function type `Nat -> A`, then `t arg` has type `A arg`. -/
| app {A : Nat -> Ty} :
  Tm (Ty.Pi A) -> -- Given "⊢ t : (u : Nat) -> A u"
  (u : Nat) -> -- Given "u : Nat"
  Tm (A u) -- Conclude "t u : A u"

def TyA : Ty -> Type := fun _ => String

def foo : {A : Ty} -> (a : TyA A) -> Tm A -> Nat
--| _, _, @Tm.app A t u => 0 -- works but useless
| _, a, @Tm.app A t u => 0 -- Problem here, see below for error

The error I get on the last line is:

type mismatch
  Tm.app t u
has type
  Tm (A u) : Type 1
but is expected to have type
  Tm ?m.45216 : Type 1

From what I've gathered above, I should be able to write

| .(A u), a, @Tm.app A t u => 0

to justify this, but that just leads to another error. From what I can tell, the root problem is that @Tm.app A t u : Tm (A u), but the A u is being a pain. I wish I could simply name B := A u and then only use B instead, but that leads to even more errors.

[Kyle Miller]

So far I've found that it has something to do with not unfolding TyA?
This works:

def foo : {A : Ty} -> (a : (fun _ => String) A) -> Tm A -> Nat
| _, a, @Tm.app A t u => 0

(Or just (a : String).)

[Max Nowak 🐉]

My guess is that it works because the type of a no longer depends on A by unfolding TyA. Unfortunately in my original problem TyA is recursive and type of a actually needs to depend on A.

[Max Nowak 🐉]

I am still stuck at this problem. Maybe a mod can move this thread (or the messages since feb5) to general? I am not sure what the difference is between general and lean4 actually.

[Arthur Adjedj]

if you replace a with a wild card, it seems to get unified correctly, and the variable even appears in the context (if you use by). While this is an ugly workaround, I believe doing something like this might solve your problem:

def foo : {A : Ty} -> (a : TyA A) -> Tm A -> Nat
| _, _, @Tm.app A t u => by
  rename_i a
 --a : TyA (A u)

[Max Nowak 🐉]

Okay rename_i seems to work as a workaround! I haven't checked whether I can do what I want to do this way yet, but it looks promising! Thank you so much for getting me un-stuck. This sounds like something I should post as an issue. I don't know what causes this issue, and I don't have time to investigate. Should I just post the same MWE as an issue on github? Any other investigating I should do before I put it on github?

[Max Nowak 🐉]

There's a few related paper cuts in this thread if you scroll up, I could include them in the issue. I'm not sure whether they're the same underlying issue though. And that has been scaring me away from actually putting an issue on github. Feels like I should investigate on my own, but I never have time for that :P.

[Timo Carlin-Burns]

Here is another workaround:

inductive Ty : Type 1
| U : Ty
| Pi : (Nat -> Ty) -> Ty

/-- Typed terms. -/
inductive Tm : Ty -> Type 1
/-- A term `t` can have function type `Nat -> A`, then `t arg` has type `A arg`. -/
| app {A : Nat -> Ty} :
  Tm (Ty.Pi A) -> -- Given "⊢ t : (u : Nat) -> A u"
  (u : Nat) -> -- Given "u : Nat"
  (A_u : Ty) ->
  (h_A_u : A_u = A u) ->
  Tm A_u -- Conclude "t u : A u"

def TyA : Ty -> Type := fun _ => String

def foo : {A : Ty} -> (a : TyA A) -> Tm A -> Nat
| _, a, @Tm.app A t u _ h_A_u => by
  subst h_A_u
  sorry

There is a general piece of advice to avoid function applications in index position when defining an inductive type. I don't know if that's what's causing the problems here, but it seems like it might be. You can read more about this advice in an old Zulip thread