Repl doesn't show the type of values after being evaluated

[andrevidela]

The documentation ported from Idris 1 shows a behaviour that the current repl doesn't support: https://idris2.readthedocs.io/en/latest/tutorial/typesfuns.html#useful-data-types

This can be remedied by turning on the showtypes setting but shouldn't it be the default since the documentation shows it?

Steps to Reproduce

Open the repl

Type "hello"

Expected Behavior

Idris> "hello"
"hello" : String

Observed Behavior

Idris> "hello"
"hello"

[edwinb]

I don't know what the default should be, but the documentation should be consistent. I can't remember exactly why I preferred not showing them for Idris 2, but iirc there were some cases where it was quite expensive due to needing to evaluate a lot that wasn't needed for just showing the value. I think also when I'm evaluating I'm generally just interested in the value, and can see the type with :t.

I suppose the documentation could say at the beginning how to get Idris to show the types.