Mem synthesis fails

Stream: lean4

[Marcus Rossel]

In the following MWE:

constant X : Type _

mutual

inductive A
  | mk (b : B)

inductive B
  | mk (a : X → A) (b : X → B)

end

example (a : A) (as : List A) (h : a ∈ as) : True := sorry

... Lean complains on the last line about h:

failed to synthesize instance
  Mem A (List A)

Even adding:

instance : Mem A (List A) where
  mem a l := l.mem a

... doesn't resolve the issue. But changing basically anything about the definition of B resolves the issue.

Is this intended?

[Horatiu Cheval]

Where is a Mem from? I remember it not being in core Lean 4 but only defined in mathlib 4

[Horatiu Cheval]

At least the error I get is simply expected token at ∈

[Marcus Rossel]

Ah, I do have Mathlib4 imported (commit from 2022-02-08).

[Mario Carneiro]

what are your imports? Even if mathlib4 is a dependency this code would still not work

[Marcus Rossel]

Mario Carneiro said:

what are your imports? Even if mathlib4 is a dependency this code would still not work

Only mathlib. Here's a full setup that reproduces the issue: https://github.com/marcusrossel/mwe/tree/mem-synthesis-fails

[Marcus Rossel]

And here's a version without any imports:

constant X : Type _

mutual

inductive A
  | mk (b : B)

inductive B
  | mk (a : X → A) (b : X → B)

end

class Mem (α : outParam $ Type u) (γ : Type v) where
  mem : α → γ → Prop

infix:50 " ∈ " => Mem.mem

def mem (a : α) : List α → Prop
  | [] => False
  | (b :: l) => a = b ∨ mem a l

instance : Mem α (List α) := ⟨mem⟩

example (a : A) (as : List A) (h : a ∈ as) : True := sorry

[Leonardo de Moura]

The issue is due to universe contraints. Note that A and B have two universe parameters: one for each X.

set_option pp.all true
#print A
#print B

You did not specify these universe parameters in your example. The following works

example (a : A.{u, v}) (as : List A.{u, v}) (h : a ∈ as) : True := sorry

Another option is to simplify your mutual definition and make sure both Xs are using the same universe

mutual

inductive A
  | mk (b : B)

inductive B
  | mk (a : X.{u} → A) (b : X.{u} → B)

end

[Leonardo de Moura]

Without specifying the universes in your original example, type class resolution fails when trying to solve

max ?u.1701 ?u.1700 =?= max ?u.1706 ?u.1705

Lean 4 does not approximate the solution using

?u.1701  =?= ?u.1706
?u.1700 =?= ?u.1705

[Marcus Rossel]

Leonardo de Moura said:

The issue is due to universe contraints. Note that A and B have two universe parameters: one for each X.

I don't understand why each X has its own universe parameter.
Is this somehow related to the fact that X is declared as a constant?

Or perhaps as a related question: How could it happen that I use Xs from different universes in the same definition? And are there any other types where this is a thing?

[Marcus Rossel]

But thanks, this helped solve my issue!

[Horatiu Cheval]

I don't think it's related to constant X : Type _, the same happens if you replace it with some universe polymorphic def, like def X := Type _

[Horatiu Cheval]

I guess each X is getting its own parameter because Lean tries to be as polymorphic as possible, so each occurrence of the same (modulo universe) term is universe independent from the other? Like

set_option pp.universes true

def p : (α → α) × (β → β) := ⟨id, id⟩
#check @p
-- @p.{u_1, u_2} : {α : Type u_1} → {β : Type u_2} → Prod.{u_1, u_2} (α → α) (β → β)

[Marcus Rossel]

Wouldn't the analogous definition be def X : Type _ := <something> though?

[Horatiu Cheval]

Well yeah, it's def x : Type _ := Type _ :)