Kind mismatches with AnyK in rank-2 types
The following module:
{-# LANGUAGE Rank2Types #-}
module KindBug where
type T = forall f a. f a
foo :: T
foo = undefined
bar :: forall f a. f a
bar = foo
- ..produces the following error:
[1 of 1] Compiling KindBug ( KindBug.hs, KindBug.o )
KindBug.hs:10:7:
Kind incompatibility when matching types:
f0 :: AnyK -> *
f :: * -> *
Expected type: f a
Actual type: f0 a0
Relevant bindings include bar :: f a (bound at KindBug.hs:10:1)
In the expression: foo
In an equation for ‘bar’: bar = foo
Note that no extensions are enabled other than rank-2 types.
Enabling and using kind annotations fixes the error, as does replacing the type synonym with its definition in the type signature of foo.
Similar errors can also be generated with PolyKinds enabled and less plausible code, e.g. (return undefined :: forall f a. f a) :: f a
. The non-PolyKinds example is simplified from some actual code, where the type synonym was similar to the ones used in lens, and is the simplest example I could find (with help from Shachaf on IRC) that resembled real code.
I searched for existing tickets and the closest I could find are #7916 (closed) and #5935 (closed), both of which are already fixed.
Also, according to glguy (Eric Mertens) just now in #haskell-lens, the same error occurs in the 7.10 branch and in 7.11.20150120.
Trac metadata
Trac field | Value |
---|---|
Version | 7.8.4 |
Type | Bug |
TypeOfFailure | OtherFailure |
Priority | normal |
Resolution | Unresolved |
Component | Compiler |
Test case | |
Differential revisions | |
BlockedBy | |
Related | |
Blocking | |
CC | |
Operating system | |
Architecture |