@[mk_iff] causes a type error

[eric-wieser]

The following fails with a weird error when mk_iff is uncommented:

import data.list.basic

universe u

def nary_rel (α : Type u) : ℕ → Type u
| 0 := α → Prop
| (n + 1) := α → nary_rel n

-- @[mk_iff]
inductive list.nwise {α : Type u} : Π n, nary_rel α n → list α → Prop
| zero (r : nary_rel α 0) (l : list α) (h : ∀ x ∈ l, r x) : list.nwise 0 r l
| nil {n} (r : nary_rel α _) : list.nwise (n + 1) r []
| cons {n} (r : nary_rel α (n+1)) (x : α) (xs : list α)
  (hx : list.nwise n (r x) xs) (hxs : list.nwise (n + 1) r xs) : list.nwise _ r (x :: xs)

The error is on the r x in the | zero constructor, and is:

infer type failed, function expected at
  ᾰ x
term
  ᾰ
has type
  nary_rel α n

[digama0]

I think this error makes sense. It tried to write down something like list.nwise n r l <-> (∀ x ∈ l, r x) \/ ... and got hit by a type error there because r is not a function when n is generic. What do you want the theorem to look like?

Aside: This inductive looks better suited as a definition by recursion on n and then l.

[eric-wieser]

Aside: This inductive looks better suited as a definition by recursion on n and then l.

Indeed, I was just trying to compare the inductive type vs recursive def approach. What I actually have is along the lines of:

def nary_rel (α : Type u) : ℕ → Type u
| 0 := α → Prop
| (n + 1) := α → nary_rel n

def list.nwise {α : Type u} : Π n, nary_rel α n → list α → Prop
| 0 r l := ∀ x ∈ l, r x
| (n + 1) r [] := true
| (n + 1) r (x :: xs) := xs.nwise _ (r x) ∧ xs.nwise _ r

@[simp] lemma list.nwise_zero (r : nary_rel α 0) (l : list α) :
  l.nwise _ r ↔ ∀ x ∈ l, r x :=
by cases l; simp [list.nwise]

lemma nwise_iff_pairwise {α : Type u} (l : list α) (r : α → α → Prop) :
  l.pairwise r ↔ l.nwise 1 r :=
begin
  induction l,
  { simp [list.nwise], },
  { simp only [list.nwise, list.pairwise_cons, l_ih],
    refine and_congr _ iff.rfl,
    dsimp [nat.add_zero, list.nwise],
    rw list.nwise_zero, },
end

but I assumed since pairwise was defined inductively, there was some advantage to doing so. Annoying the above creates four equation lemmas not three.

[eric-wieser]

What do you want the theorem to look like?

Honestly I have no idea, I expected mk_iff to produce some message telling me the type is unsupported, rather than tricking me into thinking my inductive itself has an error.

[YaelDillies]

Is the error message better in Lean 4? Should we open an issue?

[digama0]

The error message is essentially the same:

function expected
  a✝¹ x

However the message appears on the word mk_iff rather than the inductive itself, so it seems less likely to cause Eric's specific confusion.

[YaelDillies]

Okay, let's close this then. I hope we do eventually get better error all around, though.