Type mismatch with Qq library

Stream: lean4

[Heather Macbeth]

Suppose I wanted to parse an expression of the form (a + (b + c)) + d into a list [a, b, c, d] (this is a simplified problem but I can #xy if needed). Here is my quick attempt to do this with quote4:

import Qq

open Lean Qq

def parse {v : Level} (M : Q(Type v)) (x : Q($M)) : MetaM (Q(List $M)) := do
  match x with
  | ~q(@HAdd.hAdd $N $N $N _ $x $y) =>
    let .defEq (_ : $M =Q $N) ← isDefEqQ M N | throwError "FIXME let's deal with this later"
    let a : Q(List $M) ← parse M x
    let b : Q(List $M) ← parse M y
    pure q($a ++ $b)
  | e => pure q([$e])

This produces the following error:

type mismatch
  ?m✝ + ?m✝¹
has type
  ?m✝ : Type ?u.370
but is expected to have type
  «$M» : Type v

Can someone explain this error? What am I doing wrong?

[Mario Carneiro]

Here's an alternative version:

partial def parse {v : Level} (M : Q(Type v)) (x : Q($M)) : MetaM (List Q($M)) := do
  match x with
  | ~q(@HAdd.hAdd $N₁ $N₂ _ (_) $x $y) =>
    let .defEq _ ← isDefEqQ (u := v) M N₁ | throwError "FIXME let's deal with this later"
    let .defEq _ ← isDefEqQ (u := v) M N₂ | throwError "FIXME let's deal with this later"
    let a ← parse M x
    let b ← parse M y
    pure (a ++ b)
  | e => pure [e]

[𝚠𝚘𝚓𝚌𝚒𝚎𝚌𝚑 𝚗𝚊𝚠𝚛𝚘𝚌𝚔𝚒]

In ~q(#HAdd.hAdd $N $N $N _ $x $y), you are specifying that the return type of the expression is N; but it is M by assumption, and Lean cannot unify them. Here is a simpler example of the same issue:

inductive Abc : Nat → Type where
  | mk : (n : Nat) → Abc n

example  : Abc 0 → Nat
  /-
  type mismatch
    Abc.mk a
  has type
    Abc a : Type
  but is expected to have type
    Abc 0 : Type
  -/
  | .mk a => sorry

[𝚠𝚘𝚓𝚌𝚒𝚎𝚌𝚑 𝚗𝚊𝚠𝚛𝚘𝚌𝚔𝚒]

In Mario's version, ~q(@HAdd.hAdd $N₁ $N₂ _ (_) $x $y) leaves the output type unconstrained. And, afaict, it uses (_) because if you use _ in an instance position with Qq, Lean will try to infer it and fail.

[Heather Macbeth]

Thank you both, this helps a lot. Also this
Wojciech Nawrocki said:

In Mario's version, ~q(@HAdd.hAdd $N₁ $N₂ _ (_) $x $y) leaves the output type unconstrained. And, afaict, it uses (_) because if you use _ in an instance position with Qq, Lean will try to infer it and fail.

was new to me (and probably the missing piece of syntax that prevented me from bashing through by trial and error).

[Heather Macbeth]

By the way, I had hoped that after I pointed out to Qq that M and N₁ were the same, I would be able to use things of type Q(M) and Q(N₁) interchangeably. This is not the case (I'm getting errors from this). Is there a standard workaround here?

[Heather Macbeth]

For example, is there a syntax for matching like

  | ~q(@HAdd.hAdd M M _ (_) $x $y)

which really enforces that the things in the two M-spots are Ms?

[Eric Wieser]

If you want to only match homogeneous addition you can use HAdd.hAdd _ _ _ (@instHAdd $M (_)) $x $y

[Eric Wieser]

The syntax you ask for doesn't exist for Qq, just as it doesn't for syntax or regular matches