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

1. ..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