My complaint (such as it is) is only concerning the wording of the second error message (on flatten). To me, a type variable appearing is always (implicitly) quantified universally. Here the derived type had an existential qualification. (Right?) In that case it would be nice to have some indication that that was what was going on.