`:doc` should show types as they were written

[alissa-tung]

Steps to Reproduce

data Issue : Nat -> Type where
  MkCons : (n : Nat) -> (0 p : n = 42) -> Issue n

Expected Behavior

Main> :doc Issue
Main.Issue : Nat -> Type
  Totality: total
  Constructor: MkCons : (n : Nat) -> (0 p : n = 42) -> Issue n

Observed Behavior

Main> :doc Issue
Main.Issue : Nat -> Type
  Totality: total
  Constructor: MkCons : (n : Nat) -> (0 _ : n = 42) -> Issue n

[gallais]

IIRC that's due to the fact we are using the elaborated type rather than the source one. We saw similar issues in the html backend at some point. It may not be the easiest to fix but it would be useful for sure given that named application is a thing so names are important.

[alissa-tung]

Redundant newlines and brackets:

Main> :let (::.) : List a -> a -> List a
Main> :let infixl 7 ::.
Main> :let z : Tx (gamma ::. a ::. b ::. c)
Main> :t z
Main.z : Tx (((gamma ::. a) ::. b) ::. c)

Main> :let (::::) : List a -> a -> List a
Main> :doc (::::)    
Main.:::: : List a -> a -> List a

Main>

and I am wondering why (::)'s docs have a different color to other operators.

[gallais]

• Red is constructor
• Green is definition
• Blue is type constructor

[gallais]

A possible fix:

1. Modify PiInfo so that Explicit carries a Maybe Name recording whether the user had provided an explicit name
2. Patch the pretty printer in Idris.Pretty to use that name if it is present, even if the Pi is not dependent

Step 1. will break a lot of code I presume but these errors should be super easy to fix. You'll just have to follow the compiler as it chases type error after type error. I may eventually do it on a day I'm looking for a zen extended refactoring.