[GHC] #14151: Invisible kind variable referenced in typeclass instance error message

24 Aug 2017

      #14151: Invisible kind variable referenced in typeclass instance error message
-------------------------------------+-------------------------------------
           Reporter:  andrewthad     |             Owner:  (none)
               Type:  bug            |            Status:  new
           Priority:  normal         |         Milestone:
          Component:  Compiler       |           Version:  8.2.1
           Keywords:                 |  Operating System:  Unknown/Multiple
       Architecture:                 |   Type of failure:  None/Unknown
  Unknown/Multiple                   |
          Test Case:                 |        Blocked By:
           Blocking:                 |   Related Tickets:
Differential Rev(s):                 |         Wiki Page:
-------------------------------------+-------------------------------------
 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
   (==) = eqForall
 }}}

 When 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.

-- 
Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14151
GHC http://www.haskell.org/ghc/
The Glasgow Haskell Compiler