Opened 4 years ago

Last modified 9 months ago

#10675 new bug

GHC does not check the functional dependency consistency condition correctly

Reported by: simonpj Owned by:
Priority: normal Milestone:
Component: Compiler Version: 7.10.1
Keywords: FunDeps Cc: diatchki, dimitris, goldfire, jstolarek
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: None/Unknown Test Case:
Blocked By: Blocking:
Related Tickets: Differential Rev(s):
Wiki Page:

Description (last modified by simonpj)

Consider

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

class C x a b | a -> b where
  op :: x -> a -> b
instance C Bool [x] [x]
instance C Char x y => C Char [x] [Maybe y]

f x = op True [x]

Should these two instance declarations be accepted? The two instances don't contradict each other, but neither do they agree as all published work on FDs says they should! They are inconsistent in the sense of Definition 6 of the FDs through CHRs paper.

Sadly GHC does not currently reject these as inconsistent. As a result it'll use both instance for improvement. In the definition of f for example we get

  C Bool [alpha] beta

where x:alpha and the result type of f is beta. By using both instances for improvement we get

  C Bool [Maybe gamma] [Maybe gamma]

That can be solved, so we get

f :: Maybe x -> [Maybe x]

But where did that Maybe come from? It's really nothing to do with it.

Examples in the testsuite that exploit this loophole are

   ghci/scripts                         ghci047
   polykinds                            T9106
   typecheck/should_compile             FD4
   typecheck/should_compile             T7875 

I'm not sure what the right thing here is.

Change History (22)

comment:1 Changed 4 years ago by simonpj

Description: modified (diff)

comment:2 Changed 4 years ago by simonpj

Cc: diatchki dimitris goldfire added

comment:3 Changed 4 years ago by jstolarek

Cc: jstolarek added

comment:4 Changed 4 years ago by osa1

Cc: osa1 added

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

In d53d8089/ghc:

Refactoring around FunDeps

This refactoring was triggered by Trac #10675.

We were using 'improveClsFD' (previously called 'checkClsFD') for
both
  * Improvement: improving a constraint against top-level instances
  * Consistency: checking when two top-level instances are
    consistent

Using the same code for both seemed attractive at the time, but
it's just too complicated.  So I've split it:
 * Improvement: improveClsFD
 * Consistency: checkFunDeps

Much clearer now!

comment:6 Changed 4 years ago by goldfire

Simon says:

I'm not sure what the right thing here is.

I say that we should reject these programs. They're bogus! This might make some affected people complain, but the situation seems similar to what happened between 7.6 and 7.8 where the FD check was tightened (most recently). Some people's programs stopped working, but it was all for a good reason.

The examples all look like an attempt to encode instance chains. GHC has hitherto failed to notice the overlap, but it's been there all along. Happily, each of these examples could straightforwardly (if verbosely and unpleasantly) be refactored to use closed type families.

Or, if we ever get around to finishing the work for #8634, folks who want the old behavior can just call their functional dependency to be dysfunctional (which it really is) and get on with it.

comment:7 Changed 4 years ago by rwbarton

See also #9210, where a potential fix broke the same four test cases.

comment:8 Changed 4 years ago by simonpj

Yes, good link!

I agree with Richard: we just just make these programs illegal. #9210 is a particularly egregious case of what can go wrong otherwise.

I would like Iavor's opinion before doing this.

Simon

comment:9 Changed 2 years ago by AntC

Should these two instance declarations be accepted?

Depends what you mean by "accepted". I think the case is suffering from GHC's delayed/lazy instance enforcement, as affects the complications of confluence around partially overlapping instances.

The C Char ... instance clearly could never work -- its constraint needs an infinite regress on C Char [[[[ ... ]]]] .... Is anybody saying that instance on its own should be rejected? If so, see counter-example/highly valuable exploit below.

It's an interesting experiment trying to find valid calls for f [I'm using 7.10]. This works: f (Just "quoi?"). This doesn't: f ("quoi") -- GHC complains "Couldn't match expected type 'Maybe y0' with actual type '[Char]'".

So GHC is applying the fundep a -> b Consistency Condition as per Definition 6 in the CHRs/Mark Jones 2000 paper. It is taking [x] [Maybe y] to infer that in [x] [x] we must have x ~ Maybe y -- as the O.P. is saying.

I think we've no reason to reject this example. Or perhaps Iavor could explain what "loophole" this opens up? Can it result in type incoherence?

Before we reject this example as bogus, @Richard, I think there are examples similar to it that might get caught in the crossfire. [That's the reason I arrived here, because I'm trying to understand how/why the FunDeps work for it.] The classic Type-level type equality test:

class TTypeEq (a :: *) (a' :: *) (b :: Bool) | a a' -> b
instance TTypeEq a a True
instance (b ~ False) => TTypeEq a a' b

Seems to break Definition 6. There's a substitution for the two instances that makes the determinants of the FunDep equal, namely {a' ~ a}. And under that substitution, the dependents are not equal {b vs True}. FWIW, Hugs applies a stricter interpretation of Definition 6, with the consequence no such declaration of TTypeEq is accepted [explored in Oleg/Ralf/Keean's HList paper]. Hugs also rejects the two instances in the O.P. as inconsistent.

Or if we include substitution {b ~ True}, that substitution invalidates the constraint on the False instance. Clearly GHC isn't evaluating the instance's constraints for consistency with its improvement of the class parameters.

We can't write that second instance as:

instance TTypeEq a a' False

GHC complains "Functional Dependencies conflict between instance declarations"

What would any proposed fix for this ticket do to a class like?

class TTypeEq2 x a a' b | a a' -> b
instance TTypeEq2 Bool a a True
instance TTypeEq2 Char a a True
instance (b ~ False) Bool a a' b
instance (b ~ False) Char a a' b
Last edited 2 years ago by AntC (previous) (diff)

comment:10 Changed 2 years ago by simonpj

Keywords: FunDeps added

comment:11 Changed 2 years ago by AntC

Some afterthoughts:

  • What if the instances from the O.P. were declared in separate modules? Then GHC couldn't apply the mutual improvement. Would it reject the instances as inconsistent?
  • I find the statement of Definition 6 in the CHR paper a bit imprecise. Mark Jones 2000 paper is clearer [Section 6.1]. It says "if tX and sX have a most general unifier U, then UtY = UsY." where tX, sX are the determinant types from the instance decl, tY, sY are the dependents.
  • I wonder if what GHC is doing to apply that test is rather than UtY = UsY, it's checking UtY ~ UsY -- that is, checking unifiability rather than equality(?) That would explain the behaviour with the TTypeEq examples.
  • Re the "dysfunctional" Functional Dependencies ;-), we could do with some better way of writing instances to give maximum help for type improvement. Currently you keep running up against instance-FunDep conflicts. And I don't think Injective type functions help much. For example type-level Plus over Nats, with three-way FunDeps. [Yes I know Oleg worked it out years ago, but it's a tour de force.]

comment:12 Changed 2 years ago by diatchki

Hello,

I just saw this, sorry for the very late reply.

I don't think that the original example technically violates the FD property as the second instance (the one with C Char ...) is vacuous and doesn't actually add any new instances to C (there is no base case). The first instance on its own is OK, so the whole program is OK. I am not sure that this is an easy thing to spot in general though.

There is, however, a real problem with the consistency checking of FDs, as illustrated by the following example:

class F tag a b | a -> b
class G     a b | a -> b
class H     a b | a -> b

instance G a b => F Int  [a] [b]
instance H a b => F Char [a] [b]
instance G Int Int
instance H Int Char

These instances are accepted by GHC 8.0.1 but are inconsistent, because we can derive both F Int [Int] [Int] and F Char [Int] [Char] which violates the FD on F.

Last edited 2 years ago by diatchki (previous) (diff)

comment:13 Changed 2 years ago by AntC

Thanks Iavor,

  • Yes the C Char ... instance is vacuous. I think GHC must accept it, because for all it knows there is some other instance decl for C that will provide a base case. That tells us we should be cautious if an instance (or set of instances) is accepted: the instances alone are weak evidence until/unless we can prove they can be inhabited.
  • I think what Simon's worried about is that the two instance decls have got entangled. And yet they don't overlap. So I'd be suspicious we'd see different behaviour under separate compilation.
  • Your instances for F break the FunDep coverage condition, so presumably you needed UndecidableInstances. What's reasonable to expect after that? I did get some types to inhabit those instances; and yes they were inconsistent with the Fundeps on F.
  • I guess GHC with UndecidableInstances sees there's a constraint on the instance (G, H), and that constraint carries a FunDep, so delegates the FunDep to it. We know GHC doesn't/can't chase round all the constraints, because it can't see all the instances. It delays that check to the use site -- but then that only considers the instances selected at that site.
  • Constraints like you've put are useful -- the type-level Type Equality test example. Arguably any such Type Equality test breaks Definition 6 Consistency condition. To express a Type Equality test as close as I can to your example:
class TypeEq          a a' b | a a' -> b
class TypeCastTrue    a a' b | a a' -> b
class TypeCastFalse   a a' b | a a' -> b

instance TypeCastTrue  a a  b => TypeEq a a  b
instance TypeCastFalse a a' b => TypeEq a a' b
instance TypeCastTrue  a a' True
instance TypeCastFalse a a' False
  • Does your example actually do any harm anywhere? Could some distant module end up treating an Int as a Char/segfaulting?
Last edited 2 years ago by AntC (previous) (diff)

comment:14 Changed 2 years ago by AntC

hmm curiouser and curiouser. Going back to the O.P., I see this behaviour at both GHC 7.10 and 8.0.1:

  • Take out the instance C Char ...; and f is happy with any type of operand, not necessarily a Maybe.
  • Keep in the instance C Char ...; but give f a signature and again it's happy:

f :: (C Bool [a] [a]) => a -> [a]

  • Keep in the instance C Char ...; give f this signature, and we're back needing Maybe:

f :: (C Bool [a] b) => a -> b

So there is something wrong: why is the C Char ... instance getting tangled up with the C Bool ... instance? The only connection would be checking conformance with FunDeps; but that should be only for validation, not 'type improvement' for function f(?)

Last edited 2 years ago by AntC (previous) (diff)

comment:15 Changed 2 years ago by simonpj

Let me note that the commit in comment:5 added this note

Note [Bogus consistency check]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
In checkFunDeps we check that a new ClsInst is consistent with all the
ClsInsts in the environment.

The bogus aspect is discussed in Trac #10675. Currenty it if the two
types are *contradicatory*, using (isNothing . tcUnifyTys).  But all
the papers say we should check if the two types are *equal* thus
   not (substTys subst rtys1 `eqTypes` substTys subst rtys2)
For now I'm leaving the bogus form because that's the way it has
been for years.

Would someone like to fix the bogus-ness as suggested, and check what, if anything, goes wrong. (See #9210 comment:4 for some possible testsuite failures. Maybe they SHOULD fail.) It'd be worth checking what Hackage libraries build before, but fail to build after. This has been wrong for a long time.

comment:16 in reply to:  15 Changed 2 years ago by AntC

Replying to simonpj:

Thanks Simon. I fear we're in danger of getting two separate issues confused. (I guess that comes with the territory.) On the narrow issue raised in the O.P.:

  • If both instance decls are to be accepted, nevertheless, at sites where the first C Bool instance applies, op True should accept any [alpha] and return exactly type [alpha].
  • Note that the C Bool instance meets the coverage conditions/doesn't need UndecidableInstances.
  • I'm saying: once the instance is selected, GHC should treat that use site as if that's the only instance.
  • So where your O.P. says "As a result [of accepting both instance decls], it'll use both instances for improvement.", I think that's just plain wrong.

I don't see anything in the FDs-via-CHRs paper Definition 6 (or in Mark Jones 2000 paper) to suggest attempting mutual improvement. The Consitency Condition is purely about validating instances.

The bulk of your comment is on the different issue of whether those instances should be accepted together. I'll reply separately.

comment:17 in reply to:  15 Changed 2 years ago by AntC

Replying to simonpj: On the broader issue of should those instances be accepted together

Let me note that the commit in comment:5 added this note

... Currenty [checking] if the two types are *contradicatory*,
 using (isNothing . tcUnifyTys).  But all the papers say
we should check if the two types are *equal* thus ...

Thank you. So that confirms my suspicion in comment:11, bullet 3.

For now I'm leaving the bogus form because that's the way it has
been for years.

Yes I think that's wise, given how many fragile programs are out there using FunDeps and overlaps.

Would someone like to fix the bogus-ness as suggested, and check what, if anything, goes wrong.

I'm keen to help, but lack the resources or expertise.

It'd be worth checking what Hackage libraries build before, but fail to build after.

I would guess that any library using type-level programming switches on UndecidableInstances by default, whether or not it actually needs it.

(... Maybe they SHOULD fail.) This has been wrong for a long time.

Given the howls every time GHC tries to apply the FunDep rules more strictly; and given how long a time it's been wrong; I wonder if there's a softly-softly strategy?

  • Move from module-wide UndecidableInstances to a per-instance {-# UNDECIDABLE #-} pragma. (Same idea as with {-# OVERLAP* #-}.)
  • The Coverage Condition is defined in terms of checks on each instance alone, so it's just more closely targetting the logic.
  • Being in the instance gives a more in-your-face signal that this instance is suspicious -- essentially the programmer is acknowledging GHC can't necessarily enforce the Consistency Condition.
  • And I suspect a large proportion of instances do obey the Coverage Conditions.

Could we go further to a per-parameter-per-instance flag?

  • The idiom I see is there's a bare type var in the instance decl, for the target of the FunDep. The type var doesn't appear elsewhere in the head, so it's breaking the Coverage Condition. But there's an equality constraint on it, where the improved type would meet the Coverage Condition. Like:
    instance (b ~ False) => TTypeEq a a' b    -- breaks Coverage, compare:
    instance                TTypeEq a a' False  -- Coverage OK
    
  • The reason for the bare type var is to ensure this instance is {-# OVERLAPPABLE #-}; and a more specific instance will override it.

With {-# LANGUAGE IrrefutableInstanceParams #-} (or some equally ugly name), you can go:

instance TTypeEq a a' ~False   -- tilde prefix ? maybe too subtle

This:

  1. Is syntactic sugar for the form with Equality constraint, for a fresh-generated type var.
  2. Means the compiler can validate the Coverage Condition, so this doesn't need {-# UNDECIDABLE #-}.
  3. Lets the dog see the rabbit: the compiler can check the Consistency Condition.

[To bikeshed about syntax, it's pleasing ~ is already the prefix for irrefutable pattern matches, and the operator for type Equality constraints. It appearing within the instance head is currently illegal syntax; but I guess with a very badly formed head, it might be confused with a type operator(?)]

Last edited 2 years ago by AntC (previous) (diff)

comment:18 Changed 2 years ago by rwbarton

Well let's please not continue using the word "undecidable" to have anything to do with the coverage conditions. I can't imagine it was originally anything but an oversight to have UndecidableInstances completely disable the coverage conditions. UndecidableInstances is supposed to be just about termination of instance search.

comment:19 in reply to:  description Changed 17 months ago by AntC

Replying to simonpj:

Should these two instance declarations be accepted?

  • I'm going to argue they should
  • In addition to the bogusness documented on this ticket, there's a design weakness in the FunDep consistency check.
  • Exploiting that with malice aforethought, there's some disturbing behaviour

Argument to accept: Yes GHC's consistency check is bogus/contrary to all the literature. But it's been in place since at least 2004. Lot's of code relies on it. So we can provide no grounds to reject the instances, unless we can look also at other class params not involved in the FunDep. But then according to the Type Families work, a FunDep should be equivalent to a superclass equi constraint with a Type Family call. I.e.

class C x a b | a -> b where             -- O.P.
class (F a ~ b) => C x a b where         -- Type Family F

The Type Family can look only at the class's second parameter. The (weird) unification behaviour described in the O.P. is in effect trying to reverse engineer F's equations from the class instances. So ghc must unify. OTOH there's no definition for F you could write that would be consistent with where ghc ends up in the type for function f.

Design weakness: in ghc checking instances for FunDep consistency is that it only checks (and unifies) pairwise. It doesn't check all instances globally. Then arguably Definition 6 (Consistency Condition) in the FunDeps via CHRs paper is too weak. (Note that the definition of Functional Dependency in database theory quantifies across all rows in a table.)

Disturbing behaviour: consider this exploit

{-# LANGUAGE as per O.P. #-}

class C x a b | a -> b where          -- as O.P.
   op :: x -> a -> b
instance C Bool [x] (x, Bool)
instance C Char x y => C Char [x] (Int, y)
instance C Char x y => C Char [x] (y, y)

f x = op True [x]                     -- as O.P.

Quick: what type inferred for f? What odds would you lay it's f :: Int -> (Int, Int)?

Luckily we can't actually call f: Couldn't match type 'Bool' with 'Int'. So the True parameter to op in f's rhs is trying to pick the 'right' instance for C.

More disturbingly, if you switch round the order of instances, you'll get a different inferred type for f: it's the unifier of whichever are the last two instances. (Full disclosure: this is at ghc 8.0.1. Sensitivity to ordering of instances sounds like #9210, but that seems to have gone away at 8.0.)

The fix in all these examples is to make the FunDep full (which it really should be)

class C x a b | x a -> b where

comment:20 Changed 14 months ago by AntC

There's two reasons (at least) by which the OP program should be rejected (going by the FDs through CHRs paper):

  1. GHC's Fundep consistency check is bogus, as comment:15 explains.
  2. The FD is non-full. Paper section 6.1/Definition 13/Theorem 2 (Liberal-FD confluence).

For non-full FDs, section 6.2 says to 'project' the FD on to a superclass constraint, and 'project' the class's instances:

class (C_FD a b) => C x a b where               -- no FD here, it's in the constraint
  op :: x -> a -> b

class C_FD a b | a -> b

instance C_FD [x] [x]
instance C Char x y => C_FD [x] [Maybe y]       -- luckily we can take the context from C's instance

Now we can see those instances for C_FD overlap (another no-no for the paper). Furthermore there's no substitution ordering.

The paper (Fig. 2) says to derive CHRs from all instances and solve to a consistent and confluent set of rules.

So (after we've held our noses and looked the other way as we breach the rules) type improvement ends up unifying the C_FD instances.

In particular, Fig. 2 applies from the class decl and instance decls alone. It doesn't wait to see whether/where instances apply.

What I can't explain is why the same doesn't apply for the TTypeEq example comment:9. (The Fig. 2 process incorporates any constraints from instances.) For this ticket it must be that it's breaking 2 rules.

I agree with the comment:15 sentiment that "This has been wrong for a long time."/by implication 'fixing' it to reject such programs will break stuff. Then I suggest two warnings:

  • -Wfundep-consistency-bogus where after applying the unifying substitution between instances, the types are not equal but merely unifiable. (Reported against an instance, as per the current consistency check -- if contradictory, reject the instances, as currently.)
  • -Wfundep-nonfull-noncovered where a FunDep is non-full and there is no class constraint covering just the tyvars for the FunDep. (Reported against the class decl. Hmm hmm needs checking whether the constraining class has a FunDep of the right cover.)

Note BTW the paper (section 6.3) has some fancy footwork for 'multi-range FDs':

class D1 x a b | a -> b x  where ...             -- counts as full, and equivalent to

class D2 x a b | a -> b, a -> x  where ...       -- this

class D3 x a b | a -> b, b -> x  where ...       -- and/or this

"There are in fact also cases where we can transform single-range FDs into equivalent multi-range FDs. This has the advantage that non-full single-range FDs become full multi-range FDs and then we can apply the results from Section 6.1."

Definition 5 (Basic Conditions) apply at all times:

  • "The instance declarations must not overlap."

comment:21 Changed 11 months ago by AntC

Applying the suggested rules here

  • The instances on the O.P. get rejected as inconsistent under the FunDep, because

A) Upon unifying the a parameter positions (argument to the FunDep),

applying the substitution to the b position does not give equal type for the result.

B) i) The FunDep is not full.

ii) The instance heads overall are in no substitution ordering (they're apart).

If you insist on those instances then perhaps B) i) could be relaxed, so that you go either (using current GHC to infer the types for f)

instance C Bool [x] [x]                                     -- per O.P.

instance {-# OVERLAPPABLE #-} C' x a b => C x a b  where    -- catch-all
  op = op'

class C' x a b  | a -> b  where
  op' :: x -> a -> b
instance C Char x y => C' Char [x] [Maybe y]                -- per O.P. but indirect

f x = op True [x]                                           -- per O.P.
-- inferred ===> f :: C Bool [a] [a] => a -> [a]

or

instance C Char x y => C Char [x] [Maybe y]                 -- per O.P.

instance {-# OVERLAPPABLE #-} C'' x a b => C x a b  where   -- catch-all
  op = op''

class C'' x a b  | a -> b  where
  op'' :: x -> a -> b
instance C'' Bool [x] [x]                                   -- per O.P. but indirect

f x = op True [x]                                           -- per O.P.
-- inferred ===> f :: a -> [a]

Last edited 11 months ago by AntC (previous) (diff)

comment:22 Changed 9 months ago by osa1

Cc: osa1 removed
Note: See TracTickets for help on using tickets.