#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