DIfferent Typeable constraints behaviour in GHC2021 & Haskell2010

Learn
#1

Hi all!

I have the following program tested with ghc 9.2.2, it shows different behavior when using GHC2021 or Haskell2010:

-- GHC version: 9.2.2
{-# OPTIONS_GHC -Wall #-}
{-# LANGUAGE FlexibleContexts    #-}
{-# LANGUAGE GHC2021             #-}
-- {-# LANGUAGE Haskell2010         #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications    #-}
{-# LANGUAGE TypeFamilies        #-}

import           Data.Kind     (Type)
import           Data.Proxy    (Proxy (..))
import           Data.Typeable (Typeable)


class Typeable a => Typeable' a where
  tag :: Proxy a -> String

class Typeable' a => Typeable'' a where
  type T1 a :: Type
  type T2 a :: Type

data A a = A
  { val1 :: T1 a
  , val2 :: T2 a
  }

-- * Does not work in GHC2021, but Haskell2010
instance Typeable'' a => Typeable' (A a) where
-- * Works in GHC2021
-- instance (Typeable'' a, Typeable (A a)) => Typeable' (A a) where
   tag _ = "A/" ++ tag (Proxy @a)

data B
instance Typeable' B where
  tag _ = "B"
instance Typeable'' B where
  type T1 B = String
  type T2 B = Int

main :: IO ()
main = do
  let a = A "hello" 42 :: A B
  putStrLn $ tag (Proxy @(A B)) ++ ": " ++ show(val1 a) ++ show(val2 a)

By using GHC2021, this does not compile where I got:

ghc2021-and-typeable.hs:28:10-40: error: …
    • Could not deduce (Typeable k)
        arising from the superclasses of an instance declaration
      from the context: Typeable'' a
        bound by the instance declaration
        at /home/hellwolf/Projects/my/haskell-examples/2022-05-28-ghc2021-and-typeable/ghc2021-and-typeable.hs:28:10-40
    • In the instance declaration for ‘Typeable' (A a)’
   |
Compilation failed.

But if I enable {-# LANGUAGE Haskell2010 #-} instead, the program compiles and works.

The code that’s the problem is:

instance Typeable'' a => Typeable' (A a) where

Fine, I can change it to more specific constraints instead:

instance (Typeable'' a, Typeable (A a)) => Typeable' (A a) where

Now the same code compiles for both GHC2021 and Haskell2010.

One more note, I cannot isolate a case into this minimal example I wrote, that case in another project I am doing also producing this warning when using the more specific “Typeable” constraint:

https://downloads.haskell.org/~ghc/latest/docs/html/users_guide/using-warnings.html?highlight=simplifiable%20class%20constraints#ghc-flag--Wsimplifiable-class-constraints

It seems making sense, since why on earth should I need to declare something explicitly “Typeable” anyhow?

But I cannot make a minimal example that can demonstrate this warning appearing when fixing the first issue.

Thank your for your time,

2 Likes
#2

Since the error message mentions a type/kind variable k, I’d guess this is caused by PolyKinds which is included in GHC2021, but not in Haskell2010. Maybe the error will go away if you write explicit kind signatures for everything.

Update: Yeah, if you add the line:

type A :: Type -> Type

Then it compiles without errors with GHC2021.

3 Likes
#3

Thank you @jaror!

That indeed solved it, although I can’t find a general guideline here now. Should we start to explicitly write kind signatures everywhere now, like function signatures?

#4

Looking at it a bit deeper, I think the problem is that Typeable a is only defined if the kind of a is also Typeable. So perhaps the best way to fix this issue is to add Typeable constraints on the kinds of any class that has Typeable as superclass. In your case:

class (Typeable a, Typeable k) => Typeable' (a :: k) where

Ideally, GHC would be able to deduce that Typeable (a :: k) implies Typeable k, but it seems like GHC is not smart enough for that yet. Maybe that would be a good GHC issue or proposal.

1 Like
#5

Interesting, that does fix it too, but I’m not sure I understand what does Typeable k even mean anymore…

Let me try, in case of:

instance Typeable'' a => Typeable' (A a) where

Isn’t A a :: Type ?

Worse, actually I omitted something from the minimum code:


class (Typeable a, Typeable k) => Typeable' (a :: k) where
  tag :: Proxy a -> String
  tagFromValue :: a -> String
  tagFromValue _ = tag (Proxy @a)

Now tagFromValue wouldn’t work:

ghc2021-and-typeable.hs:17:20: error: …
    • Expected a type, but ‘a’ has kind ‘k’
    • In the type signature: tagFromValue :: (a :: Type) -> String
      In the class declaration for ‘Typeable'’
   |
Compilation failed.

Hooray :confused:

P.S.:

I reported to DIfferent Typeable constraints behaviour in GHC2021 & Haskell2010 (#21678) · Issues · Glasgow Haskell Compiler / GHC · GitLab

#6

Yeah, arguments to functions can only ever have kind Type (or more accurately TYPE rep for some rep :: RuntimeRep), so if you write tagFromValue :: a -> String then a is already forced to have kind Type. Then you can no longer use an unconstraint kind variable k. But the advantage is that you also no longer need to write the extra constraint. Your original version should now work as expected:


class (Typeable a) => Typeable' a where
  tag :: Proxy a -> String
  tagFromValue :: a -> String
  tagFromValue _ = tag (Proxy @a)
#7

Thank you Jaro. I would still need the kind signature in Typeable' a :: k and Typeable constraint of k if want to avoid the kind signature for A a.

fwiw, I put the final version to haskell-examples/ghc2021-and-typeable.hs at master · hellwolf/haskell-examples · GitHub, noteably:

class (Typeable k, Typeable a) => Typeable' (a :: k) where
  tag :: Proxy a -> String

tagFromValue :: forall a. Typeable' a => a -> String
tagFromValue _ = tag (Proxy @a)

I seem to have failed to convene the message in DIfferent Typeable constraints behaviour in GHC2021 & Haskell2010 (#21678) · Issues · Glasgow Haskell Compiler / GHC · GitLab that it isn’t quite clear why with PolyKinds enabled, I would have to explicitly say Typeable k where k is a “kind”. But after reading 7.8. Kind polymorphism a bit, I guess it’s just some stuff I need to learn a bit more first.

Cheers!