equation compiler bad term

Stream: general

[Bhavik Mehta]

namespace list

def thing {ι : Type*} : ℕ → list ι → list (ι → ℕ)
| 0 l := [λ _, 0]
| (n+1) [] := []
| (n+1) (x :: xs) := (range n).bind (λ i, thing i xs)

lemma thing_zero {ι : Type*} (l : list ι) :
  thing 0 l = [λ _, 0] :=
begin
  refl,
end

Here's my example - the proof refl is accepted (as is by exact rfl) in tactic mode, but the overall definition gives me an error:

type mismatch at definition 'list.thing_zero', has type
  ∀ {ι : Type u_1} (l : list ι), thing 0 l = thing 0 l
but is expected to have type
  ∀ {ι : Type u_1} (l : list ι), thing 0 l = [λ (_x : ι), 0]

By looking at #print prefix list.thing, it shows four equations, splitting the first case into two - why does this happen? Also, is it possible for a more helpful error message here: from the definition I gave, I expected those two types to be the same thing

[Mario Carneiro]

Oh, that is a weird definition. It looks like it's going to be an induction on n but it's not

[Mario Carneiro]

if you reverse the order of arguments to make it clearer it errors where you would expect

def thing {ι : Type*} : list ι → ℕ → list (ι → ℕ)
| l 0 := [λ _, 0]
| [] (n+1) := []
| (x :: xs) (n+1) := (range n).bind (λ i, thing xs i)

lemma thing_zero {ι : Type*} (l : list ι) :
  thing l 0 = [λ _, 0] :=
rfl -- error

[Mario Carneiro]

I'm not sure how but you have somehow tricked the elaborator into thinking this is rfl when it's not. Looking at the generated definitions it definitely will not be a rfl proof, and the kernel knows what's up

[Mario Carneiro]

in any case the correct proof is

lemma thing_zero {ι : Type*} (l : list ι) :
  thing 0 l = [λ _, 0] :=
by cases l; refl

[Bhavik Mehta]

Yeah I figured that doing cases would work, but I guess I'm surprised at why the generated definitions are what they are - I would have thought it'd be something like: if the nat is zero then it's this, otherwise case-split on the list