Ambiguity checker overeager on "ambiguous" kind variables

Consider the following shenanigans:

{-# LANGUAGE PolyKinds, DataKinds, TypeFamilies,
             ExistentialQuantification #-}

module Bug where

import Data.Proxy

data TyFun :: * -> * -> *
type family Apply (f :: TyFun k1 k2 -> *) (x :: k1) :: k2

data LeftSym0 l =
  forall arg. Apply LeftSym0 arg ~ Left arg => LS0KI (Proxy arg)

Compiling (with -fprint-explicit-foralls -fprint-explicit-kinds) gives this error message:

/Users/rae/temp/Bug.hs:12:3:
    Could not deduce ((~)
                        (Either k3 k0)
                        (Apply (Either k3 k0) k3 (LeftSym0 k0 k3) arg)
                        ('Left k3 k0 arg))
    from the context ((~)
                        (Either k3 k2)
                        (Apply (Either k3 k2) k3 (LeftSym0 k2 k3) arg)
                        ('Left k3 k2 arg))
      bound by the type of the constructor ‘LS0KI’:
                 (~)
                   (Either k3 k2)
                   (Apply (Either k3 k2) k3 (LeftSym0 k2 k3) arg)
                   ('Left k3 k2 arg) =>
                 Proxy k3 arg -> LeftSym0 k k1 l
      at /Users/rae/temp/Bug.hs:12:3
    The type variable ‘k0’ is ambiguous
    In the ambiguity check for:
      forall (k :: BOX)
             (k1 :: BOX)
             (l :: TyFun k1 (Either k1 k))
             (k2 :: BOX)
             (k3 :: BOX)
             (arg :: k3).
      (~)
        (Either k3 k2)
        (Apply (Either k3 k2) k3 (LeftSym0 k2 k3) arg)
        ('Left k3 k2 arg) =>
      Proxy k3 arg -> LeftSym0 k k1 l
    To defer the ambiguity check to use sites, enable AllowAmbiguousTypes
    In the definition of data constructor ‘LS0KI’
    In the data declaration for ‘LeftSym0’

The file compiles without incident with -XAllowAmbiguousTypes.

What's interesting is that, then, the following separate module compiles:

{-# LANGUAGE PolyKinds, DataKinds, TypeFamilies #-}

module B2 where

import Bug
import Data.Proxy

type instance Apply LeftSym0 x = Left x

foo = LS0KI Proxy

It seems that LS0KI's type was not so ambiguous after all.

I would want to reduce the test case, but it's hard to figure out what GHC is thinking here, as it reports an ambiguous k0 variable, which does not appear in the type it is examining. A few rather naive attempts to reduce failed.

Trac metadata

Trac field	Value
Version	7.8.2
Type	Bug
TypeOfFailure	OtherFailure
Priority	normal
Resolution	Unresolved
Component	Compiler
Test case
Differential revisions
BlockedBy
Related
Blocking
CC
Operating system
Architecture