`foldr-++` (Lists): the postulated form is misleading and causing type mismatch

[adql]

In exercise foldr-++ the student is asked to show that

foldr _⊗_ e (xs ++ ys) ≡ foldr _⊗_ (foldr _⊗_ e ys) xs

Later in the chapter, in section "Monoids", this is postulated as specialized to a monoidal action:

postulate
  foldr-++ : ∀ {A : Set} (_⊗_ : A → A → A) (e : A) (xs ys : List A) →
    foldr _⊗_ e (xs ++ ys) ≡ foldr _⊗_ (foldr _⊗_ e ys) xs

Notice especially the types of _⊗_ and e.

Since this has to be commented out in order to solve the exercise above, the student might adopt the type signature to be used in their own solution. This is not a problem for solving that exercise – however, the next exercise foldr-∷ asks:

Show as a consequence of foldr-++ above that

xs ++ ys ≡ foldr ∷ ys xs

This doesn't work with the postulated type signature since _∷_ : A → List A → List A and [] : List A , whereas foldr-++ is postulated with _⊗_ : A → A → A and e : A. This misleads the student to unnecessary frustration.

I suggest postulating foldr-++ in the exercise's subsection itself (as usually done throughout the book) with ∀ {A B : Set} (_⊗_ : A → B → B) (e : B) ....

[wadler]

Thank you for your thoughtful suggestion.

I'd be delighted to accept a pull request along the lines you suggest.