Invisible kind variable referenced in typeclass instance error message
Here is a minimal example:
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
newtype HFix h a = HFix (h (HFix h) a)
class EqForall f where
eqForall :: f a -> f a -> Bool
class EqHetero h where
eqHetero :: (forall x. f x -> f x -> Bool) -> h f a -> h f a -> Bool
instance EqHetero h => EqForall (HFix h) where
eqForall (HFix a) (HFix b) = eqHetero eqForall a b
instance EqHetero h => Eq (HFix h a) where
(==) = eqForallWhen we build this with GHC 8.2.1, we get the following error message:
instance_head.hs:18:10: error:
• Variable ‘k’ occurs more often
in the constraint ‘EqHetero h’ than in the instance head
(Use UndecidableInstances to permit this)
• In the instance declaration for ‘Eq (HFix h a)’
|
18 | instance EqHetero h => Eq (HFix h a) where
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^The error message is bad, although most people trying to do this kind of thing can probably reason that there is an invisible k and that h :: (k -> Type) -> k -> Type and that a :: k. I don't really see a way to improve it, but I thought I would bring it up.
Also, should the typechecker even reject this? I don't have a great understanding of how GHC's restrictions for keep things decidable work, but a repeated invisible variable seems like it's a somewhat different thing than a repeated visible variable. I'm likely wrong about this, but I just wanted to raise the question.
Trac metadata
| Trac field | Value |
|---|---|
| Version | 8.2.1 |
| Type | Bug |
| TypeOfFailure | OtherFailure |
| Priority | normal |
| Resolution | Unresolved |
| Component | Compiler |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | |
| Operating system | |
| Architecture |