Re: [GHC] #12369: data families shouldn't be required to have return kind *, data instances should

27 Jul 2017

      #12369: data families shouldn't be required to have return kind *, data instances
should
-------------------------------------+-------------------------------------
        Reporter:  ekmett            |                Owner:  (none)
            Type:  feature request   |               Status:  closed
        Priority:  normal            |            Milestone:  8.4.1
       Component:  Compiler (Type    |              Version:  8.0.1
  checker)                           |
      Resolution:  fixed             |             Keywords:  TypeInType
Operating System:  Unknown/Multiple  |         Architecture:
                                     |  Unknown/Multiple
 Type of failure:  None/Unknown      |            Test Case:  indexed-
                                     |  types/should_compile/T12369
      Blocked By:                    |             Blocking:
 Related Tickets:                    |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------

Comment (by Iceland_jack):

 Could this work for `Constraint`s? GHC already accepts (maybe something to
 do with #11715)

 {{{
 $ ghci -ignore-dot-ghci
 GHCi, version 8.3.20170605: http://www.haskell.org/ghc/  :? for help
 Prelude> :set -XTypeInType -XTypeFamilies
 Prelude> import Data.Kind
 Prelude Data.Kind> data family COMPOSE k1 k2 k3 :: (k1 -> Type) -> (k2 ->
 k1) -> (k2 -> Constraint)
 Prelude Data.Kind>
 }}}

 but it cannot be used afaik, also fails with a return kind of `TYPE
 IntRep`.

 {{{
 Prelude Data.Kind GHC.Prim GHC.Exts> data family COMPOSE k1 k2 k3 :: (k1
 -> Type) -> (k2 -> k1) -> (k2 -> TYPE IntRep)

 <interactive>:8:1: error:
     • Kind signature on data type declaration has non-* return kind
         (k1 -> *) -> (k2 -> k1) -> k2 -> TYPE 'IntRep
     • In the data family declaration for ‘COMPOSE’
 }}}

 It would be interesting to combine

 {{{#!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
 }}}

 as instances of a 'data' family indexed by `Type`, `kk -> Type`,
 `Constraint`, `kk -> Constraint` but I'm not sure if it's meaningful

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

 data instance Compose Type :: (k' -> Type) -> (k -> k') -> (k -> Type)
 where
   Compose :: f (g a) -> Compose Type f g a

 -- Hijacking DatatypeContexts syntax
 data instance f (g a)   => Compose Constraint         f g a
 data instance f (g a) b => Compose (kk -> Constraint) f g a b
 }}}

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