Strangeness with FunDeps

{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTSyntax #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE FunctionalDependencies #-}
import GHC.TypeLits 
data (:::) :: Symbol -> * -> * where
    Field :: sy ::: t

class Replaced (sy :: Symbol) a b (xs :: [*]) (ys :: [*]) | sy a b xs -> ys, sy a b ys -> xs

instance Replaced sy a b ((sy ::: a) ': xs) ((sy ::: b) ': ys)

results in

Illegal instance declaration for [...]                                  
      Multiple uses of this instance may be inconsistent
      with the functional dependencies of the class

The guess is that the FunDep Checker chokes on [*], as that error message doesn't make sense in this context.

What I'm trying to do is to express "xs is ys and ys is xs with a and b interchanged at sy", all in a single predicate because my current type family implementation needs two and explodes the inferred types.

Trac metadata

Trac field	Value
Version	7.7
Type	Bug
TypeOfFailure	OtherFailure
Priority	normal
Resolution	Unresolved
Component	Compiler
Test case
Differential revisions
BlockedBy
Related
Blocking
CC
Operating system
Architecture

changed weight to 5

added Tbug Trac import labels

The error makes sense to me: sy, a, b and ((sy ::: a) ': xs) do not jointly determine ((sy ::: b) ': ys), because the whole ys part is free. (And the same for the other fundep.)

Perhaps the error message could be more specific, saying what I said above? something like

Illegal instance declaration for [...]                                  
      Multiple uses of this instance may be inconsistent
      with the functional dependencies of the class:
          `sy', `a', `b' and `((sy ::: a) ': xs)' do not
          jointly determine `((sy ::: b) ': ys)'

Extra clarity would be good here since there are existing libraries that use fundeps incorrectly, that will stop compiling in 7.8, and I anticipate a slew of bug reports otherwise. See for example #1241 (closed)##8356 (closed).

What I'm trying to do is to express "xs is ys and ys is xs with a and b interchanged at sy", all in a single predicate because my current type family implementation needs two and explodes the inferred types.

In that case, perhaps you intended

instance Replaced sy a b ((sy ::: a) ': xs) ((sy ::: b) ': xs) -- note xs twice

Yes, the more specific error message looks very helpful.

In the end, I got the code working:

class Replaced sy a b xs ys | sy a b xs -> ys, sy a b ys -> xs -- , sy xs -> a, sy ys -> b

instance Replaced sy a b xs ys => Replaced sy a b ((sy ::: a) ': xs) ((sy ::: b) ': ys)
instance Replaced sy a b ((sy ::: a) ': '[]) ((sy ::: b) ': '[])
instance Replaced sy a b xs ys => Replaced sy a b ((sy' ::: c) ': xs) ((sy' ::: c) ': ys)
instance Replaced sy a b ((sy' ::: c) ': '[]) ((sy' ::: c) ': '[])

However I don't see any way how to enable the commented out constraints without bumping into overlaps further down the line. ~~I *do* know that the list always contains sy, so the base cases don't affect the fact that a and b are always inferable from xs and ys.~~

I appreciate you trying to fix the old bug, but please make that behaviour disableable. I might just be able to muggle through otherwise with the added inconsistency :)

For reference, here's the whole code:

http://lpaste.net/93383

1. ..trying to minimise the inferred type for foo, both with and without li fixed. With the added sy ys -> b constraint, the ElemTy sy ys ~ b constraint on mapKey could be elided.

Thanks for the suggestion; I'll improve the error message (patch coming).

I don't remember all the issues about the coverage condition, but I think there were very good reasons for enforcing it. I'm adding Iavor to the cc list; he may comment.

Simon

mentioned in commit bceeb016

closed

Error message improved. Here it is for tcfail170:

tcfail170.hs:7:10:
    Illegal instance declaration for ‛C [p] [q]’
      The coverage condition fails in class ‛C’
        for functional dependency: ‛a -> b’
      Reason: lhs type ‛[p]’ does not deternine rhs type ‛[q]’
    In the instance declaration for ‛C [p] [q]’

Trac metadata

Trac field	Value
Resolution	Unresolved → ResolvedFixed
Test case	→ typecheck/should_fail/tcfail170

The testcase tcfail170 triggers a pprTrace in FunDeps.lhs. Is this intended?

$ ghc-7.7.20131027 tcfail170
[1 of 1] Compiling ShouldFail       ( tcfail170.hs, tcfail170.o )
cic main:ShouldFail.C{tc roB} [[p{tv aoE} [sk]], [q{tv aoF} [sk]]]
    ([a{tv aoC} [tv]], [b{tv aoD} [tv]])
    [(aoE, p{tv aoE} [sk])]
    [(aoF, q{tv aoF} [sk])]
    [(aoE, p{tv aoE} [sk])]
    []

tcfail170.hs:7:10:
    Illegal instance declaration for ‛C [p] [q]’
      The coverage condition fails in class ‛C’
        for functional dependency: ‛a -> b’
      Reason: lhs type ‛[p]’ does not determine rhs type ‛[q]’
    In the instance declaration for ‛C [p] [q]’

It's a trace that should have been removed, but the test suite runs (rightly or wrongly) with -fno-debug-output which suppresses it.

I'd be happy if someone had a moment to delete that line.

Simon

mentioned in commit eaa4682b

mentioned in issue #8634

mentioned in issue #9227 (closed)

added Pnormal label