Re: [GHC] #12131: Can't solve constraints with UndecidableSuperClasses but can infer kind (+ undesired order of kinds)

29 May 2016

      #12131: Can't solve constraints with UndecidableSuperClasses but can infer kind (+
undesired order of kinds)
-------------------------------------+-------------------------------------
        Reporter:  Iceland_jack      |                Owner:
            Type:  bug               |               Status:  new
        Priority:  normal            |            Milestone:
       Component:  Compiler          |              Version:  8.0.1
      Resolution:                    |             Keywords:
                                     |  UndecidableSuperClasses
Operating System:  Unknown/Multiple  |         Architecture:
                                     |  Unknown/Multiple
 Type of failure:  None/Unknown      |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:  #11480 #12025     |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------

Comment (by Iceland_jack):

 Also true for

 {{{#!hs
 data Product (p :: Cat i) (q :: Cat j) :: Cat (i, j) where
   Product :: p (Fst a) (Fst b) -> q (Snd a) (Snd b) -> Product p q a b
 }}}

 with code from
 [https://github.com/ekmett/hask/blob/master/src/Hask/Category/Polynomial.hs
 Polynomial.hs] and
 [https://github.com/ekmett/hask/blob/master/src/Hask/Category.hs
 Category.hs] adapted:

 {{{#!hs
 type family
   Fst (p :: (i,j)) :: i where
   Fst '(a, _) = a

 type family
   Snd (q :: (i,j)) :: j where
   Snd '(_, b) = b

 type family
   NatDom (f :: Cat (i -> j)) :: Cat i where
   NatDom (Nat p _) = p

 type family
   NatCod (f :: Cat (i -> j)) :: Cat j where
   NatCod (Nat _ q) = q

 type Opd f = Op (Dom f)
 type Dom2 p = NatDom (Cod p)
 type Cod2 p = NatCod (Cod p)

 class    (Ob p (Fst a), Ob q (Snd a)) => ProductOb (p :: Cat i) (q :: Cat
 j) (a :: (i,j))
 instance (Ob p (Fst a), Ob q (Snd a)) => ProductOb (p :: Cat i) (q :: Cat
 j) (a :: (i,j))

 instance (Category p, Category q) => Functor (Product p q) where
   type Dom (Product p q) = Op (Product (Opd p) (Opd q))
   type Cod (Product p q) = Nat (Product (Dom2 p) (Dom2 q)) (->)

 instance (Category p, Category q, ProductOb p q a) => Functor (Product p q
 a) where
   type Dom (Product p q a) = Product (Dom2 p) (Dom2 q)
   type Cod (Product p q a) = (->)
   fmap = (.)

 instance (Category p, Category q) => Category (Product p q) where
   type Ob (Product p q) = ProductOb p q
   id = Product id id
   Product f f' . Product g g' = Product (f . g) (f' . g')

   target = undefined
   source = undefined
 }}}

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