The warnDefaulting option doesn't affect some REPL printing

[atomb]

For example:

Cryptol> :set warnDefaulting=off
Cryptol> 42 : [_]
Showing a specific instance of polymorphic result:
  * Using '6' for type wildcard (_)
0x2a
Cryptol> 42
Showing a specific instance of polymorphic result:
  * Using 'Integer' for type argument 'rep' of 'Cryptol::number'
42
Cryptol>

Maybe the warnDefaulting option should control these messages, too? These are, of course, messages that are specific to the REPL. Does warnDefaulting only apply to defaulting that occurs during normal type checking?

[yav]

Yes, warnDefaulting currenly only suppresses the actual warnings generated during type checking.

These messages are not really warnings, but rather it is Cryptol reporting on what it's doing, much like when it says "Loading...". I can see how they look similar to the other warnings though, even thought the algorithm used is quite different.

I don't have a strong opinion if this behavior should be controlled by warDefaulting or another flag.

[brianhuffman]

I checked with version 2.5.0, and its behavior matches the current behavior: warnDefaulting=off suppresses only the warnings for defaulting during type checking; it does not suppress the message when you ask to evaluate a polymorphic thing and it picks a type instance for you. So at least this is not a regression.

I guess we could do one of three things:

1. Make warnDefaulting suppress REPL defaulting as well
2. Make a new :set option to suppress only REPL defaulting messages
3. Do nothing

None of these would be hard to do. Probably the hardest part of 2 would be choosing the name of the new option.

[yav]

Does anyone have a strong preference on this? I am leaning towards 1, for simplicity. My thinking is that if you don't care about defaulting in your source code, you probably don't care about the slightly different version at the command line either, and 1 is that path of least surprise, even though it is a little less flexible than 2.

[atomb]

I'd lean toward 1, as well. It seems like the path of least surprise, as you say.

[brianhuffman]

I'll go ahead and implement option 1.