Seemingly inappropriate "expecting one more argument" error in polykinded class

[illissius]

Triggered by the following code:

{-# LANGUAGE PolyKinds, GADTs #-}

data Proxy a

class Foo a where
    foo :: a ~ f i => Proxy (Foo f)

GHC writes:

test.hs:6:34:
    Expecting one more argument to `f'
    In the type `a ~ f i => Proxy (Foo f)'
    In the class declaration for `Foo'

It seems to me that given Foo :: forall k. k -> Constraint, Proxy :: forall k. k -> *, a :: k, f :: k1 -> k, that Foo in Proxy (Foo f) should be instantiated at k1 -> k, and Proxy at Constraint, and that this should work.

[illissius]

If instead of Proxy (Foo f) I write Proxy (Bar f) or Proxy f, there is no error.

[simonpj@…]

commit 8691041c8360aba98d3e1489b7804a5d83dcab70

Author: Simon Peyton Jones <simonpj@microsoft.com>
Date:   Mon Oct 15 15:52:02 2012 +0100

    Improve error reporting for kind occurs-checks
    
    Fixes Trac #7328.

 compiler/typecheck/TcHsType.lhs |   36 +++++++++++++++++-------
 compiler/typecheck/TcUnify.lhs  |   57 +++++++++++++++++++++-----------------
 2 files changed, 56 insertions(+), 37 deletions(-)

[simonpj]

Worth trying to merge... but not if it's hard.

[igloo]

Several conflicts, so not merging.