Non-confluence in the solver
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.)