Opened 6 years ago

Closed 6 years ago

Last modified 6 years ago

#8356 closed bug (fixed)

Strangeness with FunDeps

Reported by: ksf Owned by:
Priority: normal Milestone:
Component: Compiler Version: 7.7
Keywords: Cc: diatchki
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: GHC rejects valid program Test Case: typecheck/should_fail/tcfail170
Blocked By: Blocking:
Related Tickets: Differential Rev(s):
Wiki Page:

Description

{-# 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.

Change History (9)

comment:1 Changed 6 years ago by rwbarton

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 http://ghc.haskell.org/trac/ghc/ticket/1241#comment:22.

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

comment:2 Changed 6 years ago by ksf

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 :)

Last edited 6 years ago by ksf (previous) (diff)

comment:3 Changed 6 years ago by ksf

For reference, here's the whole code:

http://lpaste.net/93383

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

comment:4 Changed 6 years ago by simonpj

Cc: diatchki added

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

comment:5 Changed 6 years ago by unknown <simonpj@…>

In bceeb0167804e3325b48d4b360fddd68e29735a2/ghc:

Improve error reporting of fundep coverage condition failure

This modest improvement is motivated by Trac #8356

comment:6 Changed 6 years ago by simonpj

Resolution: fixed
Status: newclosed
Test Case: typecheck/should_fail/tcfail170

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]’

comment:7 Changed 6 years ago by monoidal

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]’

comment:8 Changed 6 years ago by simonpj

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

comment:9 Changed 6 years ago by Krzysztof Gogolewski <krz.gogolewski@…>

In eaa4682b68348eb3b49a0bf2700abc58be820555/ghc:

Remove debugging output (#8356)
Note: See TracTickets for help on using tickets.