Opened 6 years ago

Closed 15 months ago

#2247 closed bug (fixed)

GHC accepts FD violations, unless the conflicing instances are used

Reported by: claus Owned by:
Priority: normal Milestone:
Component: Compiler (Type checker) Version: 6.9
Keywords: TF vs FD Cc:
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: None/Unknown Difficulty: Unknown
Test Case: typecheck/should_fail/T2247 Blocked By:
Blocking: Related Tickets:

Description

consider

class FD a b | a -> b
instance CFD a b => FD a b

class {- FD a b => -} CFD a b
instance CFD Bool Char
instance CFD Bool Bool

f :: CFD Bool Bool => Bool
f = True

g :: CFD Bool Char => Bool
g = False

f' :: FD Bool Bool => Bool
f' = True

g' :: FD Bool Char => Bool
g' = False

the class instance for FD is odd, because there is no guarantee that instances of CFD comply to the FD (and Hugs rejects that instance, unless the superclass constraint for CFD is uncommented). as it stands, this code specifies two FD-conflicting instances of class FD, but they are implied, not explicit.

GHCi accepts this code, and only complains if the two conflicting instances are used, explicitly, in the same expression:

*Main> f
True
*Main> g
False
*Main> (f,g)
(True,False)
*Main> f'
True
*Main> g'
False
*Main> (f',g')

<interactive>:1:0:
    Couldn't match expected type `Bool' against inferred type `Char'
    When using functional dependencies to combine
      FD Bool Char, arising from a use of `g'' at <interactive>:1:4-5
      FD Bool Bool, arising from a use of `f'' at <interactive>:1:1-2
    When generalising the type(s) for `it'
*Main> do {let {x=f} ;let {y=g} ; return (x,y) }
(True,False)
*Main> do {let {x=f'} ;let {y=g'} ; return (x,y) }

<interactive>:1:0:
    Couldn't match expected type `Char' against inferred type `Bool'
    When using functional dependencies to combine
      FD Bool Bool, arising from a use of `f'' at <interactive>:1:11-12
      FD Bool Char, arising from a use of `g'' at <interactive>:1:23-24
    When generalising the type(s) for `it'
*Main> let x=f'
*Main> let y=g'
*Main> (x,y)
(True,False)

so we can have FD-conflicting instances in the same code, even use them in the same GHCi session, as long as they don't meet in the same line..

for further details and questions, see this message:
some questions about type improvement, FDs vs TFs, and Hugs vs GHCi

Change History (9)

comment:1 Changed 6 years ago by claus

here is a slight variation that does not rely on a GHCi session to raise the issue

module Improve where

class FD a b | a -> b
instance CFD a b => FD a b

class {- FD a b => -} CFD a b
instance CFD Bool Char
instance CFD Bool Bool

f' :: FD Bool Bool => Bool
f' = True

g' :: FD Bool Char => Bool
g' = False

x = f'
module Main where
import Improve

y = g'

main = print (x,y)

GHC (6.9.20080217) accepts this, and the executable outputs (True,False), even though the first component depends on instance FD Bool Bool while the second depends on instance FD Bool Char.

Inlining x as f' is sufficient to raise the expected error message.

comment:2 follow-up: Changed 6 years ago by simonpj

  • Difficulty set to Unknown
  • Resolution set to duplicate
  • Status changed from new to closed

I assume you are using some flags?

ghc -c -XFunctionalDependencies Foo.hs -XMultiParamTypeClasses

Foo.hs:5:1:
    Illegal instance declaration for `FD a b'
        (All instance types must be of the form (T a1 ... an)
         where a1 ... an are distinct type *variables*
         Use -XFlexibleInstances if you want to disable this.)
    In the instance declaration for `FD a b'

Adding -XFlexibleInstances gives

bash-3.1$ ghc -c -XFunctionalDependencies Foo.hs -XMultiParamTypeClasses -XFlexibleInstances

Foo.hs:5:1:
    Constraint is no smaller than the instance head
      in the constraint: CFD a b
    (Use -fallow-undecidable-instances to permit this)
    In the instance declaration for `FD a b'

Foo.hs:5:1:
    Illegal instance declaration for `FD a b'
        (the Coverage Condition fails for one of the functional dependencies;
         Use -fallow-undecidable-instances to permit this)
    In the instance declaration for `FD a b'

In fact to get Improve to compile you need

$gpj -c -XFunctionalDependencies  
        -XMultiParamTypeClasses 
        -XFlexibleInstances 
        -fallow-undecidable-instances 
        -XFlexibleContexts
        Foo.hs

The offending one is -fallow-undecidable-instances, and this ticket is an excellent example of #1241. Currently saying -fallow-undecidable-instances lifts the coverage condition. I acknowledge that this isn't the Right Thing in #1241, but it doesn't threaten type soundness (ie programs will not seg-fault).

So I'm going to close this bug and link to it from #1241. Re-open if I have misunderstood.

Simon

comment:3 in reply to: ↑ 2 Changed 6 years ago by claus

  • Resolution duplicate deleted
  • Status changed from closed to reopened

Replying to simonpj:

I assume you are using some flags?

always!-) in fact, as you can see from this little example, using GHC has become very inconvenient due to the proliferation of flags. first, i have to iterate to figure out which flags i need to get my code accepted. then, i have to do the same again because the GHCi session does *not* inherit the LANGUAGE pragmas from the module i load..

it doesn't help that UndecidableInstances is needed so often for perfectly decidable code. in this case, delegating to another constraint that is no smaller than the original already requires this extension, independent of coverage.

In fact to get Improve to compile you need

$gpj -c -XFunctionalDependencies  
        -XMultiParamTypeClasses 
        -XFlexibleInstances 
        -fallow-undecidable-instances 
        -XFlexibleContexts
        Foo.hs

The offending one is -fallow-undecidable-instances, and this ticket is an excellent example of #1241. Currently saying -fallow-undecidable-instances lifts the coverage condition. I acknowledge that this isn't the Right Thing in #1241, but it doesn't threaten type soundness (ie programs will not seg-fault).

So I'm going to close this bug and link to it from #1241. Re-open if I have misunderstood.

yes and no. yes, for the current implementation of FDs in GHC; no, in principle.

neither coverage nor fullness appear necessary for confluence (cf. Restoring Confluence for Functional Dependencies, T. Schrijvers, M. Sulzmann), and a confluent implementation of FDs should raise all inconsistencies, with the exception of dead code (the ticket example was meant to highlight this gap, see also the discussion of forward inference in http://www.haskell.org/pipermail/haskell-cafe/2008-April/042219.html).

the variation shows clearly that GHC drops FD/improvement-related information, so that not even all conflicts in live constraints are flagged. it seems that one of the places where improvement-related information is dropped is separate compilation (if all FD-relevant constraints were cached as they arise, and preserved in interface files, inlining across module boundaries ought to make no difference, right?).

note also this reduced variation

class FD a b | a -> b
instance CFD a b => FD a b

class FD a b => CFD a b
instance CFD Bool Char
-- instance CFD Bool Bool

which is accepted by Hugs (in Hugs mode), in spite of its presumably stricter conditions. yet, on uncommenting the second CFD instance, Hugs notices the FD-inconsistency immediately, while GHCi doesn't (and the other variations show that GHC won't necessarily notice the issue later, either).

so, the two tickets are linked, but if one looks beyond ruling out this kind of example (and #1241 seemed to tend in the direction of finding less restrictive conditions than GHC has, not more restrictive conditions than Hugs has), there seems to be more going on. at the very least, this ticket should be looked into when #1241 gets fixed, in case it isn't covered by the same fix.

comment:4 Changed 6 years ago by igloo

  • Milestone set to _|_

#1241 is _|_, so I guess this should be too

comment:5 Changed 6 years ago by simonmar

  • Architecture changed from Unknown to Unknown/Multiple

comment:6 Changed 6 years ago by simonmar

  • Operating System changed from Unknown to Unknown/Multiple

comment:7 Changed 15 months ago by iavor.diatchki@…

commit fe61599ffebb27924c4beef47b6237542644f3f4

Author: Iavor S. Diatchki <iavor.diatchki@gmail.com>
Date:   Sun Jan 13 16:29:10 2013 -0800

    Use a version of the coverage condition even with UndecidableInstances.
    
    This fixes bug #1241 and #2247.  When UndecidableInstances are on,
    we use the "Liberal Coverage Condition", which is what GHC used to do in
    the past.  This is the gist of the check:
    
    class C a b | a -> b
    instance theta => C t1 t2
    
    we check that `fvs t2` is a subset of `fd-closure(theta,fvs t1)`.
    
    This is strictly more general than the coverage condition, while
    it still guarantees consistency with the FDs of the class.  This
    check is completely orthogonal to termination (it by no means guarantees
    it).
    
    I am not sure of the role of the "coverage condition" in termination---
    the comments suggest that it is important.  This is why, for the moment,
    we only use this check when UndecidableInstances are on.

 compiler/typecheck/TcValidity.lhs |    8 ++++-
 compiler/types/FunDeps.lhs        |   65 ++++++++++++++++++++++++++++++++++++-
 2 files changed, 71 insertions(+), 2 deletions(-)

comment:8 Changed 15 months ago by monoidal

  • Type of failure set to None/Unknown

After Iavor's commit the code is rightfully rejected. Close as fixed?

comment:9 Changed 15 months ago by simonpj

  • Resolution set to fixed
  • Status changed from new to closed
  • Test Case set to typecheck/should_fail/T2247

Correct, thanks.

Note: See TracTickets for help on using tickets.