[GHC] #8566: Given kind equalities are discarded

[GHC]

#8566: Given kind equalities are discarded
-------------------------------------+------------------------------------
        Reporter:  dreixel           |            Owner:
            Type:  bug               |           Status:  new
        Priority:  normal            |        Milestone:
       Component:  Compiler          |          Version:  7.7
      Resolution:                    |         Keywords:
Operating System:  Unknown/Multiple  |     Architecture:  Unknown/Multiple
 Type of failure:  None/Unknown      |       Difficulty:  Unknown
       Test Case:  polykinds/T8566   |       Blocked By:
        Blocking:                    |  Related Tickets:
-------------------------------------+------------------------------------

Comment (by simonpj):

 Aha.  But there is a real difference between the two:
 {{{
   MkT :: forall (u:*). forall (k:BOX), (b:k). (u ~ Proxy k b) => Proxy k b
 -> T u
   SNil :: forall (k:BOX) (xs:[k]). (xs ~ '[] k) => Sing22 k xs
 }}}
 (I've used `Sing22` for the data type for `Sing (xs:[k])`.)

 In `SNil` the `k` is univerally quantified over the whole thing.  In `MkT`
 the `k` is existentially quantified, ''and'' involved in an equality
 constraint.

 So I rephrase my proposal: '''reject any data constructor with an
 existentially quantified kind variable that is mentioned in an equality
 constraint'''.

 Of course "mentioned in an equality constraint" is itself not too obvious
 (think superclasses and constraint kinds).  But is the direction of travel
 right?

 Simon

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