Default Signature messes up arity of type constructor

I have a situation that's shown up in my quantification library that I believe is an issue with GHC's typeclass method defaulting mechanism. Here is a self-contained example:

{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DefaultSignatures #-}
{-# LANGUAGE GADTs #-}

import Data.Type.Equality

class EqForall f where
  eqForall :: f a -> f a -> Bool

class EqForall f => EqForallPoly f where
  eqForallPoly :: f a -> f b -> Bool
  default eqForallPoly :: TestEquality f => f a -> f b -> Bool
  eqForallPoly = defaultEqForallPoly

defaultEqForallPoly :: (TestEquality f, EqForall f) => f a -> f b -> Bool
defaultEqForallPoly x y = case testEquality x y of
  Nothing -> False
  Just Refl -> eqForall x y

data Atom = AtomInt | AtomString | AtomBool

data Value (a :: Atom) where
  ValueInt :: Int -> Value 'AtomInt
  ValueString :: String -> Value 'AtomString
  ValueBool :: Bool -> Value 'AtomBool

instance TestEquality Value where
  testEquality (ValueInt _) (ValueInt _) = Just Refl
  testEquality (ValueString _) (ValueString _) = Just Refl
  testEquality (ValueBool _) (ValueBool _) = Just Refl
  testEquality _ _ = Nothing

instance EqForall Value where
  eqForall (ValueInt a) (ValueInt b) = a == b
  eqForall (ValueString a) (ValueString b) = a == b
  eqForall (ValueBool a) (ValueBool b) = a == b

instance EqForallPoly Value

main :: IO ()
main = putStrLn "done"

This fails to compile both with GHC 8.0 and with GHC 8.2rc3. The error reads:

default_sig_limitation.hs:40:10: error:
    • Expecting one more argument to ‘Value’
      Expected a type, but ‘Value’ has kind ‘Atom -> *’
    • In the type ‘Value’
      In the expression: Main.$dmeqForallPoly @Value
      In an equation for ‘eqForallPoly’:
          eqForallPoly = Main.$dmeqForallPoly @Value

If I replace EqForallPoly instance with something more explicit, it will compile just fine:

instance EqForallPoly Value where
  eqForallPoly = defaultEqForallPoly

Fortunately, this workaround isn't bad at all. I don't really mind it, but I thought I'd bring it up here in case it bites someone else in the future.

Trac metadata

Trac field	Value
Version	8.0.1
Type	Bug
TypeOfFailure	OtherFailure
Priority	normal
Resolution	Unresolved
Component	Compiler
Test case
Differential revisions
BlockedBy
Related
Blocking
CC
Operating system
Architecture