GHC issueshttps://gitlab.haskell.org/ghc/ghc/-/issues2023-08-07T22:30:08Zhttps://gitlab.haskell.org/ghc/ghc/-/issues/16560Documentation: alleged UndecidableInstances loopiness doesn't loop2023-08-07T22:30:08ZAnthony 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#undecidable-instances) that is alleged "would make the typechecker loop", doesn'...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#undecidable-instances) 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/18851Non-confluence in the solver2022-09-06T11:40:53ZRichard Eisenbergrae@richarde.devNon-confluence in the solverIn #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 ex...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. (EDIT: Furthermore, more hammering in this direction discovered non-confluence even *without* functional dependencies. See https://gitlab.haskell.org/ghc/ghc/-/issues/18851#note_318471.)
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 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](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/19126Dubious FunDep behaviour, even for a 'textbook' example with non dodgy extens...2021-02-16T20:34:27ZAnthony ClaydenDubious FunDep behaviour, even for a 'textbook' example with non dodgy extensions## Summary
GHC's behaviour for a 'textbook' FunDep instance (without the known-to-be-dodgy extensions) is not as per the theory in the 'FunDeps via CHRs' 2006 paper.
In itself this is not problematic; there's an easy workaround; indeed...## Summary
GHC's behaviour for a 'textbook' FunDep instance (without the known-to-be-dodgy extensions) is not as per the theory in the 'FunDeps via CHRs' 2006 paper.
In itself this is not problematic; there's an easy workaround; indeed FunDepers probably take it 'this is how GHC works'. But the workaround needs `UndecidableInstances`, which removes any confidence about confluence and termination across all instances in the module.
(I'm documenting this in context of a whirl of recent issues #18759, #18851 and ref [this comment](https://github.com/ghc-proposals/ghc-proposals/pull/374#issuecomment-750491151) on a github proposal.)
## Steps to reproduce
Consider this classic textbook FunDep, from the Jones 2000 paper
{-# LANGUAGE MultiParamTypeClasses, FunctionalDependencies, FlexibleInstances, FlexibleContexts #-}
class Collects e ce | ce -> e where
member :: e -> ce -> Bool
-- etc
instance Eq e => Collects e [e] where
member = elem
x1 = member True [False, False, True] -- ===> True
x2 = member undefined ([] :: [Bool]) -- ===> False
The FunDeps via CHRs paper [Section 4.2/Fig 2 translation rules] says that instance should be equivalent to this:
{-# LANGUAGE UndecidableInstances, GADTs #-}
class CollectF2 e ce | ce -> e where
memberF2 :: e -> ce -> Bool
instance (a ~ e, Eq e) => CollectF2 a [e] where
memberF2 = elem
Using `~` constraint to explicitly apply the type improvement (needs `GADTs`), and bare tyvar `a` in the instance head as target for the improvement (needs `UndecidableInstances`).
## Expected behavior
This instance and its non-confluent consequence should be rejected:
instance {-# OVERLAPPABLE #-} (a ~ ()) => Collects a [e] where
member _ _ = False
x3 = member () [False, False, True] -- ===> False
Compare:
instance {-# OVERLAPPABLE #-} (a ~ ()) => CollectF2 a [e] where
memberF2 _ _ = False
-- error: Duplicate instance declarations:
Best practice for using FunDeps (see examples cited in the github comments) is to use instance heads in a style per `CollectF2` with a bare fresh tyvar as the target. This needs `UndecidableInstances` even though the type improvement via `~` is perfectly decidable. That extension is module-wide, and allows exactly the non-confluence with that `instance (a ~ ()) => Collects a [e]` it was seeking to avoid. FunDepers must be disciplined in how they write instances.
## Environment
* GHC version used: 8.10.2
Optional:
* Operating System: Windows 8
* System Architecture:https://gitlab.haskell.org/ghc/ghc/-/issues/181298.10: Overlapping instances claimed where there are none (or crash in 8.8)2020-07-01T16: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 `generics-sop`),
either sends GHC into endless allocation loop (8.8),
or produces a self-contradictory error message:
```haskell
{-# LANGUAGE AllowAmbiguousTypes #-}
{-...## Summary
The following snippet (some of the code coming from `generics-sop`),
either sends GHC into endless allocation loop (8.8),
or produces a self-contradictory 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, `generics-sop` 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`:
```
[nix-shell:~/lift]$ ghc ~/ghc-instance-self-overlapping[ghc-instance-self-overlapping.hs](/uploads/adca7101458489bc35d16ceaf00af943/ghc-instance-self-overlapping.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:15-18
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/13061Incorrect constraints given single flexible undecidable instance.2019-07-07T18: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 #-...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.