GHC issueshttps://gitlab.haskell.org/ghc/ghc/-/issues2020-10-03T12:38:44Zhttps://gitlab.haskell.org/ghc/ghc/-/issues/15316Regarding coherence and implication loops in presence of QuantifiedConstraints2020-10-03T12: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
me...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 -freduction-depth=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 -freduction-depth=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 Gamarihttps://gitlab.haskell.org/ghc/ghc/-/issues/15359Quantified constraints do not work with equality constraints2019-07-07T18: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 r...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 user-specified 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 user-specified 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)2019-08-05T08: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 Undec...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 -ddump-deriv
|
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 -ddump-deriv\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.1