Make the HaskStrong type representation Kind-indexed, and many supporting changes (see long comment).
This patch makes a whole lot of interlocking changes, with the
ultimate (accomplished) goal of changing the HaskStrong type
representation ("HaskType") so that it is indexed by the Haskell Kind
of the type. As a result, the auxiliary well-kindedness judgment
\vdash_{ty} is no longer necessary.
Other changes in this patch:
- Added Coq ToString class (similar to Haskell's Show class)
- Massive reduction in volume of code extracted for string literals
- Decidable equality on HaskStrong's
- Much more reliable HaskWeakToStrong, although it has regressed
a bit in terms of number of cases handled; this will be remediated
shortly.
20 files changed: