[GHC] #11740: RFC kind synonyms

[GHC]

#11740: RFC kind synonyms
-------------------------------------+-------------------------------------
        Reporter:  Iceland_jack      |                Owner:
            Type:  bug               |               Status:  new
        Priority:  normal            |            Milestone:
       Component:  Compiler          |              Version:  7.10.3
      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:                    |
-------------------------------------+-------------------------------------
Description changed by Iceland_jack:

@@ -66,1 +66,1 @@
- -- ToContext (fs :: [TypeClass]) :: TypeClass where
+ -- ToContext (fs :: [* -> Constraint]) :: * -> Constraint where
@@ -68,1 +68,1 @@
-   ToContext (fs :: [* -> Constraint]) :: * -> Constraint where
+   ToContext (fs :: [TypeClass]) :: TypeClass where

New description:

 Are any of these useful now that we have kind synonyms:

 {{{#!hs
 -- Control.Category
 type Cat k     = k -> k -> Type

 -- Data.Kind
 type Kind      = Type
 type Types     = [Type]
 type TypeClass = Type -> Constraint
 }}}

 `Cat` is not limited to `Control.Category` but applies in all
 [https://github.com/ekmett/hask/blob/master/src/Hask/Category.hs#L68
 hask],
 [https://github.com/mikeizbicki/subhask/blob/b5433b959914d8214bcc4f130ff1b3ddbe589e50/src/SubHask/Category.hs#L108
 subhask] and is defined by
 [https://github.com/ttuegel/recategorize/blob/master/src/Category/Category.hs#L81
 recategorize].

 It lets you rewrite:

 {{{#!hs
 -- newtype Yoneda (p :: i -> i -> *) (a :: i) (b :: i) = Op { getOp :: p b
 a }
 newtype Yoneda :: Cat i -> Cat i where
   Op :: { getOp :: p b a } -> Yoneda p a b

 -- type family Op (p :: i -> i -> *) :: i -> i -> * where
 type family Op (p :: Cat i) :: Cat i where
   Op (Yoneda p) = p
   Op p = Yoneda p

 -- data CatT (cat :: * -> * -> *) (a :: k) (b :: k) (cat1 :: k -> k -> *)
 (cat2 :: k -> k -> *)
 data CatT (cat :: Cat Type) (a :: k) (b :: k) (cat1 :: Cat k) (cat2 :: Cat
 k)

 -- class (Category' (Dom f), Category' (Cod f)) => Functor (f :: i -> j)
 where
 --   type Dom f :: i -> i -> *
 --   type Cod f :: j -> j -> *
 class (Category' (Dom f), Category' (Cod f)) => Functor (f :: i -> j)
 where
   type Dom f :: Cat i
   type Cod f :: Cat j

 -- data Nat (p :: i -> i -> *) (q :: j -> j -> *) (f :: i -> j) (g :: i ->
 j) where
 data Nat (p :: Cat i) (q :: Cat j) (f :: i -> j) (g :: i -> j) where

 -- instance Cartesian ((->) :: * -> * -> *) where
 instance Cartesian ((->) :: Cat Type) where
 }}}

 and

 {{{#!hs
 -- class    (f x, g x) => And (f :: * -> Constraint) (g :: * ->
 Constraint) (x :: *)
 -- instance (f x, g x) => And (f :: * -> Constraint) (g :: * ->
 Constraint) (x :: *)
 class    (f x, g x) => And (f :: TypeClass) (g :: TypeClass) (x :: *)
 instance (f x, g x) => And (f :: TypeClass) (g :: TypeClass) (x :: *)

 -- ToContext (fs :: [* -> Constraint]) :: * -> Constraint where
 type family
   ToContext (fs :: [TypeClass]) :: TypeClass where
   ToContext (f:g:fs) = And f (ToContext (g:fs))
   ToContext '[f]     = f
 }}}

--

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