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

 Replying to [comment:4 Iceland_jack]:
 > 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
 > }}}

 This is an interesting thought. It can be done in today's syntax:

 {{{#!hs
 type (:~:) = ((:~~:) :: k -> k -> Type)

 pattern Refl :: () => (a ~ b) => a :~: b
 pattern Refl = HRefl
 }}}

 I wonder what the consequences are (if any) of reimplementing `:~:` and
 `Refl` this way.

 >
 > > 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?

 This should be a proposal to the libraries mailing list first. What
 supporting functions will you have? Perhaps if we use the pattern synonym
 approach for `:~:` then many existing functions can be reused. I'd be
 quite pleased if you spearhead this!

 >
 > ----
 >
 > 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
 > }}}

 Yes. This is slightly more general than quantifying over `k` at the top.

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

 No. Why would you think there is? `HTestEquality (Const e)` (with your new
 `Const`) is well-kinded, but I can't imagine an implementation for
 `hTestEquality`.

 In general, it's best to quantify over kinds as late as possible, because
 GHC can't reshuffle where the quantifications are like it can in terms.
 (When we get `-XDependentTypes`, this deficiency will be resolved.) It may
 not be worth the effort, but in theory, we should redefine datatypes to
 have kind quantifications as far to the right as possible. This includes
 the following preferred declaration for `:~~:`:

 {{{
 data (:~~:) :: forall k1. k1 -> forall k2. k2 -> Type where
   HRefl :: a :~~: a
 }}}

 Sadly, then, there seems to be no way to define `:~:` in terms of `:~~:`.
 GHC just isn't smart enough to get the kind quantification to work.
 (Relatedly: kind quantification around type synonyms is very murky and not
 quite specified.)

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