[GHC] #13998: Default Signature messes up arity of type constructor

19 Jul 2017

      #13998: Default Signature messes up arity of type constructor
-------------------------------------+-------------------------------------
           Reporter:  andrewthad     |             Owner:  (none)
               Type:  bug            |            Status:  new
           Priority:  normal         |         Milestone:
          Component:  Compiler       |           Version:  8.0.1
           Keywords:                 |  Operating System:  Unknown/Multiple
       Architecture:                 |   Type of failure:  None/Unknown
  Unknown/Multiple                   |
          Test Case:                 |        Blocked By:
           Blocking:                 |   Related Tickets:
Differential Rev(s):                 |         Wiki Page:
-------------------------------------+-------------------------------------
 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.

-- 
Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13998
GHC http://www.haskell.org/ghc/
The Glasgow Haskell Compiler