How to make impredicative types work with type classes

2
votes

I was seeing what I could do with ImpredicativeTypes and wanted to see what exactly I could do with them. When I ran to what I feel is some strange behavior when it comes to their interaction with TypeClasses.

:t mempty
mempty :: forall a. Monoid a => a

:t Right
Right :: forall a b. b -> Either a b

So I figured I could combine them to make an impredicatively typed expression:

:t Right mempty
Right mempty :: forall a b. Monoid b => Either a b

Looks like the extension does not infer impredicative types, which doesn't seem all that unreasonable, as I know that type inference is not always possible in the general case when you start adding features like this.

So I decided that I would just make the fact that I wanted an impredicative type explicit:

:t Right mempty :: forall a. Either a (forall b. Monoid b => b)

Which to me seemed very reasonable, as I am literally just pasting over the b in the Right type signature with the type of mempty, and then not lifting the forall.

But it give me the following error:

No instance for (Monoid (forall b. Monoid b => b))

Which seems rather absurd. Since every Monoid is an instance of Monoid by definition.

Can someone explain to me what exactly is going on here? Is the issue that it would be too difficult or impossible to actually decide on one instance when actually using the type, and thus GHC really means "No unambiguous / decidable instance for..." rather than "No instance..."?

As a side note when you take typeclasses out of the situation everything appears to work ok:

:t Right undefined :: forall a. Either a (forall b. b)

Type checks and gives me back the impredicative type I specified.

1
haskelltypeclassimpredicativetypes
Some of what's going on here is pretty clear, though: GHC needed to make mempty :: forall b. Monoid b => b, but mempty :: Monoid m => m, so it picked m = (forall b. Monoid b => b) and then tried to solve the constraint Monoid (forall b. Monoid b => b), which of course it couldn't (there aren't instances for polytypes). - Reid Barton
I'm voting to close this question as off-topic because according to the GHC documentation, ImpredicativeTypes is "extremely flaky", "highly experimental" and "certainly un-supported". It also makes reference to what this feature would do "if it worked". There's simply no point in trying to use this extension unless and until it is fixed. IMHO, the current proposed fix is too invasive. - dfeuer
Reid was making an informed guess. At present, I don't think anyone actually understands the effects of the extension. Most notably, type system hacker extraordinaire Richard Eisenberg has made multiple deep changes to the type system over the past couple years without making any effort to keep the extension up to date with those changes. This is basically because nobody has yet figured out exactly how it should behave, and it's never behaved well enough to make it tractable to even maintain its behavior. - dfeuer
Well there definitely aren't any instances for polytypes. The question is about how GHC decides whether to pick m = b and then generalize, to get mempty :: forall b. Monoid b => b, or to just pick m = (forall b. Monoid b => b). - Reid Barton
This is not special to Monoid, mempty, Right, or lack of class instance for polytypes - e.g. (,) 0 :: (forall b. Show b => b) -> (Int, forall b. Show b => b) just by itself is not well typed. Impredictive types don't work well at all .. the only way I've gotten this to type check is with (Right `asTypeOf` (undefined :: (forall b. Monoid b => b) -> Either () (forall b. Monoid b => b))) mempty, but I sure can't tell you why it works. - user2407038

1 Answers

1
votes

So this question isn't marked as unanswered I guess I will just reiterate what was said in the comments.

Basically ImpredicativeTypes is totally unsupported, and no one really knows how it even should work. So trying to do anything meaningful with it in its current state is a bad idea. So the answer is just: "don't try to do that".