Bad type error message in presence of overloading

[mn200]

E.g.:

``(GENLIST (++) n = GENLIST f) n``;
Exception-
   HOL_ERR
     {message =
      "on line 3, characters 10-13:\nCouldn't infer type for overloaded name ++",
      origin_function = "type-analysis", origin_structure = "Preterm"} raised

There is a more fundamental error at a higher level (the equality must return bool, and to then try to apply this to anything is problematic.

[mn200]

The original post's behaviour isn't visible in standard core HOL. It can be seen by first doing something like

Overload "++" = “SUM_MAP”;

so as to guarantee an overload problem. When there isn't an overload, the error reported is that caused by trying to write GENLIST APPEND n. It's not obvious to me whether that or the higher-level error should take precedence.