#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