Annotation of PolyKinded structures (unhelpfully) prompts UndecidableInstances
Summary
The error message provided when GHC infers the kind of an otherwise poly-kinded structure is unhelpful. I recognize that this might not be the highest priority, but I do think Haskell's error messages here could be better.
Steps to reproduce
Let's say I have a little program like
{-# LANGUAGE PolyKinds #-}
class Foo a
data Bar (f :: * -> *)
instance (Foo (f Bool)) => Foo (Bar f)
main :: IO ()
main = pure ()
Everything compiles and is happy and fun.
(This is stripped down for clarity; imagine lots of irrelevant methods and constructors and other spinning parts in the case where I actually hit this.)
Now let's say you foolishly add a method to Foo
like so:
class Foo a where
foo :: Int -> [a]
GHC errors, saying:
• The constraint ‘Foo (f Bool)’
is no smaller than the instance head ‘Foo (Bar f)’
(Use UndecidableInstances to permit this)
• In the instance declaration for ‘Foo (Bar f)’
What happened here was that by mentioning [a]
we've pinned down the kind of a
. A similar effect can be produced simply by annotating the kind of a
like so:
class Foo (a :: *)
Before this kind was specified, the decidability checker on the instance was satisfied, but afterwards it chokes and demands UndecidableInstances
. My guess of why it's doing this is that there's an implicit kind showing up in the context afterwards, and so it no longer knows that the context is smaller than the head. *shrug*
Expected behavior
I would hope that annotating the kind of a class would not affect known-to-be-valid instances of that class elsewhere. At the very least I'd hope that the decidability checker would report in its error that it only failed because of an inferred kind when PolyKinds is active. Best of all would be if the decidability checker could handle having kinds specified in cases like this.
Environment
Tested on GHC 8.6 and 8.8.