[GHC] #9019: Ambiguity checker overeager on "ambiguous" kind variables

[GHC]

#9019: Ambiguity checker overeager on "ambiguous" kind variables
------------------------------------+-------------------------------------
       Reporter:  goldfire          |             Owner:
           Type:  bug               |            Status:  new
       Priority:  normal            |         Milestone:
      Component:  Compiler          |           Version:  7.8.2
       Keywords:                    |  Operating System:  Unknown/Multiple
   Architecture:  Unknown/Multiple  |   Type of failure:  None/Unknown
     Difficulty:  Unknown           |         Test Case:
     Blocked By:                    |          Blocking:
Related Tickets:                    |
------------------------------------+-------------------------------------
 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.

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