GitLab

In #18759 (starting at #18759 (comment 306441) and then refined in #18759 (comment 306722), but you don't need to read that ticket to understand this one), we explored various ways of disabling the coverage condition for functional dependencies. In #18759 (comment 307486), @simonpj asks whether these techniques can disrupt confluence.

They can. (EDIT: Furthermore, more hammering in this direction discovered non-confluence even without functional dependencies. See #18851 (comment 318471).)

Here is the example:

{-# LANGUAGE FunctionalDependencies, FlexibleInstances, UndecidableInstances,
             ScopedTypeVariables, TypeFamilies, TypeApplications,
             FlexibleContexts, AllowAmbiguousTypes #-}

module Bug where

class C a b | a -> b
instance C Int b => C Int b

class IsInt int
instance int ~ Int => IsInt int

data A
instance Show A where
  show _ = "A"
data B
instance Show B where
  show _ = "B"

f :: forall a b c int. (Show a, Show b, Show c, C int a, C int b, C int c, IsInt int) => String
f = show (undefined :: c)

g = f @A @B

g evaluates to "B". If I switch the order of the C int a and C int b constraints in the type of f, g will evaluate to "A". Urgh.

(Sidenote: this file needs AllowAmbiguousTypes, but there are no ambiguous types here. That bug is reported as #18850.)

What's going on? When calling f from g, GHC needs to figure out how to instantiate the type variables a, b, c, and int, and GHC must find dictionaries to supply for all the class constraints. First, GHC creates unification variables a0, b0, c0, and int0. The type applications tell us a0 := A and b0 := B. Good. Then we have these constraints:

[W] w1 : Show A
[W] w2 : Show B
[W] w3 : Show c0
[W] w4 : C int0 A
[W] w5 : C int0 B
[W] w6 : C int0 c0
[W] w7 : IsInt int0

GHC processes these in the order given. w1 and w2 are easily despatched. w3 doesn't make any progress at all. Neither does w4 or w5. So we're then in this state:

worklist: [W] w6 : C int0 c0
          [W] w7 : IsInt int0
inerts: [W] w3 : Show c0
        [W] w4 : C int0 A
        [W] w5 : C int0 B

We then look at w6. It doesn't make progress. But then GHC looks at the inerts, and sees that w4 and w5 have the same first argument to C (int0) as the work item w6. Because of the functional dependency on C, this means that c0 must match the second argument to C in the inert. The problem is that there are two such inerts! GHC chooses the last one, arbitrarily. Thus, we get c0 := B and carry on. If the constraints were processed in a different order, we'd end up with c0 := A. This is classic non-confluence.

Why have IsInt here? It's to slow down GHC. If we just wrote an explicit Int in the type signature for f, then GHC would eagerly solve w4' : C Int A and w5' : C Int B. When processing w6' : C Int c0, GHC wouldn't have any inerts to look at. Instead, it would look at the instance for C, which is unhelpful in this case. Indeed, moving the IsInt int constraint earlier (before the C constraints) in f's type signature causes GHC to error, as it doesn't know how to instantiate c0, having lost the hints from the inerts. (More non-confluence!)

What to do? I think the next step is to compare this to the constraint-handling rules paper, which proves confluence, and see whether that paper has a mistake, or where GHC violates an assumption in that paper. (Probably the latter: my instance for C is very naughty.)