[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 goldfire):

 I think that would be bad.

 For example, take the singleton for lists:

 {{{
 data instance Sing (xs :: [k]) where
   SNil :: Sing '[]
   SCons :: Sing h -> Sing t -> Sing (h ': t)
 }}}

 The constructors expand to
 {{{
 SNil :: forall (k :: BOX) (xs :: [k]). (xs ~ '[] k) => Sing [k] xs
 SCons :: forall (k :: BOX) (xs :: [k]). forall (h :: k) (t :: [k]). (xs ~
 ((':) k h t)) => Sing k h -> Sing [k] t -> Sing [k] xs
 }}}

 (If you get suspicious of the `[k]` in the return type, it's because I
 didn't unfold the `data instance` piece of it. With that unfolded, the
 return type's indices are indeed variables.)

 These equalities mention kind variables, and yet I would be quite sad
 without them.

 Or did I miss something here?

 PS: I take back my claim about `k` being existential and `unA` being ill-
 typed. Simon is right.

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