GHC issueshttps://gitlab.haskell.org/ghc/ghc//issues20190707T18:13:01Zhttps://gitlab.haskell.org/ghc/ghc//issues/15359Quantified constraints do not work with equality constraints20190707T18:13:01ZRichard Eisenbergrae@richarde.devQuantified constraints do not work with equality constraintsFeeling abusive toward GHC this morning, I tried this:
```hs
class C a b
data Dict c where
Dict :: c => Dict c
foo :: (forall a b. C a b => a ~ b) => Dict (C a b) > a > b
foo Dict x = x
```
I thought it wouldn't work, and I was right:
```
• Class ‘~’ does not support userspecified instances
• In the quantified constraint ‘forall (a :: k) (b :: k).
C a b =>
a ~ b’
In the type signature:
foo :: (forall a b. C a b => a ~ b) => Dict (C a b) > a > b
```
Good. But then I tried something more devious:
```hs
class C a b
class a ~ b => D a b
data Dict c where
Dict :: c => Dict c
foo :: (forall a b. C a b => D a b) => Dict (C a b) > a > b
foo Dict x = x
```
This also fails, with ` Couldn't match expected type ‘b’ with actual type ‘a’`.
I'm fine with the second case failing (because I think anything else would be very challenging), but the error message is unfortunate. According to the semantics of class constraints and quantified constraints, this case should be accepted. So if we reject it, we should have a good reason  like we offer in the first case. Essentially, we need to explain that any logical entailment of an equality constraint simply doesn't hold in the presence of a quantified constraint. I neither know a good pithy way of explaining that to users nor how to detect when to do so.
<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":"Quantified constraints do not work with equality constraints","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"8.6.1","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.5","keywords":["QuantifiedConstraints"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"Feeling abusive toward GHC this morning, I tried this:\r\n\r\n{{{#!hs\r\nclass C a b\r\n\r\ndata Dict c where\r\n Dict :: c => Dict c\r\n\r\nfoo :: (forall a b. C a b => a ~ b) => Dict (C a b) > a > b\r\nfoo Dict x = x\r\n}}}\r\n\r\nI thought it wouldn't work, and I was right:\r\n\r\n{{{\r\n • Class ‘~’ does not support userspecified instances\r\n • In the quantified constraint ‘forall (a :: k) (b :: k).\r\n C a b =>\r\n a ~ b’\r\n In the type signature:\r\n foo :: (forall a b. C a b => a ~ b) => Dict (C a b) > a > b\r\n}}}\r\n\r\nGood. But then I tried something more devious:\r\n\r\n{{{#!hs\r\nclass C a b\r\nclass a ~ b => D a b\r\n\r\ndata Dict c where\r\n Dict :: c => Dict c\r\n\r\nfoo :: (forall a b. C a b => D a b) => Dict (C a b) > a > b\r\nfoo Dict x = x\r\n}}}\r\n\r\nThis also fails, with ` Couldn't match expected type ‘b’ with actual type ‘a’`.\r\n\r\nI'm fine with the second case failing (because I think anything else would be very challenging), but the error message is unfortunate. According to the semantics of class constraints and quantified constraints, this case should be accepted. So if we reject it, we should have a good reason  like we offer in the first case. Essentially, we need to explain that any logical entailment of an equality constraint simply doesn't hold in the presence of a quantified constraint. I neither know a good pithy way of explaining that to users nor how to detect when to do so.","type_of_failure":"OtherFailure","blocking":[]} >Feeling abusive toward GHC this morning, I tried this:
```hs
class C a b
data Dict c where
Dict :: c => Dict c
foo :: (forall a b. C a b => a ~ b) => Dict (C a b) > a > b
foo Dict x = x
```
I thought it wouldn't work, and I was right:
```
• Class ‘~’ does not support userspecified instances
• In the quantified constraint ‘forall (a :: k) (b :: k).
C a b =>
a ~ b’
In the type signature:
foo :: (forall a b. C a b => a ~ b) => Dict (C a b) > a > b
```
Good. But then I tried something more devious:
```hs
class C a b
class a ~ b => D a b
data Dict c where
Dict :: c => Dict c
foo :: (forall a b. C a b => D a b) => Dict (C a b) > a > b
foo Dict x = x
```
This also fails, with ` Couldn't match expected type ‘b’ with actual type ‘a’`.
I'm fine with the second case failing (because I think anything else would be very challenging), but the error message is unfortunate. According to the semantics of class constraints and quantified constraints, this case should be accepted. So if we reject it, we should have a good reason  like we offer in the first case. Essentially, we need to explain that any logical entailment of an equality constraint simply doesn't hold in the presence of a quantified constraint. I neither know a good pithy way of explaining that to users nor how to detect when to do so.
<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":"Quantified constraints do not work with equality constraints","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"8.6.1","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.5","keywords":["QuantifiedConstraints"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"Feeling abusive toward GHC this morning, I tried this:\r\n\r\n{{{#!hs\r\nclass C a b\r\n\r\ndata Dict c where\r\n Dict :: c => Dict c\r\n\r\nfoo :: (forall a b. C a b => a ~ b) => Dict (C a b) > a > b\r\nfoo Dict x = x\r\n}}}\r\n\r\nI thought it wouldn't work, and I was right:\r\n\r\n{{{\r\n • Class ‘~’ does not support userspecified instances\r\n • In the quantified constraint ‘forall (a :: k) (b :: k).\r\n C a b =>\r\n a ~ b’\r\n In the type signature:\r\n foo :: (forall a b. C a b => a ~ b) => Dict (C a b) > a > b\r\n}}}\r\n\r\nGood. But then I tried something more devious:\r\n\r\n{{{#!hs\r\nclass C a b\r\nclass a ~ b => D a b\r\n\r\ndata Dict c where\r\n Dict :: c => Dict c\r\n\r\nfoo :: (forall a b. C a b => D a b) => Dict (C a b) > a > b\r\nfoo Dict x = x\r\n}}}\r\n\r\nThis also fails, with ` Couldn't match expected type ‘b’ with actual type ‘a’`.\r\n\r\nI'm fine with the second case failing (because I think anything else would be very challenging), but the error message is unfortunate. According to the semantics of class constraints and quantified constraints, this case should be accepted. So if we reject it, we should have a good reason  like we offer in the first case. Essentially, we need to explain that any logical entailment of an equality constraint simply doesn't hold in the presence of a quantified constraint. I neither know a good pithy way of explaining that to users nor how to detect when to do so.","type_of_failure":"OtherFailure","blocking":[]} >8.8.1https://gitlab.haskell.org/ghc/ghc//issues/15334(forall x. c x, forall x. d x) is not equivalent to forall x. (c x, d x)20190805T08:46:55ZRyan Scott(forall x. c x, forall x. d x) is not equivalent to forall x. (c x, d x)Consider the following code:
```hs
{# LANGUAGE DeriveTraversable #}
{# LANGUAGE ExistentialQuantification #}
{# LANGUAGE TypeFamilies #}
{# LANGUAGE QuantifiedConstraints #}
{# LANGUAGE StandaloneDeriving #}
{# LANGUAGE UndecidableInstances #}
module Foo where
import Data.Kind
type family F a :: Type > Type
newtype WrappedF a b = WrapF (F a b)
deriving instance Functor (F a) => Functor (WrappedF a)
deriving instance Foldable (F a) => Foldable (WrappedF a)
deriving instance Traversable (F a) => Traversable (WrappedF a)
data SomeF b = forall a. MkSomeF (WrappedF a b)
deriving instance (forall a. Functor (WrappedF a)) => Functor SomeF
deriving instance (forall a. Foldable (WrappedF a)) => Foldable SomeF
deriving instance ( forall a. Functor (WrappedF a)
, forall a. Foldable (WrappedF a)
, forall a. Traversable (WrappedF a)
) => Traversable SomeF
```
This typechecks. However, the last `Traversable SomeF` is a bit unfortunate in that is uses three separate `forall a.`s. I attempted to factor this out, like so:
```hs
deriving instance (forall a. ( Functor (WrappedF a)
, Foldable (WrappedF a)
, Traversable (WrappedF a)
)) => Traversable SomeF
```
But then the file no longer typechecked!
```
$ /opt/ghc/8.6.1/bin/ghc Foo.hs
[1 of 1] Compiling Foo ( Foo.hs, Foo.o )
Foo.hs:21:1: error:
• Could not deduce (Functor (F a))
arising from the superclasses of an instance declaration
from the context: forall a.
(Functor (WrappedF a), Foldable (WrappedF a),
Traversable (WrappedF a))
bound by the instance declaration at Foo.hs:(21,1)(24,52)
• In the instance declaration for ‘Traversable SomeF’

21  deriving instance (forall a. ( Functor (WrappedF a)
 ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^...
Foo.hs:21:1: error:
• Could not deduce (Foldable (F a))
arising from the superclasses of an instance declaration
from the context: forall a.
(Functor (WrappedF a), Foldable (WrappedF a),
Traversable (WrappedF a))
bound by the instance declaration at Foo.hs:(21,1)(24,52)
• In the instance declaration for ‘Traversable SomeF’

21  deriving instance (forall a. ( Functor (WrappedF a)
 ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^...
Foo.hs:21:1: error:
• Could not deduce (Traversable (F a1))
arising from a use of ‘traverse’
from the context: forall a.
(Functor (WrappedF a), Foldable (WrappedF a),
Traversable (WrappedF a))
bound by the instance declaration at Foo.hs:(21,1)(24,52)
or from: Applicative f
bound by the type signature for:
traverse :: forall (f :: * > *) a b.
Applicative f =>
(a > f b) > SomeF a > f (SomeF b)
at Foo.hs:(21,1)(24,52)
• In the second argument of ‘fmap’, namely ‘(traverse f a1)’
In the expression: fmap (\ b1 > MkSomeF b1) (traverse f a1)
In an equation for ‘traverse’:
traverse f (MkSomeF a1) = fmap (\ b1 > MkSomeF b1) (traverse f a1)
When typechecking the code for ‘traverse’
in a derived instance for ‘Traversable SomeF’:
To see the code I am typechecking, use ddumpderiv

21  deriving instance (forall a. ( Functor (WrappedF a)
 ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^...
```
Richard suspects that this is a bug in the way quantified constraints expands superclasses, so I decided to post it here.
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.5 
 Type  Bug 
 TypeOfFailure  OtherFailure 
 Priority  normal 
 Resolution  Unresolved 
 Component  Compiler (Type checker) 
 Test case  
 Differential revisions  
 BlockedBy  
 Related  
 Blocking  
 CC  
 Operating system  
 Architecture  
</details>
<! {"blocked_by":[],"summary":"(forall x. c x, forall x. d x) is not equivalent to forall x. (c x, d x)","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"8.6.1","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.5","keywords":["QuantifiedConstraints"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"Consider the following code:\r\n\r\n{{{#!hs\r\n{# LANGUAGE DeriveTraversable #}\r\n{# LANGUAGE ExistentialQuantification #}\r\n{# LANGUAGE TypeFamilies #}\r\n{# LANGUAGE QuantifiedConstraints #}\r\n{# LANGUAGE StandaloneDeriving #}\r\n{# LANGUAGE UndecidableInstances #}\r\nmodule Foo where\r\n\r\nimport Data.Kind\r\n\r\ntype family F a :: Type > Type\r\nnewtype WrappedF a b = WrapF (F a b)\r\nderiving instance Functor (F a) => Functor (WrappedF a)\r\nderiving instance Foldable (F a) => Foldable (WrappedF a)\r\nderiving instance Traversable (F a) => Traversable (WrappedF a)\r\n\r\ndata SomeF b = forall a. MkSomeF (WrappedF a b)\r\n\r\nderiving instance (forall a. Functor (WrappedF a)) => Functor SomeF\r\nderiving instance (forall a. Foldable (WrappedF a)) => Foldable SomeF\r\nderiving instance ( forall a. Functor (WrappedF a)\r\n , forall a. Foldable (WrappedF a)\r\n , forall a. Traversable (WrappedF a)\r\n ) => Traversable SomeF\r\n}}}\r\n\r\nThis typechecks. However, the last `Traversable SomeF` is a bit unfortunate in that is uses three separate `forall a.`s. I attempted to factor this out, like so:\r\n\r\n{{{#!hs\r\nderiving instance (forall a. ( Functor (WrappedF a)\r\n , Foldable (WrappedF a)\r\n , Traversable (WrappedF a)\r\n )) => Traversable SomeF\r\n}}}\r\n\r\nBut then the file no longer typechecked!\r\n\r\n{{{\r\n$ /opt/ghc/8.6.1/bin/ghc Foo.hs\r\n[1 of 1] Compiling Foo ( Foo.hs, Foo.o )\r\n\r\nFoo.hs:21:1: error:\r\n • Could not deduce (Functor (F a))\r\n arising from the superclasses of an instance declaration\r\n from the context: forall a.\r\n (Functor (WrappedF a), Foldable (WrappedF a),\r\n Traversable (WrappedF a))\r\n bound by the instance declaration at Foo.hs:(21,1)(24,52)\r\n • In the instance declaration for ‘Traversable SomeF’\r\n \r\n21  deriving instance (forall a. ( Functor (WrappedF a)\r\n  ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^...\r\n\r\nFoo.hs:21:1: error:\r\n • Could not deduce (Foldable (F a))\r\n arising from the superclasses of an instance declaration\r\n from the context: forall a.\r\n (Functor (WrappedF a), Foldable (WrappedF a),\r\n Traversable (WrappedF a))\r\n bound by the instance declaration at Foo.hs:(21,1)(24,52)\r\n • In the instance declaration for ‘Traversable SomeF’\r\n \r\n21  deriving instance (forall a. ( Functor (WrappedF a)\r\n  ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^...\r\n\r\nFoo.hs:21:1: error:\r\n • Could not deduce (Traversable (F a1))\r\n arising from a use of ‘traverse’\r\n from the context: forall a.\r\n (Functor (WrappedF a), Foldable (WrappedF a),\r\n Traversable (WrappedF a))\r\n bound by the instance declaration at Foo.hs:(21,1)(24,52)\r\n or from: Applicative f\r\n bound by the type signature for:\r\n traverse :: forall (f :: * > *) a b.\r\n Applicative f =>\r\n (a > f b) > SomeF a > f (SomeF b)\r\n at Foo.hs:(21,1)(24,52)\r\n • In the second argument of ‘fmap’, namely ‘(traverse f a1)’\r\n In the expression: fmap (\\ b1 > MkSomeF b1) (traverse f a1)\r\n In an equation for ‘traverse’:\r\n traverse f (MkSomeF a1) = fmap (\\ b1 > MkSomeF b1) (traverse f a1)\r\n When typechecking the code for ‘traverse’\r\n in a derived instance for ‘Traversable SomeF’:\r\n To see the code I am typechecking, use ddumpderiv\r\n \r\n21  deriving instance (forall a. ( Functor (WrappedF a)\r\n  ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^...\r\n}}}\r\n\r\nRichard suspects that this is a bug in the way quantified constraints expands superclasses, so I decided to post it here.","type_of_failure":"OtherFailure","blocking":[]} >Consider the following code:
```hs
{# LANGUAGE DeriveTraversable #}
{# LANGUAGE ExistentialQuantification #}
{# LANGUAGE TypeFamilies #}
{# LANGUAGE QuantifiedConstraints #}
{# LANGUAGE StandaloneDeriving #}
{# LANGUAGE UndecidableInstances #}
module Foo where
import Data.Kind
type family F a :: Type > Type
newtype WrappedF a b = WrapF (F a b)
deriving instance Functor (F a) => Functor (WrappedF a)
deriving instance Foldable (F a) => Foldable (WrappedF a)
deriving instance Traversable (F a) => Traversable (WrappedF a)
data SomeF b = forall a. MkSomeF (WrappedF a b)
deriving instance (forall a. Functor (WrappedF a)) => Functor SomeF
deriving instance (forall a. Foldable (WrappedF a)) => Foldable SomeF
deriving instance ( forall a. Functor (WrappedF a)
, forall a. Foldable (WrappedF a)
, forall a. Traversable (WrappedF a)
) => Traversable SomeF
```
This typechecks. However, the last `Traversable SomeF` is a bit unfortunate in that is uses three separate `forall a.`s. I attempted to factor this out, like so:
```hs
deriving instance (forall a. ( Functor (WrappedF a)
, Foldable (WrappedF a)
, Traversable (WrappedF a)
)) => Traversable SomeF
```
But then the file no longer typechecked!
```
$ /opt/ghc/8.6.1/bin/ghc Foo.hs
[1 of 1] Compiling Foo ( Foo.hs, Foo.o )
Foo.hs:21:1: error:
• Could not deduce (Functor (F a))
arising from the superclasses of an instance declaration
from the context: forall a.
(Functor (WrappedF a), Foldable (WrappedF a),
Traversable (WrappedF a))
bound by the instance declaration at Foo.hs:(21,1)(24,52)
• In the instance declaration for ‘Traversable SomeF’

21  deriving instance (forall a. ( Functor (WrappedF a)
 ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^...
Foo.hs:21:1: error:
• Could not deduce (Foldable (F a))
arising from the superclasses of an instance declaration
from the context: forall a.
(Functor (WrappedF a), Foldable (WrappedF a),
Traversable (WrappedF a))
bound by the instance declaration at Foo.hs:(21,1)(24,52)
• In the instance declaration for ‘Traversable SomeF’

21  deriving instance (forall a. ( Functor (WrappedF a)
 ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^...
Foo.hs:21:1: error:
• Could not deduce (Traversable (F a1))
arising from a use of ‘traverse’
from the context: forall a.
(Functor (WrappedF a), Foldable (WrappedF a),
Traversable (WrappedF a))
bound by the instance declaration at Foo.hs:(21,1)(24,52)
or from: Applicative f
bound by the type signature for:
traverse :: forall (f :: * > *) a b.
Applicative f =>
(a > f b) > SomeF a > f (SomeF b)
at Foo.hs:(21,1)(24,52)
• In the second argument of ‘fmap’, namely ‘(traverse f a1)’
In the expression: fmap (\ b1 > MkSomeF b1) (traverse f a1)
In an equation for ‘traverse’:
traverse f (MkSomeF a1) = fmap (\ b1 > MkSomeF b1) (traverse f a1)
When typechecking the code for ‘traverse’
in a derived instance for ‘Traversable SomeF’:
To see the code I am typechecking, use ddumpderiv

21  deriving instance (forall a. ( Functor (WrappedF a)
 ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^...
```
Richard suspects that this is a bug in the way quantified constraints expands superclasses, so I decided to post it here.
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.5 
 Type  Bug 
 TypeOfFailure  OtherFailure 
 Priority  normal 
 Resolution  Unresolved 
 Component  Compiler (Type checker) 
 Test case  
 Differential revisions  
 BlockedBy  
 Related  
 Blocking  
 CC  
 Operating system  
 Architecture  
</details>
<! {"blocked_by":[],"summary":"(forall x. c x, forall x. d x) is not equivalent to forall x. (c x, d x)","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"8.6.1","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.5","keywords":["QuantifiedConstraints"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"Consider the following code:\r\n\r\n{{{#!hs\r\n{# LANGUAGE DeriveTraversable #}\r\n{# LANGUAGE ExistentialQuantification #}\r\n{# LANGUAGE TypeFamilies #}\r\n{# LANGUAGE QuantifiedConstraints #}\r\n{# LANGUAGE StandaloneDeriving #}\r\n{# LANGUAGE UndecidableInstances #}\r\nmodule Foo where\r\n\r\nimport Data.Kind\r\n\r\ntype family F a :: Type > Type\r\nnewtype WrappedF a b = WrapF (F a b)\r\nderiving instance Functor (F a) => Functor (WrappedF a)\r\nderiving instance Foldable (F a) => Foldable (WrappedF a)\r\nderiving instance Traversable (F a) => Traversable (WrappedF a)\r\n\r\ndata SomeF b = forall a. MkSomeF (WrappedF a b)\r\n\r\nderiving instance (forall a. Functor (WrappedF a)) => Functor SomeF\r\nderiving instance (forall a. Foldable (WrappedF a)) => Foldable SomeF\r\nderiving instance ( forall a. Functor (WrappedF a)\r\n , forall a. Foldable (WrappedF a)\r\n , forall a. Traversable (WrappedF a)\r\n ) => Traversable SomeF\r\n}}}\r\n\r\nThis typechecks. However, the last `Traversable SomeF` is a bit unfortunate in that is uses three separate `forall a.`s. I attempted to factor this out, like so:\r\n\r\n{{{#!hs\r\nderiving instance (forall a. ( Functor (WrappedF a)\r\n , Foldable (WrappedF a)\r\n , Traversable (WrappedF a)\r\n )) => Traversable SomeF\r\n}}}\r\n\r\nBut then the file no longer typechecked!\r\n\r\n{{{\r\n$ /opt/ghc/8.6.1/bin/ghc Foo.hs\r\n[1 of 1] Compiling Foo ( Foo.hs, Foo.o )\r\n\r\nFoo.hs:21:1: error:\r\n • Could not deduce (Functor (F a))\r\n arising from the superclasses of an instance declaration\r\n from the context: forall a.\r\n (Functor (WrappedF a), Foldable (WrappedF a),\r\n Traversable (WrappedF a))\r\n bound by the instance declaration at Foo.hs:(21,1)(24,52)\r\n • In the instance declaration for ‘Traversable SomeF’\r\n \r\n21  deriving instance (forall a. ( Functor (WrappedF a)\r\n  ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^...\r\n\r\nFoo.hs:21:1: error:\r\n • Could not deduce (Foldable (F a))\r\n arising from the superclasses of an instance declaration\r\n from the context: forall a.\r\n (Functor (WrappedF a), Foldable (WrappedF a),\r\n Traversable (WrappedF a))\r\n bound by the instance declaration at Foo.hs:(21,1)(24,52)\r\n • In the instance declaration for ‘Traversable SomeF’\r\n \r\n21  deriving instance (forall a. ( Functor (WrappedF a)\r\n  ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^...\r\n\r\nFoo.hs:21:1: error:\r\n • Could not deduce (Traversable (F a1))\r\n arising from a use of ‘traverse’\r\n from the context: forall a.\r\n (Functor (WrappedF a), Foldable (WrappedF a),\r\n Traversable (WrappedF a))\r\n bound by the instance declaration at Foo.hs:(21,1)(24,52)\r\n or from: Applicative f\r\n bound by the type signature for:\r\n traverse :: forall (f :: * > *) a b.\r\n Applicative f =>\r\n (a > f b) > SomeF a > f (SomeF b)\r\n at Foo.hs:(21,1)(24,52)\r\n • In the second argument of ‘fmap’, namely ‘(traverse f a1)’\r\n In the expression: fmap (\\ b1 > MkSomeF b1) (traverse f a1)\r\n In an equation for ‘traverse’:\r\n traverse f (MkSomeF a1) = fmap (\\ b1 > MkSomeF b1) (traverse f a1)\r\n When typechecking the code for ‘traverse’\r\n in a derived instance for ‘Traversable SomeF’:\r\n To see the code I am typechecking, use ddumpderiv\r\n \r\n21  deriving instance (forall a. ( Functor (WrappedF a)\r\n  ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^...\r\n}}}\r\n\r\nRichard suspects that this is a bug in the way quantified constraints expands superclasses, so I decided to post it here.","type_of_failure":"OtherFailure","blocking":[]} >8.8.1https://gitlab.haskell.org/ghc/ghc//issues/15316Regarding coherence and implication loops in presence of QuantifiedConstraints20201003T12:38:44ZmniipRegarding coherence and implication loops in presence of QuantifiedConstraintsFirst of all this piece of code:
```hs
{# LANGUAGE RankNTypes, QuantifiedConstraints #}
 NB: disabling these if enabled:
{# LANGUAGE NoUndecidableInstances, NoUndecidableSuperClasses #}
import Data.Proxy
class Class a where
method :: a
subsume :: (Class a => Class b) => Proxy a > Proxy b > ((Class a => Class b) => r) > r
subsume _ _ x = x
value :: Proxy a > a
value p = subsume p p method
```
This produces a nonterminating `value` even though nothing warranting recursion was used.
Adding:
```hs
value' :: Class a => Proxy a > a
value' p = subsume p p method
```
Produces a `value'` that is legitimately equivalent to `method` in that it equals to the value in the dictionary whenever an instance exists (and doesn't typecheck otherwise). Thus two identical expressions in different instance contexts end up having different values (violating coherence?)
If we add:
```hs
joinSubsume :: Proxy a > ((Class a => Class a) => r) > r
joinSubsume p x = subsume p p x
```
The fact that this typechecks suggests that GHC is able to infer `Class a => Class a` at will, which doesn't seem wrong. However, the fact that `Class a` is solved from `Class a => Class a` via an infinite loop of implication constraints is questionable. Probably even outright wrong in absence of `UndecidableInstances`.
Another issue is the following:
```hs
{# LANGUAGE ConstraintKinds #}
subsume' :: Proxy c > ((c => c) => r) > r
subsume' _ x = x
```
```
• Reduction stack overflow; size = 201
When simplifying the following type: c
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 type signature:
subsume' :: Proxy c > ((c => c) => r) > r
```
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.4.3 
 Type  Bug 
 TypeOfFailure  OtherFailure 
 Priority  high 
 Resolution  Unresolved 
 Component  Compiler (Type checker) 
 Test case  
 Differential revisions  
 BlockedBy  
 Related  
 Blocking  
 CC  
 Operating system  
 Architecture  
</details>
<! {"blocked_by":[],"summary":"Regarding coherence and implication loops in presence of QuantifiedConstraints","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"8.6.1","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.4.3","keywords":["QuantifiedConstraints"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"First of all this piece of code:\r\n{{{#!hs\r\n{# LANGUAGE RankNTypes, QuantifiedConstraints #}\r\n NB: disabling these if enabled:\r\n{# LANGUAGE NoUndecidableInstances, NoUndecidableSuperClasses #}\r\n\r\nimport Data.Proxy\r\n\r\nclass Class a where\r\n\t method :: a\r\n\r\nsubsume :: (Class a => Class b) => Proxy a > Proxy b > ((Class a => Class b) => r) > r\r\nsubsume _ _ x = x\r\n\r\nvalue :: Proxy a > a\r\nvalue p = subsume p p method\r\n}}}\r\n\r\nThis produces a nonterminating `value` even though nothing warranting recursion was used.\r\n\r\nAdding:\r\n{{{#!hs\r\nvalue' :: Class a => Proxy a > a\r\nvalue' p = subsume p p method\r\n}}}\r\nProduces a `value'` that is legitimately equivalent to `method` in that it equals to the value in the dictionary whenever an instance exists (and doesn't typecheck otherwise). Thus two identical expressions in different instance contexts end up having different values (violating coherence?)\r\n\r\nIf we add:\r\n{{{#!hs\r\njoinSubsume :: Proxy a > ((Class a => Class a) => r) > r\r\njoinSubsume p x = subsume p p x\r\n}}}\r\nThe fact that this typechecks suggests that GHC is able to infer `Class a => Class a` at will, which doesn't seem wrong. However, the fact that `Class a` is solved from `Class a => Class a` via an infinite loop of implication constraints is questionable. Probably even outright wrong in absence of `UndecidableInstances`.\r\n\r\nAnother issue is the following:\r\n{{{#!hs\r\n{# LANGUAGE ConstraintKinds #}\r\nsubsume' :: Proxy c > ((c => c) => r) > r\r\nsubsume' _ x = x\r\n}}}\r\n{{{\r\n • Reduction stack overflow; size = 201\r\n When simplifying the following type: c\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 type signature:\r\n subsume' :: Proxy c > ((c => c) => r) > r\r\n}}}","type_of_failure":"OtherFailure","blocking":[]} >First of all this piece of code:
```hs
{# LANGUAGE RankNTypes, QuantifiedConstraints #}
 NB: disabling these if enabled:
{# LANGUAGE NoUndecidableInstances, NoUndecidableSuperClasses #}
import Data.Proxy
class Class a where
method :: a
subsume :: (Class a => Class b) => Proxy a > Proxy b > ((Class a => Class b) => r) > r
subsume _ _ x = x
value :: Proxy a > a
value p = subsume p p method
```
This produces a nonterminating `value` even though nothing warranting recursion was used.
Adding:
```hs
value' :: Class a => Proxy a > a
value' p = subsume p p method
```
Produces a `value'` that is legitimately equivalent to `method` in that it equals to the value in the dictionary whenever an instance exists (and doesn't typecheck otherwise). Thus two identical expressions in different instance contexts end up having different values (violating coherence?)
If we add:
```hs
joinSubsume :: Proxy a > ((Class a => Class a) => r) > r
joinSubsume p x = subsume p p x
```
The fact that this typechecks suggests that GHC is able to infer `Class a => Class a` at will, which doesn't seem wrong. However, the fact that `Class a` is solved from `Class a => Class a` via an infinite loop of implication constraints is questionable. Probably even outright wrong in absence of `UndecidableInstances`.
Another issue is the following:
```hs
{# LANGUAGE ConstraintKinds #}
subsume' :: Proxy c > ((c => c) => r) > r
subsume' _ x = x
```
```
• Reduction stack overflow; size = 201
When simplifying the following type: c
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 type signature:
subsume' :: Proxy c > ((c => c) => r) > r
```
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.4.3 
 Type  Bug 
 TypeOfFailure  OtherFailure 
 Priority  high 
 Resolution  Unresolved 
 Component  Compiler (Type checker) 
 Test case  
 Differential revisions  
 BlockedBy  
 Related  
 Blocking  
 CC  
 Operating system  
 Architecture  
</details>
<! {"blocked_by":[],"summary":"Regarding coherence and implication loops in presence of QuantifiedConstraints","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"8.6.1","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.4.3","keywords":["QuantifiedConstraints"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"First of all this piece of code:\r\n{{{#!hs\r\n{# LANGUAGE RankNTypes, QuantifiedConstraints #}\r\n NB: disabling these if enabled:\r\n{# LANGUAGE NoUndecidableInstances, NoUndecidableSuperClasses #}\r\n\r\nimport Data.Proxy\r\n\r\nclass Class a where\r\n\t method :: a\r\n\r\nsubsume :: (Class a => Class b) => Proxy a > Proxy b > ((Class a => Class b) => r) > r\r\nsubsume _ _ x = x\r\n\r\nvalue :: Proxy a > a\r\nvalue p = subsume p p method\r\n}}}\r\n\r\nThis produces a nonterminating `value` even though nothing warranting recursion was used.\r\n\r\nAdding:\r\n{{{#!hs\r\nvalue' :: Class a => Proxy a > a\r\nvalue' p = subsume p p method\r\n}}}\r\nProduces a `value'` that is legitimately equivalent to `method` in that it equals to the value in the dictionary whenever an instance exists (and doesn't typecheck otherwise). Thus two identical expressions in different instance contexts end up having different values (violating coherence?)\r\n\r\nIf we add:\r\n{{{#!hs\r\njoinSubsume :: Proxy a > ((Class a => Class a) => r) > r\r\njoinSubsume p x = subsume p p x\r\n}}}\r\nThe fact that this typechecks suggests that GHC is able to infer `Class a => Class a` at will, which doesn't seem wrong. However, the fact that `Class a` is solved from `Class a => Class a` via an infinite loop of implication constraints is questionable. Probably even outright wrong in absence of `UndecidableInstances`.\r\n\r\nAnother issue is the following:\r\n{{{#!hs\r\n{# LANGUAGE ConstraintKinds #}\r\nsubsume' :: Proxy c > ((c => c) => r) > r\r\nsubsume' _ x = x\r\n}}}\r\n{{{\r\n • Reduction stack overflow; size = 201\r\n When simplifying the following type: c\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 type signature:\r\n subsume' :: Proxy c > ((c => c) => r) > r\r\n}}}","type_of_failure":"OtherFailure","blocking":[]} >8.8.1Ben GamariBen Gamari