#12708: RFC: Representation polymorphic Num -------------------------------------+------------------------------------- Reporter: Iceland_jack | 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): This is a pipe dream, `Logic` offers cool possibilities. [https://hackage.haskell.org/package/sbv-5.12/docs/src/Data-SBV- BitVectors-Model.html sbv] has `EqSymbolic` which is an `Eq a` where `Logic a ~ SBool` : {{{#!hs infix 4 .==, ./= class EqSymbolic a where (.==), (./=) :: a -> a -> SBool }}} This could be the regular `Eq` if we had something like (with `Boolean` taken from ticket:10592#comment:12) {{{#!hs class Boolean (Logic a) => Eq (a :: TYPE rep) where type Logic a :: TYPE (Rep rep) (==) :: a -> a -> Logic a a == b = not (a /= b) (/=) :: a -> a -> Logic a a /= b = not (a == b) instance Eq (SBV a) where type Logic (SBV a) = SBool (==) :: SBV a -> SBV a -> SBool SBV a == SBV b = SBV (svEqual a b) instance EqSymbolic (SArray a b) where type Logic (SArray a b) = SBool (==) :: SArray a b -> SArray a b -> SBool SArray a == SArray b = SBV (eqSArr a b) }}} We lose `EqSymbolic Bool` but `... => EqSymbolic [a]` would survive in a different form. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12708#comment:16 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler