That speaks to why PolyKinds is needed in the long run. I don’t doubt that! (Especially after this report.) My point is merely that PolyKinds is disruptive, and that is likely to undermine confidence in the default Haskell that GHC accepts — really the reverse of what we were hoping to achieve with the new standard configuration. Chris

On 6 Jul 2022, at 04:51, Cale Gibbard wrote:

I can remember quite a few times where GHC presented me with an incomprehensible and confused-sounding error message, but then the actual problem was that PolyKinds was off, and upon turning it on, there was no longer any problem -- it's to the point that enabling PolyKinds is one of the first things I try if I find myself disagreeing with GHC on whether something typechecks.

On Tue, 5 Jul 2022 at 23:46, Chris Dornan mailto:chris@chrisdornan.com> wrote: I think we can learn to write code for PolyKinds in time, but in my experience it is quite disruptive right now, and could sow FUD around the new consensus we are trying to build.

My inclination would be to revert to Haskell2010 as the default for GHC until we can build confidence around a configuration that we are confident won’t be disruptive.

At a minimum I would create ghc2022 = ghc2021 \ {PolyKinds} and make that the default for ghc-9.4.

What do y’all think?

...

On 5 Jul 2022, at 16:02, Richard Eisenberg mailto:lists@richarde.dev> wrote:

I find that surprising, and disappointing. I think of PolyKinds as largely innocuous, except in strange scenarios, which is why PolyKinds is included in GHC2021. If that is wrong, perhaps we should consider not including PolyKinds in GHC2023...

It would be interesting to learn more about what's going wrong.

Richard

...

On Jul 5, 2022, at 10:26 AM, Chris Dornan mailto:chris@chrisdornan.com> wrote:

yup, i should have started there—all my recent troubles have come from PolyKinds!

On Tue, 5 Jul 2022 at 15:00, Richard Eisenberg mailto:lists@richarde.dev> wrote: This is PolyKinds, which generalizes the kind of D, meaning that satisfying the Typeable a superclass constraint of C also requires a Typeable k constraint, where (a :: k).

Richard

...

On Jul 2, 2022, at 12:49 AM, Chris Dornan mailto:chris@chrisdornan.com> wrote:

Quick quiz: the below Haskell2010 ‘Phantoms' module (also in this Gist: https://gist.github.com/cdornan/f75cd8024434d998c87610cbb7fb6ab3 https://gist.github.com/cdornan/f75cd8024434d998c87610cbb7fb6ab3) appears (for me on GHC 9.2.2 and 9.2.3) to not be a GHC2021 module, reporting this error under the latter configuration:

Phantoms.hs:22:10: error: • Could not deduce (Typeable k) arising from the superclasses of an instance declaration from the context: (C a, Typeable a) bound by the instance declaration at Phantoms.hs:22:10-36 • In the instance declaration for ‘S (D a)’ | 22 | instance (C a,Typeable a) => S (D a) where smethod = undefined | ^^^^^^^^^^^^^^^^^^^^^^^^^^^

Phantoms.hs:22:10: error: • Could not deduce (Typeable k) arising from the superclasses of an instance declaration from the context: (C a, Typeable a) bound by the instance declaration at Phantoms.hs:22:10-36 • In the instance declaration for ‘S (D a)’ | 22 | instance (C a,Typeable a) => S (D a) where smethod = undefined

The question is which language extension(s) are giving rise to these errors?

The ‘Phantoms' module is this:

{-# LANGUAGE DerivingVia #-}

module Phantoms where

import Data.Typeable

class C a where cmethod :: Proxy a -> ()

class (Show a, Typeable a) => S a where smethod :: a -> Int

newtype UsingD a = UsingD { getUsingD :: a }

newtype D a = D { getD :: Int } deriving (Show) via UsingD (D a)

instance (C a,Typeable a) => S (D a) where smethod = undefined

instance (C a,Typeable a) => Show (UsingD a) where showsPrec = undefined

instance (C a) => C (D a) where cmethod _ = undefined

_______________________________________________ ghc-steering-committee mailing list ghc-steering-committee@haskell.org mailto:ghc-steering-committee@haskell.org https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committee https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committee

_______________________________________________ ghc-steering-committee mailing list ghc-steering-committee@haskell.org mailto:ghc-steering-committee@haskell.org https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committee https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committee

Also, the Foo not matching Foo case isn't even the worst -- at least there you can tell something is up, because it's absurd on the face of it. The worse examples are cases where there's a type error caused by lack of PolyKinds that if you thought about it long enough, would seem absurd, but the compiler isn't *obviously* saying something wrong -- then you potentially waste a whole bunch of time trying to reason it out before discovering that just turning PolyKinds on fixes the issue. Probably the real answer is just to fix GHC's error message printing, but in the meantime... On Wed, 6 Jul 2022 at 00:10, Cale Gibbard wrote:

Yeah, I'd just hesitate to turn it off by default, because GHC seems much saner overall with PolyKinds on, at least in my experience. It may depend on which packages/libraries you're often importing. I have a feeling that the cases crop up when you import something that was defined using PolyKinds, but your module is not compiled with PolyKinds and GHC then fails to unify and then prints some nonsense that struggles to avoid mentioning the polymorphically-kinded reality of things (iirc, it's even said things along the lines of that it couldn't match type Foo with Foo). I don't have an example handy right at the moment, but I've run into them often enough in practice to recommend people just turn the extension on.

On Tue, 5 Jul 2022 at 23:58, Chris Dornan wrote:

...

That speaks to why PolyKinds is needed in the long run. I don’t doubt that! (Especially after this report.)

My point is merely that PolyKinds is disruptive, and that is likely to undermine confidence in the default Haskell that GHC accepts — really the reverse of what we were hoping to achieve with the new standard configuration.

Chris

On 6 Jul 2022, at 04:51, Cale Gibbard wrote:

I can remember quite a few times where GHC presented me with an incomprehensible and confused-sounding error message, but then the actual problem was that PolyKinds was off, and upon turning it on, there was no longer any problem -- it's to the point that enabling PolyKinds is one of the first things I try if I find myself disagreeing with GHC on whether something typechecks.

On Tue, 5 Jul 2022 at 23:46, Chris Dornan wrote:

...

I think we can learn to write code for PolyKinds in time, but in my experience it is quite disruptive right now, and could sow FUD around the new consensus we are trying to build.

My inclination would be to revert to Haskell2010 as the default for GHC until we can build confidence around a configuration that we are confident won’t be disruptive.

At a minimum I would create ghc2022 = ghc2021 \ {PolyKinds} and make that the default for ghc-9.4.

What do y’all think?

On 5 Jul 2022, at 16:02, Richard Eisenberg wrote:

I find that surprising, and disappointing. I think of PolyKinds as largely innocuous, except in strange scenarios, which is why PolyKinds is included in GHC2021. If that is wrong, perhaps we should consider not including PolyKinds in GHC2023...

It would be interesting to learn more about what's going wrong.

Richard

On Jul 5, 2022, at 10:26 AM, Chris Dornan wrote:

yup, i should have started there—all my recent troubles have come from PolyKinds!

On Tue, 5 Jul 2022 at 15:00, Richard Eisenberg wrote:

...

This is PolyKinds, which generalizes the kind of D, meaning that satisfying the Typeable a superclass constraint of C also requires a Typeable k constraint, where (a :: k).

Richard

...

On Jul 2, 2022, at 12:49 AM, Chris Dornan wrote:

Quick quiz: the below Haskell2010 ‘Phantoms' module (also in this Gist: https://gist.github.com/cdornan/f75cd8024434d998c87610cbb7fb6ab3) appears (for me on GHC 9.2.2 and 9.2.3) to not be a GHC2021 module, reporting this error under the latter configuration:

Phantoms.hs:22:10: error: • Could not deduce (Typeable k) arising from the superclasses of an instance declaration from the context: (C a, Typeable a) bound by the instance declaration at Phantoms.hs:22:10-36 • In the instance declaration for ‘S (D a)’ | 22 | instance (C a,Typeable a) => S (D a) where smethod = undefined | ^^^^^^^^^^^^^^^^^^^^^^^^^^^

Phantoms.hs:22:10: error: • Could not deduce (Typeable k) arising from the superclasses of an instance declaration from the context: (C a, Typeable a) bound by the instance declaration at Phantoms.hs:22:10-36 • In the instance declaration for ‘S (D a)’ | 22 | instance (C a,Typeable a) => S (D a) where smethod = undefined

The question is which language extension(s) are giving rise to these errors?

The ‘Phantoms' module is this:

{-# LANGUAGE DerivingVia #-}

module Phantoms where

import Data.Typeable

class C a where cmethod :: Proxy a -> ()

class (Show a, Typeable a) => S a where smethod :: a -> Int

newtype UsingD a = UsingD { getUsingD :: a }

newtype D a = D { getD :: Int } deriving (Show) via UsingD (D a)

instance (C a,Typeable a) => S (D a) where smethod = undefined

instance (C a,Typeable a) => Show (UsingD a) where showsPrec = undefined

instance (C a) => C (D a) where cmethod _ = undefined

_______________________________________________ ghc-steering-committee mailing list ghc-steering-committee@haskell.org

https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committee

_______________________________________________ ghc-steering-committee mailing list ghc-steering-committee@haskell.org https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committee

I am going to strengthen my statement and keep restating it — PolyKinds is for sure our destination, the path to it is the question. I am just as perplexed as Simon on why it is breaking like this and it would be great to understand it better. Chris

On 6 Jul 2022, at 09:35, Simon Peyton Jones wrote:

Like Richard, I'd be sad to think that PolyKinds is causing problems, and would like to understand better. For example, at the term level we wioudl not dream of making monomorphism the default! So why would we do that at the type level? Maybe it is a shortcoming of inference or error messages.

However the error is a bit perplexing.

class (Typeable a) => S a

newtype D a = D { getD :: Int }

instance (Typeable a) => S (D a)

We get the error Chris shows. But it looks as if we have done all that is needful. We need (Typeable (D a)) and we have provided (Typeable a). What gives? Well, what we really need is (Typeable (D @k a)), and for that we need (Typeable k) too. But that's very far from clear.

I sort of wonder: if we have (Typeable t) should that not give us (Typeable k) where (t :: k)? That would require us to have a function typeRepKind :: TypeRep (a::k) -> TypeRep k, and I don't know how hard that is to get.

Simon

On Tue, 5 Jul 2022 at 16:03, Richard Eisenberg mailto:lists@richarde.dev> wrote: I find that surprising, and disappointing. I think of PolyKinds as largely innocuous, except in strange scenarios, which is why PolyKinds is included in GHC2021. If that is wrong, perhaps we should consider not including PolyKinds in GHC2023...

It would be interesting to learn more about what's going wrong.

Richard

...

On Jul 5, 2022, at 10:26 AM, Chris Dornan mailto:chris@chrisdornan.com> wrote:

yup, i should have started there—all my recent troubles have come from PolyKinds!

On Tue, 5 Jul 2022 at 15:00, Richard Eisenberg mailto:lists@richarde.dev> wrote: This is PolyKinds, which generalizes the kind of D, meaning that satisfying the Typeable a superclass constraint of C also requires a Typeable k constraint, where (a :: k).

Richard

...

On Jul 2, 2022, at 12:49 AM, Chris Dornan mailto:chris@chrisdornan.com> wrote:

Quick quiz: the below Haskell2010 ‘Phantoms' module (also in this Gist: https://gist.github.com/cdornan/f75cd8024434d998c87610cbb7fb6ab3 https://gist.github.com/cdornan/f75cd8024434d998c87610cbb7fb6ab3) appears (for me on GHC 9.2.2 and 9.2.3) to not be a GHC2021 module, reporting this error under the latter configuration:

Phantoms.hs:22:10: error: • Could not deduce (Typeable k) arising from the superclasses of an instance declaration from the context: (C a, Typeable a) bound by the instance declaration at Phantoms.hs:22:10-36 • In the instance declaration for ‘S (D a)’ | 22 | instance (C a,Typeable a) => S (D a) where smethod = undefined | ^^^^^^^^^^^^^^^^^^^^^^^^^^^

Phantoms.hs:22:10: error: • Could not deduce (Typeable k) arising from the superclasses of an instance declaration from the context: (C a, Typeable a) bound by the instance declaration at Phantoms.hs:22:10-36 • In the instance declaration for ‘S (D a)’ | 22 | instance (C a,Typeable a) => S (D a) where smethod = undefined

The question is which language extension(s) are giving rise to these errors?

The ‘Phantoms' module is this:

{-# LANGUAGE DerivingVia #-}

module Phantoms where

import Data.Typeable

class C a where cmethod :: Proxy a -> ()

class (Show a, Typeable a) => S a where smethod :: a -> Int

newtype UsingD a = UsingD { getUsingD :: a }

newtype D a = D { getD :: Int } deriving (Show) via UsingD (D a)

instance (C a,Typeable a) => S (D a) where smethod = undefined

instance (C a,Typeable a) => Show (UsingD a) where showsPrec = undefined

instance (C a) => C (D a) where cmethod _ = undefined

_______________________________________________ ghc-steering-committee mailing list ghc-steering-committee@haskell.org mailto:ghc-steering-committee@haskell.org https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committee https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committee

_______________________________________________ ghc-steering-committee mailing list ghc-steering-committee@haskell.org mailto:ghc-steering-committee@haskell.org https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committee https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committee

On Jul 6, 2022, at 4:35 AM, Simon Peyton Jones wrote:

I sort of wonder: if we have (Typeable t) should that not give us (Typeable k) where (t :: k)? That would require us to have a function typeRepKind :: TypeRep (a::k) -> TypeRep k, and I don't know how hard that is to get.

We have that function. It's called typeRepKind. What we need for this example is a superclass constraint: class Typeable k => Typeable (a :: k) which would probably require UndecidableSuperClasses, but otherwise might just work. Richard

On Jul 6, 2022, at 8:00 AM, Chris Dornan wrote:

Richard are you satisfied that my example program is invalid under PolyKinds?

Yes. But I think as we've started to piece together, the real problem in this example is a missing superclass constraint on Typeable, not a fundamental shortcoming of PolyKinds. (I do acknowledge that extra polymorphism can introduce trouble, but given the fact that PolyKinds introduces parametric polymorphism -- unlike the ad hoc polymorphism of OverloadedStrings -- I think these cases should be rare.) It would be interesting to see whether fixing Typeable in this way fixes other problems Chris has run into. Richard