[GHC] #10109: Kinds aren't checked in the coverage condition

23 Feb 2015

      #10109: Kinds aren't checked in the coverage condition
-------------------------------------+-------------------------------------
              Reporter:  goldfire    |             Owner:
                  Type:  bug         |            Status:  new
              Priority:  normal      |         Milestone:
             Component:  Compiler    |           Version:  7.10.1-rc2
              Keywords:              |  Operating System:  Unknown/Multiple
          Architecture:              |   Type of failure:  None/Unknown
  Unknown/Multiple                   |        Blocked By:
             Test Case:              |   Related Tickets:
              Blocking:              |
Differential Revisions:              |
-------------------------------------+-------------------------------------
 Following on from the debate in #9103 (but you don't need to read that
 ticket), I found a curiosity.

 The following module fails to compile, complaining about the unsatisfied
 coverage condition:

 {{{
 {-# LANGUAGE PolyKinds, MultiParamTypeClasses, FunctionalDependencies,
              FlexibleInstances, UndecidableInstances #-}

 module Bug where

 data Succ a

 class Add (a :: k1) (b :: k2) (ab :: k3) | a b -> ab, a ab -> b
 instance (Add a b ab) => Add (Succ a) b (Succ ab)
 }}}

 With `-fprint-explicit-kinds`, I get

 {{{
 Bug.hs:9:10:
     Illegal instance declaration for
       ‘Add * k * (Succ k a) b (Succ k ab)’
       The liberal coverage condition fails in class ‘Add’
         for functional dependency: ‘a b -> ab’
       Reason: lhs types ‘Succ k a’, ‘b’
         do not jointly determine rhs type ‘Succ k ab’
     In the instance declaration for ‘Add (Succ a) b (Succ ab)’
 }}}

 But, when I add `k3` to the right-hand side of the first functional
 dependency (viz.

 {{{
 {-# LANGUAGE PolyKinds, MultiParamTypeClasses, FunctionalDependencies,
              FlexibleInstances, UndecidableInstances #-}

 module Bug where

 data Succ a

 class Add (a :: k1) (b :: k2) (ab :: k3) | a b -> ab k3, a ab -> b
 instance (Add a b ab) => Add (Succ a) b (Succ ab)
 }}}

 ) I get

 {{{
 [1 of 1] Compiling Bug              ( Bug.hs, interpreted )
 Ok, modules loaded: Bug.
 }}}

 I always assumed that fixing a type in a fundep also fixed its kind.

 I get the same behavior in 7.8 as in 7.10.1RC2.

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