Strange :help output for newtypes and enums

[RyanGlScott]

Given this Cryptol file:

newtype T a = { unT : a }

If you type :help T at the REPL, you'll get:

Main> :help T

newtype T a
    T : {a} {unT : a} -> T a
            ---------
Name defined in module Main

This is unsatisfactory for a couple of reasons:

1. The :help output doesn't state the kind of T. This is inconsistent with how :help displays other type constructors, e.g.,

   Main> :help Z
   
   primitive type Z : # -> *
   

2. The pretty-printed definition of T "re-quantifies" a, as it displays both newtype T a and T : {a} {unT : a} -> T a. Really, the a in newtype T a ought to scope over the type of T so that it is displayed like this:

   newtype T a =
     T { unT : a}
   

The same issues apply to enums (#1602) as well.

[RyanGlScott]

Things are now somewhat better in the sum-types branch, since :help T now prints:

Main> :help T

newtype T a

            ---------

Constructor of T
    T : {a} {unT : a} -> T a

The newtype T a part feels strange, however. I can't help but wonder if that should just be newtype T : * -> *, per (1) above.

---

The :help output for enums is arguably still broken. If you have this:

enum Maybe a = Nothing | Just a

Then :help Maybe yields:

enum Maybe a
    Nothing : {a} Maybe a
    Just : {a} a -> Maybe a

Which still exhibits issue (2) above. For symmetry with newtypes, perhaps that should be:

enum Maybe : * -> *

            ---------

Constructors of Maybe
    Nothing : {a} Maybe a
    Just : {a} a -> Maybe a

[yav]

The ----- separator happens automatically when a name lives in multiple namespaces (e.g, try :help +), so I don't think we can do the 2nd suggestion nicely.

Perhaps the thing to do would be when showing information about an enum to just show the names of constructors without their types. If the user needs to know more about the them, they can :help explicitly on them? So something like:

enum Maybe : * -> *

  Constructors: `Nothing`, `Just`

Custom documentation goes here, if any.

Thoughts?

[RyanGlScott]

The ----- separator happens automatically when a name lives in multiple namespaces (e.g, try :help +), so I don't think we can do the 2nd suggestion nicely.

Ah, my mistake. Please disregard that part of my suggestion.

Perhaps the thing to do would be when showing information about an enum to just show the names of constructors without their types. If the user needs to know more about the them, they can :help explicitly on them?

I like that suggestion.