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 |