GHC issueshttps://gitlab.haskell.org/ghc/ghc//issues20200519T15:35:06Zhttps://gitlab.haskell.org/ghc/ghc//issues/18150QuantifiedConstraints cannot refer to KnownNat20200519T15:35:06ZKoz RossQuantifiedConstraints cannot refer to KnownNat## Summary
If you attempt to write a quantified constraint involving ``KnownNat``, GHC will inform you that ``Class KnownNat does not support userspecified instances``. Given that no instances are being defined here (see 'Steps to reproduce' for an example), this is at least an unclear error message. It's also strange that it's not possible to express quantified constraints with ``KnownNat``.
## Steps to reproduce
Attempt to compile the following code:
```haskell
{# LANGUAGE DataKinds #}
{# LANGUAGE QuantifiedConstraints #}
{# LANGUAGE TypeFamilies #}
module Baz where
import Data.Kind (Type)
import GHC.TypeNats (KnownNat, Nat)
class (forall n. KnownNat n => KnownNat (f n)) => Foo (f :: Nat > Nat) where
type Bar n :: Nat
```
This will emit the error message described in the summary.
## Expected behavior
Either to compile, or to give an error message more indicative of what the true problem is.
## Environment
* GHC version used: 8.10.1
Optional:
* Operating System: GNU/Linux
* System Architecture: x86_64## Summary
If you attempt to write a quantified constraint involving ``KnownNat``, GHC will inform you that ``Class KnownNat does not support userspecified instances``. Given that no instances are being defined here (see 'Steps to reproduce' for an example), this is at least an unclear error message. It's also strange that it's not possible to express quantified constraints with ``KnownNat``.
## Steps to reproduce
Attempt to compile the following code:
```haskell
{# LANGUAGE DataKinds #}
{# LANGUAGE QuantifiedConstraints #}
{# LANGUAGE TypeFamilies #}
module Baz where
import Data.Kind (Type)
import GHC.TypeNats (KnownNat, Nat)
class (forall n. KnownNat n => KnownNat (f n)) => Foo (f :: Nat > Nat) where
type Bar n :: Nat
```
This will emit the error message described in the summary.
## Expected behavior
Either to compile, or to give an error message more indicative of what the true problem is.
## Environment
* GHC version used: 8.10.1
Optional:
* Operating System: GNU/Linux
* System Architecture: x86_64https://gitlab.haskell.org/ghc/ghc//issues/17959Cannot use Type Synonym with QuantifiedConstraints in GHC 8.8: "Illegal type ...20200408T23:37:06ZFabio MogaveroCannot use Type Synonym with QuantifiedConstraints in GHC 8.8: "Illegal type synonym family application"Consider the following simple snippet with three classes, one of which has an associated type synonym:
~~~haskell
{# LANGUAGE FlexibleContexts, QuantifiedConstraints, TypeFamilies #}
class A c
class B c
class (A (D c) => B (D c)) => C c where
type D c
~~~
GHC 8.6.5 compiles it like a charm, but both GHC 8.8.2 and 8.8.3 fail to compile with the following message:
~~~"compiler crash"
• Illegal type synonym family application ‘D c’ in instance:
B (D c)
• In the quantified constraint ‘A (D c) => B (D c)’
In the context: A (D c) => B (D c)
While checking the superclasses of class ‘C’
In the class declaration for ‘C’
~~~
Now, I am not sure if this is really a bug or, instead, a correction to the compiler, but I do not actually see why the snippet should fail to compile.
/label ~"needs triage"
/label ~bug
/label ~TypeFamilies
/label ~QuantifiedConstraintsConsider the following simple snippet with three classes, one of which has an associated type synonym:
~~~haskell
{# LANGUAGE FlexibleContexts, QuantifiedConstraints, TypeFamilies #}
class A c
class B c
class (A (D c) => B (D c)) => C c where
type D c
~~~
GHC 8.6.5 compiles it like a charm, but both GHC 8.8.2 and 8.8.3 fail to compile with the following message:
~~~"compiler crash"
• Illegal type synonym family application ‘D c’ in instance:
B (D c)
• In the quantified constraint ‘A (D c) => B (D c)’
In the context: A (D c) => B (D c)
While checking the superclasses of class ‘C’
In the class declaration for ‘C’
~~~
Now, I am not sure if this is really a bug or, instead, a correction to the compiler, but I do not actually see why the snippet should fail to compile.
/label ~"needs triage"
/label ~bug
/label ~TypeFamilies
/label ~QuantifiedConstraintshttps://gitlab.haskell.org/ghc/ghc//issues/17802QuantifiedConstraints don't work with equality constraints on type families20200220T16:46:33ZSebastian GrafQuantifiedConstraints don't work with equality constraints on type familiesI'm quite confident that this is a duplicate of some prior issue (#14860?), but this is different enough from all tickets I skimmed so far. This program is rejected:
```hs
{# LANGUAGE QuantifiedConstraints #}
{# LANGUAGE TypeFamilies #}
{# LANGUAGE KindSignatures #}
module Lib where
data T a = T a
type family F a
x :: (forall a. T a ~ F a) => F Int
x = T 42
```
```
src.hs:10:6: error:
• Couldn't match type ‘F a’ with ‘T a’
• In the ambiguity check for ‘x’
To defer the ambiguity check to use sites, enable AllowAmbiguousTypes
In the type signature: x :: (forall a. T a ~ F a) => F Int

10  x :: (forall a. T a ~ F a) => F Int
 ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
```
And I'm unsure why. In my head this should just work.
@matheus23 and I would really like to use it in !2315 to generalise constraints of the form `XRec pass (HsExpr pass) ~ Located (HsExpr pass)` (generalise over the syntactic entity `HsExpr pass`, that is).I'm quite confident that this is a duplicate of some prior issue (#14860?), but this is different enough from all tickets I skimmed so far. This program is rejected:
```hs
{# LANGUAGE QuantifiedConstraints #}
{# LANGUAGE TypeFamilies #}
{# LANGUAGE KindSignatures #}
module Lib where
data T a = T a
type family F a
x :: (forall a. T a ~ F a) => F Int
x = T 42
```
```
src.hs:10:6: error:
• Couldn't match type ‘F a’ with ‘T a’
• In the ambiguity check for ‘x’
To defer the ambiguity check to use sites, enable AllowAmbiguousTypes
In the type signature: x :: (forall a. T a ~ F a) => F Int

10  x :: (forall a. T a ~ F a) => F Int
 ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
```
And I'm unsure why. In my head this should just work.
@matheus23 and I would really like to use it in !2315 to generalise constraints of the form `XRec pass (HsExpr pass) ~ Located (HsExpr pass)` (generalise over the syntactic entity `HsExpr pass`, that is).https://gitlab.haskell.org/ghc/ghc//issues/17737Recursive superclass check is defeated by quantified constraints20200310T14:21:59ZRichard Eisenbergrae@richarde.devRecursive superclass check is defeated by quantified constraintsThis is accepted:
```hs
{# LANGUAGE QuantifiedConstraints, KindSignatures, ConstraintKinds #}
module Bug where
import Data.Kind
class ((() :: Constraint) => C a) => C a
```
The vacuous constraint `()` hides the recursive superclass `C a`. Note that I do not have `RecursiveSuperclasses` enabled.
The culprit is `TcTyDecls.checkClassCycles`.
This is not a "real" bug report, in that I found the problem only by reading the source code, not by observing the misbehavior. Still, it shouldn't be hard to fix. Should we just look through quantified constraints always?This is accepted:
```hs
{# LANGUAGE QuantifiedConstraints, KindSignatures, ConstraintKinds #}
module Bug where
import Data.Kind
class ((() :: Constraint) => C a) => C a
```
The vacuous constraint `()` hides the recursive superclass `C a`. Note that I do not have `RecursiveSuperclasses` enabled.
The culprit is `TcTyDecls.checkClassCycles`.
This is not a "real" bug report, in that I found the problem only by reading the source code, not by observing the misbehavior. Still, it shouldn't be hard to fix. Should we just look through quantified constraints always?Richard Eisenbergrae@richarde.devRichard Eisenbergrae@richarde.devhttps://gitlab.haskell.org/ghc/ghc//issues/17563Validity check quantified constraints20201213T22:02:03ZRichard Eisenbergrae@richarde.devValidity check quantified constraintsThis module is accepted:
```hs
{# LANGUAGE QuantifiedConstraints #}
module Bug2 where
blah :: (forall a. a b ~ a c) => b > c
blah = undefined
```
But it shouldn't be: it uses `~` with neither `GADTs` nor `TypeFamilies` enabled.This module is accepted:
```hs
{# LANGUAGE QuantifiedConstraints #}
module Bug2 where
blah :: (forall a. a b ~ a c) => b > c
blah = undefined
```
But it shouldn't be: it uses `~` with neither `GADTs` nor `TypeFamilies` enabled.8.10.2https://gitlab.haskell.org/ghc/ghc//issues/17347:kind fails with certain QuantifiedConstraints since 8.820191014T12:51:45ZJakob Brünker:kind fails with certain QuantifiedConstraints since 8.8## Description and Steps to reproduce
in GHCi:
```haskell
:set XQuantifiedConstraints XExplicitForAll XConstraintKinds XUndecidableInstances XAllowAmbiguousTypes XNoStarIsType
 This works:
() :: forall a b . (a => b ~ b) => ()
 This fails
 Illegal type synonym family application ‘GHC.Types.Any @Type’ in instance:
 (b :: GHC.Types.Any @Type) ~ (b :: GHC.Types.Any @Type)
:kind forall a b . (a => b ~ b) => ()
 Slight changes make it work, these are all okay:
:kind forall a b . (a => b ~ b) => b
:kind forall a b . (a => b ~ a) => ()
:kind forall a b . (b => b ~ b) => ()
```
This works in 8.6.5.
The reason `XNoStarIsType` is here is because otherwise the error message confusingly contains `@*`, which wouldn't be parsed as visible kind application (correctly it would have to be `@(*)`).
## Expected behavior
I expect `:kind forall a b . (a => b ~ b) => ()` to return `Type`, as it does in 8.6.5.
## Environment
* GHC version used:
HEAD (8.9.0.20191012)## Description and Steps to reproduce
in GHCi:
```haskell
:set XQuantifiedConstraints XExplicitForAll XConstraintKinds XUndecidableInstances XAllowAmbiguousTypes XNoStarIsType
 This works:
() :: forall a b . (a => b ~ b) => ()
 This fails
 Illegal type synonym family application ‘GHC.Types.Any @Type’ in instance:
 (b :: GHC.Types.Any @Type) ~ (b :: GHC.Types.Any @Type)
:kind forall a b . (a => b ~ b) => ()
 Slight changes make it work, these are all okay:
:kind forall a b . (a => b ~ b) => b
:kind forall a b . (a => b ~ a) => ()
:kind forall a b . (b => b ~ b) => ()
```
This works in 8.6.5.
The reason `XNoStarIsType` is here is because otherwise the error message confusingly contains `@*`, which wouldn't be parsed as visible kind application (correctly it would have to be `@(*)`).
## Expected behavior
I expect `:kind forall a b . (a => b ~ b) => ()` to return `Type`, as it does in 8.6.5.
## Environment
* GHC version used:
HEAD (8.9.0.20191012)https://gitlab.haskell.org/ghc/ghc//issues/17295Nonconfluence with QuantifiedConstraints20200603T14:16:02ZJames PayorNonconfluence with QuantifiedConstraintsEDIT: The ticket was original discovered in the context of the ambiguity checker, and it took some time to figure out that this has nothing to do with ambiguity: it's just about nonconfluence in the constraint solver. See helpful examples in https://gitlab.haskell.org/ghc/ghc/issues/17295#note_226331 and https://gitlab.haskell.org/ghc/ghc/issues/17295#note_237871
The ambiguity checker seems to be doing strange things in the presence of quantified constraints.
In particular, you can cause it to try and start solving for arbitrary equalities, which I find strange. And it won't listen to `AllowAmbiguousTypes`.
\[*edit* @Ericson2314 comment with smaller example: https://gitlab.haskell.org/ghc/ghc/issues/17295#note_231973]
Here's a minimized example:
```haskell
{# LANGUAGE QuantifiedConstraints #}
{# LANGUAGE RankNTypes #}
{# LANGUAGE TypeFamilies #}
{# LANGUAGE AllowAmbiguousTypes #}  This fails with and without AllowAmbiguousTypes...
data A
data B
foo :: (A ~ B => a ~ A) => (a ~ A => ()) > ()
foo _ = ()
```
GHC reports:
```
error:
• Couldn't match type ‘A’ with ‘B’
• In the ambiguity check for ‘foo’
In the type signature:
foo :: (A ~ B => a ~ A) => (a ~ A => ()) > ()
```
I haven't been able to provoke this behaviour without quantified constraints.
I've tested the above with GHC 8.8.1, though it's also likely broken on HEAD too.EDIT: The ticket was original discovered in the context of the ambiguity checker, and it took some time to figure out that this has nothing to do with ambiguity: it's just about nonconfluence in the constraint solver. See helpful examples in https://gitlab.haskell.org/ghc/ghc/issues/17295#note_226331 and https://gitlab.haskell.org/ghc/ghc/issues/17295#note_237871
The ambiguity checker seems to be doing strange things in the presence of quantified constraints.
In particular, you can cause it to try and start solving for arbitrary equalities, which I find strange. And it won't listen to `AllowAmbiguousTypes`.
\[*edit* @Ericson2314 comment with smaller example: https://gitlab.haskell.org/ghc/ghc/issues/17295#note_231973]
Here's a minimized example:
```haskell
{# LANGUAGE QuantifiedConstraints #}
{# LANGUAGE RankNTypes #}
{# LANGUAGE TypeFamilies #}
{# LANGUAGE AllowAmbiguousTypes #}  This fails with and without AllowAmbiguousTypes...
data A
data B
foo :: (A ~ B => a ~ A) => (a ~ A => ()) > ()
foo _ = ()
```
GHC reports:
```
error:
• Couldn't match type ‘A’ with ‘B’
• In the ambiguity check for ‘foo’
In the type signature:
foo :: (A ~ B => a ~ A) => (a ~ A => ()) > ()
```
I haven't been able to provoke this behaviour without quantified constraints.
I've tested the above with GHC 8.8.1, though it's also likely broken on HEAD too.https://gitlab.haskell.org/ghc/ghc//issues/16502Nested quantified constraints don't work20200326T19:00:35ZSimon Peyton JonesNested quantified constraints don't workConsider this, spun off from #14860:
```
{# LANGUAGE FlexibleContexts #}
{# LANGUAGE FlexibleInstances #}
{# LANGUAGE MultiParamTypeClasses #}
{# LANGUAGE QuantifiedConstraints #}
{# LANGUAGE ScopedTypeVariables #}
{# LANGUAGE TypeFamilies #}
{# LANGUAGE UndecidableInstances #}
{# LANGUAGE InstanceSigs #}
module Foo where
class (forall c. c ~ T a => Show (c b)) => ShowT a b
instance Show (T a b) => ShowT a b
class (forall b. Show b => ShowT a b) => C a where
type family T a :: * > *
data D a = MkD (T a Int)
instance C a => Show (D a) where
showsPrec p (MkD x)
= (showParen (p > 10) $ showString "MkD " . showsPrec 11 x)
```
When typechecking the final `instance` decl we get
```
T14860a.hs:22:49: error:
• Could not deduce (Show (T a Int))
arising from a use of ‘showsPrec’
from the context: C a
bound by the instance declaration at T14860a.hs:20:1026
```
but this is bogus. We have
```
g1: [G] C a  Given by the instance
g2: [G] forall b. Show b => ShowT a b  Superclass of g1
g3: [G] forall b c. (Show b, c ~ T a) => Show (c b)  Superclass of g2
w1: [W] Show (T a Int)  Wanted by the rhs of showsPrec
```
Well, that wanted should match `g3`! But it doesn't because `g3` ends up with a funny type
```
g3: [G] forall b. Show b => forall c. (Show b, c ~ T a) => Show (c b)
```
and that doens't work well at all.
Should not be hard to fix this.
EDIT: In the end, we don't think we really should accept this program, because it purports to solve `Show (a b)` for any `a` and `b`  an unlikely proposition. But the current (now that !2283 has landed) error message complains about default methods, which is poor form. We should fix the error message.Consider this, spun off from #14860:
```
{# LANGUAGE FlexibleContexts #}
{# LANGUAGE FlexibleInstances #}
{# LANGUAGE MultiParamTypeClasses #}
{# LANGUAGE QuantifiedConstraints #}
{# LANGUAGE ScopedTypeVariables #}
{# LANGUAGE TypeFamilies #}
{# LANGUAGE UndecidableInstances #}
{# LANGUAGE InstanceSigs #}
module Foo where
class (forall c. c ~ T a => Show (c b)) => ShowT a b
instance Show (T a b) => ShowT a b
class (forall b. Show b => ShowT a b) => C a where
type family T a :: * > *
data D a = MkD (T a Int)
instance C a => Show (D a) where
showsPrec p (MkD x)
= (showParen (p > 10) $ showString "MkD " . showsPrec 11 x)
```
When typechecking the final `instance` decl we get
```
T14860a.hs:22:49: error:
• Could not deduce (Show (T a Int))
arising from a use of ‘showsPrec’
from the context: C a
bound by the instance declaration at T14860a.hs:20:1026
```
but this is bogus. We have
```
g1: [G] C a  Given by the instance
g2: [G] forall b. Show b => ShowT a b  Superclass of g1
g3: [G] forall b c. (Show b, c ~ T a) => Show (c b)  Superclass of g2
w1: [W] Show (T a Int)  Wanted by the rhs of showsPrec
```
Well, that wanted should match `g3`! But it doesn't because `g3` ends up with a funny type
```
g3: [G] forall b. Show b => forall c. (Show b, c ~ T a) => Show (c b)
```
and that doens't work well at all.
Should not be hard to fix this.
EDIT: In the end, we don't think we really should accept this program, because it purports to solve `Show (a b)` for any `a` and `b`  an unlikely proposition. But the current (now that !2283 has landed) error message complains about default methods, which is poor form. We should fix the error message.https://gitlab.haskell.org/ghc/ghc//issues/16442QuantifiedConstraints runtime loopiness  simplifier ticks(?)20190328T06:54:48ZAnthony ClaydenQuantifiedConstraints runtime loopiness  simplifier ticks(?)Consider these `QuantifiedConstraints` aimed at reinforcing a FunDep (from [this comment](https://gitlab.haskell.org/ghc/ghc/issues/16430#note_187582))
{# LANGUAGE QuantifiedConstraints, { etc } #}
class (forall b. F Int b => b ~ Bool,
forall b. F String b => b ~ Char )
=> F a b  a > b
instance F Int Bool
instance F String Char
class D a where { op :: F a b => a > b }
instance D Int where { op _ = True }
instance D String where { op _ = 'c' }
This compiles OK, no warnings with `Wall` set.
*> :t op "hello"
op "hello" :: Char
*> op "hello"  runs forever
[^C]Interrupted.
I see no reason this should be looping: `op` doesn't inspect its argument, just returns a literal.
On GHC 8.6.4 and 8.6.1; Windows platform.Consider these `QuantifiedConstraints` aimed at reinforcing a FunDep (from [this comment](https://gitlab.haskell.org/ghc/ghc/issues/16430#note_187582))
{# LANGUAGE QuantifiedConstraints, { etc } #}
class (forall b. F Int b => b ~ Bool,
forall b. F String b => b ~ Char )
=> F a b  a > b
instance F Int Bool
instance F String Char
class D a where { op :: F a b => a > b }
instance D Int where { op _ = True }
instance D String where { op _ = 'c' }
This compiles OK, no warnings with `Wall` set.
*> :t op "hello"
op "hello" :: Char
*> op "hello"  runs forever
[^C]Interrupted.
I see no reason this should be looping: `op` doesn't inspect its argument, just returns a literal.
On GHC 8.6.4 and 8.6.1; Windows platform.https://gitlab.haskell.org/ghc/ghc//issues/16365Inconsistency in quantified constraint solving20190707T18:00:22ZRyan ScottInconsistency in quantified constraint solvingConsider the following program:
```hs
{# LANGUAGE ConstraintKinds #}
{# LANGUAGE ExistentialQuantification #}
{# LANGUAGE FlexibleContexts #}
{# LANGUAGE FlexibleInstances #}
{# LANGUAGE MultiParamTypeClasses #}
{# LANGUAGE QuantifiedConstraints #}
{# LANGUAGE TypeFamilies #}
{# LANGUAGE UndecidableInstances #}
module Bug where
import Data.Kind
import Data.Proxy
class C a where
m :: a > ()
data Dict c = c => Dict

type family F a :: Type > Type
class C (F a b) => CF a b
instance C (F a b) => CF a b
works1 :: (forall z. CF a z) => Proxy (a, b) > Dict (CF a b)
works1 _ = Dict
works2 :: ( CF a b) => Proxy (a, b) > Dict (C (F a b))
works2 _ = Dict
works3, fails :: (forall z. CF a z) => Proxy (a, b) > Dict (C (F a b))
works3 p  Dict < works1 p = Dict
fails _ = Dict
```
`fails`, as its name suggests, fails to typecheck:
```
$ /opt/ghc/8.6.3/bin/ghc Bug.hs
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
Bug.hs:33:11: error:
• Could not deduce (C (F a b)) arising from a use of ‘Dict’
from the context: forall z. CF a z
bound by the type signature for:
fails :: forall a b.
(forall z. CF a z) =>
Proxy (a, b) > Dict (C (F a b))
at Bug.hs:31:171
• In the expression: Dict
In an equation for ‘fails’: fails _ = Dict

33  fails _ = Dict
 ^^^^
```
But I see no reason why this shouldn't typecheck. After all, the fact that `works1` typechecks proves that GHC's constraint solver is perfectly capable of deducing that `(forall z. CF a z)` implies `(CF a b)`, and the fact that `works2` typechecks proves that GHC's constraint solver is perfectly capable of deducing that `(CF a b)` implies that `(C (F a b))`. Why then can GHC's constraint solver not connect the dots and deduce that `(forall z. CF a z)` implies `(C (F a b))` (in the type of `fails`)?
Note that something with the type `(forall z. CF a z) => Proxy (a, b) > Dict (C (F a b))` //can// be made to work if you explicitly guide GHC along with explicit patternmatching on a `Dict`, as `works3` demonstrates. But I claim that this shouldn't be necessary.
Moreover, in this variation of the program above:
```hs
 <as above>

data G a :: Type > Type
class C (G a b) => CG a b
instance C (G a b) => CG a b
works1' :: (forall z. CG a z) => Proxy (a, b) > Dict (CG a b)
works1' _ = Dict
works2' :: ( CG a b) => Proxy (a, b) > Dict (C (G a b))
works2' _ = Dict
works3' :: (forall z. CG a z) => Proxy (a, b) > Dict (C (G a b))
works3' _ = Dict
```
`works3'` needs no explicit `Dict` patternmatching to typecheck.
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.6.3 
 Type  Bug 
 TypeOfFailure  OtherFailure 
 Priority  normal 
 Resolution  Unresolved 
 Component  Compiler 
 Test case  
 Differential revisions  
 BlockedBy  
 Related  
 Blocking  
 CC  
 Operating system  
 Architecture  
</details>
<! {"blocked_by":[],"summary":"Inconsistency in quantified constraint solving","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.6.3","keywords":["QuantifiedConstraints"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"Consider the following program:\r\n\r\n{{{#!hs\r\n{# LANGUAGE ConstraintKinds #}\r\n{# LANGUAGE ExistentialQuantification #}\r\n{# LANGUAGE FlexibleContexts #}\r\n{# LANGUAGE FlexibleInstances #}\r\n{# LANGUAGE MultiParamTypeClasses #}\r\n{# LANGUAGE QuantifiedConstraints #}\r\n{# LANGUAGE TypeFamilies #}\r\n{# LANGUAGE UndecidableInstances #}\r\nmodule Bug where\r\n\r\nimport Data.Kind\r\nimport Data.Proxy\r\n\r\nclass C a where\r\n m :: a > ()\r\n\r\ndata Dict c = c => Dict\r\n\r\n\r\n\r\ntype family F a :: Type > Type\r\nclass C (F a b) => CF a b\r\ninstance C (F a b) => CF a b\r\n\r\nworks1 :: (forall z. CF a z) => Proxy (a, b) > Dict (CF a b)\r\nworks1 _ = Dict\r\n\r\nworks2 :: ( CF a b) => Proxy (a, b) > Dict (C (F a b))\r\nworks2 _ = Dict\r\n\r\nworks3, fails :: (forall z. CF a z) => Proxy (a, b) > Dict (C (F a b))\r\nworks3 p  Dict < works1 p = Dict\r\nfails _ = Dict\r\n}}}\r\n\r\n`fails`, as its name suggests, fails to typecheck:\r\n\r\n{{{\r\n$ /opt/ghc/8.6.3/bin/ghc Bug.hs\r\n[1 of 1] Compiling Bug ( Bug.hs, Bug.o )\r\n\r\nBug.hs:33:11: error:\r\n • Could not deduce (C (F a b)) arising from a use of ‘Dict’\r\n from the context: forall z. CF a z\r\n bound by the type signature for:\r\n fails :: forall a b.\r\n (forall z. CF a z) =>\r\n Proxy (a, b) > Dict (C (F a b))\r\n at Bug.hs:31:171\r\n • In the expression: Dict\r\n In an equation for ‘fails’: fails _ = Dict\r\n \r\n33  fails _ = Dict\r\n  ^^^^\r\n}}}\r\n\r\nBut I see no reason why this shouldn't typecheck. After all, the fact that `works1` typechecks proves that GHC's constraint solver is perfectly capable of deducing that `(forall z. CF a z)` implies `(CF a b)`, and the fact that `works2` typechecks proves that GHC's constraint solver is perfectly capable of deducing that `(CF a b)` implies that `(C (F a b))`. Why then can GHC's constraint solver not connect the dots and deduce that `(forall z. CF a z)` implies `(C (F a b))` (in the type of `fails`)?\r\n\r\nNote that something with the type `(forall z. CF a z) => Proxy (a, b) > Dict (C (F a b))` //can// be made to work if you explicitly guide GHC along with explicit patternmatching on a `Dict`, as `works3` demonstrates. But I claim that this shouldn't be necessary.\r\n\r\nMoreover, in this variation of the program above:\r\n\r\n{{{#!hs\r\n <as above>\r\n\r\n\r\ndata G a :: Type > Type\r\nclass C (G a b) => CG a b\r\ninstance C (G a b) => CG a b\r\n\r\nworks1' :: (forall z. CG a z) => Proxy (a, b) > Dict (CG a b)\r\nworks1' _ = Dict\r\n\r\nworks2' :: ( CG a b) => Proxy (a, b) > Dict (C (G a b))\r\nworks2' _ = Dict\r\n\r\nworks3' :: (forall z. CG a z) => Proxy (a, b) > Dict (C (G a b))\r\nworks3' _ = Dict\r\n}}}\r\n\r\n`works3'` needs no explicit `Dict` patternmatching to typecheck.","type_of_failure":"OtherFailure","blocking":[]} >Consider the following program:
```hs
{# LANGUAGE ConstraintKinds #}
{# LANGUAGE ExistentialQuantification #}
{# LANGUAGE FlexibleContexts #}
{# LANGUAGE FlexibleInstances #}
{# LANGUAGE MultiParamTypeClasses #}
{# LANGUAGE QuantifiedConstraints #}
{# LANGUAGE TypeFamilies #}
{# LANGUAGE UndecidableInstances #}
module Bug where
import Data.Kind
import Data.Proxy
class C a where
m :: a > ()
data Dict c = c => Dict

type family F a :: Type > Type
class C (F a b) => CF a b
instance C (F a b) => CF a b
works1 :: (forall z. CF a z) => Proxy (a, b) > Dict (CF a b)
works1 _ = Dict
works2 :: ( CF a b) => Proxy (a, b) > Dict (C (F a b))
works2 _ = Dict
works3, fails :: (forall z. CF a z) => Proxy (a, b) > Dict (C (F a b))
works3 p  Dict < works1 p = Dict
fails _ = Dict
```
`fails`, as its name suggests, fails to typecheck:
```
$ /opt/ghc/8.6.3/bin/ghc Bug.hs
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
Bug.hs:33:11: error:
• Could not deduce (C (F a b)) arising from a use of ‘Dict’
from the context: forall z. CF a z
bound by the type signature for:
fails :: forall a b.
(forall z. CF a z) =>
Proxy (a, b) > Dict (C (F a b))
at Bug.hs:31:171
• In the expression: Dict
In an equation for ‘fails’: fails _ = Dict

33  fails _ = Dict
 ^^^^
```
But I see no reason why this shouldn't typecheck. After all, the fact that `works1` typechecks proves that GHC's constraint solver is perfectly capable of deducing that `(forall z. CF a z)` implies `(CF a b)`, and the fact that `works2` typechecks proves that GHC's constraint solver is perfectly capable of deducing that `(CF a b)` implies that `(C (F a b))`. Why then can GHC's constraint solver not connect the dots and deduce that `(forall z. CF a z)` implies `(C (F a b))` (in the type of `fails`)?
Note that something with the type `(forall z. CF a z) => Proxy (a, b) > Dict (C (F a b))` //can// be made to work if you explicitly guide GHC along with explicit patternmatching on a `Dict`, as `works3` demonstrates. But I claim that this shouldn't be necessary.
Moreover, in this variation of the program above:
```hs
 <as above>

data G a :: Type > Type
class C (G a b) => CG a b
instance C (G a b) => CG a b
works1' :: (forall z. CG a z) => Proxy (a, b) > Dict (CG a b)
works1' _ = Dict
works2' :: ( CG a b) => Proxy (a, b) > Dict (C (G a b))
works2' _ = Dict
works3' :: (forall z. CG a z) => Proxy (a, b) > Dict (C (G a b))
works3' _ = Dict
```
`works3'` needs no explicit `Dict` patternmatching to typecheck.
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.6.3 
 Type  Bug 
 TypeOfFailure  OtherFailure 
 Priority  normal 
 Resolution  Unresolved 
 Component  Compiler 
 Test case  
 Differential revisions  
 BlockedBy  
 Related  
 Blocking  
 CC  
 Operating system  
 Architecture  
</details>
<! {"blocked_by":[],"summary":"Inconsistency in quantified constraint solving","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.6.3","keywords":["QuantifiedConstraints"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"Consider the following program:\r\n\r\n{{{#!hs\r\n{# LANGUAGE ConstraintKinds #}\r\n{# LANGUAGE ExistentialQuantification #}\r\n{# LANGUAGE FlexibleContexts #}\r\n{# LANGUAGE FlexibleInstances #}\r\n{# LANGUAGE MultiParamTypeClasses #}\r\n{# LANGUAGE QuantifiedConstraints #}\r\n{# LANGUAGE TypeFamilies #}\r\n{# LANGUAGE UndecidableInstances #}\r\nmodule Bug where\r\n\r\nimport Data.Kind\r\nimport Data.Proxy\r\n\r\nclass C a where\r\n m :: a > ()\r\n\r\ndata Dict c = c => Dict\r\n\r\n\r\n\r\ntype family F a :: Type > Type\r\nclass C (F a b) => CF a b\r\ninstance C (F a b) => CF a b\r\n\r\nworks1 :: (forall z. CF a z) => Proxy (a, b) > Dict (CF a b)\r\nworks1 _ = Dict\r\n\r\nworks2 :: ( CF a b) => Proxy (a, b) > Dict (C (F a b))\r\nworks2 _ = Dict\r\n\r\nworks3, fails :: (forall z. CF a z) => Proxy (a, b) > Dict (C (F a b))\r\nworks3 p  Dict < works1 p = Dict\r\nfails _ = Dict\r\n}}}\r\n\r\n`fails`, as its name suggests, fails to typecheck:\r\n\r\n{{{\r\n$ /opt/ghc/8.6.3/bin/ghc Bug.hs\r\n[1 of 1] Compiling Bug ( Bug.hs, Bug.o )\r\n\r\nBug.hs:33:11: error:\r\n • Could not deduce (C (F a b)) arising from a use of ‘Dict’\r\n from the context: forall z. CF a z\r\n bound by the type signature for:\r\n fails :: forall a b.\r\n (forall z. CF a z) =>\r\n Proxy (a, b) > Dict (C (F a b))\r\n at Bug.hs:31:171\r\n • In the expression: Dict\r\n In an equation for ‘fails’: fails _ = Dict\r\n \r\n33  fails _ = Dict\r\n  ^^^^\r\n}}}\r\n\r\nBut I see no reason why this shouldn't typecheck. After all, the fact that `works1` typechecks proves that GHC's constraint solver is perfectly capable of deducing that `(forall z. CF a z)` implies `(CF a b)`, and the fact that `works2` typechecks proves that GHC's constraint solver is perfectly capable of deducing that `(CF a b)` implies that `(C (F a b))`. Why then can GHC's constraint solver not connect the dots and deduce that `(forall z. CF a z)` implies `(C (F a b))` (in the type of `fails`)?\r\n\r\nNote that something with the type `(forall z. CF a z) => Proxy (a, b) > Dict (C (F a b))` //can// be made to work if you explicitly guide GHC along with explicit patternmatching on a `Dict`, as `works3` demonstrates. But I claim that this shouldn't be necessary.\r\n\r\nMoreover, in this variation of the program above:\r\n\r\n{{{#!hs\r\n <as above>\r\n\r\n\r\ndata G a :: Type > Type\r\nclass C (G a b) => CG a b\r\ninstance C (G a b) => CG a b\r\n\r\nworks1' :: (forall z. CG a z) => Proxy (a, b) > Dict (CG a b)\r\nworks1' _ = Dict\r\n\r\nworks2' :: ( CG a b) => Proxy (a, b) > Dict (C (G a b))\r\nworks2' _ = Dict\r\n\r\nworks3' :: (forall z. CG a z) => Proxy (a, b) > Dict (C (G a b))\r\nworks3' _ = Dict\r\n}}}\r\n\r\n`works3'` needs no explicit `Dict` patternmatching to typecheck.","type_of_failure":"OtherFailure","blocking":[]} >https://gitlab.haskell.org/ghc/ghc//issues/16140Cannot create type synonym for quantified constraint without ImpredicativeTypes20190707T18:01:19ZAshley YakeleyCannot create type synonym for quantified constraint without ImpredicativeTypes```hs
{# LANGUAGE KindSignatures, RankNTypes, ConstraintKinds, QuantifiedConstraints, FlexibleInstances, UndecidableInstances #}
module Bug where
type F1 (f :: * > *) = forall a. Eq (f a)
class (Functor f, F1 f) => C f
instance (Functor f, F1 f) => C f
type F2 f = (Functor f, F1 f)
```
```
Bug.hs:7:1: error:
• Illegal polymorphic type: F1 f
GHC doesn't yet support impredicative polymorphism
• In the type synonym declaration for ‘F2’

7  type F2 f = (Functor f, F1 f)
 ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
```
(GHC accepts the program with ImpredicativeTypes.)
`(Functor f, F1 f)` is allowed as a superclass constraint, and as an instance constraint, but a type synonym cannot be made for it.
Not sure if this really counts as a bug ("just switch on ImpredicativeTypes"), but I think it's worth discussing. I prefer to keep ImpredicativeTypes switched off, but if something can be a constraint, shouldn't I be able to create a type synonym of it?
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.6.3 
 Type  Bug 
 TypeOfFailure  OtherFailure 
 Priority  normal 
 Resolution  Unresolved 
 Component  Compiler 
 Test case  
 Differential revisions  
 BlockedBy  
 Related  
 Blocking  
 CC  
 Operating system  
 Architecture  
</details>
<! {"blocked_by":[],"summary":"Cannot create type synonym for quantified constraint without ImpredicativeTypes","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.6.3","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"{{{#!hs\r\n{# LANGUAGE KindSignatures, RankNTypes, ConstraintKinds, QuantifiedConstraints, FlexibleInstances, UndecidableInstances #}\r\nmodule Bug where\r\n\r\ntype F1 (f :: * > *) = forall a. Eq (f a)\r\nclass (Functor f, F1 f) => C f\r\ninstance (Functor f, F1 f) => C f\r\ntype F2 f = (Functor f, F1 f)\r\n}}}\r\n\r\n{{{\r\nBug.hs:7:1: error:\r\n • Illegal polymorphic type: F1 f\r\n GHC doesn't yet support impredicative polymorphism\r\n • In the type synonym declaration for ‘F2’\r\n \r\n7  type F2 f = (Functor f, F1 f)\r\n  ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^\r\n}}}\r\n\r\n(GHC accepts the program with ImpredicativeTypes.)\r\n\r\n`(Functor f, F1 f)` is allowed as a superclass constraint, and as an instance constraint, but a type synonym cannot be made for it.\r\n\r\nNot sure if this really counts as a bug (\"just switch on ImpredicativeTypes\"), but I think it's worth discussing. I prefer to keep ImpredicativeTypes switched off, but if something can be a constraint, shouldn't I be able to create a type synonym of it?","type_of_failure":"OtherFailure","blocking":[]} >```hs
{# LANGUAGE KindSignatures, RankNTypes, ConstraintKinds, QuantifiedConstraints, FlexibleInstances, UndecidableInstances #}
module Bug where
type F1 (f :: * > *) = forall a. Eq (f a)
class (Functor f, F1 f) => C f
instance (Functor f, F1 f) => C f
type F2 f = (Functor f, F1 f)
```
```
Bug.hs:7:1: error:
• Illegal polymorphic type: F1 f
GHC doesn't yet support impredicative polymorphism
• In the type synonym declaration for ‘F2’

7  type F2 f = (Functor f, F1 f)
 ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
```
(GHC accepts the program with ImpredicativeTypes.)
`(Functor f, F1 f)` is allowed as a superclass constraint, and as an instance constraint, but a type synonym cannot be made for it.
Not sure if this really counts as a bug ("just switch on ImpredicativeTypes"), but I think it's worth discussing. I prefer to keep ImpredicativeTypes switched off, but if something can be a constraint, shouldn't I be able to create a type synonym of it?
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.6.3 
 Type  Bug 
 TypeOfFailure  OtherFailure 
 Priority  normal 
 Resolution  Unresolved 
 Component  Compiler 
 Test case  
 Differential revisions  
 BlockedBy  
 Related  
 Blocking  
 CC  
 Operating system  
 Architecture  
</details>
<! {"blocked_by":[],"summary":"Cannot create type synonym for quantified constraint without ImpredicativeTypes","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.6.3","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"{{{#!hs\r\n{# LANGUAGE KindSignatures, RankNTypes, ConstraintKinds, QuantifiedConstraints, FlexibleInstances, UndecidableInstances #}\r\nmodule Bug where\r\n\r\ntype F1 (f :: * > *) = forall a. Eq (f a)\r\nclass (Functor f, F1 f) => C f\r\ninstance (Functor f, F1 f) => C f\r\ntype F2 f = (Functor f, F1 f)\r\n}}}\r\n\r\n{{{\r\nBug.hs:7:1: error:\r\n • Illegal polymorphic type: F1 f\r\n GHC doesn't yet support impredicative polymorphism\r\n • In the type synonym declaration for ‘F2’\r\n \r\n7  type F2 f = (Functor f, F1 f)\r\n  ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^\r\n}}}\r\n\r\n(GHC accepts the program with ImpredicativeTypes.)\r\n\r\n`(Functor f, F1 f)` is allowed as a superclass constraint, and as an instance constraint, but a type synonym cannot be made for it.\r\n\r\nNot sure if this really counts as a bug (\"just switch on ImpredicativeTypes\"), but I think it's worth discussing. I prefer to keep ImpredicativeTypes switched off, but if something can be a constraint, shouldn't I be able to create a type synonym of it?","type_of_failure":"OtherFailure","blocking":[]} >https://gitlab.haskell.org/ghc/ghc//issues/16139GHC confused about type synonym kind with QuantifiedConstraints20200715T11:48:06ZAshley YakeleyGHC confused about type synonym kind with QuantifiedConstraints```hs
{# LANGUAGE KindSignatures, RankNTypes, ConstraintKinds, QuantifiedConstraints #}
module Bug where
import Data.Constraint
type E (c :: * > Constraint) = forall (a :: *). Eq a => c a
```
```
Bug.hs:5:58: error:
• Expected a type, but ‘c a’ has kind ‘Constraint’
• In the type ‘forall (a :: *). Eq a => c a’
In the type declaration for ‘E’

5  type E (c :: * > Constraint) = forall (a :: *). Eq a => c a
 ^^^
```
Note that GHC accepts the program when the `Eq a` constraint is removed.
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.6.3 
 Type  Bug 
 TypeOfFailure  OtherFailure 
 Priority  normal 
 Resolution  Unresolved 
 Component  Compiler 
 Test case  
 Differential revisions  
 BlockedBy  
 Related  
 Blocking  
 CC  
 Operating system  
 Architecture  
</details>
<! {"blocked_by":[],"summary":"GHC confused about type synonym kind with QuantifiedConstraints","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.6.3","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"{{{#!hs\r\n{# LANGUAGE KindSignatures, RankNTypes, ConstraintKinds, QuantifiedConstraints #}\r\nmodule Bug where\r\nimport Data.Constraint\r\n\r\ntype E (c :: * > Constraint) = forall (a :: *). Eq a => c a\r\n}}}\r\n\r\n{{{\r\nBug.hs:5:58: error:\r\n • Expected a type, but ‘c a’ has kind ‘Constraint’\r\n • In the type ‘forall (a :: *). Eq a => c a’\r\n In the type declaration for ‘E’\r\n \r\n5  type E (c :: * > Constraint) = forall (a :: *). Eq a => c a\r\n  ^^^\r\n}}}\r\n\r\nNote that GHC accepts the program when the `Eq a` constraint is removed.","type_of_failure":"OtherFailure","blocking":[]} >```hs
{# LANGUAGE KindSignatures, RankNTypes, ConstraintKinds, QuantifiedConstraints #}
module Bug where
import Data.Constraint
type E (c :: * > Constraint) = forall (a :: *). Eq a => c a
```
```
Bug.hs:5:58: error:
• Expected a type, but ‘c a’ has kind ‘Constraint’
• In the type ‘forall (a :: *). Eq a => c a’
In the type declaration for ‘E’

5  type E (c :: * > Constraint) = forall (a :: *). Eq a => c a
 ^^^
```
Note that GHC accepts the program when the `Eq a` constraint is removed.
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.6.3 
 Type  Bug 
 TypeOfFailure  OtherFailure 
 Priority  normal 
 Resolution  Unresolved 
 Component  Compiler 
 Test case  
 Differential revisions  
 BlockedBy  
 Related  
 Blocking  
 CC  
 Operating system  
 Architecture  
</details>
<! {"blocked_by":[],"summary":"GHC confused about type synonym kind with QuantifiedConstraints","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.6.3","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"{{{#!hs\r\n{# LANGUAGE KindSignatures, RankNTypes, ConstraintKinds, QuantifiedConstraints #}\r\nmodule Bug where\r\nimport Data.Constraint\r\n\r\ntype E (c :: * > Constraint) = forall (a :: *). Eq a => c a\r\n}}}\r\n\r\n{{{\r\nBug.hs:5:58: error:\r\n • Expected a type, but ‘c a’ has kind ‘Constraint’\r\n • In the type ‘forall (a :: *). Eq a => c a’\r\n In the type declaration for ‘E’\r\n \r\n5  type E (c :: * > Constraint) = forall (a :: *). Eq a => c a\r\n  ^^^\r\n}}}\r\n\r\nNote that GHC accepts the program when the `Eq a` constraint is removed.","type_of_failure":"OtherFailure","blocking":[]} >https://gitlab.haskell.org/ghc/ghc//issues/15888Quantified constraints can be loopy20190707T18:02:34ZRichard Eisenbergrae@richarde.devQuantified constraints can be loopyConsider this abuse:
```hs
{# LANGUAGE QuantifiedConstraints, UndecidableInstances #}
module Bug where
data T1 a
data T2 a
class C a where
meth :: a
instance (forall a. C (T2 a)) => C (T1 b) where
meth = error "instance T1"
instance (forall a. C (T1 a)) => C (T2 b) where
meth = error "instance T2"
example :: T1 Int
example = meth
```
GHC says
```
• Reduction stack overflow; size = 201
When simplifying the following type: C (T1 a)
Use freductiondepth=0 to disable this check
(any upper bound you could choose might fail unpredictably with
minor updates to GHC, so disabling the check is recommended if
you're sure that type checking should terminate)
• In the expression: meth
In an equation for ‘example’: example = meth
```
Of course, I've taken on some responsibility for my actions here by saying `UndecidableInstances`, but GHC really should be able to figure this out. Here's what's happening:
1. We get a Wanted `C (T1 Int)`.
1. GHC chooses the appropriate instance, emitting a Wanted `forall a. C (T2 a)`.
1. GHC skolemizes the `a` to `a1` and tries solve a Wanted `C (T2 a1)`.
1. GHC chooses the appropriate instance, emitting a Wanted `forall a. C (T1 a)`.
1. GHC skolemizes the `a` to `a2` and tries to solve a Wanted `C (T1 a2)`.
And around and around we go.
(This loop is guessed at from knowing GHC's algorithms in general. I did not look at a trace.)
We *could* get this one, though. Before skolemizing, we could stash the Wanted in the `inert_solved_dicts`, which is where we record uses of toplevel instances. (See `Note [Solved dictionaries]` in TcSMonad.) Then, later, when we see the same Wanted arise again, we would just use the cached value, making a wellformed recursive dictionary.
This deficiency was discovered in `singletons` (https://github.com/goldfirere/singletons/issues/371). Perhaps that's not "the wild", but it's not quite contrived either.
Note that we don't need two datatypes to trigger this, but having one recursive instance like this seems awfully silly.
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.6.2 
 Type  Bug 
 TypeOfFailure  OtherFailure 
 Priority  normal 
 Resolution  Unresolved 
 Component  Compiler 
 Test case  
 Differential revisions  
 BlockedBy  
 Related  
 Blocking  
 CC  
 Operating system  
 Architecture  
</details>
<! {"blocked_by":[],"summary":"Quantified constraints can be loopy","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"8.6.3","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.6.2","keywords":["QuantifiedConstraints"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"Consider this abuse:\r\n\r\n{{{#!hs\r\n{# LANGUAGE QuantifiedConstraints, UndecidableInstances #}\r\n\r\nmodule Bug where\r\n\r\ndata T1 a\r\ndata T2 a\r\n\r\nclass C a where\r\n meth :: a\r\n\r\ninstance (forall a. C (T2 a)) => C (T1 b) where\r\n meth = error \"instance T1\"\r\n\r\ninstance (forall a. C (T1 a)) => C (T2 b) where\r\n meth = error \"instance T2\"\r\n\r\nexample :: T1 Int\r\nexample = meth\r\n}}}\r\n\r\nGHC says\r\n\r\n{{{\r\n • Reduction stack overflow; size = 201\r\n When simplifying the following type: C (T1 a)\r\n Use freductiondepth=0 to disable this check\r\n (any upper bound you could choose might fail unpredictably with\r\n minor updates to GHC, so disabling the check is recommended if\r\n you're sure that type checking should terminate)\r\n • In the expression: meth\r\n In an equation for ‘example’: example = meth\r\n}}}\r\n\r\nOf course, I've taken on some responsibility for my actions here by saying `UndecidableInstances`, but GHC really should be able to figure this out. Here's what's happening:\r\n\r\n1. We get a Wanted `C (T1 Int)`.\r\n\r\n2. GHC chooses the appropriate instance, emitting a Wanted `forall a. C (T2 a)`.\r\n\r\n3. GHC skolemizes the `a` to `a1` and tries solve a Wanted `C (T2 a1)`.\r\n\r\n4. GHC chooses the appropriate instance, emitting a Wanted `forall a. C (T1 a)`.\r\n\r\n5. GHC skolemizes the `a` to `a2` and tries to solve a Wanted `C (T1 a2)`.\r\n\r\nAnd around and around we go.\r\n\r\n(This loop is guessed at from knowing GHC's algorithms in general. I did not look at a trace.)\r\n\r\nWe ''could'' get this one, though. Before skolemizing, we could stash the Wanted in the `inert_solved_dicts`, which is where we record uses of toplevel instances. (See `Note [Solved dictionaries]` in TcSMonad.) Then, later, when we see the same Wanted arise again, we would just use the cached value, making a wellformed recursive dictionary.\r\n\r\nThis deficiency was discovered in `singletons` (https://github.com/goldfirere/singletons/issues/371). Perhaps that's not \"the wild\", but it's not quite contrived either.\r\n\r\nNote that we don't need two datatypes to trigger this, but having one recursive instance like this seems awfully silly.","type_of_failure":"OtherFailure","blocking":[]} >Consider this abuse:
```hs
{# LANGUAGE QuantifiedConstraints, UndecidableInstances #}
module Bug where
data T1 a
data T2 a
class C a where
meth :: a
instance (forall a. C (T2 a)) => C (T1 b) where
meth = error "instance T1"
instance (forall a. C (T1 a)) => C (T2 b) where
meth = error "instance T2"
example :: T1 Int
example = meth
```
GHC says
```
• Reduction stack overflow; size = 201
When simplifying the following type: C (T1 a)
Use freductiondepth=0 to disable this check
(any upper bound you could choose might fail unpredictably with
minor updates to GHC, so disabling the check is recommended if
you're sure that type checking should terminate)
• In the expression: meth
In an equation for ‘example’: example = meth
```
Of course, I've taken on some responsibility for my actions here by saying `UndecidableInstances`, but GHC really should be able to figure this out. Here's what's happening:
1. We get a Wanted `C (T1 Int)`.
1. GHC chooses the appropriate instance, emitting a Wanted `forall a. C (T2 a)`.
1. GHC skolemizes the `a` to `a1` and tries solve a Wanted `C (T2 a1)`.
1. GHC chooses the appropriate instance, emitting a Wanted `forall a. C (T1 a)`.
1. GHC skolemizes the `a` to `a2` and tries to solve a Wanted `C (T1 a2)`.
And around and around we go.
(This loop is guessed at from knowing GHC's algorithms in general. I did not look at a trace.)
We *could* get this one, though. Before skolemizing, we could stash the Wanted in the `inert_solved_dicts`, which is where we record uses of toplevel instances. (See `Note [Solved dictionaries]` in TcSMonad.) Then, later, when we see the same Wanted arise again, we would just use the cached value, making a wellformed recursive dictionary.
This deficiency was discovered in `singletons` (https://github.com/goldfirere/singletons/issues/371). Perhaps that's not "the wild", but it's not quite contrived either.
Note that we don't need two datatypes to trigger this, but having one recursive instance like this seems awfully silly.
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.6.2 
 Type  Bug 
 TypeOfFailure  OtherFailure 
 Priority  normal 
 Resolution  Unresolved 
 Component  Compiler 
 Test case  
 Differential revisions  
 BlockedBy  
 Related  
 Blocking  
 CC  
 Operating system  
 Architecture  
</details>
<! {"blocked_by":[],"summary":"Quantified constraints can be loopy","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"8.6.3","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.6.2","keywords":["QuantifiedConstraints"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"Consider this abuse:\r\n\r\n{{{#!hs\r\n{# LANGUAGE QuantifiedConstraints, UndecidableInstances #}\r\n\r\nmodule Bug where\r\n\r\ndata T1 a\r\ndata T2 a\r\n\r\nclass C a where\r\n meth :: a\r\n\r\ninstance (forall a. C (T2 a)) => C (T1 b) where\r\n meth = error \"instance T1\"\r\n\r\ninstance (forall a. C (T1 a)) => C (T2 b) where\r\n meth = error \"instance T2\"\r\n\r\nexample :: T1 Int\r\nexample = meth\r\n}}}\r\n\r\nGHC says\r\n\r\n{{{\r\n • Reduction stack overflow; size = 201\r\n When simplifying the following type: C (T1 a)\r\n Use freductiondepth=0 to disable this check\r\n (any upper bound you could choose might fail unpredictably with\r\n minor updates to GHC, so disabling the check is recommended if\r\n you're sure that type checking should terminate)\r\n • In the expression: meth\r\n In an equation for ‘example’: example = meth\r\n}}}\r\n\r\nOf course, I've taken on some responsibility for my actions here by saying `UndecidableInstances`, but GHC really should be able to figure this out. Here's what's happening:\r\n\r\n1. We get a Wanted `C (T1 Int)`.\r\n\r\n2. GHC chooses the appropriate instance, emitting a Wanted `forall a. C (T2 a)`.\r\n\r\n3. GHC skolemizes the `a` to `a1` and tries solve a Wanted `C (T2 a1)`.\r\n\r\n4. GHC chooses the appropriate instance, emitting a Wanted `forall a. C (T1 a)`.\r\n\r\n5. GHC skolemizes the `a` to `a2` and tries to solve a Wanted `C (T1 a2)`.\r\n\r\nAnd around and around we go.\r\n\r\n(This loop is guessed at from knowing GHC's algorithms in general. I did not look at a trace.)\r\n\r\nWe ''could'' get this one, though. Before skolemizing, we could stash the Wanted in the `inert_solved_dicts`, which is where we record uses of toplevel instances. (See `Note [Solved dictionaries]` in TcSMonad.) Then, later, when we see the same Wanted arise again, we would just use the cached value, making a wellformed recursive dictionary.\r\n\r\nThis deficiency was discovered in `singletons` (https://github.com/goldfirere/singletons/issues/371). Perhaps that's not \"the wild\", but it's not quite contrived either.\r\n\r\nNote that we don't need two datatypes to trigger this, but having one recursive instance like this seems awfully silly.","type_of_failure":"OtherFailure","blocking":[]} >8.6.3https://gitlab.haskell.org/ghc/ghc//issues/15409Quantified constraints halfwork with equality constraints20200123T19:17:10ZAntCQuantified constraints halfwork with equality constraintsExperimenting from the comments in #15359 ... This is using 8.6.0.alpha2 20180714
```
{# LANGUAGE QuantifiedConstraints #}
 plus the usual suspects
 And over typelevel Booleans
class ((c ~ 'True) => (a ~ 'True),  Surprise 1
(c ~ 'True) => (b ~ 'True))
=> And' (a :: Bool) (b :: Bool) (c :: Bool)  a b > c
instance ()  Surprise 2
=> And' 'True b b
instance (('False ~ 'True) => (b ~ 'True))  Surprise 3
=> And' 'False b 'False
y :: (And' a b 'True) => ()  Surprise 4
y = ()
```
1. Those superclass constraints are accepted, with equalities in the implications.
1. The `And 'True b b` instance is accepted without needing further constraints.
?So GHC can figure the implications hold from looking at the instance head.
1. For the `And' 'False b 'False` instance, GHC can't figure the `(c ~ 'True) => (b ~ 'True)` superclass constraint holds.
Just substituting into the implication from the instance head seems to satisfy it.
So now we have a neversatisfiable antecedent.
Rejection message if instance constraints omitted is
```
* Could not deduce: b ~ 'True
arising from the superclasses of an instance declaration
from the context: 'False ~ 'True
bound by a quantified context at ...
```
1. The signature for `y` is rejected `Could not deduce (And' a0 b0 'True)`.
(The message suggests `AllowAmbiguousTypes`, but that just postpones the error.)
I was hoping the superclass constraints would spot that `c ~ 'True` and improve `a, b` from the implications.
1. No surprise that replacing all the `(~)` with `Coercible` produces the same rejections.
1. I did try putting the whole `And` logic in a class without FunDeps. This was accepted:
```
class (( a ~ 'True) => (b ~ c),
( a ~ 'False) => (c ~ 'False),
( c ~ 'True) => (a ~ 'True),
( c ~ 'True) => (b ~ 'True) )
=> And3 (a :: Bool) (b :: Bool) (c :: Bool)  no FunDep
```
> But attempts to write instances and or/use the class evinced only a torrent of obscure messages, including
```
* Overlapping instances for b ~ 'True
arising from the superclasses of an instance declaration
Matching givens (or their superclasses):
c ~ 'True
bound by a quantified context at ...
Matching instances:
instance [incoherent] forall k (a :: k) (b :: k). (a ~ b) => a ~ b
 Defined in `Data.Type.Equality'
```
> So GHC is creating instances for `(~)` on the fly?
> (I can supply more details if that would help.)
Chiefly I'm thinking that if allowing `(~)` in `QuantifiedConstraints` is only teasing and never effective, there should be a clear rejection message.
*pace* Simon's comments, I don't see any of those `(~)` implications for `And` as "useless" or "redundant".
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.4.3 
 Type  Bug 
 TypeOfFailure  OtherFailure 
 Priority  normal 
 Resolution  Unresolved 
 Component  Compiler 
 Test case  
 Differential revisions  
 BlockedBy  
 Related  
 Blocking  
 CC  
 Operating system  Windows 
 Architecture  
</details>
<! {"blocked_by":[],"summary":"Quantified constraints halfwork with equality constraints","status":"New","operating_system":"Windows","component":"Compiler","related":[],"milestone":"8.6.1","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.4.3","keywords":["QuantifiedConstraints"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"Experimenting from the comments in ticket:15359 ... This is using 8.6.0.alpha2 20180714\r\n\r\n{{{\r\n{# LANGUAGE QuantifiedConstraints #}\r\n  plus the usual suspects\r\n\r\n And over typelevel Booleans\r\n\r\nclass ((c ~ 'True) => (a ~ 'True),  Surprise 1\r\n (c ~ 'True) => (b ~ 'True))\r\n => And' (a :: Bool) (b :: Bool) (c :: Bool)  a b > c\r\n\r\ninstance ()  Surprise 2\r\n => And' 'True b b\r\ninstance (('False ~ 'True) => (b ~ 'True))  Surprise 3\r\n => And' 'False b 'False\r\n\r\ny :: (And' a b 'True) => ()  Surprise 4\r\ny = ()\r\n\r\n}}}\r\n\r\n1. Those superclass constraints are accepted, with equalities in the implications.\r\n\r\n2. The `And 'True b b` instance is accepted without needing further constraints.\r\n ?So GHC can figure the implications hold from looking at the instance head.\r\n\r\n3. For the `And' 'False b 'False` instance, GHC can't figure the `(c ~ 'True) => (b ~ 'True)` superclass constraint holds.\r\n Just substituting into the implication from the instance head seems to satisfy it.\r\n So now we have a neversatisfiable antecedent.\r\n Rejection message if instance constraints omitted is\r\n\r\n{{{\r\n * Could not deduce: b ~ 'True\r\n arising from the superclasses of an instance declaration\r\n from the context: 'False ~ 'True\r\n bound by a quantified context at ...\r\n}}}\r\n\r\n4. The signature for `y` is rejected `Could not deduce (And' a0 b0 'True)`.\r\n (The message suggests `AllowAmbiguousTypes`, but that just postpones the error.)\r\n\r\nI was hoping the superclass constraints would spot that `c ~ 'True` and improve `a, b` from the implications.\r\n\r\n5. No surprise that replacing all the `(~)` with `Coercible` produces the same rejections.\r\n\r\n6. I did try putting the whole `And` logic in a class without FunDeps. This was accepted:\r\n\r\n{{{\r\nclass (( a ~ 'True) => (b ~ c),\r\n ( a ~ 'False) => (c ~ 'False),\r\n ( c ~ 'True) => (a ~ 'True),\r\n ( c ~ 'True) => (b ~ 'True) )\r\n => And3 (a :: Bool) (b :: Bool) (c :: Bool)  no FunDep\r\n\r\n}}}\r\n\r\n But attempts to write instances and or/use the class evinced only a torrent of obscure messages, including\r\n\r\n{{{\r\n * Overlapping instances for b ~ 'True\r\n arising from the superclasses of an instance declaration\r\n Matching givens (or their superclasses):\r\n c ~ 'True\r\n bound by a quantified context at ...\r\n Matching instances:\r\n instance [incoherent] forall k (a :: k) (b :: k). (a ~ b) => a ~ b\r\n  Defined in `Data.Type.Equality'\r\n}}}\r\n\r\n So GHC is creating instances for `(~)` on the fly?\r\n\r\n (I can supply more details if that would help.)\r\n\r\nChiefly I'm thinking that if allowing `(~)` in `QuantifiedConstraints` is only teasing and never effective, there should be a clear rejection message.\r\n\r\n''pace'' Simon's comments, I don't see any of those `(~)` implications for `And` as \"useless\" or \"redundant\".","type_of_failure":"OtherFailure","blocking":[]} >Experimenting from the comments in #15359 ... This is using 8.6.0.alpha2 20180714
```
{# LANGUAGE QuantifiedConstraints #}
 plus the usual suspects
 And over typelevel Booleans
class ((c ~ 'True) => (a ~ 'True),  Surprise 1
(c ~ 'True) => (b ~ 'True))
=> And' (a :: Bool) (b :: Bool) (c :: Bool)  a b > c
instance ()  Surprise 2
=> And' 'True b b
instance (('False ~ 'True) => (b ~ 'True))  Surprise 3
=> And' 'False b 'False
y :: (And' a b 'True) => ()  Surprise 4
y = ()
```
1. Those superclass constraints are accepted, with equalities in the implications.
1. The `And 'True b b` instance is accepted without needing further constraints.
?So GHC can figure the implications hold from looking at the instance head.
1. For the `And' 'False b 'False` instance, GHC can't figure the `(c ~ 'True) => (b ~ 'True)` superclass constraint holds.
Just substituting into the implication from the instance head seems to satisfy it.
So now we have a neversatisfiable antecedent.
Rejection message if instance constraints omitted is
```
* Could not deduce: b ~ 'True
arising from the superclasses of an instance declaration
from the context: 'False ~ 'True
bound by a quantified context at ...
```
1. The signature for `y` is rejected `Could not deduce (And' a0 b0 'True)`.
(The message suggests `AllowAmbiguousTypes`, but that just postpones the error.)
I was hoping the superclass constraints would spot that `c ~ 'True` and improve `a, b` from the implications.
1. No surprise that replacing all the `(~)` with `Coercible` produces the same rejections.
1. I did try putting the whole `And` logic in a class without FunDeps. This was accepted:
```
class (( a ~ 'True) => (b ~ c),
( a ~ 'False) => (c ~ 'False),
( c ~ 'True) => (a ~ 'True),
( c ~ 'True) => (b ~ 'True) )
=> And3 (a :: Bool) (b :: Bool) (c :: Bool)  no FunDep
```
> But attempts to write instances and or/use the class evinced only a torrent of obscure messages, including
```
* Overlapping instances for b ~ 'True
arising from the superclasses of an instance declaration
Matching givens (or their superclasses):
c ~ 'True
bound by a quantified context at ...
Matching instances:
instance [incoherent] forall k (a :: k) (b :: k). (a ~ b) => a ~ b
 Defined in `Data.Type.Equality'
```
> So GHC is creating instances for `(~)` on the fly?
> (I can supply more details if that would help.)
Chiefly I'm thinking that if allowing `(~)` in `QuantifiedConstraints` is only teasing and never effective, there should be a clear rejection message.
*pace* Simon's comments, I don't see any of those `(~)` implications for `And` as "useless" or "redundant".
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.4.3 
 Type  Bug 
 TypeOfFailure  OtherFailure 
 Priority  normal 
 Resolution  Unresolved 
 Component  Compiler 
 Test case  
 Differential revisions  
 BlockedBy  
 Related  
 Blocking  
 CC  
 Operating system  Windows 
 Architecture  
</details>
<! {"blocked_by":[],"summary":"Quantified constraints halfwork with equality constraints","status":"New","operating_system":"Windows","component":"Compiler","related":[],"milestone":"8.6.1","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.4.3","keywords":["QuantifiedConstraints"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"Experimenting from the comments in ticket:15359 ... This is using 8.6.0.alpha2 20180714\r\n\r\n{{{\r\n{# LANGUAGE QuantifiedConstraints #}\r\n  plus the usual suspects\r\n\r\n And over typelevel Booleans\r\n\r\nclass ((c ~ 'True) => (a ~ 'True),  Surprise 1\r\n (c ~ 'True) => (b ~ 'True))\r\n => And' (a :: Bool) (b :: Bool) (c :: Bool)  a b > c\r\n\r\ninstance ()  Surprise 2\r\n => And' 'True b b\r\ninstance (('False ~ 'True) => (b ~ 'True))  Surprise 3\r\n => And' 'False b 'False\r\n\r\ny :: (And' a b 'True) => ()  Surprise 4\r\ny = ()\r\n\r\n}}}\r\n\r\n1. Those superclass constraints are accepted, with equalities in the implications.\r\n\r\n2. The `And 'True b b` instance is accepted without needing further constraints.\r\n ?So GHC can figure the implications hold from looking at the instance head.\r\n\r\n3. For the `And' 'False b 'False` instance, GHC can't figure the `(c ~ 'True) => (b ~ 'True)` superclass constraint holds.\r\n Just substituting into the implication from the instance head seems to satisfy it.\r\n So now we have a neversatisfiable antecedent.\r\n Rejection message if instance constraints omitted is\r\n\r\n{{{\r\n * Could not deduce: b ~ 'True\r\n arising from the superclasses of an instance declaration\r\n from the context: 'False ~ 'True\r\n bound by a quantified context at ...\r\n}}}\r\n\r\n4. The signature for `y` is rejected `Could not deduce (And' a0 b0 'True)`.\r\n (The message suggests `AllowAmbiguousTypes`, but that just postpones the error.)\r\n\r\nI was hoping the superclass constraints would spot that `c ~ 'True` and improve `a, b` from the implications.\r\n\r\n5. No surprise that replacing all the `(~)` with `Coercible` produces the same rejections.\r\n\r\n6. I did try putting the whole `And` logic in a class without FunDeps. This was accepted:\r\n\r\n{{{\r\nclass (( a ~ 'True) => (b ~ c),\r\n ( a ~ 'False) => (c ~ 'False),\r\n ( c ~ 'True) => (a ~ 'True),\r\n ( c ~ 'True) => (b ~ 'True) )\r\n => And3 (a :: Bool) (b :: Bool) (c :: Bool)  no FunDep\r\n\r\n}}}\r\n\r\n But attempts to write instances and or/use the class evinced only a torrent of obscure messages, including\r\n\r\n{{{\r\n * Overlapping instances for b ~ 'True\r\n arising from the superclasses of an instance declaration\r\n Matching givens (or their superclasses):\r\n c ~ 'True\r\n bound by a quantified context at ...\r\n Matching instances:\r\n instance [incoherent] forall k (a :: k) (b :: k). (a ~ b) => a ~ b\r\n  Defined in `Data.Type.Equality'\r\n}}}\r\n\r\n So GHC is creating instances for `(~)` on the fly?\r\n\r\n (I can supply more details if that would help.)\r\n\r\nChiefly I'm thinking that if allowing `(~)` in `QuantifiedConstraints` is only teasing and never effective, there should be a clear rejection message.\r\n\r\n''pace'' Simon's comments, I don't see any of those `(~)` implications for `And` as \"useless\" or \"redundant\".","type_of_failure":"OtherFailure","blocking":[]} >9.0.1https://gitlab.haskell.org/ghc/ghc//issues/15351QuantifiedConstraints ignore FunctionalDependencies20201203T08:24:56ZaaronvargoQuantifiedConstraints ignore FunctionalDependenciesThe following code fails to compile:
```hs
{# LANGUAGE QuantifiedConstraints #}
{# LANGUAGE FunctionalDependencies #}
class C a b  a > b where
foo :: a > b
bar :: (forall a. C (f a) Int) => f a > String
bar = show . foo
```
```
• Could not deduce (Show a0) arising from a use of ‘show’
...
The type variable ‘a0’ is ambiguous
• Could not deduce (C (f a) a0) arising from a use of ‘foo’
...
The type variable ‘a0’ is ambiguous
```
Yet it ought to work, since this is perfectly fine with toplevel instances:
```hs
instance C [a] Int where ...
baz :: [a] > String
baz = show . foo
```The following code fails to compile:
```hs
{# LANGUAGE QuantifiedConstraints #}
{# LANGUAGE FunctionalDependencies #}
class C a b  a > b where
foo :: a > b
bar :: (forall a. C (f a) Int) => f a > String
bar = show . foo
```
```
• Could not deduce (Show a0) arising from a use of ‘show’
...
The type variable ‘a0’ is ambiguous
• Could not deduce (C (f a) a0) arising from a use of ‘foo’
...
The type variable ‘a0’ is ambiguous
```
Yet it ought to work, since this is perfectly fine with toplevel instances:
```hs
instance C [a] Int where ...
baz :: [a] > String
baz = show . foo
```https://gitlab.haskell.org/ghc/ghc//issues/15347QuantifiedConstraints: Implication constraints with type families don't work20190918T06:46:06ZaaronvargoQuantifiedConstraints: Implication constraints with type families don't workThis may be related to #14860, but I think it's different.
The following code fails to compile:
```hs
{# LANGUAGE QuantifiedConstraints #}
{# LANGUAGE TypeFamilies #}
{# LANGUAGE AllowAmbiguousTypes #}
{# LANGUAGE RankNTypes #}
{# LANGUAGE GADTs #}
{# LANGUAGE ConstraintKinds #}
import Prelude()
import Data.Kind
data Dict c = c => Dict
type family F a :: Constraint
foo :: forall a b. (a => F b, a) => Dict (F b)
foo = Dict
```
```
• Could not deduce: F b arising from a use of ‘Dict’
from the context: (a => F b, a)
```
Yet the following all do compile:
```hs
bar :: forall a. F a => Dict (F a)
bar = Dict
baz :: forall a b. (a => b, a) => Dict b
baz = Dict
qux :: forall a b c. (a => c, a, c ~ F b) => Dict (F b)
qux = Dict
```
It seems that a wanted `F b` can be solved with a given `F b`, but not with a given `a => F b`, which is bizarre. The fact that `qux` still works is also strange, as it means that you get a different result if you first simplify by substituting `c = F b`.
As a more practical example, the following similarly fails to compile, due to the `Cod f` type family:
```hs
 in addition to the above extensions
{# LANGUAGE FlexibleContexts #}
{# LANGUAGE MultiParamTypeClasses #}
{# LANGUAGE FunctionalDependencies #}
class Ob p a
class (forall a. Ob (Dom f) a => Ob (Cod f) (f a)) => Functor f where
type Dom f
type Cod f
liftOb :: forall f a. (Functor f, Ob (Dom f) a) => Dict (Ob (Cod f) (f a))
liftOb = Dict
```
While a version which uses fundeps instead does compile:
```hs
class (forall a. Ob dom a => Ob cod (f a)) => Functor dom cod f  f > dom cod
liftOb :: forall f a dom cod. (Functor dom cod f, Ob dom a) => Dict (Ob cod (f a))
liftOb = Dict
```This may be related to #14860, but I think it's different.
The following code fails to compile:
```hs
{# LANGUAGE QuantifiedConstraints #}
{# LANGUAGE TypeFamilies #}
{# LANGUAGE AllowAmbiguousTypes #}
{# LANGUAGE RankNTypes #}
{# LANGUAGE GADTs #}
{# LANGUAGE ConstraintKinds #}
import Prelude()
import Data.Kind
data Dict c = c => Dict
type family F a :: Constraint
foo :: forall a b. (a => F b, a) => Dict (F b)
foo = Dict
```
```
• Could not deduce: F b arising from a use of ‘Dict’
from the context: (a => F b, a)
```
Yet the following all do compile:
```hs
bar :: forall a. F a => Dict (F a)
bar = Dict
baz :: forall a b. (a => b, a) => Dict b
baz = Dict
qux :: forall a b c. (a => c, a, c ~ F b) => Dict (F b)
qux = Dict
```
It seems that a wanted `F b` can be solved with a given `F b`, but not with a given `a => F b`, which is bizarre. The fact that `qux` still works is also strange, as it means that you get a different result if you first simplify by substituting `c = F b`.
As a more practical example, the following similarly fails to compile, due to the `Cod f` type family:
```hs
 in addition to the above extensions
{# LANGUAGE FlexibleContexts #}
{# LANGUAGE MultiParamTypeClasses #}
{# LANGUAGE FunctionalDependencies #}
class Ob p a
class (forall a. Ob (Dom f) a => Ob (Cod f) (f a)) => Functor f where
type Dom f
type Cod f
liftOb :: forall f a. (Functor f, Ob (Dom f) a) => Dict (Ob (Cod f) (f a))
liftOb = Dict
```
While a version which uses fundeps instead does compile:
```hs
class (forall a. Ob dom a => Ob cod (f a)) => Functor dom cod f  f > dom cod
liftOb :: forall f a dom cod. (Functor dom cod f, Ob dom a) => Dict (Ob cod (f a))
liftOb = Dict
```https://gitlab.haskell.org/ghc/ghc//issues/15020PatternSynonyms: Problems with quantified constraints / foralls20200123T19:26:36ZIcelandjackPatternSynonyms: Problems with quantified constraints / forallsI couldn't find a way to implement `PLam2` as a simply bidirectional pattern synonym, I expected it to work but I recall a similar ticket. I couldn't find it though.
```hs
{# Language RankNTypes, PatternSynonyms, ViewPatterns #}
newtype Lam1 = Lam1 (forall xx mm. Monad mm => mm xx)
pattern PLam1 :: (forall xx mm. Monad mm => mm xx) > Lam1
pattern PLam1 a = Lam1 a

newtype Lam2 a = Lam2 (forall mm. Monad mm => mm a)
newtype Forall f = Forall (forall xx. f xx)
 · FAILS ·
 pattern PLam2 :: (forall xx mm. Monad mm => mm xx) > Forall Lam2
 pattern PLam2 lam = Forall (Lam2 lam)

get :: Forall Lam2 > forall xx mm. Monad mm => mm xx
get (Forall (Lam2 lam)) = lam
pattern PLam3 :: (forall xx mm. Monad mm => mm xx) > Forall Lam2
pattern PLam3 lam < (get > lam)
where PLam3 lam = Forall (Lam2 lam)
```
The complaint is `V`, I wonder if this is a limitation of PatternSynonyms
```
• Couldn't match type ‘xx0’ with ‘xx’
because type variable ‘xx’ would escape its scope
This (rigid, skolem) type variable is bound by
a type expected by the context:
forall xx (mm :: * > *). Monad mm => mm xx
at Test.hs:16:3436
Expected type: mm xx
Actual type: mm xx0
• In the declaration for pattern synonym ‘PLam2’
• Relevant bindings include
lam :: forall (mm :: * > *). Monad mm => mm xx0
(bound at Test.hs:16:34)

16  pattern PLam2 lam = Forall (Lam2 lam)
 ^^^
```I couldn't find a way to implement `PLam2` as a simply bidirectional pattern synonym, I expected it to work but I recall a similar ticket. I couldn't find it though.
```hs
{# Language RankNTypes, PatternSynonyms, ViewPatterns #}
newtype Lam1 = Lam1 (forall xx mm. Monad mm => mm xx)
pattern PLam1 :: (forall xx mm. Monad mm => mm xx) > Lam1
pattern PLam1 a = Lam1 a

newtype Lam2 a = Lam2 (forall mm. Monad mm => mm a)
newtype Forall f = Forall (forall xx. f xx)
 · FAILS ·
 pattern PLam2 :: (forall xx mm. Monad mm => mm xx) > Forall Lam2
 pattern PLam2 lam = Forall (Lam2 lam)

get :: Forall Lam2 > forall xx mm. Monad mm => mm xx
get (Forall (Lam2 lam)) = lam
pattern PLam3 :: (forall xx mm. Monad mm => mm xx) > Forall Lam2
pattern PLam3 lam < (get > lam)
where PLam3 lam = Forall (Lam2 lam)
```
The complaint is `V`, I wonder if this is a limitation of PatternSynonyms
```
• Couldn't match type ‘xx0’ with ‘xx’
because type variable ‘xx’ would escape its scope
This (rigid, skolem) type variable is bound by
a type expected by the context:
forall xx (mm :: * > *). Monad mm => mm xx
at Test.hs:16:3436
Expected type: mm xx
Actual type: mm xx0
• In the declaration for pattern synonym ‘PLam2’
• Relevant bindings include
lam :: forall (mm :: * > *). Monad mm => mm xx0
(bound at Test.hs:16:34)

16  pattern PLam2 lam = Forall (Lam2 lam)
 ^^^
```https://gitlab.haskell.org/ghc/ghc//issues/14995QuantifiedConstraints: Incorrect pretty printing20190707T18:14:45ZIcelandjackQuantifiedConstraints: Incorrect pretty printingThis code from [OutsideIn(X)](https://www.microsoft.com/enus/research/wpcontent/uploads/2016/02/jfpoutsidein.pdf) compiles
```hs
{# Language FlexibleInstances, MultiParamTypeClasses, GADTs, QuantifiedConstraints #}
class C a
class B a b where op :: a > b
instance C a => B a [a] where op = undefined
data R a where
MkR :: C a => a > R a
k :: (C a => B a b) => R a > b
k (MkR x) = op x
```
but prettyprinting `k` prints `B a b => ..` instead of `(C a => B a b) => ..`
```
$ ghci ignoredotghci hs/228bug.hs
GHCi, version 8.5.20180128: http://www.haskell.org/ghc/ :? for help
[1 of 1] Compiling Main ( hs/228bug.hs, interpreted )
Ok, one module loaded.
*Main> :t k
k :: B a b => R a > b
*Main>
```This code from [OutsideIn(X)](https://www.microsoft.com/enus/research/wpcontent/uploads/2016/02/jfpoutsidein.pdf) compiles
```hs
{# Language FlexibleInstances, MultiParamTypeClasses, GADTs, QuantifiedConstraints #}
class C a
class B a b where op :: a > b
instance C a => B a [a] where op = undefined
data R a where
MkR :: C a => a > R a
k :: (C a => B a b) => R a > b
k (MkR x) = op x
```
but prettyprinting `k` prints `B a b => ..` instead of `(C a => B a b) => ..`
```
$ ghci ignoredotghci hs/228bug.hs
GHCi, version 8.5.20180128: http://www.haskell.org/ghc/ :? for help
[1 of 1] Compiling Main ( hs/228bug.hs, interpreted )
Ok, one module loaded.
*Main> :t k
k :: B a b => R a > b
*Main>
```https://gitlab.haskell.org/ghc/ghc//issues/14958QuantifiedConstraints: Doesn't apply implication for existential?20190707T18:14:53ZIcelandjackQuantifiedConstraints: Doesn't apply implication for existential?This fails
```hs
{# Language GADTs, RankNTypes, ConstraintKinds, QuantifiedConstraints, AllowAmbiguousTypes #}
data Foo where
Foo :: (forall x. ((forall y. cls y => Num y), cls x) => x) > Foo
a :: Foo
a = Foo 10
```
```
$ ... ignoredotghci /tmp/Optic.hs
GHCi, version 8.5.20180128: http://www.haskell.org/ghc/ :? for help
[1 of 1] Compiling Main ( /tmp/Optic.hs, interpreted )
/tmp/Optic.hs:7:9: error:
• Could not deduce (Num x) arising from the literal ‘10’
from the context: (forall y. cls0 y => Num y, cls0 x)
bound by a type expected by the context:
forall x. (forall y. cls0 y => Num y, cls0 x) => x
at /tmp/Optic.hs:7:510
Possible fix:
add (Num x) to the context of
a type expected by the context:
forall x. (forall y. cls0 y => Num y, cls0 x) => x
• In the first argument of ‘Foo’, namely ‘10’
In the expression: Foo 10
In an equation for ‘a’: a = Foo 10

7  a = Foo 10
 ^^
Failed, no modules loaded.
Prelude>
```
GHC knows that `cls ~=> Num` but still GHC cannot deduce `Num x` from `cls x`.

The reason for trying this is creating a `newtype` for optics where we still get subsumption
```hs
{# Language GADTs, RankNTypes, ConstraintKinds, QuantifiedConstraints, AllowAmbiguousTypes, ApplicativeDo, TypeOperators, MultiParamTypeClasses, FlexibleInstances, UndecidableInstances, PolyKinds, FlexibleContexts #}
data Optic cls s a where
Optic :: (forall f. cls f => (a > f a) > (s > f s)) > Optic cls s a
class (forall x. f x => g x) => (f ~=> g)
instance (forall x. f x => g x) => (f ~=> g)
_1 :: cls ~=> Functor => Optic cls (a, b) a
_1 = Optic $ \f (a, b) > do
a' < f a
pure (a', b)
lens_1 :: Optic Functor (a, b) a
lens_1 = _1
trav_1 :: Optic Applicative (a, b) a
trav_1 = _1
```
and I wanted to move `cls ~=> Functor` into the `Optic` type itself.
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.5 
 Type  Bug 
 TypeOfFailure  OtherFailure 
 Priority  normal 
 Resolution  Unresolved 
 Component  Compiler 
 Test case  
 Differential revisions  
 BlockedBy  
 Related  
 Blocking  
 CC  
 Operating system  
 Architecture  
</details>
<! {"blocked_by":[],"summary":"QuantifiedConstraints: Doesn't apply implication for existential?","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.5","keywords":["QuantifiedConstraints,","wipT2893"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"This fails\r\n\r\n{{{#!hs\r\n{# Language GADTs, RankNTypes, ConstraintKinds, QuantifiedConstraints, AllowAmbiguousTypes #}\r\n\r\ndata Foo where\r\n Foo :: (forall x. ((forall y. cls y => Num y), cls x) => x) > Foo\r\n\r\na :: Foo\r\na = Foo 10\r\n}}}\r\n\r\n{{{\r\n$ ... ignoredotghci /tmp/Optic.hs\r\nGHCi, version 8.5.20180128: http://www.haskell.org/ghc/ :? for help\r\n[1 of 1] Compiling Main ( /tmp/Optic.hs, interpreted )\r\n\r\n/tmp/Optic.hs:7:9: error:\r\n • Could not deduce (Num x) arising from the literal ‘10’\r\n from the context: (forall y. cls0 y => Num y, cls0 x)\r\n bound by a type expected by the context:\r\n forall x. (forall y. cls0 y => Num y, cls0 x) => x\r\n at /tmp/Optic.hs:7:510\r\n Possible fix:\r\n add (Num x) to the context of\r\n a type expected by the context:\r\n forall x. (forall y. cls0 y => Num y, cls0 x) => x\r\n • In the first argument of ‘Foo’, namely ‘10’\r\n In the expression: Foo 10\r\n In an equation for ‘a’: a = Foo 10\r\n \r\n7  a = Foo 10\r\n  ^^\r\nFailed, no modules loaded.\r\nPrelude> \r\n}}}\r\n\r\nGHC knows that `cls ~=> Num` but still GHC cannot deduce `Num x` from `cls x`.\r\n\r\n\r\n\r\nThe reason for trying this is creating a `newtype` for optics where we still get subsumption \r\n\r\n{{{#!hs\r\n{# Language GADTs, RankNTypes, ConstraintKinds, QuantifiedConstraints, AllowAmbiguousTypes, ApplicativeDo, TypeOperators, MultiParamTypeClasses, FlexibleInstances, UndecidableInstances, PolyKinds, FlexibleContexts #}\r\n\r\ndata Optic cls s a where\r\n Optic :: (forall f. cls f => (a > f a) > (s > f s)) > Optic cls s a\r\n\r\nclass (forall x. f x => g x) => (f ~=> g)\r\ninstance (forall x. f x => g x) => (f ~=> g)\r\n\r\n_1 :: cls ~=> Functor => Optic cls (a, b) a\r\n_1 = Optic $ \\f (a, b) > do\r\n a' < f a\r\n pure (a', b)\r\n\r\nlens_1 :: Optic Functor (a, b) a\r\nlens_1 = _1\r\n\r\ntrav_1 :: Optic Applicative (a, b) a\r\ntrav_1 = _1\r\n}}}\r\n\r\nand I wanted to move `cls ~=> Functor` into the `Optic` type itself.","type_of_failure":"OtherFailure","blocking":[]} >This fails
```hs
{# Language GADTs, RankNTypes, ConstraintKinds, QuantifiedConstraints, AllowAmbiguousTypes #}
data Foo where
Foo :: (forall x. ((forall y. cls y => Num y), cls x) => x) > Foo
a :: Foo
a = Foo 10
```
```
$ ... ignoredotghci /tmp/Optic.hs
GHCi, version 8.5.20180128: http://www.haskell.org/ghc/ :? for help
[1 of 1] Compiling Main ( /tmp/Optic.hs, interpreted )
/tmp/Optic.hs:7:9: error:
• Could not deduce (Num x) arising from the literal ‘10’
from the context: (forall y. cls0 y => Num y, cls0 x)
bound by a type expected by the context:
forall x. (forall y. cls0 y => Num y, cls0 x) => x
at /tmp/Optic.hs:7:510
Possible fix:
add (Num x) to the context of
a type expected by the context:
forall x. (forall y. cls0 y => Num y, cls0 x) => x
• In the first argument of ‘Foo’, namely ‘10’
In the expression: Foo 10
In an equation for ‘a’: a = Foo 10

7  a = Foo 10
 ^^
Failed, no modules loaded.
Prelude>
```
GHC knows that `cls ~=> Num` but still GHC cannot deduce `Num x` from `cls x`.

The reason for trying this is creating a `newtype` for optics where we still get subsumption
```hs
{# Language GADTs, RankNTypes, ConstraintKinds, QuantifiedConstraints, AllowAmbiguousTypes, ApplicativeDo, TypeOperators, MultiParamTypeClasses, FlexibleInstances, UndecidableInstances, PolyKinds, FlexibleContexts #}
data Optic cls s a where
Optic :: (forall f. cls f => (a > f a) > (s > f s)) > Optic cls s a
class (forall x. f x => g x) => (f ~=> g)
instance (forall x. f x => g x) => (f ~=> g)
_1 :: cls ~=> Functor => Optic cls (a, b) a
_1 = Optic $ \f (a, b) > do
a' < f a
pure (a', b)
lens_1 :: Optic Functor (a, b) a
lens_1 = _1
trav_1 :: Optic Applicative (a, b) a
trav_1 = _1
```
and I wanted to move `cls ~=> Functor` into the `Optic` type itself.
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.5 
 Type  Bug 
 TypeOfFailure  OtherFailure 
 Priority  normal 
 Resolution  Unresolved 
 Component  Compiler 
 Test case  
 Differential revisions  
 BlockedBy  
 Related  
 Blocking  
 CC  
 Operating system  
 Architecture  
</details>
<! {"blocked_by":[],"summary":"QuantifiedConstraints: Doesn't apply implication for existential?","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.5","keywords":["QuantifiedConstraints,","wipT2893"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"This fails\r\n\r\n{{{#!hs\r\n{# Language GADTs, RankNTypes, ConstraintKinds, QuantifiedConstraints, AllowAmbiguousTypes #}\r\n\r\ndata Foo where\r\n Foo :: (forall x. ((forall y. cls y => Num y), cls x) => x) > Foo\r\n\r\na :: Foo\r\na = Foo 10\r\n}}}\r\n\r\n{{{\r\n$ ... ignoredotghci /tmp/Optic.hs\r\nGHCi, version 8.5.20180128: http://www.haskell.org/ghc/ :? for help\r\n[1 of 1] Compiling Main ( /tmp/Optic.hs, interpreted )\r\n\r\n/tmp/Optic.hs:7:9: error:\r\n • Could not deduce (Num x) arising from the literal ‘10’\r\n from the context: (forall y. cls0 y => Num y, cls0 x)\r\n bound by a type expected by the context:\r\n forall x. (forall y. cls0 y => Num y, cls0 x) => x\r\n at /tmp/Optic.hs:7:510\r\n Possible fix:\r\n add (Num x) to the context of\r\n a type expected by the context:\r\n forall x. (forall y. cls0 y => Num y, cls0 x) => x\r\n • In the first argument of ‘Foo’, namely ‘10’\r\n In the expression: Foo 10\r\n In an equation for ‘a’: a = Foo 10\r\n \r\n7  a = Foo 10\r\n  ^^\r\nFailed, no modules loaded.\r\nPrelude> \r\n}}}\r\n\r\nGHC knows that `cls ~=> Num` but still GHC cannot deduce `Num x` from `cls x`.\r\n\r\n\r\n\r\nThe reason for trying this is creating a `newtype` for optics where we still get subsumption \r\n\r\n{{{#!hs\r\n{# Language GADTs, RankNTypes, ConstraintKinds, QuantifiedConstraints, AllowAmbiguousTypes, ApplicativeDo, TypeOperators, MultiParamTypeClasses, FlexibleInstances, UndecidableInstances, PolyKinds, FlexibleContexts #}\r\n\r\ndata Optic cls s a where\r\n Optic :: (forall f. cls f => (a > f a) > (s > f s)) > Optic cls s a\r\n\r\nclass (forall x. f x => g x) => (f ~=> g)\r\ninstance (forall x. f x => g x) => (f ~=> g)\r\n\r\n_1 :: cls ~=> Functor => Optic cls (a, b) a\r\n_1 = Optic $ \\f (a, b) > do\r\n a' < f a\r\n pure (a', b)\r\n\r\nlens_1 :: Optic Functor (a, b) a\r\nlens_1 = _1\r\n\r\ntrav_1 :: Optic Applicative (a, b) a\r\ntrav_1 = _1\r\n}}}\r\n\r\nand I wanted to move `cls ~=> Functor` into the `Optic` type itself.","type_of_failure":"OtherFailure","blocking":[]} >https://gitlab.haskell.org/ghc/ghc//issues/14896QuantifiedConstraints: GHC does doesn't discharge constraints if they are qua...20190707T18:15:08ZIcelandjackQuantifiedConstraints: GHC does doesn't discharge constraints if they are quantifiedThis came up on a [reddit thread](https://www.reddit.com/r/haskell/comments/8257mz/how_quantifiedconstraints_can_let_us_put_join/dv8hfxb/),
```hs
{# Language QuantifiedConstraints #}
class (forall aa. Functor (bi aa)) => Bifunctor bi where
first :: (a > a') > (bi a b > bi a' b)
bimap :: Bifunctor bi => (a > a') > (b > b') > (bi a b > bi a' b')
bimap f g = first f . fmap g
```
This is the type we want for `bimap` even if we mix & match `Bifunctor` and `Functor`. We already know that we can `fmap @(bi xx)` for any `xx` but this is not the inferred type.
Instead GHC infers a type (tidied up) with a superfluous `Functor` constraint
```hs
bimap :: (Bifunctor bi, Functor (bi a)) => (a > a') > (b > b') > (bi a b > bi a' b')
```
Indeed postcomposing with a superfluous `fmap @(bi a') id` incurs yet another `Functor` constraint
```hs
bimap :: (Bifunctor bi, Functor (bi a), Functor (bi a')) => (a > a') > (b > b') > (bi a b > bi a' b')
bimap f g = fmap id . first f . fmap g
```
A terminology question, I'm not sure how to phrase what GHC isn't doing to the `Functor` constraints: ‘discharge’?This came up on a [reddit thread](https://www.reddit.com/r/haskell/comments/8257mz/how_quantifiedconstraints_can_let_us_put_join/dv8hfxb/),
```hs
{# Language QuantifiedConstraints #}
class (forall aa. Functor (bi aa)) => Bifunctor bi where
first :: (a > a') > (bi a b > bi a' b)
bimap :: Bifunctor bi => (a > a') > (b > b') > (bi a b > bi a' b')
bimap f g = first f . fmap g
```
This is the type we want for `bimap` even if we mix & match `Bifunctor` and `Functor`. We already know that we can `fmap @(bi xx)` for any `xx` but this is not the inferred type.
Instead GHC infers a type (tidied up) with a superfluous `Functor` constraint
```hs
bimap :: (Bifunctor bi, Functor (bi a)) => (a > a') > (b > b') > (bi a b > bi a' b')
```
Indeed postcomposing with a superfluous `fmap @(bi a') id` incurs yet another `Functor` constraint
```hs
bimap :: (Bifunctor bi, Functor (bi a), Functor (bi a')) => (a > a') > (b > b') > (bi a b > bi a' b')
bimap f g = fmap id . first f . fmap g
```
A terminology question, I'm not sure how to phrase what GHC isn't doing to the `Functor` constraints: ‘discharge’?