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.
So this question isn't marked as unanswered I guess I will just reiterate what was said in the comments.
Basically
ImpredicativeTypesis 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".