GHC issueshttps://gitlab.haskell.org/ghc/ghc/-/issues2022-02-24T11:31:39Zhttps://gitlab.haskell.org/ghc/ghc/-/issues/20071Overlapping instances mentioning constructor-bound type variables give no error2022-02-24T11:31:39Zaadaa-fgtaaOverlapping instances mentioning constructor-bound type variables give no error## Summary
Constraints mentioning type variable bound by data constructor are solved even when they trigger overlapping instances.
## Steps to reproduce
```haskell
{-# LANGUAGE FlexibleInstances, ExistentialQuantification #-}
module ...## Summary
Constraints mentioning type variable bound by data constructor are solved even when they trigger overlapping instances.
## Steps to reproduce
```haskell
{-# LANGUAGE FlexibleInstances, ExistentialQuantification #-}
module Bug where
import Data.Proxy
class Foo x where
x :: Proxy x -> String
instance Foo Int where
x _ = "Int"
instance Foo a where
x _ = "-"
data SomeProxy = forall x . SomeProxy (Proxy x)
foo :: SomeProxy -> String
foo (SomeProxy p) = x p
```
This code compiles without an error, although `Foo Int` and `Foo a` are obviously overlapping. Encoding existential type via universal quantification fails as expected
```haskell
bar :: ((forall x . Proxy x -> String) -> String) -> String
bar f = f x
```
```
• Overlapping instances for Foo x arising from a use of ‘x’
Matching instances:
instance Foo a -- Defined at Bug.hs:15:10
instance Foo Int -- Defined at Bug.hs:12:10
(The choice depends on the instantiation of ‘x’
To pick the first instance above, use IncoherentInstances
when compiling the other instance declarations)
```
## Expected behavior
Compiling `foo` gives the same error as `bar`.
## Environment
* GHC version used: 8.10.4, 9.0.1, 9.3.20210504
* Operating System: Linux (NixOS)
* System Architecture: x86-64https://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/18850Instance/given overlap trips up the ambiguity check2020-10-29T19:00:42ZRichard Eisenbergrae@richarde.devInstance/given overlap trips up the ambiguity checkThursday is a good day to abuse GHC. So I said this:
```hs
{-# LANGUAGE TypeFamilies, FlexibleInstances #-}
module Bug where
class IsBool bool
instance bool ~ Bool => IsBool bool
class C a
instance C Bool
f :: (C bool, IsBool bool) ...Thursday is a good day to abuse GHC. So I said this:
```hs
{-# LANGUAGE TypeFamilies, FlexibleInstances #-}
module Bug where
class IsBool bool
instance bool ~ Bool => IsBool bool
class C a
instance C Bool
f :: (C bool, IsBool bool) => ()
f = ()
```
To me, `f`'s type is unambiguous: the `IsBool bool` constraint fixes the type variable `bool` to be `Bool`. But GHC says
```
/Users/rae/temp/Bug2.hs:11:6: error:
• Could not deduce (C bool0)
from the context: (C bool, IsBool bool)
bound by the type signature for:
f :: forall bool. (C bool, IsBool bool) => ()
at /Users/rae/temp/Bug2.hs:11:6-32
The type variable ‘bool0’ is ambiguous
• In the ambiguity check for ‘f’
To defer the ambiguity check to use sites, enable AllowAmbiguousTypes
In the type signature: f :: (C bool, IsBool bool) => ()
|
11 | f :: (C bool, IsBool bool) => ()
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^
```
But maybe I'm wrong. Is the type really ambiguous? No. When I say
```hs
{-# LANGUAGE TypeFamilies, FlexibleInstances, AllowAmbiguousTypes #-}
module Bug where
class IsBool bool
instance bool ~ Bool => IsBool bool
class C a
instance C Bool
f :: (C bool, IsBool bool) => ()
f = ()
g = f
```
my program is accepted. I've added `AllowAmbiguousTypes` and the binding `g = f`. That binding is accepted -- no type applications or other funny business. This suggests that `f`'s type is not actually ambiguous.
What's going on is an over-eager instance/given overlap; see `Note [Instance and Given overlap]` in `GHC.Tc.Solver.Interact`. That Note ends with
```
All of this is disgustingly delicate, so to discourage people from writing
simplifiable class givens, we warn about signatures that contain them;
see GHC.Tc.Validity Note [Simplifiable given constraints].
```
But I don't get the warning! Even in my second program, which is error-free. Hunting further into `GHC.Tc.Validity`, I find this code:
```hs
checkSimplifiableClassConstraint env dflags ctxt cls tys
| not (wopt Opt_WarnSimplifiableClassConstraints dflags)
= return ()
| xopt LangExt.MonoLocalBinds dflags
= return ()
| ...
```
where the `...` includes generating a warning. Of course, I *do* have `-XMonoLocalBinds`, as implied by `-XTypeFamilies`. What happens when I disable this (with an explicit `-XNoMonoLocalBinds`)?
```
/Users/rae/temp/Bug2.hs:11:6: warning: [-Wsimplifiable-class-constraints]
• The constraint ‘IsBool bool’ matches
instance (bool ~ Bool) => IsBool bool
-- Defined at /Users/rae/temp/Bug2.hs:6:10
This makes type inference for inner bindings fragile;
either use MonoLocalBinds, or simplify it using the instance
• In the type signature: f :: (C bool, IsBool bool) => ()
|
11 | f :: (C bool, IsBool bool) => ()
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^
```
Good. The warning fires.
My conclusions:
1. My first program really ought to be accepted. The type is not ambiguous. I'm willing to concede this point to "disgustingly delicate", though, if we don't see an easy way to fix.
2. It looks the warning should fire even when `-XMonoLocalBinds` is in effect. My program has no local generalization involved. How would users disable the warnings? By not writing a simplifiable Given.https://gitlab.haskell.org/ghc/ghc/-/issues/18836GHC does not reject overlapping instances2020-11-09T14:01:37ZdminuosoGHC does not reject overlapping instancesThis example was mentioned on the mailing list by Daniel Díaz at https://mail.haskell.org/pipermail/haskell-cafe/2020-October/132815.html
GHC does not reject this program:
```haskell
{-# LANGUAGE FlexibleInstances #-}
newtype Foo = Foo...This example was mentioned on the mailing list by Daniel Díaz at https://mail.haskell.org/pipermail/haskell-cafe/2020-October/132815.html
GHC does not reject this program:
```haskell
{-# LANGUAGE FlexibleInstances #-}
newtype Foo = Foo Int
instance {-# OVERLAPS #-} Show (Maybe Foo) where
show _ = "foo"
newtype W a = W (Maybe a)
instance Show a => Show (W a) where
show (W a) = show a -- This should not be allowed. Which `Show (Maybe a)` should be used?
foo :: Show a => W a -> String
foo a = show a
main :: IO ()
main = pure ()
```
There's two overlapping instances here:
```haskell
instance Show a => Show (Maybe a) -- Defined in ‘GHC.Show’
instance [overlap ok] Show (Maybe Foo) -- Defined at ex1.hs:3:27
```
If we tried to solve for `Show (Maybe a)` a different way, GHC complains as it should:
```haskell
foo' :: Show a => Maybe a -> String
foo' a = show a
```
```
ex1.hs:6:8: error:
• Overlapping instances for Show (Maybe a)
arising from a use of ‘show’
Matching instances:
instance Show a => Show (Maybe a) -- Defined in ‘GHC.Show’
instance [overlap ok] Show (Maybe Foo) -- Defined at ex1.hs:3:27
(The choice depends on the instantiation of ‘a’
To pick the first instance above, use IncoherentInstances
when compiling the other instance declarations)
• In the expression: show
In an equation for ‘foo'’: foo' = show
|
6 | foo' = show
```
It seems to me, that one of two things must be true:
- The algorithm described in https://downloads.haskell.org/~ghc/latest/docs/html/users_guide/glasgow_exts.html#overlapping-instances is incorrect and the algorithm behaves differently for instance selection inside instances.
- GHC makes an incoherent instance selection herehttps://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/17765Documentation for FunctionalDependencies is misleading/incomplete (and their ...2020-02-20T16:51:39ZJakob BrünkerDocumentation for FunctionalDependencies is misleading/incomplete (and their behavior confusing) wrt overlapping instances## Summary
The GHC user's guide mentions in *9.8.2.2.2. Adding functional dependencies*, for `class D a b | a -> b where ...`:
> The compiler, on the other hand, is responsible for ensuring that the set of instances that are in scope a...## Summary
The GHC user's guide mentions in *9.8.2.2.2. Adding functional dependencies*, for `class D a b | a -> b where ...`:
> The compiler, on the other hand, is responsible for ensuring that the set of instances that are in scope at any given point in the program is consistent with any declared dependencies. For example, the following pair of instance declarations cannot appear together in the same scope because they violate the dependency for D, even though either one on its own would be acceptable:
>
> ```haskell
> instance D Bool Int where ...
> instance D Bool Char where ...
> ```
This leaves out what happens when polymorphic types are used in instances, and some of the behavior of functional dependencies in that case is not what I would expect judging by the documentation, but I suspect that they work as intended.
To illustrate:
```haskell
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE FlexibleInstances #-}
module FunDeps where
class C a b | a -> b where
foo :: a -> b
-- It is unclear to me why I can write both of these instances together - it
-- seems as though this should violate the dependency
instance C a a where
foo = id
instance C a () where
foo = const ()
-- understandably not fine, due to Overlapping instances
-- ex0 = foo () :: ()
-- fine
ex1 = foo 'x' :: Char
-- also fine
-- However, the User's guide says "The notation `a -> b` [...] indicates that the `a`
-- parameter uniquely determines the `b` parameter, and might be read as “a determines b.”"
-- From this I would expect that an expression like `foo 'x'` has a uniquely determined
-- type, but evidently, this is not so, since it can have both type `Char` and `()`.
ex2 = foo 'x' :: ()
-- not fine, with confusing error message
-- Why does it expect the argument of `foo` to be of type `()` when, with
-- an annotation, it accepts a `Char` argument?
-- In fact, it looks like it selected the `C a a` instance and from it determined that
-- it needs to solve a `C Char ()` constraint, which seems paradoxical.
-- Naively I would expect GHC to talk about an ambiguous type variable, which
-- is what happens if the functional dependency is removed.
ex3 = foo 'x'
{-
FunDeps.hs:25:7: error:
• Couldn't match type ‘Char’ with ‘()’
arising from a functional dependency between:
constraint ‘C Char ()’ arising from a use of ‘foo’
instance ‘C a a’ at FunDeps.hs:9:10-14
• In the expression: foo 'x'
In an equation for ‘ex3’: ex3 = foo 'x'
|
25 | ex3 = foo 'x'
| ^^^^^^^
-}
```
Another interesting aspect is that entering `() :: C Bool () => ()` in GHCi will produce the exact same warning twice, though I don't know if that's expected behavior:
```haskell
<interactive>:45:7: warning: [-Wsimplifiable-class-constraints]
• The constraint ‘C Bool ()’ matches
instance C a () -- Defined at FunDeps.hs:15:10
This makes type inference for inner bindings fragile;
either use MonoLocalBinds, or simplify it using the instance
• In an expression type signature: C Bool () => ()
In the expression: () :: C Bool () => ()
In an equation for ‘it’: it = () :: C Bool () => ()
<interactive>:45:7: warning: [-Wsimplifiable-class-constraints]
• The constraint ‘C Bool ()’ matches
instance C a () -- Defined at FunDeps.hs:15:10
This makes type inference for inner bindings fragile;
either use MonoLocalBinds, or simplify it using the instance
• In an expression type signature: C Bool () => ()
In the expression: () :: C Bool () => ()
In an equation for ‘it’: it = () :: C Bool () => ()
```
## Environment
* GHC version used: 8.11.0.20200127https://gitlab.haskell.org/ghc/ghc/-/issues/15632Undependable Dependencies2020-10-30T21:05:15ZAntCUndependable DependenciesConsider
```hs
{-# LANGUAGE MultiParamTypeClasses, FunctionalDependencies,
GADTs, FlexibleInstances, FlexibleContexts,
UndecidableInstances #-}
data Hither = Hither deriving (Eq, Show, Read) -- just th...Consider
```hs
{-# LANGUAGE MultiParamTypeClasses, FunctionalDependencies,
GADTs, FlexibleInstances, FlexibleContexts,
UndecidableInstances #-}
data Hither = Hither deriving (Eq, Show, Read) -- just three
data Thither = Thither deriving (Eq, Show, Read) -- distinct
data Yon = Yon deriving (Eq, Show, Read) -- types
class Whither a b | a -> b where
whither :: a -> b -> b
-- instance Whither Int Hither where -- rejected: FunDep conflict
-- whither _ y = y -- with Thither instance, so
instance {-# OVERLAPPING #-} (b ~ Hither) => Whither Int b where
whither _ y = y
instance {-# OVERLAPS #-} Whither a Thither where
whither _ y = y
instance {-# OVERLAPPABLE #-} (b ~ Yon) => Whither a b where
whither _ y = y
f :: Whither Int b => Int -> b -> b
f = whither
g :: Whither Bool b => Bool -> b -> b
g = whither
```
Should those three instances be accepted together? In particular, the published work on FDs (including the FDs through CHRs paper) says the `Thither` instance should behave as if:
```hs
instance (beta ~ Thither) => Whither a beta where ...
```
(in which `beta` is a unification variable and the `~` constraint is type improvement under the FD.) But now the instance head is the same as the `Yon` instance, modulo alpha renaming; with the constraints being contrary.
That's demonstrated by the inferred/improved type for `g`:
```hs
*Whither> :t g
===> g :: Bool -> Thither -> Thither -- and yet
*Whither> g True Yon
===> Yon
```
What do I expect here?
- At least the `Thither` and `Yon` instances to be rejected as inconsistent under the FunDep.
- (The `Hither` instance is also inconsistent, going by the strict interpretation in published work. But GHC's rule here is bogus, as documented in Trac #10675.)
Exploiting Overlapping instances is essential to making this go wrong. The published work shies away from considering `FunDeps + Overlap`; and yet specifying the semantics as if the instances used bare unification variables is almost inevitably going give overlaps -- especially if there are multiple FDs.
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ------------ |
| Version | 8.6.1-beta1 |
| Type | Bug |
| TypeOfFailure | OtherFailure |
| Priority | normal |
| Resolution | Unresolved |
| Component | Compiler |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | #10675 |
| Blocking | |
| CC | |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"Undependable Dependencies","status":"New","operating_system":"","component":"Compiler","related":[10675],"milestone":"8.6.1","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.6.1-beta1","keywords":["FunctionalDependencies,","OverlappingInstances"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"Consider\r\n\r\n{{{#!hs\r\n{-# LANGUAGE MultiParamTypeClasses, FunctionalDependencies,\r\n GADTs, FlexibleInstances, FlexibleContexts,\r\n UndecidableInstances #-}\r\n\r\n\r\ndata Hither = Hither deriving (Eq, Show, Read)\t\t-- just three\r\ndata Thither = Thither deriving (Eq, Show, Read)\t-- distinct\r\ndata Yon = Yon deriving (Eq, Show, Read)\t\t-- types\r\n\r\nclass Whither a b | a -> b where\r\n whither :: a -> b -> b\r\n\r\n-- instance Whither Int Hither where\t-- rejected: FunDep conflict\r\n-- whither _ y = y\t\t\t-- with Thither instance, so\r\n\r\ninstance {-# OVERLAPPING #-} (b ~ Hither) => Whither Int b where\r\n whither _ y = y\r\n\r\ninstance {-# OVERLAPS #-} Whither a Thither where\r\n whither _ y = y\r\ninstance {-# OVERLAPPABLE #-} (b ~ Yon) => Whither a b where\r\n whither _ y = y\r\n\r\nf :: Whither Int b => Int -> b -> b\r\nf = whither\r\n\r\ng :: Whither Bool b => Bool -> b -> b\r\ng = whither\r\n}}}\r\n\r\nShould those three instances be accepted together? In particular, the published work on FDs (including the FDs through CHRs paper) says the `Thither` instance should behave as if:\r\n\r\n{{{#!hs\r\ninstance (beta ~ Thither) => Whither a beta where ...\r\n}}}\r\n(in which `beta` is a unification variable and the `~` constraint is type improvement under the FD.) But now the instance head is the same as the `Yon` instance, modulo alpha renaming; with the constraints being contrary.\r\n\r\nThat's demonstrated by the inferred/improved type for `g`:\r\n\r\n{{{#!hs\r\n*Whither> :t g\r\n===> g :: Bool -> Thither -> Thither -- and yet\r\n\r\n*Whither> g True Yon\r\n===> Yon\r\n}}}\r\n\r\nWhat do I expect here?\r\n* At least the `Thither` and `Yon` instances to be rejected as inconsistent under the FunDep.\r\n* (The `Hither` instance is also inconsistent, going by the strict interpretation in published work. But GHC's rule here is bogus, as documented in Trac #10675.)\r\n\r\nExploiting Overlapping instances is essential to making this go wrong. The published work shies away from considering `FunDeps + Overlap`; and yet specifying the semantics as if the instances used bare unification variables is almost inevitably going give overlaps -- especially if there are multiple FDs.","type_of_failure":"OtherFailure","blocking":[]} -->8.6.1