This should describe the new TypeInType feature for users.
Thanks, this looks great!
Here are some comments from a read-through. If you 'd like to wait to handle these and merge this as-is that would be fine with me.
It might be good to be a bit more clear that you can't use the *standard* Data.Maybe.Just constructor on an unboxed type; as-written I'm a bit concerned that the reader might mistakenly think that they couldn't define their own Maybe with unboxed contents.
It would be nice to either introduce TYPE before this point or refer the reader elsewhere for further discussion. In particular, it might be helpful to say that * is in fact TYPE 'PtrRepLifted so they understand how unboxed and boxed types are related in their kinds.
Nit: perhaps instead of "it is easy to see" say "it follows".
I know you didn't write this, but I do wish that the names in this example were a bit less terse; Zero and Succ seem like reasonable compromises.
It might be a good idea that we denote the promoted constructors with a tick as this hasn't been explicitly mentioned yet.
This could be a bit clearer (and the commas are currently redundant). Perhaps,
This is a nice crisp explanation.
Perhaps add a parenthetical "(where implicit parameters are denoted by braces)" to clear up any confusion.
Is it possible to be a bit more precise here? Obviously the reader will need to see the section below for the full story, but perhaps just a couple sentences hitting the major points would be helpful.
Could you add an index entry for CUSK? This should be something like,
.. index:: single: CUSK single: complete user-supplied kind signature
I wish there were an index entry and proper definition for "principal type".
Thanks for writing this down.
Perhaps this also deserves a mention in the release notes.
Perhaps index entries for TYPE and runtime representation polymorphism would be appropriate here.
Hmm, what happened to the indentation here?
This should be -fprint-explicit-runtime-reps.
.. index:: pair: Type equality constraints; kind heterogeneous
Perhaps it would be more clear to say "kind-heterogeneous" here.
Many thanks for read-through.
I mentioned the bit about *, but see the reference to TYPE at the end of the paragraph.
This would belong in a glossary, which would be a lovely new chapter in the manual. Other great candidates for inclusion there: "polymorphism", "lifted", "boxed", "dictionary", "heterogeneous", ...
This isn't new, though. I just added some missing documentation for an already-existing feature.
Nasty, nasty tabs. Go away, tabs!