GHC issueshttps://gitlab.haskell.org/ghc/ghc//issues20201109T13:52:11Zhttps://gitlab.haskell.org/ghc/ghc//issues/18851Nonconfluence around functional dependencies20201109T13:52:11ZRichard Eisenbergrae@richarde.devNonconfluence around functional dependenciesIn #18759 (starting at https://gitlab.haskell.org/ghc/ghc//issues/18759#note_306441 and then refined in https://gitlab.haskell.org/ghc/ghc//issues/18759#note_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 https://gitlab.haskell.org/ghc/ghc//issues/18759#note_307486, @simonpj asks whether these techniques can disrupt confluence.
They can.
Here is the example:
```hs
{# 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 nonconfluence.
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 nonconfluence!)
What to do? I think the next step is to compare this to the [constrainthandling rules paper](https://www.researchgate.net/profile/Martin_Sulzmann/publication/213885702_Understanding_Functional_Dependencies_via_Constraint_Handling_Rules/links/09e41511297969891f000000.pdf), 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.)In #18759 (starting at https://gitlab.haskell.org/ghc/ghc//issues/18759#note_306441 and then refined in https://gitlab.haskell.org/ghc/ghc//issues/18759#note_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 https://gitlab.haskell.org/ghc/ghc//issues/18759#note_307486, @simonpj asks whether these techniques can disrupt confluence.
They can.
Here is the example:
```hs
{# 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 nonconfluence.
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 nonconfluence!)
What to do? I think the next step is to compare this to the [constrainthandling rules paper](https://www.researchgate.net/profile/Martin_Sulzmann/publication/213885702_Understanding_Functional_Dependencies_via_Constraint_Handling_Rules/links/09e41511297969891f000000.pdf), 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.)https://gitlab.haskell.org/ghc/ghc//issues/181298.10: Overlapping instances claimed where there are none (or crash in 8.8)20200701T16:47:56ZSerge Kosyrev8.10: Overlapping instances claimed where there are none (or crash in 8.8)## Summary
The following snippet (some of the code coming from `genericssop`),
either sends GHC into endless allocation loop (8.8),
or produces a selfcontradictory error message:
```haskell
{# LANGUAGE AllowAmbiguousTypes #}
{# LANGUAGE DataKinds #}
{# LANGUAGE FlexibleInstances #}
{# LANGUAGE GADTs #}
{# LANGUAGE KindSignatures #}
{# LANGUAGE PolyKinds #}
{# LANGUAGE RankNTypes #}
{# LANGUAGE TypeFamilies #}
{# LANGUAGE ConstraintKinds #}
{# LANGUAGE FlexibleContexts #}
{# LANGUAGE MultiParamTypeClasses #}
{# LANGUAGE TypeOperators #}
{# LANGUAGE UndecidableInstances #}
{# LANGUAGE UndecidableSuperClasses #}
import Data.Kind (Constraint)
import Data.Proxy (Proxy)
import Data.Typeable (Typeable)
 First, `genericssop` code, intact.

type family
AllF (c :: k > Constraint) (xs :: [k]) :: Constraint where
AllF _c '[] = ()
AllF c (x ': xs) = (c x, All c xs)
class (AllF c xs, SListI xs) => All (c :: k > Constraint) (xs :: [k])
instance All c '[]
instance (c x, All c xs) => All c (x ': xs) where
class Top x
instance Top x
type SListI = All Top
 Next, user code, minimised.

data GADT
= forall (xs :: [*]) (a :: *)
. (Top a, All Typeable xs)
=> GADT
withSomePipe'
:: GADT
> (forall (xs :: [*])
. (Proxy xs > GADT)
> GADT)
> GADT
withSomePipe' GADT f = f (const GADT)
```
8.10.1 says there are overlapping instances, but only lists one,
which isn't terribly surprising, as there is indeed just one instance for `Top`:
```
[nixshell:~/lift]$ ghc ~/ghcinstanceselfoverlapping[ghcinstanceselfoverlapping.hs](/uploads/adca7101458489bc35d16ceaf00af943/ghcinstanceselfoverlapping.hs).hs
[1 of 1] Compiling Main ( /home/desktop/repro.hs, /home/desktop/repro.o )
/home/desktop/repro.hs:1:1: error:
The IO action `main' is not defined in module `Main'

1  {# LANGUAGE AllowAmbiguousTypes #}
 ^
/home/desktop/repro.hs:45:33: error:
* Overlapping instances for Top a0 arising from a use of `GADT'
Matching givens (or their superclasses):
Top a
bound by a pattern with constructor:
GADT :: forall (xs :: [*]) a. (Top a, All Typeable xs) => GADT,
in an equation for withSomePipe'
at /home/desktop/repro.hs:45:1518
Matching instances:
instance forall k (x :: k). Top x
 Defined at /home/desktop/repro.hs:30:10
(The choice depends on the instantiation of `a0')
* In the first argument of `const', namely `GADT'
In the first argument of `f', namely `(const GADT)'
In the expression: f (const GADT)

45  withSomePipe' GADT f = f (const GADT)
```
## Steps to reproduce
With either ghc 8.10.1 or ghc 8.8.3:
ghc repro.hs
## Expected behavior
The compiler shouldn't contradict itself in the error message, and it certainly needn't crash,
although the latter part was fixed in the new release.
## Environment
* GHC version used: 8.8.3 / 8.10.1
Optional:
* Operating System:
* System Architecture:## Summary
The following snippet (some of the code coming from `genericssop`),
either sends GHC into endless allocation loop (8.8),
or produces a selfcontradictory error message:
```haskell
{# LANGUAGE AllowAmbiguousTypes #}
{# LANGUAGE DataKinds #}
{# LANGUAGE FlexibleInstances #}
{# LANGUAGE GADTs #}
{# LANGUAGE KindSignatures #}
{# LANGUAGE PolyKinds #}
{# LANGUAGE RankNTypes #}
{# LANGUAGE TypeFamilies #}
{# LANGUAGE ConstraintKinds #}
{# LANGUAGE FlexibleContexts #}
{# LANGUAGE MultiParamTypeClasses #}
{# LANGUAGE TypeOperators #}
{# LANGUAGE UndecidableInstances #}
{# LANGUAGE UndecidableSuperClasses #}
import Data.Kind (Constraint)
import Data.Proxy (Proxy)
import Data.Typeable (Typeable)
 First, `genericssop` code, intact.

type family
AllF (c :: k > Constraint) (xs :: [k]) :: Constraint where
AllF _c '[] = ()
AllF c (x ': xs) = (c x, All c xs)
class (AllF c xs, SListI xs) => All (c :: k > Constraint) (xs :: [k])
instance All c '[]
instance (c x, All c xs) => All c (x ': xs) where
class Top x
instance Top x
type SListI = All Top
 Next, user code, minimised.

data GADT
= forall (xs :: [*]) (a :: *)
. (Top a, All Typeable xs)
=> GADT
withSomePipe'
:: GADT
> (forall (xs :: [*])
. (Proxy xs > GADT)
> GADT)
> GADT
withSomePipe' GADT f = f (const GADT)
```
8.10.1 says there are overlapping instances, but only lists one,
which isn't terribly surprising, as there is indeed just one instance for `Top`:
```
[nixshell:~/lift]$ ghc ~/ghcinstanceselfoverlapping[ghcinstanceselfoverlapping.hs](/uploads/adca7101458489bc35d16ceaf00af943/ghcinstanceselfoverlapping.hs).hs
[1 of 1] Compiling Main ( /home/desktop/repro.hs, /home/desktop/repro.o )
/home/desktop/repro.hs:1:1: error:
The IO action `main' is not defined in module `Main'

1  {# LANGUAGE AllowAmbiguousTypes #}
 ^
/home/desktop/repro.hs:45:33: error:
* Overlapping instances for Top a0 arising from a use of `GADT'
Matching givens (or their superclasses):
Top a
bound by a pattern with constructor:
GADT :: forall (xs :: [*]) a. (Top a, All Typeable xs) => GADT,
in an equation for withSomePipe'
at /home/desktop/repro.hs:45:1518
Matching instances:
instance forall k (x :: k). Top x
 Defined at /home/desktop/repro.hs:30:10
(The choice depends on the instantiation of `a0')
* In the first argument of `const', namely `GADT'
In the first argument of `f', namely `(const GADT)'
In the expression: f (const GADT)

45  withSomePipe' GADT f = f (const GADT)
```
## Steps to reproduce
With either ghc 8.10.1 or ghc 8.8.3:
ghc repro.hs
## Expected behavior
The compiler shouldn't contradict itself in the error message, and it certainly needn't crash,
although the latter part was fixed in the new release.
## Environment
* GHC version used: 8.8.3 / 8.10.1
Optional:
* Operating System:
* System Architecture:https://gitlab.haskell.org/ghc/ghc//issues/16560Documentation: alleged UndecidableInstances loopiness doesn't loop20190425T09:34:24ZAnthony ClaydenDocumentation: alleged UndecidableInstances loopiness doesn't loopThe example code in the User Guide for [the UndecidableInstances extension](https://downloads.haskell.org/~ghc/8.6.4/docs/html/users_guide/glasgow_exts.html#undecidableinstances) that is alleged "would make the typechecker loop", doesn't:
> class D a
> class F a b  a>b
> instance F [a] [[a]]
> instance (D c, F a c) => D [a]  'c' is not mentioned in the head
That is with
fD :: (D x, Show x) => x > String
fD x = show x
y = fD [[()]]
The constraint checking from wanted `D [[()]]` to `F [()] c` strips away one `[ ]`. The improvement `F [()] [[()]]` puts it back. Presumably the `D c` constraint i.e. `D [[()]]` says: oh, I've already seen a wanted like that, no need to check it again. (Perhaps it didn't used to be so smart.)
Change that `D` instance to this, and the typechecker does loop
instance (D c, F [a] c) => D [a]
GHC 8.6.4 on Windows architecture.
(The other example discussed there, with the "somewhat strange" definition using `.*.` does indeed cause loopiness.)
P.S. might it be an idea to offer a documentation template? The 'bug' template didn't seem to apply. I've put a 'documentation' Label.The example code in the User Guide for [the UndecidableInstances extension](https://downloads.haskell.org/~ghc/8.6.4/docs/html/users_guide/glasgow_exts.html#undecidableinstances) that is alleged "would make the typechecker loop", doesn't:
> class D a
> class F a b  a>b
> instance F [a] [[a]]
> instance (D c, F a c) => D [a]  'c' is not mentioned in the head
That is with
fD :: (D x, Show x) => x > String
fD x = show x
y = fD [[()]]
The constraint checking from wanted `D [[()]]` to `F [()] c` strips away one `[ ]`. The improvement `F [()] [[()]]` puts it back. Presumably the `D c` constraint i.e. `D [[()]]` says: oh, I've already seen a wanted like that, no need to check it again. (Perhaps it didn't used to be so smart.)
Change that `D` instance to this, and the typechecker does loop
instance (D c, F [a] c) => D [a]
GHC 8.6.4 on Windows architecture.
(The other example discussed there, with the "somewhat strange" definition using `.*.` does indeed cause loopiness.)
P.S. might it be an idea to offer a documentation template? The 'bug' template didn't seem to apply. I've put a 'documentation' Label.https://gitlab.haskell.org/ghc/ghc//issues/13061Incorrect constraints given single flexible undecidable instance.20190707T18:23:53ZJCarrIncorrect constraints given single flexible undecidable instance.If a class has an instance in the form F a =\> G a in its file, and no other instances, then the functions in G a will have the constraint F a, rather than G a.
Example file
```hs
{# LANGUAGE FlexibleInstances, UndecidableInstances #}
class A a where
f :: a > a
instance {# OVERLAPPABLE #} Eq a => A a where
f = id
```
f will have type Eq a =\> a \> a \> Bool.
Consider the functions
```hs
g, h, i :: A a => a > a
g = f
h = let f' = f in f
i = f' where
f' = f
```
h and i will both fail to typecheck.
If we add:
```hs
instance A Int where
f = id
```
Then f will have the correct type A a =\> a \> a \> Bool.If a class has an instance in the form F a =\> G a in its file, and no other instances, then the functions in G a will have the constraint F a, rather than G a.
Example file
```hs
{# LANGUAGE FlexibleInstances, UndecidableInstances #}
class A a where
f :: a > a
instance {# OVERLAPPABLE #} Eq a => A a where
f = id
```
f will have type Eq a =\> a \> a \> Bool.
Consider the functions
```hs
g, h, i :: A a => a > a
g = f
h = let f' = f in f
i = f' where
f' = f
```
h and i will both fail to typecheck.
If we add:
```hs
instance A Int where
f = id
```
Then f will have the correct type A a =\> a \> a \> Bool.