Re: [GHC] #14048: Data instances of kind Constraint

29 Jul 2017

      #14048: Data instances of kind Constraint
-------------------------------------+-------------------------------------
        Reporter:  Iceland_jack      |                Owner:  (none)
            Type:  bug               |               Status:  new
        Priority:  normal            |            Milestone:
       Component:  Compiler          |              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:  #12369            |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------

Comment (by Iceland_jack):

 Let me first throw some ideas out there to see if this even makes sense:

 Some data types have a related type class, for example `TypeRep` &
 `Typeable`, `Sing` & `SingI`

 {{{#!hs
 TypeRep  :: k -> Type
 Typeable :: k -> Constraint

 Sing  :: k -> Type
 SingI :: k -> Constraint
 }}}

 and classes that work for types as well as constructors

 {{{#!hs
 Eq  :: Type                   -> Constraint
 Eq1 :: (Type -> Type)         -> Constraint
 Eq2 :: (Type -> Type -> Type) -> Constraint
 }}}

 ----

 It could completely re-use the syntax of type classes

 {{{#!hs
 data family Sing (a :: k) :: k'

 data instance
   Sing (a :: Bool) where
   SFalse :: Sing False
   STrue  :: Sing True

 -- creates a class of kind `Sing :: k -> Constraint'
 class Sing (a :: k) where
   sing :: Sing a

 instance Sing (False :: Bool) where
   sing :: Sing (False :: Bool)
   sing = SFalse

 instance Sing (True :: Bool) where
   sing :: Sing (True :: Bool)
   sing = STrue
 }}}

 This lets us unify many names,

 {{{#!hs
 data family (,) :: k -> k -> k

 -- (,) :: Type -> Type -> Type
 data instance (a, b) = (a, b)

 -- (,) :: (k -> Type) -> (k -> Type) -> (k -> Type)
 data instance (f, g) a = Pair (f a) (g a)

 -- (,) :: (k -> k' -> Type) -> (k -> k' -> Type) -> (k -> k' -> Type)
 data instance (f, g) a b = Pair (f a b) (g a b)

 -- (,) :: Constraint -> Constraint -> Constraint
 class    (a, b) => (a, b)
 instance (a, b) => (a, b)

 -- (,) :: (k -> Constraint) -> (k -> Constraint) -> (k -> Constraint)
 class    (f a, g a) => (f, g) a
 instance (f a, g a) => (f, g) a
 }}}

 if you don't see a problem with this I can submit a proposal

-- 
Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14048#comment:2
GHC http://www.haskell.org/ghc/
The Glasgow Haskell Compiler