[GHC] #13814: Unable to resolve instance for polykinded superclass constraint on associated-type-family.

[GHC]

#13814: Unable to resolve instance for polykinded superclass constraint on
associated-type-family.
-------------------------------------+-------------------------------------
        Reporter:  isovector         |                Owner:  (none)
            Type:  bug               |               Status:  new
        Priority:  normal            |            Milestone:
       Component:  Compiler          |              Version:  8.0.1
      Resolution:                    |             Keywords:  polykinds,
                                     |  type families
Operating System:  Unknown/Multiple  |         Architecture:
 Type of failure:  GHC rejects       |  Unknown/Multiple
  valid program                      |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:                    |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------

Comment (by simonpj):

 You say you expected
 {{{
 class Back k1 (FrontBack k1 k t) =>
       Front k (t :: k) where
   ...
 }}}
 But this is jolly odd, becuase the constraint mentions `k1`, which is not
 bound in the bit after the `=>`.  Would you expect this to be OK?
 {{{
 class C a b => D a where
  op1 :: a -> Int -> a
 }}}
 Well no!  Think of the data type declaration that arises from class decl:
 {{{
 data D a where
   MkD :: C a b => (a->Int->a) -> D a
 }}}
 That `b` can only be existential, which isn't at all what we want.

 So perhaps we want this
 {{{
 class Back k1 (FrontBack k1 k t) =>
       Front k k1 (t :: k) where
   ...
 }}}
 That makes more sense.  (What is instead happening today is that the `k1`
 is being defaulted to `Any`.)

 But that too is problematic.  Suppose there was a class-op:
 {{{
 class Back k1 (FrontBack k1 k t) =>
       Front k k1 (t :: k) where
   type family FrontBack k (t :: k) :: k1
   op :: Proxy k t -> Int
 }}}
 Now the type of `op` is rather ambiguous
 {{{
 op :: forall k k1 (t::k). Front k k1 t => Proxy k t -> Int
 }}}
 So nothing fixes `k1, so it'll be difficult to discharge the `Front`
 contraint from any givens.

 So simply addind kind variables from the superclass constraints isn't
 going to work.  But defaulting them isn't very good either.  Maybe we
 should complain about the unresolved kind variables in the class decl?

 The real problem is that `Back` is too polymorphic.  If it had kind `k ->
 k` we'd probably be fine.

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