Opened 3 years ago

Closed 3 years ago

Last modified 7 months ago

#10109 closed bug (fixed)

Kinds aren't checked in the coverage condition

Reported by: goldfire Owned by:
Priority: normal Milestone: 7.10.2
Component: Compiler Version: 7.10.1-rc2
Keywords: FunDeps Cc: jan.stolarek@…
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: None/Unknown Test Case: typecheck/should_compile/T10109
Blocked By: Blocking:
Related Tickets: Differential Rev(s):
Wiki Page:

Description

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.

Change History (6)

comment:1 Changed 3 years ago by goldfire

As a further curiosity, both versions of the program above fail without UndecidableInstances. How does UndecidableInstances affect the coverage condition check? Is this documented?

comment:2 Changed 3 years ago by jstolarek

Cc: jan.stolarek@… added

comment:3 Changed 3 years ago by Simon Peyton Jones <simonpj@…>

In 49d9b009a2affb6015b8f6e2f15e4660a53c0d9a/ghc:

Fix fundep coverage-condition check for poly-kinds

See Note [Closing over kinds in coverage] in FunDeps.
I'd already fixed this bug once, for Trac #8391, but I put the
call to closeOverKinds in the wrong place, so Trac #10109
failed.  (It checks the /liberal/ coverage condition, which

The fix was easy: move the call to the right place!

comment:4 Changed 3 years ago by simonpj

Status: newmerge
Test Case: typecheck/should_compile/T10109

Sorry for the slightly garbled commit message, but the main payload is right!

comment:5 Changed 3 years ago by thoughtpolice

Milestone: 7.10.2
Resolution: fixed
Status: mergeclosed

This was actually merged a while back; just not closed (see d5c089208735014a09d43b1ee757f52ddbfc92bf).

comment:6 Changed 7 months ago by simonpj

Keywords: FunDeps added
Note: See TracTickets for help on using tickets.