Re: [GHC] #12102: “Constraints in kinds” illegal family application in instance (+ documentation issues?)

[GHC]

#12102: “Constraints in kinds” illegal family application in instance (+
documentation issues?)
-------------------------------------+-------------------------------------
        Reporter:  Iceland_jack      |                Owner:  (none)
            Type:  bug               |               Status:  new
        Priority:  normal            |            Milestone:
       Component:  Compiler          |              Version:  8.0.1
      Resolution:                    |             Keywords:  TypeInType
Operating System:  Unknown/Multiple  |         Architecture:
                                     |  Unknown/Multiple
 Type of failure:  None/Unknown      |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:                    |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------

Comment (by goldfire):

 Good questions. Here are my thoughts:

 - Satisfying kind-level equality constraints is implemented in
 `Inst.tcInstBinderX`, called when a type is applied to some arguments. The
 code there handles both unboxed equality and boxed equality.

 - The "no `case`" problem in Simon's comment:5 is quite true. But this is
 OK, because such an equality constraint can never be a Given: constraints
 in types can't be used within the same type, but (I believe) these
 constraints scope only over a type (never a term).

 - This last point makes these new constraints somewhat like datatype
 contexts, but one does not desugar into the other.

 - Clearly, the output from `:info` is horrible.

 - The "no `forall` needed" is an interaction with CUSKs. This point should
 be clarified in the manual.

 - "Constrained type families" interacts poorly with today's story for kind
 families: constrained type families requires the use of class constraints,
 but class constraints aren't currently allowed in kinds. It would seem
 that it's best to implement constrained type families in the context of
 Dependent Haskell.

 - Bottom line: this feature is probably a misfire. It ''is'' marginally
 useful, as I think the example from the manual demonstrates. (That seems
 useful to me, at least.) But the implementation is very ad-hoc, and the
 fact that these constraints never appear as Givens take much of the air
 out of them. It would be easy enough to remove this feature for 8.2.

--
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/12102#comment:6>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler