[GHC] #14048: Data instances of kind Constraint

28 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
           Keywords:                 |  Operating System:  Unknown/Multiple
       Architecture:                 |   Type of failure:  None/Unknown
  Unknown/Multiple                   |
          Test Case:                 |        Blocked By:
           Blocking:                 |   Related Tickets:  #12369
Differential Rev(s):                 |         Wiki Page:
-------------------------------------+-------------------------------------
 Continuation of #12369.

 Allow data instances ending in `Constraint`.

 This may be a bug but GHC already accepts (something to do with #11715)
 `data family Bot :: Constraint` but I can't make instances of it. Also
 fails  for `data family Bot :: TYPE IntRep`.

 I propose letting users take these disparate data types and type classes

 {{{#!hs
 data Compose :: (k' -> Type) -> (k -> k') -> (k -> Type) where
   Compose :: f (g a) -> Compose f g a

 data Compose2 :: (k' -> (kk -> Type)) -> (k -> k') -> (k -> (kk -> Type))
 where
   Compose2 :: f (g a) b -> Compose2 f g a b

 -- ComposeC :: (k' -> Constraint) -> (k -> k') -> (k -> Constraint)
 class    f (g a) => ComposeC f g a
 instance f (g a) => ComposeC f g a

 -- ComposeC2 :: (k' -> (kk -> Constraint)) -> (k -> k') -> (k -> (kk ->
 Constraint))
 class    f (g a) b => ComposeC2 f g a b
 instance f (g a) b => ComposeC2 f g a b
 }}}

 and unify them as instances of a 'data' family indexed by `Type`, `kk ->
 Type`, `Constraint`, `kk -> Constraint`.

 (Same can be done for `Data.Functor.Product` and `class (f a, g a) =>
 ProductC f g a`):

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

 data instance (f · g) a where
   Compose :: f (g a) -> (f · g) a

 data instance (f · g) a b where
   Compose2 :: f (g a) b -> (f · g) a b

 instance f (g a)   => (f · g) a
 instance f (g a) b => (f · g) a b
 }}}

 ----

 TODO Once we have #1311 allow data instances of unlifted types.

 ----

 Fun note: `(·) @(kk -> Type)` is used by
 [https://gist.github.com/ekmett/48f1b578cadeeaeee7a309ec6933d7ec Kmett]
 (as `Tensor`) & to motivate [http://i.cs.hku.hk/~bruno/papers/hs2017.pdf
 quantified class constraints], this should automatically pick the right
 data instance:

 {{{#!hs
 instance (Trans t, Trans t') => Trans (t · t') where
   lift :: Monad m => m ~> (t · t') m
   lift = Compose2 . lift @t . lift @t'
 }}}

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