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 |