#13702 error messages: specialized error messages for non-functors - #13865
Conversation
|
I think we should iterate a bit on the proposed message in the first case.
First, I think that you mean that a structure was expected, right? Second, I'm worried that the wording "This module should not be a functor" could be confusing to users which use "module" as a synonym for "structure". I would write simply:
or maybe a "plain structure" or a "(non-functor) structure" or a "(non-parametrized) structure". |
|
You are right that structure will be clearer. For your second point, I believe that
is clear even for people that doesn't make a clear distinction between functors and structures, or use |
|
I have updated the wording; and removed an unreachable code path for abstract module types. |
As reported in #13702, functors appearing in a context where non-functor where expected, for instance
are handled by the generic functor parameters mismatch error message:
which is not easy to decipher.
This PR proposes to specialize the error message to reduce it to a simpler
with a variant when the expected type is incompatible with the body of the functor
The reverse situation of structure appearing where a functor was expected is handled symmetrically
without the symmetrical hint of suggesting adding abstractions, which does not seems likely to be correct.