GHC issueshttps://gitlab.haskell.org/ghc/ghc//issues20201021T22:23:07Zhttps://gitlab.haskell.org/ghc/ghc//issues/18873Quantified equality constraints are not used for rewriting20201021T22:23:07ZRichard Eisenbergrae@richarde.devQuantified equality constraints are not used for rewritingIf I say
```hs
type family F a b where
F [_] b = b
f :: forall a b. (a ~ [b]) => F a b > b
f x = x
```
GHC smiles upon me: the equality constraint rewrites `a` to `[b]`, and then `F [b] b` can reduce to `b`, and all is well.
But if I say
```hs
type family F a b where
F [_] b = b
class Truth
instance Truth
f :: forall a b. (Truth => a ~ [b]) => F a b > b
f x = x
```
I get an error, saying `F a b` does not match `b`. This is because the equality, hidden behind `Truth`, is not used for rewriting, and thus GHC cannot figure out that `F a b` can reduce.
I don't see an easy solution here.
This isn't just me grousing: a problem on !4149 could be worked around if GHC used such equalities for rewriting. And so if we can solve this problem, we can solve the other one. My expectation is that we won't solve this one, though.If I say
```hs
type family F a b where
F [_] b = b
f :: forall a b. (a ~ [b]) => F a b > b
f x = x
```
GHC smiles upon me: the equality constraint rewrites `a` to `[b]`, and then `F [b] b` can reduce to `b`, and all is well.
But if I say
```hs
type family F a b where
F [_] b = b
class Truth
instance Truth
f :: forall a b. (Truth => a ~ [b]) => F a b > b
f x = x
```
I get an error, saying `F a b` does not match `b`. This is because the equality, hidden behind `Truth`, is not used for rewriting, and thus GHC cannot figure out that `F a b` can reduce.
I don't see an easy solution here.
This isn't just me grousing: a problem on !4149 could be worked around if GHC used such equalities for rewriting. And so if we can solve this problem, we can solve the other one. My expectation is that we won't solve this one, though.https://gitlab.haskell.org/ghc/ghc//issues/18213GND generates code that instantiates coerce too much20201031T21:03:41ZRyan ScottGND generates code that instantiates coerce too muchConsider this code from https://gitlab.haskell.org/ghc/ghc/issues/18148#note_270603:
```hs
{# LANGUAGE AllowAmbiguousTypes #}
{# LANGUAGE DataKinds #}
{# LANGUAGE DerivingStrategies #}
{# LANGUAGE FlexibleInstances #}
{# LANGUAGE GeneralizedNewtypeDeriving #}
{# LANGUAGE PolyKinds #}
{# LANGUAGE ScopedTypeVariables #}
{# LANGUAGE StandaloneDeriving #}
module Bug where
class Foo a where
bar :: forall (x :: a). ()
bar = ()
instance Foo Int
newtype Quux a = Quux a
 deriving newtype instance _ => Foo (Quux Int)
deriving newtype instance Foo (Quux Int)
```
This typechecks in GHC 8.10.1. However, if you comment out the original `deriving newtype instance Foo (Quux Int)` line and uncomment the very similar line above it, it no longer typechecks:
```
Bug.hs:19:1: error:
• Couldn't match type ‘Int’ with ‘Quux Int’
arising from the coercion of the method ‘bar’
from type ‘forall (x :: Int). ()’
to type ‘forall (x :: Quux Int). ()’
• When deriving the instance for (Foo (Quux Int))

19  deriving newtype instance _ => Foo (Quux Int)
 ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
```
This is a strange inconsistency, given how similar these standalone `deriving` declarations are. Why does the original succeed but the line above it fail?
As it turns out, both of these really ought to fail, but the original only succeeds due to an unfortunate fluke in the way `GeneralizedNewtypeDeriving` works. Here is the code that the original declaration generates (with `ddumpderiv`):
```
==================== Derived instances ====================
Derived class instances:
instance Bug.Foo (Bug.Quux GHC.Types.Int) where
Bug.bar
= GHC.Prim.coerce @() @() (Bug.bar @GHC.Types.Int) ::
forall (x_aKF :: Bug.Quux GHC.Types.Int). ()
```
Notice that we are instantiating `coerce` with `@() @()`. But this is blatantly wrong—it really ought to be `coerce @(forall (x :: Int). ()) @(forall (x :: Quux Int). ())`, which the typechecker would reject (as it should). But GND generates `coerce @() @()` instead, and as a result, the use of `bar` on the RHS gets instantiated with `@Any`, which is not what was intended at all.
In contrast, the `deriving newtype instance _ => Foo (Quux Int)` line infers a `Coercible (forall (x :: Int). ()) (forall (x :: Quux Int). ())` constraint, which the constraint solver rejects (as it should). The original line does not use the same constraintinference machinery, so it bypasses this step.
What can be done about this? It's tempting to have the original declaration generate this code instead:
```hs
instance Foo (Quux Int) where
bar = coerce @(forall (x :: Int). ())
@(forall (x :: Quux Int). ())
bar
```
Sadly, doing so would break a number of test cases that involve quantified constraints in instance contexts, such as `T15290`. See [`Note [GND and QuantifiedConstraints]`](https://gitlab.haskell.org/ghc/ghc//blob/9afd92512b41cf6c6de3a17b474d8d4bb01158c3/compiler/GHC/Tc/Deriv/Generate.hs#L16861773) for the full story. In order to make these test cases succeed (as a part of the fix for #15290), we employed an [ugly hack](132273f34e394bf7e900d0c15e01e91edd711890) where we split the `forall`s off of any types used to instantiate `coerce` in GNDgenerated code. But, as the example above demonstrates, this hack creates just as many problems as it solves.
@simonpj believes that this hack (and all of `Note [GND and QuantifiedConstraints]`) could be avoided. I don't quite understand his grand vision, so I'll let him comment here about what his vision entails.
Another similar example of this bug arising can be found in #18148. However, that issue is ensnared in a separate discussion about the roles of arguments to type classes, as the examples in #18148 crucially involve `ConstrainedClassMethods`. The underlying bug in this issue, on the other hand, does not fundamentally involve `ConstrainedClassMethods` in any way, so @simonpj and I have decided to track it separately here.Consider this code from https://gitlab.haskell.org/ghc/ghc/issues/18148#note_270603:
```hs
{# LANGUAGE AllowAmbiguousTypes #}
{# LANGUAGE DataKinds #}
{# LANGUAGE DerivingStrategies #}
{# LANGUAGE FlexibleInstances #}
{# LANGUAGE GeneralizedNewtypeDeriving #}
{# LANGUAGE PolyKinds #}
{# LANGUAGE ScopedTypeVariables #}
{# LANGUAGE StandaloneDeriving #}
module Bug where
class Foo a where
bar :: forall (x :: a). ()
bar = ()
instance Foo Int
newtype Quux a = Quux a
 deriving newtype instance _ => Foo (Quux Int)
deriving newtype instance Foo (Quux Int)
```
This typechecks in GHC 8.10.1. However, if you comment out the original `deriving newtype instance Foo (Quux Int)` line and uncomment the very similar line above it, it no longer typechecks:
```
Bug.hs:19:1: error:
• Couldn't match type ‘Int’ with ‘Quux Int’
arising from the coercion of the method ‘bar’
from type ‘forall (x :: Int). ()’
to type ‘forall (x :: Quux Int). ()’
• When deriving the instance for (Foo (Quux Int))

19  deriving newtype instance _ => Foo (Quux Int)
 ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
```
This is a strange inconsistency, given how similar these standalone `deriving` declarations are. Why does the original succeed but the line above it fail?
As it turns out, both of these really ought to fail, but the original only succeeds due to an unfortunate fluke in the way `GeneralizedNewtypeDeriving` works. Here is the code that the original declaration generates (with `ddumpderiv`):
```
==================== Derived instances ====================
Derived class instances:
instance Bug.Foo (Bug.Quux GHC.Types.Int) where
Bug.bar
= GHC.Prim.coerce @() @() (Bug.bar @GHC.Types.Int) ::
forall (x_aKF :: Bug.Quux GHC.Types.Int). ()
```
Notice that we are instantiating `coerce` with `@() @()`. But this is blatantly wrong—it really ought to be `coerce @(forall (x :: Int). ()) @(forall (x :: Quux Int). ())`, which the typechecker would reject (as it should). But GND generates `coerce @() @()` instead, and as a result, the use of `bar` on the RHS gets instantiated with `@Any`, which is not what was intended at all.
In contrast, the `deriving newtype instance _ => Foo (Quux Int)` line infers a `Coercible (forall (x :: Int). ()) (forall (x :: Quux Int). ())` constraint, which the constraint solver rejects (as it should). The original line does not use the same constraintinference machinery, so it bypasses this step.
What can be done about this? It's tempting to have the original declaration generate this code instead:
```hs
instance Foo (Quux Int) where
bar = coerce @(forall (x :: Int). ())
@(forall (x :: Quux Int). ())
bar
```
Sadly, doing so would break a number of test cases that involve quantified constraints in instance contexts, such as `T15290`. See [`Note [GND and QuantifiedConstraints]`](https://gitlab.haskell.org/ghc/ghc//blob/9afd92512b41cf6c6de3a17b474d8d4bb01158c3/compiler/GHC/Tc/Deriv/Generate.hs#L16861773) for the full story. In order to make these test cases succeed (as a part of the fix for #15290), we employed an [ugly hack](132273f34e394bf7e900d0c15e01e91edd711890) where we split the `forall`s off of any types used to instantiate `coerce` in GNDgenerated code. But, as the example above demonstrates, this hack creates just as many problems as it solves.
@simonpj believes that this hack (and all of `Note [GND and QuantifiedConstraints]`) could be avoided. I don't quite understand his grand vision, so I'll let him comment here about what his vision entails.
Another similar example of this bug arising can be found in #18148. However, that issue is ensnared in a separate discussion about the roles of arguments to type classes, as the examples in #18148 crucially involve `ConstrainedClassMethods`. The underlying bug in this issue, on the other hand, does not fundamentally involve `ConstrainedClassMethods` in any way, so @simonpj and I have decided to track it separately here.https://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/17934Consider using specificity to disambiguate quantified constraints20200503T13:32:41ZRichard Eisenbergrae@richarde.devConsider using specificity to disambiguate quantified constraints**Summary:** Currently, quantified constraints shadow global instances. This ticket proposes to use specificity (in the sense used by overlapping instances) instead of shadowing.
**Motivation**
This looks like a sensible way of having a datatype that can store something of a type that supports some class interface:
```haskell
data Some (c :: Type > Constraint) where
Some :: c a => a > Some c
```
But now I want to write a `Show` instance. I can do this only when the existential `a` supports `Show`. But I don't wish to require that `c ~ Show`  maybe `c a` implies `Show a`. So I write this:
```haskell
instance (forall x . c x => Show x) => Show (Some c) where
showsPrec n (Some a) = showsPrec n a
```
But now this fails. The problem is that the instance gets expanded to
```haskell
instance (forall x . c x => Show x) => Show (Some c) where
showsPrec n (Some a) = showsPrec n a
show = $dmshow
```
where `$dmshow :: Show a => a > String` is the default method implementation for `show`. When typechecking this method, GHC needs to satisfy `Show (Some c)`. The context includes two possibilities: the quantified constraint, and the toplevel instance declaration. Because local instances (= quantified constraints) shadow global ones, we use the first. So we reduce `[W] Show (Some c)` to `[W] c (Some c)`, which cannot be solved, leading to disaster.
This example first came to light in https://gitlab.haskell.org/ghc/ghc/issues/16502#note_253501, where it was copied from #17794.
Taking this new approach will likely fix #16502 and allow the original program in #17202 to be accepted. See also https://gitlab.haskell.org/ghc/ghc/issues/16502#note_253501 and https://gitlab.haskell.org/ghc/ghc/issues/16502#note_259055 for more test cases.
**Background**:
The current instance lookup (as documented [here](https://downloads.haskell.org/~ghc/latest/docs/html/users_guide/glasgow_exts.html#instancelookup)) works as follows to solve a `[W] C T` constraint (for some class `C` and type `T`).
1. Look for local (nonquantified) assumptions for `[G] C T`.
2. Look for local quantified constraints whose conclusions match `C T`. If exactly one matches, select the constraint. Then, check whether any quantified constraints *unify* with `C T` (allowing any variables in `C T` to be bound). If any do, abort, complaining about potential incoherence. Otherwise, reduce `[W] C T` to the premise of the quantified constraint.
3. Same as (2), but using the global instance table.
**Proposal**:
Use specificity to disambiguate.
* Let `<=spec` denote a partial order on instance heads. `C T1 <=spec C T2` iff there exists a substitution `S` such that `S(T2) = T1`  just as is used with overlapping instances today.
* Let metavariable `I` denote givens. These can be nonquantified, quantified (local), or global.
* Define `locality(I)` be a number that denotes how local `I` is. The locality of a nonquantified given is 1, of a quantified local given is 2, and of a global is 3.
* Define partial order `<=` on instances as follows:
1. If `I1 <=spec I2` and `I2 <=spec I1`, then `I1 <= I2` is `locality(I1) <= locality(I2)`.
2. If neither `I1 <=spec I2` nor `I2 <=spec I1`, then `I1 <= I2` is `locality(I1) <= locality(I2)`.
3. Otherwise, `I1 <= I2` if `I1 <=spec I2`.
Here is the proposed instance lookup procedure:
1. Collect all givens `I` (of all localities) that match a target. Call this set `Is`. If `Is` is empty, fail.
2. Let `I0` be the minimum element of `Is` with respect to `<=`. (Consider `Is` to be setlike, discarding duplicates.) If `I0` is not defined, fail.
3. Let `Is'` be the set `Is` excluding `I0`. Case on the locality of `I0`:
* `locality(I0) = 1`: Succeed with `I0` (skipping last check, below).
* `locality(I0) = 2`: Go on to next step if `Is'` contains only global instances. If `Is'` contains local instances, fail.
* `locality(I0) = 3`: Fail if any element in `Is'` is a local quantified instance. Go on to next step if, for every `I'` in `Is'`, either `I0` is *overlapping* or `I'` is *overlappable*.
4. Collect all givens (of all localities) that *unify* with a target, excluding those in `Is`. If `IncoherentInstances` is off and this set contains at least one instances not labeled **incoherent**, fail.
5. Succeed with `I0`.
**Discussion**:
This new algorithm is meant to replicate current behavior, except in the scenario where a global instance is more specific than a local one, in which the global instance should be selected. I have tried to capture current behavior w.r.t. incoherent and overlapping instances. In any case, if my algorithm deviates from current behavior w.r.t. incoherent or overlapping instances, this deviation is unintentional.
Another possible approach is to put local and global instances on even footing (that is, set both to have locality 2) but to allow users to explicitly label local instances as overlapping. I prefer the tiered approach above, but there's something simpler about local overlapping instances, in that it's one mechanism to think about.**Summary:** Currently, quantified constraints shadow global instances. This ticket proposes to use specificity (in the sense used by overlapping instances) instead of shadowing.
**Motivation**
This looks like a sensible way of having a datatype that can store something of a type that supports some class interface:
```haskell
data Some (c :: Type > Constraint) where
Some :: c a => a > Some c
```
But now I want to write a `Show` instance. I can do this only when the existential `a` supports `Show`. But I don't wish to require that `c ~ Show`  maybe `c a` implies `Show a`. So I write this:
```haskell
instance (forall x . c x => Show x) => Show (Some c) where
showsPrec n (Some a) = showsPrec n a
```
But now this fails. The problem is that the instance gets expanded to
```haskell
instance (forall x . c x => Show x) => Show (Some c) where
showsPrec n (Some a) = showsPrec n a
show = $dmshow
```
where `$dmshow :: Show a => a > String` is the default method implementation for `show`. When typechecking this method, GHC needs to satisfy `Show (Some c)`. The context includes two possibilities: the quantified constraint, and the toplevel instance declaration. Because local instances (= quantified constraints) shadow global ones, we use the first. So we reduce `[W] Show (Some c)` to `[W] c (Some c)`, which cannot be solved, leading to disaster.
This example first came to light in https://gitlab.haskell.org/ghc/ghc/issues/16502#note_253501, where it was copied from #17794.
Taking this new approach will likely fix #16502 and allow the original program in #17202 to be accepted. See also https://gitlab.haskell.org/ghc/ghc/issues/16502#note_253501 and https://gitlab.haskell.org/ghc/ghc/issues/16502#note_259055 for more test cases.
**Background**:
The current instance lookup (as documented [here](https://downloads.haskell.org/~ghc/latest/docs/html/users_guide/glasgow_exts.html#instancelookup)) works as follows to solve a `[W] C T` constraint (for some class `C` and type `T`).
1. Look for local (nonquantified) assumptions for `[G] C T`.
2. Look for local quantified constraints whose conclusions match `C T`. If exactly one matches, select the constraint. Then, check whether any quantified constraints *unify* with `C T` (allowing any variables in `C T` to be bound). If any do, abort, complaining about potential incoherence. Otherwise, reduce `[W] C T` to the premise of the quantified constraint.
3. Same as (2), but using the global instance table.
**Proposal**:
Use specificity to disambiguate.
* Let `<=spec` denote a partial order on instance heads. `C T1 <=spec C T2` iff there exists a substitution `S` such that `S(T2) = T1`  just as is used with overlapping instances today.
* Let metavariable `I` denote givens. These can be nonquantified, quantified (local), or global.
* Define `locality(I)` be a number that denotes how local `I` is. The locality of a nonquantified given is 1, of a quantified local given is 2, and of a global is 3.
* Define partial order `<=` on instances as follows:
1. If `I1 <=spec I2` and `I2 <=spec I1`, then `I1 <= I2` is `locality(I1) <= locality(I2)`.
2. If neither `I1 <=spec I2` nor `I2 <=spec I1`, then `I1 <= I2` is `locality(I1) <= locality(I2)`.
3. Otherwise, `I1 <= I2` if `I1 <=spec I2`.
Here is the proposed instance lookup procedure:
1. Collect all givens `I` (of all localities) that match a target. Call this set `Is`. If `Is` is empty, fail.
2. Let `I0` be the minimum element of `Is` with respect to `<=`. (Consider `Is` to be setlike, discarding duplicates.) If `I0` is not defined, fail.
3. Let `Is'` be the set `Is` excluding `I0`. Case on the locality of `I0`:
* `locality(I0) = 1`: Succeed with `I0` (skipping last check, below).
* `locality(I0) = 2`: Go on to next step if `Is'` contains only global instances. If `Is'` contains local instances, fail.
* `locality(I0) = 3`: Fail if any element in `Is'` is a local quantified instance. Go on to next step if, for every `I'` in `Is'`, either `I0` is *overlapping* or `I'` is *overlappable*.
4. Collect all givens (of all localities) that *unify* with a target, excluding those in `Is`. If `IncoherentInstances` is off and this set contains at least one instances not labeled **incoherent**, fail.
5. Succeed with `I0`.
**Discussion**:
This new algorithm is meant to replicate current behavior, except in the scenario where a global instance is more specific than a local one, in which the global instance should be selected. I have tried to capture current behavior w.r.t. incoherent and overlapping instances. In any case, if my algorithm deviates from current behavior w.r.t. incoherent or overlapping instances, this deviation is unintentional.
Another possible approach is to put local and global instances on even footing (that is, set both to have locality 2) but to allow users to explicitly label local instances as overlapping. I prefer the tiered approach above, but there's something simpler about local overlapping instances, in that it's one mechanism to think about.https://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/17719Note [Do not add duplicate quantified instances] is simplistic, causing rejec...20200714T19:14:38ZRichard Eisenbergrae@richarde.devNote [Do not add duplicate quantified instances] is simplistic, causing rejection of programsCopied wholesale from https://gitlab.haskell.org/ghc/ghc/merge_requests/2283#note_242042:
Consider
```haskell
{# LANGUAGE QuantifiedConstraints, ConstraintKinds,
ExistentialQuantification #}
module Bug where
class C1 a
class (forall z. C1 z) => C2 y
class (forall y. C2 y) => C3 x
data Dict c = c => Dict
foo :: (C2 a, C3 a) => a > Dict (C1 a)
foo _ = Dict
```
Amazingly, with *either* `C2 a` or `C3 a`, `foo` is accepted. But with both, it is rejected.
The problem is that, after eagerly expanding superclasses of quantified constraints (that's the new bit), we end up with
```
[G] g1 :: forall z. C1 z  from the C2 a constraint
[G] g2 :: forall y z. C1 z  from the C3 a constraint
```
So when we want to solve `C1 a`, we don't know which quantified constraint to use, and so we stop. (Also strange: `g2` is quantified over the unused `y`. It's clear where this comes from, and it seems harmless, but it's a bit strange. This detail is *not* salient. It is *not* the reason we're struggling here.) This has been seen before, in another guise: #15244. And we have
```
{ Note [Do not add duplicate quantified instances]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Consider this (#15244):
f :: (C g, D g) => ....
class S g => C g where ...
class S g => D g where ...
class (forall a. Eq a => Eq (g a)) => S g where ...
Then in f's RHS there are two identical quantified constraints
available, one via the superclasses of C and one via the superclasses
of D. The two are identical, and it seems wrong to reject the program
because of that. But without doing duplicateelimination we will have
two matching QCInsts when we try to solve constraints arising from f's
RHS.
The simplest thing is simply to eliminate duplicates, which we do here.
}
```
which is duly implemented. However, here, we don't have duplicates  we have nearduplicates, which are not caught by the simple (`tcEqType`) check.
I wonder if the way forward is to really try to "solve" quantified instances. That is, before labeling them inert, we try to interact them with inerts. Then, we might discover that one constraint is implied by another, which will get rid of this problem (and replace that Note).Copied wholesale from https://gitlab.haskell.org/ghc/ghc/merge_requests/2283#note_242042:
Consider
```haskell
{# LANGUAGE QuantifiedConstraints, ConstraintKinds,
ExistentialQuantification #}
module Bug where
class C1 a
class (forall z. C1 z) => C2 y
class (forall y. C2 y) => C3 x
data Dict c = c => Dict
foo :: (C2 a, C3 a) => a > Dict (C1 a)
foo _ = Dict
```
Amazingly, with *either* `C2 a` or `C3 a`, `foo` is accepted. But with both, it is rejected.
The problem is that, after eagerly expanding superclasses of quantified constraints (that's the new bit), we end up with
```
[G] g1 :: forall z. C1 z  from the C2 a constraint
[G] g2 :: forall y z. C1 z  from the C3 a constraint
```
So when we want to solve `C1 a`, we don't know which quantified constraint to use, and so we stop. (Also strange: `g2` is quantified over the unused `y`. It's clear where this comes from, and it seems harmless, but it's a bit strange. This detail is *not* salient. It is *not* the reason we're struggling here.) This has been seen before, in another guise: #15244. And we have
```
{ Note [Do not add duplicate quantified instances]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Consider this (#15244):
f :: (C g, D g) => ....
class S g => C g where ...
class S g => D g where ...
class (forall a. Eq a => Eq (g a)) => S g where ...
Then in f's RHS there are two identical quantified constraints
available, one via the superclasses of C and one via the superclasses
of D. The two are identical, and it seems wrong to reject the program
because of that. But without doing duplicateelimination we will have
two matching QCInsts when we try to solve constraints arising from f's
RHS.
The simplest thing is simply to eliminate duplicates, which we do here.
}
```
which is duly implemented. However, here, we don't have duplicates  we have nearduplicates, which are not caught by the simple (`tcEqType`) check.
I wonder if the way forward is to really try to "solve" quantified instances. That is, before labeling them inert, we try to interact them with inerts. Then, we might discover that one constraint is implied by another, which will get rid of this problem (and replace that Note).https://gitlab.haskell.org/ghc/ghc//issues/17564Don't drop derived quantified constraints20191211T09:48:10ZRichard Eisenbergrae@richarde.devDon't drop derived quantified constraintsIn looking at the way quantified constraints are handled, I noticed that we drop derived quantified constraints (in `TcCanonical.solveForAll`). I don't see a reason why this is a good idea. And indeed, it causes trouble:
```hs
{# LANGUAGE QuantifiedConstraints, MultiParamTypeClasses,
KindSignatures, FlexibleInstances, TypeFamilies #}
module Bug where
import Data.Kind
class (forall (a :: Type > Type). a b ~ a c) => C b c
instance C a a
class (b ~ c) => D b c
instance D a a
foo :: C a b => a > b
foo = undefined
bar = foo
food :: D a b => a > b
food = undefined
bard = food
```
`C` and `D` should really behave identically. Yet `bar` is rejected while `bard` is accepted.
Note that the monomorphism restriction forces us to solve, not quantify over, the `C` and `D` constraints. This is intentional in this test case.
Normally, the superclasses of a wanted are emitted as derived constraints. In the case of `bard`, we start with `[W] D alpha beta`, which doesn't make progress. So we get `[D] alpha ~ beta`, which unifies the two, and then `[W] D alpha alpha` is easily dispatched. But in `bar` the `[D] forall a. a alpha ~ a beta` is dropped, leading to rejection.
The kind signature in the test case is needed because of #17562.In looking at the way quantified constraints are handled, I noticed that we drop derived quantified constraints (in `TcCanonical.solveForAll`). I don't see a reason why this is a good idea. And indeed, it causes trouble:
```hs
{# LANGUAGE QuantifiedConstraints, MultiParamTypeClasses,
KindSignatures, FlexibleInstances, TypeFamilies #}
module Bug where
import Data.Kind
class (forall (a :: Type > Type). a b ~ a c) => C b c
instance C a a
class (b ~ c) => D b c
instance D a a
foo :: C a b => a > b
foo = undefined
bar = foo
food :: D a b => a > b
food = undefined
bard = food
```
`C` and `D` should really behave identically. Yet `bar` is rejected while `bard` is accepted.
Note that the monomorphism restriction forces us to solve, not quantify over, the `C` and `D` constraints. This is intentional in this test case.
Normally, the superclasses of a wanted are emitted as derived constraints. In the case of `bard`, we start with `[W] D alpha beta`, which doesn't make progress. So we get `[D] alpha ~ beta`, which unifies the two, and then `[W] D alpha alpha` is easily dispatched. But in `bar` the `[D] forall a. a alpha ~ a beta` is dropped, leading to rejection.
The kind signature in the test case is needed because of #17562.https://gitlab.haskell.org/ghc/ghc//issues/17563Validity check quantified constraints20200604T15:17:29ZRichard 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/17562`Any` appearing in a quantified constraint20200118T00:00:32ZRichard Eisenbergrae@richarde.dev`Any` appearing in a quantified constraintIf I say
```hs
{# LANGUAGE QuantifiedConstraints, MultiParamTypeClasses #}
module Bug where
class (forall a. a b ~ a c) => C b c
```
I get
```
Bug.hs:5:1: error:
• Illegal type synonym family application ‘GHC.Types.Any
@*’ in instance:
(a b :: GHC.Types.Any @*) ~ (a c :: GHC.Types.Any @*)
• In the quantified constraint ‘forall (a :: k > GHC.Types.Any).
a b ~ a c’
In the context: forall (a :: k > GHC.Types.Any). a b ~ a c
While checking the superclasses of class ‘C’
In the class declaration for ‘C’

5  class (forall a. a b ~ a c) => C b c
 ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
```
This is a specific case of #17567. Despite superficial similarity, this is unrelated to #16775.If I say
```hs
{# LANGUAGE QuantifiedConstraints, MultiParamTypeClasses #}
module Bug where
class (forall a. a b ~ a c) => C b c
```
I get
```
Bug.hs:5:1: error:
• Illegal type synonym family application ‘GHC.Types.Any
@*’ in instance:
(a b :: GHC.Types.Any @*) ~ (a c :: GHC.Types.Any @*)
• In the quantified constraint ‘forall (a :: k > GHC.Types.Any).
a b ~ a c’
In the context: forall (a :: k > GHC.Types.Any). a b ~ a c
While checking the superclasses of class ‘C’
In the class declaration for ‘C’

5  class (forall a. a b ~ a c) => C b c
 ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
```
This is a specific case of #17567. Despite superficial similarity, this is unrelated to #16775.9.0.1Richard Eisenbergrae@richarde.devRichard Eisenbergrae@richarde.devhttps://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/17226Quantified constraints which specify associated type instances20200123T19:48:51ZsheafQuantified constraints which specify associated type instancesI have come across a situation which I believe could benefit from the ability to refine quantified constraints by adding constraints on the associated type instance declarations. For instance, consider a class with an associated type:
```haskell
class C a where
type T a :: Type
...
```
From what I understand, a quantified constraint of the form ```( forall a. C a => C (f a) )``` will be soluble when there is an instance of the form
```haskell
instance forall a. C a => C (f a)
```
My suggestion is to provide the ability to specify quantified constraints which restrict the associated type family instance declarations. In this case, we might want to insist upon the equation `type T (f a) = f (T a)`. One possible notation would use tuple and equality constraints (mirroring how one would encode this using `Dict`):
```haskell
forall a. C a => ( C (f a), T (f a) ~ f (T a) )
```
In solving this quantified constraint, we would discard all class instances which are not of the following form:
```haskell
instance forall a. C a => C (f a) where
type T (f a) = f (T a)
```
(I don't know how flexible we can afford to be in verifying this property, e.g. if the type family instance equations are not exactly as specified by the equality constraint but are equivalent to them, say after applying substitutions or using other equality constraints that might be available.)
### Example
To illustrate, I was working with the `Syntactic` type class
```haskell
class Syntactic a where
type Internal a
toAST :: a > AST (Internal a)
fromAST :: AST (Internal a) > a
```
and I wanted to restrict attention to functors `F` that are compatible with this type class, i.e. which have an instance declaration of the form
```haskell
instance Syntactic a => Syntactic (F a) where
type Internal (F a) = F (Internal a)
```
However, while I can write a quantified constraint `forall a. Syntactic a => Syntactic (f a)`, I cannot specify the additional requirement on the associated type family instance equation, so GHC will complain at usesites:
```
* Could not deduce: Internal (f a) ~ f (Internal a)
```
This can be worked around using `Dict ( Syntactic (f a), Internal (f a) ~ f (Internal a) )`, unfortunately forgoing the use of quantified constraints and introducing indirections (requiring matching on `Dict` to make the instances visible to GHC). Other than that I don't know of any tricks to bypass this limitation, but I may well be missing something (quite likely, as I don't have much experience with quantified constraints).I have come across a situation which I believe could benefit from the ability to refine quantified constraints by adding constraints on the associated type instance declarations. For instance, consider a class with an associated type:
```haskell
class C a where
type T a :: Type
...
```
From what I understand, a quantified constraint of the form ```( forall a. C a => C (f a) )``` will be soluble when there is an instance of the form
```haskell
instance forall a. C a => C (f a)
```
My suggestion is to provide the ability to specify quantified constraints which restrict the associated type family instance declarations. In this case, we might want to insist upon the equation `type T (f a) = f (T a)`. One possible notation would use tuple and equality constraints (mirroring how one would encode this using `Dict`):
```haskell
forall a. C a => ( C (f a), T (f a) ~ f (T a) )
```
In solving this quantified constraint, we would discard all class instances which are not of the following form:
```haskell
instance forall a. C a => C (f a) where
type T (f a) = f (T a)
```
(I don't know how flexible we can afford to be in verifying this property, e.g. if the type family instance equations are not exactly as specified by the equality constraint but are equivalent to them, say after applying substitutions or using other equality constraints that might be available.)
### Example
To illustrate, I was working with the `Syntactic` type class
```haskell
class Syntactic a where
type Internal a
toAST :: a > AST (Internal a)
fromAST :: AST (Internal a) > a
```
and I wanted to restrict attention to functors `F` that are compatible with this type class, i.e. which have an instance declaration of the form
```haskell
instance Syntactic a => Syntactic (F a) where
type Internal (F a) = F (Internal a)
```
However, while I can write a quantified constraint `forall a. Syntactic a => Syntactic (f a)`, I cannot specify the additional requirement on the associated type family instance equation, so GHC will complain at usesites:
```
* Could not deduce: Internal (f a) ~ f (Internal a)
```
This can be worked around using `Dict ( Syntactic (f a), Internal (f a) ~ f (Internal a) )`, unfortunately forgoing the use of quantified constraints and introducing indirections (requiring matching on `Dict` to make the instances visible to GHC). Other than that I don't know of any tricks to bypass this limitation, but I may well be missing something (quite likely, as I don't have much experience with quantified constraints).https://gitlab.haskell.org/ghc/ghc//issues/16931Quantified constraint error should show more context20200407T07:48:55ZGuillaume BouchardQuantified constraint error should show more context## Motivation
`QuantifiedConstraints` sometimes leads to incomplete error message for which it is rather difficult to understand / locate the source of the error.
See the following example:
```haskell
{# LANGUAGE KindSignatures #}
{# LANGUAGE RankNTypes, ScopedTypeVariables, QuantifiedConstraints, TypeApplications, DataKinds, ConstraintKinds, AllowAmbiguousTypes #}
module QC2 where
import GHC.TypeLits
import Data.Proxy
data Array (n :: Nat) = Array
class IsEqual t
instance KnownNat n => IsEqual (Array n)
blork :: forall c.
(forall k. { KnownNat k => } c (Array k)) =>
(forall k. c k => k > Bool) > Bool
blork f = case someNatVal 10 of
Nothing > False
Just (SomeNat (_ :: Proxy n)) > f (Array @n)
blip :: Bool
blip = blork @IsEqual (\_ > True)
```
The comment around `KnownNat k =>` can be removed to fix the following error:
```haskell
QC2.hs:22:8: error:
• No instance for (KnownNat k) arising from a use of ‘blork’
Possible fix:
add (KnownNat k) to the context of a quantified context
• In the expression: blork @IsEqual (\ _ > True)
In an equation for ‘blip’: blip = blork @IsEqual (\ _ > True)

22  blip = blork @IsEqual (\_ > True)
 ^^^^^^^^^^^^^^^^^^^^^^^^^^^
```
This error show the call site and a "Possible fix". However it does not give any hint about the location of the erroneous quantified constraint. The developer must manually locate the `blork` function and, amongs the list of quantified constraints in its context, locate the erroneous one.
Note that GHC is smart enough to use the right name for the type variable `k` in the error message, this helps a bit. However, as depicted in my example, the constraint of `blork` may many quantified constraint using all the same type variable (because they are independent).
It took me a lot of time to first understand that the error was in the `blork` function. Now I'm used to this error, but locating the erroneous quantified constraint is still difficult.
## Proposal
I'd like a more detailed error message, such as:
```haskell
QC2.hs:22:8: error:
• No instance for (KnownNat k) arising from a use of ‘blork’
Possible fix:
add (KnownNat k) to the context of a quantified context
in the `blork` function context:
15  blork :: forall c.
 (forall k. c (Array k)) =>
^^^^^^^^^^^^^^^^^^^^^^^^^^
• In the expression: blork @IsEqual (\ _ > True)
In an equation for ‘blip’: blip = blork @IsEqual (\ _ > True)

22  blip = blork @IsEqual (\_ > True)

```
I'd like something similar to the hint associated with missing constraint in this context:
```haskell
foo :: t > String
foo = show
```
```haskell
• No instance for (Show t) arising from a use of ‘show’
Possible fix:
add (Show t) to the context of
the type signature for:
foo :: forall t. t > String
• In the expression: show
In an equation for ‘foo’: foo = show
```## Motivation
`QuantifiedConstraints` sometimes leads to incomplete error message for which it is rather difficult to understand / locate the source of the error.
See the following example:
```haskell
{# LANGUAGE KindSignatures #}
{# LANGUAGE RankNTypes, ScopedTypeVariables, QuantifiedConstraints, TypeApplications, DataKinds, ConstraintKinds, AllowAmbiguousTypes #}
module QC2 where
import GHC.TypeLits
import Data.Proxy
data Array (n :: Nat) = Array
class IsEqual t
instance KnownNat n => IsEqual (Array n)
blork :: forall c.
(forall k. { KnownNat k => } c (Array k)) =>
(forall k. c k => k > Bool) > Bool
blork f = case someNatVal 10 of
Nothing > False
Just (SomeNat (_ :: Proxy n)) > f (Array @n)
blip :: Bool
blip = blork @IsEqual (\_ > True)
```
The comment around `KnownNat k =>` can be removed to fix the following error:
```haskell
QC2.hs:22:8: error:
• No instance for (KnownNat k) arising from a use of ‘blork’
Possible fix:
add (KnownNat k) to the context of a quantified context
• In the expression: blork @IsEqual (\ _ > True)
In an equation for ‘blip’: blip = blork @IsEqual (\ _ > True)

22  blip = blork @IsEqual (\_ > True)
 ^^^^^^^^^^^^^^^^^^^^^^^^^^^
```
This error show the call site and a "Possible fix". However it does not give any hint about the location of the erroneous quantified constraint. The developer must manually locate the `blork` function and, amongs the list of quantified constraints in its context, locate the erroneous one.
Note that GHC is smart enough to use the right name for the type variable `k` in the error message, this helps a bit. However, as depicted in my example, the constraint of `blork` may many quantified constraint using all the same type variable (because they are independent).
It took me a lot of time to first understand that the error was in the `blork` function. Now I'm used to this error, but locating the erroneous quantified constraint is still difficult.
## Proposal
I'd like a more detailed error message, such as:
```haskell
QC2.hs:22:8: error:
• No instance for (KnownNat k) arising from a use of ‘blork’
Possible fix:
add (KnownNat k) to the context of a quantified context
in the `blork` function context:
15  blork :: forall c.
 (forall k. c (Array k)) =>
^^^^^^^^^^^^^^^^^^^^^^^^^^
• In the expression: blork @IsEqual (\ _ > True)
In an equation for ‘blip’: blip = blork @IsEqual (\ _ > True)

22  blip = blork @IsEqual (\_ > True)

```
I'd like something similar to the hint associated with missing constraint in this context:
```haskell
foo :: t > String
foo = show
```
```haskell
• No instance for (Show t) arising from a use of ‘show’
Possible fix:
add (Show t) to the context of
the type signature for:
foo :: forall t. t > String
• In the expression: show
In an equation for ‘foo’: foo = show
```https://gitlab.haskell.org/ghc/ghc//issues/16730Instance decidability + Quantified Constraints20190618T06:34:27ZWill YagerInstance decidability + Quantified Constraints# Motivation
Consider the following program:
```Haskell
{# LANGUAGE RankNTypes, KindSignatures, QuantifiedConstraints #}
module Main where
class C a
data D (f :: * > *)
instance (forall b . C (f b)) => C (D f)
main = return ()
```
Compilation fails with
```
[1 of 1] Compiling Main ( test.hs, test.o )
test.hs:9:10: error:
• The constraint ‘C (f b)’
is no smaller than the instance head ‘C (D f)’
(Use UndecidableInstances to permit this)
• In the instance declaration for ‘C (D f)’

9  instance (forall b . C (f b)) => C (D f)
```
# Proposal
Could we slightly modify the constraintsize rule to not count type variables that are bound within the constraint towards the size of the constraint? I.e. only free type variables "escaping" the constraint would count towards its size.
As a disclaimer, I am not entirely sure this is would be correct, but intuitively it seems fine. I would appreciate input from anyone with a rigorous understanding of these mechanisms.# Motivation
Consider the following program:
```Haskell
{# LANGUAGE RankNTypes, KindSignatures, QuantifiedConstraints #}
module Main where
class C a
data D (f :: * > *)
instance (forall b . C (f b)) => C (D f)
main = return ()
```
Compilation fails with
```
[1 of 1] Compiling Main ( test.hs, test.o )
test.hs:9:10: error:
• The constraint ‘C (f b)’
is no smaller than the instance head ‘C (D f)’
(Use UndecidableInstances to permit this)
• In the instance declaration for ‘C (D f)’

9  instance (forall b . C (f b)) => C (D f)
```
# Proposal
Could we slightly modify the constraintsize rule to not count type variables that are bound within the constraint towards the size of the constraint? I.e. only free type variables "escaping" the constraint would count towards its size.
As a disclaimer, I am not entirely sure this is would be correct, but intuitively it seems fine. I would appreciate input from anyone with a rigorous understanding of these mechanisms.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/16432Commutativity of Coercible sometimes doesn't work with QuantifiedConstraints20190315T13:06:54ZMichael SloanCommutativity of Coercible sometimes doesn't work with QuantifiedConstraintsIt seems that there is a surprising interaction between the coercible constraint solver and quantified constraints. Here's some code with some explanation in the comments:
```haskell
{# LANGUAGE QuantifiedConstraints #}
import Data.Coerce
 I think this should compile, but it doesn't.

 I'd expect the quantified constraint to be instantiated to
 (Coercible (f b) b), and via commutativity of Coercible, imply
 (Coercible b (f b))
compileError0 :: forall f b. (forall a. Coercible (f a) a) => b > f b
compileError0 = coerce
 The fact that this compiles demonstrates that quantified
 constraints is needed to demonstrate the issue.
compiles0 :: forall f b. Coercible (f b) b => b > f b
compiles0 = coerce
 Instantiation as (Coercible (f b) b) works fine.
compiles1 :: forall f b. (forall a. Coercible (f a) a) => f b > b
compiles1 = coerce
 Instantiation of (forall a. Coercible a (f a)) as
 (Coercible b (f b)) works.
compiles2 :: forall f b. (forall a. Coercible a (f a)) => b > f b
compiles2 = coerce
 This is curious! It turns out that instantiation of
 (forall a. Coercible a (f a)) does indeed get combined with
 commutativity to imply (Coercible (f b) b)
compiles3 :: forall f b. (forall a. Coercible a (f a)) => f b > b
compiles3 = coerce
```
I get the following error with both `GHC8.6.4` and also GHC built from recent source, `8.9.20190304`:
```
qc.hs:10:17: error:
• Couldn't match representation of type ‘b’ with that of ‘f b’
arising from a use of ‘coerce’
‘b’ is a rigid type variable bound by
the type signature for:
compileError0 :: forall (f :: * > *) b.
(forall a. Coercible (f a) a) =>
b > f b
at qc.hs:9:170
• In the expression: coerce
In an equation for ‘compileError0’: compileError0 = coerce
• Relevant bindings include
compileError0 :: b > f b (bound at qc.hs:10:1)

10  compileError0 = coerce
```It seems that there is a surprising interaction between the coercible constraint solver and quantified constraints. Here's some code with some explanation in the comments:
```haskell
{# LANGUAGE QuantifiedConstraints #}
import Data.Coerce
 I think this should compile, but it doesn't.

 I'd expect the quantified constraint to be instantiated to
 (Coercible (f b) b), and via commutativity of Coercible, imply
 (Coercible b (f b))
compileError0 :: forall f b. (forall a. Coercible (f a) a) => b > f b
compileError0 = coerce
 The fact that this compiles demonstrates that quantified
 constraints is needed to demonstrate the issue.
compiles0 :: forall f b. Coercible (f b) b => b > f b
compiles0 = coerce
 Instantiation as (Coercible (f b) b) works fine.
compiles1 :: forall f b. (forall a. Coercible (f a) a) => f b > b
compiles1 = coerce
 Instantiation of (forall a. Coercible a (f a)) as
 (Coercible b (f b)) works.
compiles2 :: forall f b. (forall a. Coercible a (f a)) => b > f b
compiles2 = coerce
 This is curious! It turns out that instantiation of
 (forall a. Coercible a (f a)) does indeed get combined with
 commutativity to imply (Coercible (f b) b)
compiles3 :: forall f b. (forall a. Coercible a (f a)) => f b > b
compiles3 = coerce
```
I get the following error with both `GHC8.6.4` and also GHC built from recent source, `8.9.20190304`:
```
qc.hs:10:17: error:
• Couldn't match representation of type ‘b’ with that of ‘f b’
arising from a use of ‘coerce’
‘b’ is a rigid type variable bound by
the type signature for:
compileError0 :: forall (f :: * > *) b.
(forall a. Coercible (f a) a) =>
b > f b
at qc.hs:9:170
• In the expression: coerce
In an equation for ‘compileError0’: compileError0 = coerce
• Relevant bindings include
compileError0 :: b > f b (bound at qc.hs:10:1)

10  compileError0 = coerce
```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":[]} >