[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:5 goldfire]:
 > 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!

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

 I've tried it with every occurrence of `:~:` in base and it seems to work
 fine, quite a few functions became more general as a result. The change
 means `show Refl == show HRefl` (unless we use some type class magic) and

 {{{#!hs
 instance a ~~ b => Read ((a::k1) :~~: (b::k2)) where
   readsPrec d = readParen (d > 10) (\r -> [(HRefl, s) | ("HRefl",s) <- lex
 r ])

 instance a ~~ b => Enum    ((a::k1) :~~: (b::k2))
 instance a ~~ b => Bounded ((a::k1) :~~: (b::k2))
 }}}

 One downside: You may intend to use heterogeneous equality with `HRefl`
 but something else unifies the kinds without your knowledge.

 ----

 Does it make sense for `Coercible` / `Coercion` to be heterogeneous?

 {{{#!hs
 repr :: forall k1 k2 (a::k1) (b::k2). a :~~: b -> Coercion a b
 }}}

 ----

 Some weirdness about ordering of kind variables:

 {{{#!hs
 data (a::k1) :~~: (b::k2) where
   HRefl :: a :~~: a

 -- instance forall k2 k1 (a :: k1) (b :: k2). Show (a :~~: b)
 deriving instance Show (a :~~: b)
 }}}

 `k2` appears before `k1`, I can't remember if this was fixed but this
 gives you the right order `Show ((a::k1) :~~: (b::k2))`.

 ----

 Given

 {{{#!hs
 import GHC.Types

 data (a::k1) :~~: (b::k2) where
   HRefl :: a :~~: a

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

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

 Why does this work?? Shouldn't `Refl` constrain the kinds?

 {{{#!hs
 -- instance forall k1 k2 (a :: k1) (b :: k2). (a :: k1) ~~ (b :: k2) =>
 Bounded (a :~~: b)
 instance a ~~ b => Bounded ((a::k1) :~~: (b::k2)) where
   minBound = Refl
   maxBound = Refl
 }}}

 ----

 > No. Why would you think there is?

 Actually with the
 [https://github.com/koengit/KeyMonad/blob/master/paper.lhs Key monad] I
 was able to write an implementation. I'll post it in a follow up reply.

 > 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.)

 I assume `:~:` in terms of `(:~~:) :: forall k1. k1 -> forall k2. k2 ->
 Type`.

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