[GHC] #12422: Add decidable equality class

[GHC]

#12422: Add decidable equality class
-------------------------------------+-------------------------------------
        Reporter:  dfeuer            |                Owner:
            Type:  feature request   |               Status:  new
        Priority:  normal            |            Milestone:
       Component:  Core Libraries    |              Version:  8.0.1
      Resolution:                    |             Keywords:
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 Iceland_jack):

 Replying to [comment:3 goldfire]:
 > Yes, this is a higher-rank kind!
 Yikes! :)

 > 1. Making `:~:` heterogeneous would likely break client code.

 Figured as much. Is there any way to combine visible kind application
 (#12045) and unifying different type applications (#11385), let's say if I
 want to write something like

 {{{#!hs
 -- (:~~:) :: forall k1 k2. k1 -> k2 -> Type

 type (:~:) = (:~~:) @k @k :: k -> k -> Type

 -- using your syntax (visible kind abstraction?)
 type (:~:) = \@k -> (:~~:) @k @k
 }}}

 > 2. We should have `:~~:` in the standard library. But I was too
 exhausted from implementing `TypeInType` to start this debate on the
 libraries mailing list. We should really put it in for 8.2.

 Should I add it to `Data.Type.Equality` on Phab?

 ----

 Should we rewrite `Const :: Type -> k -> Type` to have the kind ...?

 {{{#!hs
 data Const :: Type -> forall k. k -> Type where
   Const :: { getConst :: a } -> Const a b
 }}}

 Is there any way to define an `HTestEquality (Const e)` instance?

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