[GHC] #9574: GHC Panic: No Skolem Info

[GHC]

#9574: GHC Panic: No Skolem Info
-------------------------------------+-------------------------------------
       Reporter:  ian_mi             |                   Owner:
           Type:  bug                |                  Status:  new
       Priority:  normal             |               Milestone:
      Component:  Compiler           |                 Version:  7.9
       Keywords:                     |        Operating System:
   Architecture:  Unknown/Multiple   |  Unknown/Multiple
     Difficulty:  Unknown            |         Type of failure:
     Blocked By:                     |  None/Unknown
Related Tickets:                     |               Test Case:
                                     |                Blocking:
                                     |  Differential Revisions:
-------------------------------------+-------------------------------------
 GHC 7.8.3 and from git both panic with

     Couldn't match kind ‘o1’ with ‘(,) o o’
       ‘o1’ is untouchable
         inside the constraints (Object (c :><: c) a)
         bound by a type expected by the context:
                    Object (c :><: c) a =>
                    Tagged a (c (FMap (ProductF c) a) (FMap (Proj2 c c) a))
         at Product.hs:35:9-15ghc: panic! (the 'impossible' happened)
   (GHC version 7.9.20140908 for x86_64-unknown-linux):
         No skolem info: o1_a6XS

 I have not yet attempted to reduce the problem at all. The offending code
 is the use of fmap here:

 {{{#!hs
 proj2 :: forall (c :: o -> o -> *). ProductCategory c => NatTr (c :><: c)
 c (ProductF c) (Proj2 c c)
 proj2 = NatTr t where
     NatTr t = fmap (CompF Proj2 IdentityF) e
     e :: NatTr (c :><: c) (c :><: c) (Comp ('KProxy :: KProxy o) (Diag c)
 (ProductF c)) (IdentityF (c :><: c))
     e = counit
 }}}

 fmap is defined as

 {{{#!hs
 fmap :: forall f (a :: o1) (b :: o1). Functor f ('KProxy :: KProxy (o1 ->
 o2)) => f -> Domain f a b -> Codomain f (FMap f a :: o2) (FMap f b :: o2)
 fmap _ = proxy morphMap (Proxy :: Proxy f)
 }}}

 while CompF is defined by

 {{{#!hs
 data CompF f g (k :: KProxy (o3 -> o4, o1 -> o2)) where
     CompF :: (Functor f ('KProxy :: KProxy (o3 -> o4)), Functor g ('KProxy
 :: KProxy (o1 -> o2))) =>
         f -> g -> CompF f g ('KProxy :: KProxy (o3 -> o4, o1 -> o2))
 }}}

 This makes some sense because there is a functional dependency between the
 functor and the kind proxy.

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