why doesn't this work?

Stream: new members

[Alex Kontorovich]

Can someone please help explain why the following:

lemma sum_plus_one1 (F:ℕ → ℝ ) (m:ℕ ) : sum (range (nat.succ m)) F = sum (range m) F + F m:=
begin
  exact sum_range_succ' F m,
end

doesn't work, and gives an error that says:

invalid type ascription, term has type
sum (range (nat.succ m)) F = sum (range m) (F ∘ nat.succ) + F 0
but is expected to have type
sum (range (nat.succ m)) F = sum (range m) F + F m

WTF?!?! Where did that "F ∘ nat.succ" come from??? The lemma is verbatim what the tactic is asking for...? Thank you!

[Reid Barton]

Well, looking at the error message, it seems that sum_range_succ' splits off the first element of the sum, not the last.

[Alex Kontorovich]

I don't follow? I literally copied and pasted what it said was "is expected to have type" into the lemma statement?

[Reid Barton]

You're reading the error message backwards, then.

[Alex Kontorovich]

Argh!!! You're right. Thanks.

[Alex Kontorovich]

Meant to use sum_range_succ instead

[Reid Barton]

GHC has a similar error message and it seems to confuse a lot of people there, too, though I never understood how. I guess it is like one of those optical illusions, where once you see it one way it is tricky to see it the other way.

[Reid Barton]

I think they may have reworded this error message in GHC recently, actually.

[Reid Barton]

I think it's the phrase "expected" type that trips people up