## Stream: new members

### Topic: why doesn't this work?

#### Alex Kontorovich (Apr 22 2020 at 13:46):

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 (Apr 22 2020 at 13:47):

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 (Apr 22 2020 at 13:48):

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

#### Reid Barton (Apr 22 2020 at 13:48):

You're reading the error message backwards, then.

#### Alex Kontorovich (Apr 22 2020 at 13:49):

Argh!!! You're right. Thanks.

#### Alex Kontorovich (Apr 22 2020 at 13:49):

Meant to use sum_range_succ instead

#### Reid Barton (Apr 22 2020 at 13:50):

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 (Apr 22 2020 at 13:51):

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

#### Reid Barton (Apr 22 2020 at 13:52):

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

Last updated: May 11 2021 at 14:11 UTC