GHC issueshttps://gitlab.haskell.org/ghc/ghc//issues20190707T18:15:24Zhttps://gitlab.haskell.org/ghc/ghc//issues/14831QuantifiedConstraints: Odd superclass constraint20190707T18:15:24ZIcelandjackQuantifiedConstraints: Odd superclass constraintThis code works
```hs
{# Language QuantifiedConstraints, RankNTypes, PolyKinds, ConstraintKinds, UndecidableInstances #}
import Data.Semigroup
newtype Free cls a = Free ()
instance (forall xx. cls xx => Semigroup xx) => Semigroup (Free cls a) where
(<>) = undefined
stimes = undefined
sconcat = undefined
 instance (forall xx. cls xx => Semigroup xx) => Monoid (Free cls a) where
 mempty = undefined
```
but uncomment the `Monoid` instance and we get
```
$ ghci ignoredotghci /tmp/I.hs
GHCi, version 8.5.20180128: http://www.haskell.org/ghc/ :? for help
[1 of 1] Compiling Main ( /tmp/I.hs, interpreted )
/tmp/I.hs:12:10: error:
• Could not deduce: cls (Free cls a)
arising from the superclasses of an instance declaration
from the context: forall xx. cls xx => Semigroup xx
bound by the instance declaration at /tmp/I.hs:12:1067
• In the instance declaration for ‘Monoid (Free cls a)’

12  instance (forall xx. cls xx => Semigroup xx) => Monoid (Free cls a) where
 ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
Failed, no modules loaded.
Prelude>
```
Is this correct behavior?
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.5 
 Type  Bug 
 TypeOfFailure  OtherFailure 
 Priority  normal 
 Resolution  Unresolved 
 Component  Compiler 
 Test case  
 Differential revisions  
 BlockedBy  
 Related  
 Blocking  
 CC  
 Operating system  
 Architecture  
</details>
<! {"blocked_by":[],"summary":"QuantifiedConstraints: Odd superclass constraint","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.5","keywords":["QuantifiedConstraints","wipT2893"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"This code works\r\n\r\n{{{#!hs\r\n{# Language QuantifiedConstraints, RankNTypes, PolyKinds, ConstraintKinds, UndecidableInstances #}\r\n\r\nimport Data.Semigroup\r\n\r\nnewtype Free cls a = Free ()\r\n\r\ninstance (forall xx. cls xx => Semigroup xx) => Semigroup (Free cls a) where\r\n (<>) = undefined \r\n stimes = undefined\r\n sconcat = undefined\r\n\r\n instance (forall xx. cls xx => Semigroup xx) => Monoid (Free cls a) where\r\n mempty = undefined \r\n}}}\r\n\r\nbut uncomment the `Monoid` instance and we get\r\n\r\n{{{\r\n$ ghci ignoredotghci /tmp/I.hs\r\nGHCi, version 8.5.20180128: http://www.haskell.org/ghc/ :? for help\r\n[1 of 1] Compiling Main ( /tmp/I.hs, interpreted )\r\n\r\n/tmp/I.hs:12:10: error:\r\n • Could not deduce: cls (Free cls a)\r\n arising from the superclasses of an instance declaration\r\n from the context: forall xx. cls xx => Semigroup xx\r\n bound by the instance declaration at /tmp/I.hs:12:1067\r\n • In the instance declaration for ‘Monoid (Free cls a)’\r\n \r\n12  instance (forall xx. cls xx => Semigroup xx) => Monoid (Free cls a) where\r\n  ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^\r\nFailed, no modules loaded.\r\nPrelude> \r\n}}}\r\n\r\nIs this correct behavior?","type_of_failure":"OtherFailure","blocking":[]} >This code works
```hs
{# Language QuantifiedConstraints, RankNTypes, PolyKinds, ConstraintKinds, UndecidableInstances #}
import Data.Semigroup
newtype Free cls a = Free ()
instance (forall xx. cls xx => Semigroup xx) => Semigroup (Free cls a) where
(<>) = undefined
stimes = undefined
sconcat = undefined
 instance (forall xx. cls xx => Semigroup xx) => Monoid (Free cls a) where
 mempty = undefined
```
but uncomment the `Monoid` instance and we get
```
$ ghci ignoredotghci /tmp/I.hs
GHCi, version 8.5.20180128: http://www.haskell.org/ghc/ :? for help
[1 of 1] Compiling Main ( /tmp/I.hs, interpreted )
/tmp/I.hs:12:10: error:
• Could not deduce: cls (Free cls a)
arising from the superclasses of an instance declaration
from the context: forall xx. cls xx => Semigroup xx
bound by the instance declaration at /tmp/I.hs:12:1067
• In the instance declaration for ‘Monoid (Free cls a)’

12  instance (forall xx. cls xx => Semigroup xx) => Monoid (Free cls a) where
 ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
Failed, no modules loaded.
Prelude>
```
Is this correct behavior?
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.5 
 Type  Bug 
 TypeOfFailure  OtherFailure 
 Priority  normal 
 Resolution  Unresolved 
 Component  Compiler 
 Test case  
 Differential revisions  
 BlockedBy  
 Related  
 Blocking  
 CC  
 Operating system  
 Architecture  
</details>
<! {"blocked_by":[],"summary":"QuantifiedConstraints: Odd superclass constraint","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.5","keywords":["QuantifiedConstraints","wipT2893"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"This code works\r\n\r\n{{{#!hs\r\n{# Language QuantifiedConstraints, RankNTypes, PolyKinds, ConstraintKinds, UndecidableInstances #}\r\n\r\nimport Data.Semigroup\r\n\r\nnewtype Free cls a = Free ()\r\n\r\ninstance (forall xx. cls xx => Semigroup xx) => Semigroup (Free cls a) where\r\n (<>) = undefined \r\n stimes = undefined\r\n sconcat = undefined\r\n\r\n instance (forall xx. cls xx => Semigroup xx) => Monoid (Free cls a) where\r\n mempty = undefined \r\n}}}\r\n\r\nbut uncomment the `Monoid` instance and we get\r\n\r\n{{{\r\n$ ghci ignoredotghci /tmp/I.hs\r\nGHCi, version 8.5.20180128: http://www.haskell.org/ghc/ :? for help\r\n[1 of 1] Compiling Main ( /tmp/I.hs, interpreted )\r\n\r\n/tmp/I.hs:12:10: error:\r\n • Could not deduce: cls (Free cls a)\r\n arising from the superclasses of an instance declaration\r\n from the context: forall xx. cls xx => Semigroup xx\r\n bound by the instance declaration at /tmp/I.hs:12:1067\r\n • In the instance declaration for ‘Monoid (Free cls a)’\r\n \r\n12  instance (forall xx. cls xx => Semigroup xx) => Monoid (Free cls a) where\r\n  ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^\r\nFailed, no modules loaded.\r\nPrelude> \r\n}}}\r\n\r\nIs this correct behavior?","type_of_failure":"OtherFailure","blocking":[]} >https://gitlab.haskell.org/ghc/ghc//issues/14832QuantifiedConstraints: Adding to the context causes failure20190707T18:15:24ZIcelandjackQuantifiedConstraints: Adding to the context causes failureWith Simon's latest changes (ticket:14733\##14832) this works:
```hs
{# Language QuantifiedConstraints, RankNTypes, PolyKinds, ConstraintKinds, UndecidableInstances, GADTs #}
import Control.Category
import Data.Kind
import Data.Coerce
data With cls a b where
With :: cls a b => With cls a b
type Coercion = With Coercible
type Refl rel = (forall xx. rel xx xx :: Constraint)
type Trans rel = (forall xx yy zz. (rel xx yy, rel yy zz) => rel xx zz :: Constraint)
instance Refl rel => Category (With rel) where
id = With
(.) = undefined
```
But strengthening the context with `Trans rel`:
```hs
instance (Refl rel, Trans rel) => Category (With rel) where
```
causes it to fail
```
GHCi, version 8.5.20180128: http://www.haskell.org/ghc/ :? for help
[1 of 1] Compiling Main ( J.hs, interpreted )
J.hs:15:10: error:
• Could not deduce: rel xx zz
from the context: (Refl rel, Trans rel)
bound by an instance declaration:
forall k (rel :: k > k > Constraint).
(Refl rel, Trans rel) =>
Category (With rel)
at J.hs:15:1053
or from: (rel xx yy, rel yy zz)
bound by a quantified context at J.hs:15:1053
• In the ambiguity check for an instance declaration
To defer the ambiguity check to use sites, enable AllowAmbiguousTypes
In the instance declaration for ‘Category (With rel)’

15  instance (Refl rel, Trans rel) => Category (With rel) where
 ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
J.hs:15:10: error:
• Could not deduce: rel xx xx
from the context: (Refl rel, Trans rel)
bound by an instance declaration:
forall k (rel :: k > k > Constraint).
(Refl rel, Trans rel) =>
Category (With rel)
at J.hs:15:1053
• In the ambiguity check for an instance declaration
To defer the ambiguity check to use sites, enable AllowAmbiguousTypes
In the instance declaration for ‘Category (With rel)’

15  instance (Refl rel, Trans rel) => Category (With rel) where
 ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
Failed, no modules loaded.
Prelude>
```
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.5 
 Type  Bug 
 TypeOfFailure  OtherFailure 
 Priority  normal 
 Resolution  Unresolved 
 Component  Compiler 
 Test case  
 Differential revisions  
 BlockedBy  
 Related  
 Blocking  
 CC  
 Operating system  
 Architecture  
</details>
<! {"blocked_by":[],"summary":"QuantifiedConstraints: Strengthening context causes failure","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.5","keywords":["QuantifiedConstraints","wipT2893"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"With Simon's latest changes (ticket:14733#comment:9) this works:\r\n\r\n{{{#!hs\r\n{# Language QuantifiedConstraints, RankNTypes, PolyKinds, ConstraintKinds, UndecidableInstances, GADTs #}\r\n\r\nimport Control.Category\r\nimport Data.Kind\r\nimport Data.Coerce\r\n\r\ndata With cls a b where\r\n With :: cls a b => With cls a b\r\n\r\ntype Coercion = With Coercible\r\n\r\ntype Refl rel = (forall xx. rel xx xx :: Constraint)\r\ntype Trans rel = (forall xx yy zz. (rel xx yy, rel yy zz) => rel xx zz :: Constraint)\r\n\r\ninstance Refl rel => Category (With rel) where\r\n id = With\r\n (.) = undefined\r\n}}}\r\n\r\nBut strengthening the context with `Trans rel`:\r\n\r\n{{{#!hs\r\ninstance (Refl rel, Trans rel) => Category (With rel) where\r\n}}}\r\n\r\ncauses it to fail\r\n\r\n{{{\r\nGHCi, version 8.5.20180128: http://www.haskell.org/ghc/ :? for help\r\n[1 of 1] Compiling Main ( J.hs, interpreted )\r\n\r\nJ.hs:15:10: error:\r\n • Could not deduce: rel xx zz\r\n from the context: (Refl rel, Trans rel)\r\n bound by an instance declaration:\r\n forall k (rel :: k > k > Constraint).\r\n (Refl rel, Trans rel) =>\r\n Category (With rel)\r\n at J.hs:15:1053\r\n or from: (rel xx yy, rel yy zz)\r\n bound by a quantified context at J.hs:15:1053\r\n • In the ambiguity check for an instance declaration\r\n To defer the ambiguity check to use sites, enable AllowAmbiguousTypes\r\n In the instance declaration for ‘Category (With rel)’\r\n \r\n15  instance (Refl rel, Trans rel) => Category (With rel) where\r\n  ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^\r\n\r\nJ.hs:15:10: error:\r\n • Could not deduce: rel xx xx\r\n from the context: (Refl rel, Trans rel)\r\n bound by an instance declaration:\r\n forall k (rel :: k > k > Constraint).\r\n (Refl rel, Trans rel) =>\r\n Category (With rel)\r\n at J.hs:15:1053\r\n • In the ambiguity check for an instance declaration\r\n To defer the ambiguity check to use sites, enable AllowAmbiguousTypes\r\n In the instance declaration for ‘Category (With rel)’\r\n \r\n15  instance (Refl rel, Trans rel) => Category (With rel) where\r\n  ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^\r\nFailed, no modules loaded.\r\nPrelude> \r\n}}}","type_of_failure":"OtherFailure","blocking":[]} >With Simon's latest changes (ticket:14733\##14832) this works:
```hs
{# Language QuantifiedConstraints, RankNTypes, PolyKinds, ConstraintKinds, UndecidableInstances, GADTs #}
import Control.Category
import Data.Kind
import Data.Coerce
data With cls a b where
With :: cls a b => With cls a b
type Coercion = With Coercible
type Refl rel = (forall xx. rel xx xx :: Constraint)
type Trans rel = (forall xx yy zz. (rel xx yy, rel yy zz) => rel xx zz :: Constraint)
instance Refl rel => Category (With rel) where
id = With
(.) = undefined
```
But strengthening the context with `Trans rel`:
```hs
instance (Refl rel, Trans rel) => Category (With rel) where
```
causes it to fail
```
GHCi, version 8.5.20180128: http://www.haskell.org/ghc/ :? for help
[1 of 1] Compiling Main ( J.hs, interpreted )
J.hs:15:10: error:
• Could not deduce: rel xx zz
from the context: (Refl rel, Trans rel)
bound by an instance declaration:
forall k (rel :: k > k > Constraint).
(Refl rel, Trans rel) =>
Category (With rel)
at J.hs:15:1053
or from: (rel xx yy, rel yy zz)
bound by a quantified context at J.hs:15:1053
• In the ambiguity check for an instance declaration
To defer the ambiguity check to use sites, enable AllowAmbiguousTypes
In the instance declaration for ‘Category (With rel)’

15  instance (Refl rel, Trans rel) => Category (With rel) where
 ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
J.hs:15:10: error:
• Could not deduce: rel xx xx
from the context: (Refl rel, Trans rel)
bound by an instance declaration:
forall k (rel :: k > k > Constraint).
(Refl rel, Trans rel) =>
Category (With rel)
at J.hs:15:1053
• In the ambiguity check for an instance declaration
To defer the ambiguity check to use sites, enable AllowAmbiguousTypes
In the instance declaration for ‘Category (With rel)’

15  instance (Refl rel, Trans rel) => Category (With rel) where
 ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
Failed, no modules loaded.
Prelude>
```
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.5 
 Type  Bug 
 TypeOfFailure  OtherFailure 
 Priority  normal 
 Resolution  Unresolved 
 Component  Compiler 
 Test case  
 Differential revisions  
 BlockedBy  
 Related  
 Blocking  
 CC  
 Operating system  
 Architecture  
</details>
<! {"blocked_by":[],"summary":"QuantifiedConstraints: Strengthening context causes failure","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.5","keywords":["QuantifiedConstraints","wipT2893"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"With Simon's latest changes (ticket:14733#comment:9) this works:\r\n\r\n{{{#!hs\r\n{# Language QuantifiedConstraints, RankNTypes, PolyKinds, ConstraintKinds, UndecidableInstances, GADTs #}\r\n\r\nimport Control.Category\r\nimport Data.Kind\r\nimport Data.Coerce\r\n\r\ndata With cls a b where\r\n With :: cls a b => With cls a b\r\n\r\ntype Coercion = With Coercible\r\n\r\ntype Refl rel = (forall xx. rel xx xx :: Constraint)\r\ntype Trans rel = (forall xx yy zz. (rel xx yy, rel yy zz) => rel xx zz :: Constraint)\r\n\r\ninstance Refl rel => Category (With rel) where\r\n id = With\r\n (.) = undefined\r\n}}}\r\n\r\nBut strengthening the context with `Trans rel`:\r\n\r\n{{{#!hs\r\ninstance (Refl rel, Trans rel) => Category (With rel) where\r\n}}}\r\n\r\ncauses it to fail\r\n\r\n{{{\r\nGHCi, version 8.5.20180128: http://www.haskell.org/ghc/ :? for help\r\n[1 of 1] Compiling Main ( J.hs, interpreted )\r\n\r\nJ.hs:15:10: error:\r\n • Could not deduce: rel xx zz\r\n from the context: (Refl rel, Trans rel)\r\n bound by an instance declaration:\r\n forall k (rel :: k > k > Constraint).\r\n (Refl rel, Trans rel) =>\r\n Category (With rel)\r\n at J.hs:15:1053\r\n or from: (rel xx yy, rel yy zz)\r\n bound by a quantified context at J.hs:15:1053\r\n • In the ambiguity check for an instance declaration\r\n To defer the ambiguity check to use sites, enable AllowAmbiguousTypes\r\n In the instance declaration for ‘Category (With rel)’\r\n \r\n15  instance (Refl rel, Trans rel) => Category (With rel) where\r\n  ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^\r\n\r\nJ.hs:15:10: error:\r\n • Could not deduce: rel xx xx\r\n from the context: (Refl rel, Trans rel)\r\n bound by an instance declaration:\r\n forall k (rel :: k > k > Constraint).\r\n (Refl rel, Trans rel) =>\r\n Category (With rel)\r\n at J.hs:15:1053\r\n • In the ambiguity check for an instance declaration\r\n To defer the ambiguity check to use sites, enable AllowAmbiguousTypes\r\n In the instance declaration for ‘Category (With rel)’\r\n \r\n15  instance (Refl rel, Trans rel) => Category (With rel) where\r\n  ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^\r\nFailed, no modules loaded.\r\nPrelude> \r\n}}}","type_of_failure":"OtherFailure","blocking":[]} >https://gitlab.haskell.org/ghc/ghc//issues/14860QuantifiedConstraints: Can't quantify constraint involving type family20200207T14:09:10ZRyan ScottQuantifiedConstraints: Can't quantify constraint involving type familyThis program fails to typecheck using the `wip/T2893` branch, to my surprise:
```hs
{# LANGUAGE AllowAmbiguousTypes #}
{# LANGUAGE GADTs #}
{# LANGUAGE QuantifiedConstraints #}
{# LANGUAGE TypeFamilies #}
{# LANGUAGE UndecidableInstances #}
module Bug where
import Data.Proxy
type family Apply (f :: * > *) a
type instance Apply Proxy a = Proxy a
data ExTyFam f where
MkExTyFam :: Apply f a > ExTyFam f
instance (forall a. Show (Apply f a)) => Show (ExTyFam f) where
show (MkExTyFam x) = show x
showsPrec = undefined  Not defining these leads to the oddities observed in
showList = undefined  https://ghc.haskell.org/trac/ghc/ticket/5927#comment:32
test :: ExTyFam Proxy > String
test = show
```
This fails with:
```
$ ghccq/inplace/bin/ghcstage2 interactive Bug.hs
GHCi, version 8.5.20180128: http://www.haskell.org/ghc/ :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
[1 of 1] Compiling Bug ( Bug.hs, interpreted )
Bug.hs:17:24: error:
• Could not deduce (Show (Apply f a)) arising from a use of ‘show’
from the context: forall a. Show (Apply f a)
bound by the instance declaration at Bug.hs:16:1057
• In the expression: show x
In an equation for ‘show’: show (MkExTyFam x) = show x
In the instance declaration for ‘Show (ExTyFam f)’

17  show (MkExTyFam x) = show x
 ^^^^^^
```
I would have expected the `(forall a. Show (Apply f a))` quantified constraint to kick in, but it didn't.
<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":"QuantifiedConstraints: Can't quantify constraint involving type family","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.5","keywords":["QuantifiedConstraints","wipT2893"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"This program fails to typecheck using the `wip/T2893` branch, to my surprise:\r\n\r\n{{{#!hs\r\n{# LANGUAGE AllowAmbiguousTypes #}\r\n{# LANGUAGE GADTs #}\r\n{# LANGUAGE QuantifiedConstraints #}\r\n{# LANGUAGE TypeFamilies #}\r\n{# LANGUAGE UndecidableInstances #}\r\nmodule Bug where\r\n\r\nimport Data.Proxy\r\n\r\ntype family Apply (f :: * > *) a\r\ntype instance Apply Proxy a = Proxy a\r\n\r\ndata ExTyFam f where\r\n MkExTyFam :: Apply f a > ExTyFam f\r\n\r\ninstance (forall a. Show (Apply f a)) => Show (ExTyFam f) where\r\n show (MkExTyFam x) = show x\r\n showsPrec = undefined  Not defining these leads to the oddities observed in\r\n showList = undefined  https://ghc.haskell.org/trac/ghc/ticket/5927#comment:32\r\n\r\ntest :: ExTyFam Proxy > String\r\ntest = show\r\n}}}\r\n\r\nThis fails with:\r\n\r\n{{{\r\n$ ghccq/inplace/bin/ghcstage2 interactive Bug.hs\r\nGHCi, version 8.5.20180128: http://www.haskell.org/ghc/ :? for help\r\nLoaded GHCi configuration from /home/rgscott/.ghci\r\n[1 of 1] Compiling Bug ( Bug.hs, interpreted )\r\n\r\nBug.hs:17:24: error:\r\n • Could not deduce (Show (Apply f a)) arising from a use of ‘show’\r\n from the context: forall a. Show (Apply f a)\r\n bound by the instance declaration at Bug.hs:16:1057\r\n • In the expression: show x\r\n In an equation for ‘show’: show (MkExTyFam x) = show x\r\n In the instance declaration for ‘Show (ExTyFam f)’\r\n \r\n17  show (MkExTyFam x) = show x\r\n  ^^^^^^\r\n}}}\r\n\r\nI would have expected the `(forall a. Show (Apply f a))` quantified constraint to kick in, but it didn't.","type_of_failure":"OtherFailure","blocking":[]} >This program fails to typecheck using the `wip/T2893` branch, to my surprise:
```hs
{# LANGUAGE AllowAmbiguousTypes #}
{# LANGUAGE GADTs #}
{# LANGUAGE QuantifiedConstraints #}
{# LANGUAGE TypeFamilies #}
{# LANGUAGE UndecidableInstances #}
module Bug where
import Data.Proxy
type family Apply (f :: * > *) a
type instance Apply Proxy a = Proxy a
data ExTyFam f where
MkExTyFam :: Apply f a > ExTyFam f
instance (forall a. Show (Apply f a)) => Show (ExTyFam f) where
show (MkExTyFam x) = show x
showsPrec = undefined  Not defining these leads to the oddities observed in
showList = undefined  https://ghc.haskell.org/trac/ghc/ticket/5927#comment:32
test :: ExTyFam Proxy > String
test = show
```
This fails with:
```
$ ghccq/inplace/bin/ghcstage2 interactive Bug.hs
GHCi, version 8.5.20180128: http://www.haskell.org/ghc/ :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
[1 of 1] Compiling Bug ( Bug.hs, interpreted )
Bug.hs:17:24: error:
• Could not deduce (Show (Apply f a)) arising from a use of ‘show’
from the context: forall a. Show (Apply f a)
bound by the instance declaration at Bug.hs:16:1057
• In the expression: show x
In an equation for ‘show’: show (MkExTyFam x) = show x
In the instance declaration for ‘Show (ExTyFam f)’

17  show (MkExTyFam x) = show x
 ^^^^^^
```
I would have expected the `(forall a. Show (Apply f a))` quantified constraint to kick in, but it didn't.
<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":"QuantifiedConstraints: Can't quantify constraint involving type family","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.5","keywords":["QuantifiedConstraints","wipT2893"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"This program fails to typecheck using the `wip/T2893` branch, to my surprise:\r\n\r\n{{{#!hs\r\n{# LANGUAGE AllowAmbiguousTypes #}\r\n{# LANGUAGE GADTs #}\r\n{# LANGUAGE QuantifiedConstraints #}\r\n{# LANGUAGE TypeFamilies #}\r\n{# LANGUAGE UndecidableInstances #}\r\nmodule Bug where\r\n\r\nimport Data.Proxy\r\n\r\ntype family Apply (f :: * > *) a\r\ntype instance Apply Proxy a = Proxy a\r\n\r\ndata ExTyFam f where\r\n MkExTyFam :: Apply f a > ExTyFam f\r\n\r\ninstance (forall a. Show (Apply f a)) => Show (ExTyFam f) where\r\n show (MkExTyFam x) = show x\r\n showsPrec = undefined  Not defining these leads to the oddities observed in\r\n showList = undefined  https://ghc.haskell.org/trac/ghc/ticket/5927#comment:32\r\n\r\ntest :: ExTyFam Proxy > String\r\ntest = show\r\n}}}\r\n\r\nThis fails with:\r\n\r\n{{{\r\n$ ghccq/inplace/bin/ghcstage2 interactive Bug.hs\r\nGHCi, version 8.5.20180128: http://www.haskell.org/ghc/ :? for help\r\nLoaded GHCi configuration from /home/rgscott/.ghci\r\n[1 of 1] Compiling Bug ( Bug.hs, interpreted )\r\n\r\nBug.hs:17:24: error:\r\n • Could not deduce (Show (Apply f a)) arising from a use of ‘show’\r\n from the context: forall a. Show (Apply f a)\r\n bound by the instance declaration at Bug.hs:16:1057\r\n • In the expression: show x\r\n In an equation for ‘show’: show (MkExTyFam x) = show x\r\n In the instance declaration for ‘Show (ExTyFam f)’\r\n \r\n17  show (MkExTyFam x) = show x\r\n  ^^^^^^\r\n}}}\r\n\r\nI would have expected the `(forall a. Show (Apply f a))` quantified constraint to kick in, but it didn't.","type_of_failure":"OtherFailure","blocking":[]} >https://gitlab.haskell.org/ghc/ghc//issues/14877QuantifiedConstraints: Can't deduce `xx' from `(xx => a, xx)'20190707T18:15:13ZIcelandjackQuantifiedConstraints: Can't deduce `xx' from `(xx => a, xx)'This works with the [latest change to the XQuantifiedConstraints branch](https://ghc.haskell.org/trac/ghc/ticket/2893#comment:34).
```hs
{# Language QuantifiedConstraints, FlexibleInstances, MultiParamTypeClasses, AllowAmbiguousTypes, RankNTypes, PolyKinds, ConstraintKinds, UndecidableInstances #}
class (forall xx. (xx => a) => Implies xx b) => F a b
instance (forall xx. (xx => a) => Implies xx b) => F a b
class (a => b) => Implies a b
instance (a => b) => Implies a b
```
but replacing `Implies xx b` with `(xx => b)` causes it to fail. I don't know if the cause of this overlaps with an existing ticket.
```hs
class (forall xx. (xx => a) => (xx => b)) => F a b
instance (forall xx. (xx => a) => (xx => b)) => F a b
 $ ghci ignoredotghci /tmp/ASD.hs
 GHCi, version 8.5.20180128: http://www.haskell.org/ghc/ :? for help
 [1 of 1] Compiling Main ( /tmp/ASD.hs, interpreted )

 /tmp/ASD.hs:4:10: error:
 • Could not deduce: xx0
 arising from the superclasses of an instance declaration
 from the context: forall (xx :: Constraint). (xx => a, xx) => b
 bound by the instance declaration at /tmp/ASD.hs:4:1053
 or from: (xx => a, xx)
 bound by a quantified context at /tmp/ASD.hs:1:1
 • In the instance declaration for ‘F a b’
 
 4  instance (forall xx. (xx => a) => (xx => b)) => F a b
  ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
 Failed, no modules loaded.
 Prelude>
```
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.2.2 
 Type  Bug 
 TypeOfFailure  OtherFailure 
 Priority  normal 
 Resolution  Unresolved 
 Component  Compiler 
 Test case  
 Differential revisions  
 BlockedBy  
 Related  
 Blocking  
 CC  
 Operating system  
 Architecture  
</details>
<! {"blocked_by":[],"summary":"QuantifiedConstraints: Can't deduce `xx' from `(xx => a, xx)'","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.2.2","keywords":["QuantifiedConstraints,","wipT2893"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"This works with the [https://ghc.haskell.org/trac/ghc/ticket/2893#comment:34 latest change to the XQuantifiedConstraints branch].\r\n\r\n{{{#!hs\r\n{# Language QuantifiedConstraints, FlexibleInstances, MultiParamTypeClasses, AllowAmbiguousTypes, RankNTypes, PolyKinds, ConstraintKinds, UndecidableInstances #}\r\n\r\nclass (forall xx. (xx => a) => Implies xx b) => F a b\r\ninstance (forall xx. (xx => a) => Implies xx b) => F a b\r\n\r\nclass (a => b) => Implies a b \r\ninstance (a => b) => Implies a b\r\n}}}\r\n\r\nbut replacing `Implies xx b` with `(xx => b)` causes it to fail. I don't know if the cause of this overlaps with an existing ticket.\r\n\r\n{{{#!hs\r\nclass (forall xx. (xx => a) => (xx => b)) => F a b\r\ninstance (forall xx. (xx => a) => (xx => b)) => F a b\r\n\r\n $ ghci ignoredotghci /tmp/ASD.hs \r\n GHCi, version 8.5.20180128: http://www.haskell.org/ghc/ :? for help\r\n [1 of 1] Compiling Main ( /tmp/ASD.hs, interpreted )\r\n \r\n /tmp/ASD.hs:4:10: error:\r\n • Could not deduce: xx0\r\n arising from the superclasses of an instance declaration\r\n from the context: forall (xx :: Constraint). (xx => a, xx) => b\r\n bound by the instance declaration at /tmp/ASD.hs:4:1053\r\n or from: (xx => a, xx)\r\n bound by a quantified context at /tmp/ASD.hs:1:1\r\n • In the instance declaration for ‘F a b’\r\n \r\n 4  instance (forall xx. (xx => a) => (xx => b)) => F a b\r\n  ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^\r\n Failed, no modules loaded.\r\n Prelude> \r\n}}}","type_of_failure":"OtherFailure","blocking":[]} >This works with the [latest change to the XQuantifiedConstraints branch](https://ghc.haskell.org/trac/ghc/ticket/2893#comment:34).
```hs
{# Language QuantifiedConstraints, FlexibleInstances, MultiParamTypeClasses, AllowAmbiguousTypes, RankNTypes, PolyKinds, ConstraintKinds, UndecidableInstances #}
class (forall xx. (xx => a) => Implies xx b) => F a b
instance (forall xx. (xx => a) => Implies xx b) => F a b
class (a => b) => Implies a b
instance (a => b) => Implies a b
```
but replacing `Implies xx b` with `(xx => b)` causes it to fail. I don't know if the cause of this overlaps with an existing ticket.
```hs
class (forall xx. (xx => a) => (xx => b)) => F a b
instance (forall xx. (xx => a) => (xx => b)) => F a b
 $ ghci ignoredotghci /tmp/ASD.hs
 GHCi, version 8.5.20180128: http://www.haskell.org/ghc/ :? for help
 [1 of 1] Compiling Main ( /tmp/ASD.hs, interpreted )

 /tmp/ASD.hs:4:10: error:
 • Could not deduce: xx0
 arising from the superclasses of an instance declaration
 from the context: forall (xx :: Constraint). (xx => a, xx) => b
 bound by the instance declaration at /tmp/ASD.hs:4:1053
 or from: (xx => a, xx)
 bound by a quantified context at /tmp/ASD.hs:1:1
 • In the instance declaration for ‘F a b’
 
 4  instance (forall xx. (xx => a) => (xx => b)) => F a b
  ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
 Failed, no modules loaded.
 Prelude>
```
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.2.2 
 Type  Bug 
 TypeOfFailure  OtherFailure 
 Priority  normal 
 Resolution  Unresolved 
 Component  Compiler 
 Test case  
 Differential revisions  
 BlockedBy  
 Related  
 Blocking  
 CC  
 Operating system  
 Architecture  
</details>
<! {"blocked_by":[],"summary":"QuantifiedConstraints: Can't deduce `xx' from `(xx => a, xx)'","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.2.2","keywords":["QuantifiedConstraints,","wipT2893"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"This works with the [https://ghc.haskell.org/trac/ghc/ticket/2893#comment:34 latest change to the XQuantifiedConstraints branch].\r\n\r\n{{{#!hs\r\n{# Language QuantifiedConstraints, FlexibleInstances, MultiParamTypeClasses, AllowAmbiguousTypes, RankNTypes, PolyKinds, ConstraintKinds, UndecidableInstances #}\r\n\r\nclass (forall xx. (xx => a) => Implies xx b) => F a b\r\ninstance (forall xx. (xx => a) => Implies xx b) => F a b\r\n\r\nclass (a => b) => Implies a b \r\ninstance (a => b) => Implies a b\r\n}}}\r\n\r\nbut replacing `Implies xx b` with `(xx => b)` causes it to fail. I don't know if the cause of this overlaps with an existing ticket.\r\n\r\n{{{#!hs\r\nclass (forall xx. (xx => a) => (xx => b)) => F a b\r\ninstance (forall xx. (xx => a) => (xx => b)) => F a b\r\n\r\n $ ghci ignoredotghci /tmp/ASD.hs \r\n GHCi, version 8.5.20180128: http://www.haskell.org/ghc/ :? for help\r\n [1 of 1] Compiling Main ( /tmp/ASD.hs, interpreted )\r\n \r\n /tmp/ASD.hs:4:10: error:\r\n • Could not deduce: xx0\r\n arising from the superclasses of an instance declaration\r\n from the context: forall (xx :: Constraint). (xx => a, xx) => b\r\n bound by the instance declaration at /tmp/ASD.hs:4:1053\r\n or from: (xx => a, xx)\r\n bound by a quantified context at /tmp/ASD.hs:1:1\r\n • In the instance declaration for ‘F a b’\r\n \r\n 4  instance (forall xx. (xx => a) => (xx => b)) => F a b\r\n  ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^\r\n Failed, no modules loaded.\r\n Prelude> \r\n}}}","type_of_failure":"OtherFailure","blocking":[]} >https://gitlab.haskell.org/ghc/ghc//issues/14879QuantifiedConstraints: Big error message + can't substitute (=>) with a class...20190707T18:15:13ZIcelandjackQuantifiedConstraints: Big error message + can't substitute (=>) with a class aliasThis compiles fine
```hs
{# Language QuantifiedConstraints, FlexibleInstances, MultiParamTypeClasses, ConstraintKinds, UndecidableInstances, GADTs, TypeOperators #}
class (a => b) => Implies a b
instance (a => b) => Implies a b
data Dict c where
Dict :: c => Dict c
type a : b = Dict (Implies a b)
class (forall xx. Implies b xx => Implies a xx) => Yo a b
instance (forall xx. Implies b xx => Implies a xx) => Yo a b
yo :: Yo a b : Implies a b
yo = Dict
```
until you replace `(=>)` with `Implies` (which should be fine?)
```hs
class (forall xx. Implies b xx `Implies` Implies a xx) => Yo a b
instance (forall xx. Implies b xx `Implies` Implies a xx) => Yo a b
```
and the error message blows up
```
$ ghci ignoredotghci SD.hs
GHCi, version 8.5.20180128: http://www.haskell.org/ghc/ :? for help
[1 of 1] Compiling Main ( SD.hs, interpreted )
SD.hs:15:6: error:
• Reduction stack overflow; size = 201
When simplifying the following type:
Implies
b
(Implies
b
(Implies
>8>8severalhundredlines>8>8
b)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
Use freductiondepth=0 to disable this check
(any upper bound you could choose might fail unpredictably with
minor updates to GHC, so disabling the check is recommended if
you're sure that type checking should terminate)
• In the expression: Dict
In an equation for ‘yo’: yo = Dict

15  yo = Dict
 ^^^^
Failed, no modules loaded.
Prelude>
```
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.5 
 Type  Bug 
 TypeOfFailure  OtherFailure 
 Priority  normal 
 Resolution  Unresolved 
 Component  Compiler 
 Test case  
 Differential revisions  
 BlockedBy  
 Related  
 Blocking  
 CC  
 Operating system  
 Architecture  
</details>
<! {"blocked_by":[],"summary":"QuantifiedConstraints: Big error message + can't substitute (=>) with a class alias","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.5","keywords":["QuantifiedConstraints,","wipT2893"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"This compiles fine\r\n\r\n{{{#!hs\r\n{# Language QuantifiedConstraints, FlexibleInstances, MultiParamTypeClasses, ConstraintKinds, UndecidableInstances, GADTs, TypeOperators #}\r\n\r\nclass (a => b) => Implies a b\r\ninstance (a => b) => Implies a b\r\n\r\ndata Dict c where\r\n Dict :: c => Dict c\r\n\r\ntype a : b = Dict (Implies a b)\r\n\r\nclass (forall xx. Implies b xx => Implies a xx) => Yo a b\r\ninstance (forall xx. Implies b xx => Implies a xx) => Yo a b\r\n\r\nyo :: Yo a b : Implies a b\r\nyo = Dict\r\n}}}\r\n\r\nuntil you replace `(=>)` with `Implies` (which should be fine?)\r\n\r\n{{{#!hs\r\nclass (forall xx. Implies b xx `Implies` Implies a xx) => Yo a b\r\ninstance (forall xx. Implies b xx `Implies` Implies a xx) => Yo a b\r\n}}}\r\n\r\nand the error message blows up\r\n\r\n{{{\r\n$ ghci ignoredotghci SD.hs\r\nGHCi, version 8.5.20180128: http://www.haskell.org/ghc/ :? for help\r\n[1 of 1] Compiling Main ( SD.hs, interpreted )\r\n\r\nSD.hs:15:6: error:\r\n • Reduction stack overflow; size = 201\r\n When simplifying the following type:\r\n Implies\r\n b\r\n (Implies\r\n b\r\n (Implies\r\n\r\n>8>8severalhundredlines>8>8\r\n\r\nb)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))\r\n Use freductiondepth=0 to disable this check\r\n (any upper bound you could choose might fail unpredictably with\r\n minor updates to GHC, so disabling the check is recommended if\r\n you're sure that type checking should terminate)\r\n • In the expression: Dict\r\n In an equation for ‘yo’: yo = Dict\r\n \r\n15  yo = Dict\r\n  ^^^^\r\nFailed, no modules loaded.\r\nPrelude> \r\n}}}","type_of_failure":"OtherFailure","blocking":[]} >This compiles fine
```hs
{# Language QuantifiedConstraints, FlexibleInstances, MultiParamTypeClasses, ConstraintKinds, UndecidableInstances, GADTs, TypeOperators #}
class (a => b) => Implies a b
instance (a => b) => Implies a b
data Dict c where
Dict :: c => Dict c
type a : b = Dict (Implies a b)
class (forall xx. Implies b xx => Implies a xx) => Yo a b
instance (forall xx. Implies b xx => Implies a xx) => Yo a b
yo :: Yo a b : Implies a b
yo = Dict
```
until you replace `(=>)` with `Implies` (which should be fine?)
```hs
class (forall xx. Implies b xx `Implies` Implies a xx) => Yo a b
instance (forall xx. Implies b xx `Implies` Implies a xx) => Yo a b
```
and the error message blows up
```
$ ghci ignoredotghci SD.hs
GHCi, version 8.5.20180128: http://www.haskell.org/ghc/ :? for help
[1 of 1] Compiling Main ( SD.hs, interpreted )
SD.hs:15:6: error:
• Reduction stack overflow; size = 201
When simplifying the following type:
Implies
b
(Implies
b
(Implies
>8>8severalhundredlines>8>8
b)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
Use freductiondepth=0 to disable this check
(any upper bound you could choose might fail unpredictably with
minor updates to GHC, so disabling the check is recommended if
you're sure that type checking should terminate)
• In the expression: Dict
In an equation for ‘yo’: yo = Dict

15  yo = Dict
 ^^^^
Failed, no modules loaded.
Prelude>
```
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.5 
 Type  Bug 
 TypeOfFailure  OtherFailure 
 Priority  normal 
 Resolution  Unresolved 
 Component  Compiler 
 Test case  
 Differential revisions  
 BlockedBy  
 Related  
 Blocking  
 CC  
 Operating system  
 Architecture  
</details>
<! {"blocked_by":[],"summary":"QuantifiedConstraints: Big error message + can't substitute (=>) with a class alias","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.5","keywords":["QuantifiedConstraints,","wipT2893"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"This compiles fine\r\n\r\n{{{#!hs\r\n{# Language QuantifiedConstraints, FlexibleInstances, MultiParamTypeClasses, ConstraintKinds, UndecidableInstances, GADTs, TypeOperators #}\r\n\r\nclass (a => b) => Implies a b\r\ninstance (a => b) => Implies a b\r\n\r\ndata Dict c where\r\n Dict :: c => Dict c\r\n\r\ntype a : b = Dict (Implies a b)\r\n\r\nclass (forall xx. Implies b xx => Implies a xx) => Yo a b\r\ninstance (forall xx. Implies b xx => Implies a xx) => Yo a b\r\n\r\nyo :: Yo a b : Implies a b\r\nyo = Dict\r\n}}}\r\n\r\nuntil you replace `(=>)` with `Implies` (which should be fine?)\r\n\r\n{{{#!hs\r\nclass (forall xx. Implies b xx `Implies` Implies a xx) => Yo a b\r\ninstance (forall xx. Implies b xx `Implies` Implies a xx) => Yo a b\r\n}}}\r\n\r\nand the error message blows up\r\n\r\n{{{\r\n$ ghci ignoredotghci SD.hs\r\nGHCi, version 8.5.20180128: http://www.haskell.org/ghc/ :? for help\r\n[1 of 1] Compiling Main ( SD.hs, interpreted )\r\n\r\nSD.hs:15:6: error:\r\n • Reduction stack overflow; size = 201\r\n When simplifying the following type:\r\n Implies\r\n b\r\n (Implies\r\n b\r\n (Implies\r\n\r\n>8>8severalhundredlines>8>8\r\n\r\nb)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))\r\n Use freductiondepth=0 to disable this check\r\n (any upper bound you could choose might fail unpredictably with\r\n minor updates to GHC, so disabling the check is recommended if\r\n you're sure that type checking should terminate)\r\n • In the expression: Dict\r\n In an equation for ‘yo’: yo = Dict\r\n \r\n15  yo = Dict\r\n  ^^^^\r\nFailed, no modules loaded.\r\nPrelude> \r\n}}}","type_of_failure":"OtherFailure","blocking":[]} >https://gitlab.haskell.org/ghc/ghc//issues/14896QuantifiedConstraints: GHC does doesn't discharge constraints if they are qua...20190707T18:15:08ZIcelandjackQuantifiedConstraints: GHC does doesn't discharge constraints if they are quantifiedThis came up on a [reddit thread](https://www.reddit.com/r/haskell/comments/8257mz/how_quantifiedconstraints_can_let_us_put_join/dv8hfxb/),
```hs
{# Language QuantifiedConstraints #}
class (forall aa. Functor (bi aa)) => Bifunctor bi where
first :: (a > a') > (bi a b > bi a' b)
bimap :: Bifunctor bi => (a > a') > (b > b') > (bi a b > bi a' b')
bimap f g = first f . fmap g
```
This is the type we want for `bimap` even if we mix & match `Bifunctor` and `Functor`. We already know that we can `fmap @(bi xx)` for any `xx` but this is not the inferred type.
Instead GHC infers a type (tidied up) with a superfluous `Functor` constraint
```hs
bimap :: (Bifunctor bi, Functor (bi a)) => (a > a') > (b > b') > (bi a b > bi a' b')
```
Indeed postcomposing with a superfluous `fmap @(bi a') id` incurs yet another `Functor` constraint
```hs
bimap :: (Bifunctor bi, Functor (bi a), Functor (bi a')) => (a > a') > (b > b') > (bi a b > bi a' b')
bimap f g = fmap id . first f . fmap g
```
A terminology question, I'm not sure how to phrase what GHC isn't doing to the `Functor` constraints: ‘discharge’?This came up on a [reddit thread](https://www.reddit.com/r/haskell/comments/8257mz/how_quantifiedconstraints_can_let_us_put_join/dv8hfxb/),
```hs
{# Language QuantifiedConstraints #}
class (forall aa. Functor (bi aa)) => Bifunctor bi where
first :: (a > a') > (bi a b > bi a' b)
bimap :: Bifunctor bi => (a > a') > (b > b') > (bi a b > bi a' b')
bimap f g = first f . fmap g
```
This is the type we want for `bimap` even if we mix & match `Bifunctor` and `Functor`. We already know that we can `fmap @(bi xx)` for any `xx` but this is not the inferred type.
Instead GHC infers a type (tidied up) with a superfluous `Functor` constraint
```hs
bimap :: (Bifunctor bi, Functor (bi a)) => (a > a') > (b > b') > (bi a b > bi a' b')
```
Indeed postcomposing with a superfluous `fmap @(bi a') id` incurs yet another `Functor` constraint
```hs
bimap :: (Bifunctor bi, Functor (bi a), Functor (bi a')) => (a > a') > (b > b') > (bi a b > bi a' b')
bimap f g = fmap id . first f . fmap g
```
A terminology question, I'm not sure how to phrase what GHC isn't doing to the `Functor` constraints: ‘discharge’?https://gitlab.haskell.org/ghc/ghc//issues/14958QuantifiedConstraints: Doesn't apply implication for existential?20190707T18:14:53ZIcelandjackQuantifiedConstraints: Doesn't apply implication for existential?This fails
```hs
{# Language GADTs, RankNTypes, ConstraintKinds, QuantifiedConstraints, AllowAmbiguousTypes #}
data Foo where
Foo :: (forall x. ((forall y. cls y => Num y), cls x) => x) > Foo
a :: Foo
a = Foo 10
```
```
$ ... ignoredotghci /tmp/Optic.hs
GHCi, version 8.5.20180128: http://www.haskell.org/ghc/ :? for help
[1 of 1] Compiling Main ( /tmp/Optic.hs, interpreted )
/tmp/Optic.hs:7:9: error:
• Could not deduce (Num x) arising from the literal ‘10’
from the context: (forall y. cls0 y => Num y, cls0 x)
bound by a type expected by the context:
forall x. (forall y. cls0 y => Num y, cls0 x) => x
at /tmp/Optic.hs:7:510
Possible fix:
add (Num x) to the context of
a type expected by the context:
forall x. (forall y. cls0 y => Num y, cls0 x) => x
• In the first argument of ‘Foo’, namely ‘10’
In the expression: Foo 10
In an equation for ‘a’: a = Foo 10

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

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

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

The reason for trying this is creating a `newtype` for optics where we still get subsumption
```hs
{# Language GADTs, RankNTypes, ConstraintKinds, QuantifiedConstraints, AllowAmbiguousTypes, ApplicativeDo, TypeOperators, MultiParamTypeClasses, FlexibleInstances, UndecidableInstances, PolyKinds, FlexibleContexts #}
data Optic cls s a where
Optic :: (forall f. cls f => (a > f a) > (s > f s)) > Optic cls s a
class (forall x. f x => g x) => (f ~=> g)
instance (forall x. f x => g x) => (f ~=> g)
_1 :: cls ~=> Functor => Optic cls (a, b) a
_1 = Optic $ \f (a, b) > do
a' < f a
pure (a', b)
lens_1 :: Optic Functor (a, b) a
lens_1 = _1
trav_1 :: Optic Applicative (a, b) a
trav_1 = _1
```
and I wanted to move `cls ~=> Functor` into the `Optic` type itself.
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.5 
 Type  Bug 
 TypeOfFailure  OtherFailure 
 Priority  normal 
 Resolution  Unresolved 
 Component  Compiler 
 Test case  
 Differential revisions  
 BlockedBy  
 Related  
 Blocking  
 CC  
 Operating system  
 Architecture  
</details>
<! {"blocked_by":[],"summary":"QuantifiedConstraints: Doesn't apply implication for existential?","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.5","keywords":["QuantifiedConstraints,","wipT2893"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"This fails\r\n\r\n{{{#!hs\r\n{# Language GADTs, RankNTypes, ConstraintKinds, QuantifiedConstraints, AllowAmbiguousTypes #}\r\n\r\ndata Foo where\r\n Foo :: (forall x. ((forall y. cls y => Num y), cls x) => x) > Foo\r\n\r\na :: Foo\r\na = Foo 10\r\n}}}\r\n\r\n{{{\r\n$ ... ignoredotghci /tmp/Optic.hs\r\nGHCi, version 8.5.20180128: http://www.haskell.org/ghc/ :? for help\r\n[1 of 1] Compiling Main ( /tmp/Optic.hs, interpreted )\r\n\r\n/tmp/Optic.hs:7:9: error:\r\n • Could not deduce (Num x) arising from the literal ‘10’\r\n from the context: (forall y. cls0 y => Num y, cls0 x)\r\n bound by a type expected by the context:\r\n forall x. (forall y. cls0 y => Num y, cls0 x) => x\r\n at /tmp/Optic.hs:7:510\r\n Possible fix:\r\n add (Num x) to the context of\r\n a type expected by the context:\r\n forall x. (forall y. cls0 y => Num y, cls0 x) => x\r\n • In the first argument of ‘Foo’, namely ‘10’\r\n In the expression: Foo 10\r\n In an equation for ‘a’: a = Foo 10\r\n \r\n7  a = Foo 10\r\n  ^^\r\nFailed, no modules loaded.\r\nPrelude> \r\n}}}\r\n\r\nGHC knows that `cls ~=> Num` but still GHC cannot deduce `Num x` from `cls x`.\r\n\r\n\r\n\r\nThe reason for trying this is creating a `newtype` for optics where we still get subsumption \r\n\r\n{{{#!hs\r\n{# Language GADTs, RankNTypes, ConstraintKinds, QuantifiedConstraints, AllowAmbiguousTypes, ApplicativeDo, TypeOperators, MultiParamTypeClasses, FlexibleInstances, UndecidableInstances, PolyKinds, FlexibleContexts #}\r\n\r\ndata Optic cls s a where\r\n Optic :: (forall f. cls f => (a > f a) > (s > f s)) > Optic cls s a\r\n\r\nclass (forall x. f x => g x) => (f ~=> g)\r\ninstance (forall x. f x => g x) => (f ~=> g)\r\n\r\n_1 :: cls ~=> Functor => Optic cls (a, b) a\r\n_1 = Optic $ \\f (a, b) > do\r\n a' < f a\r\n pure (a', b)\r\n\r\nlens_1 :: Optic Functor (a, b) a\r\nlens_1 = _1\r\n\r\ntrav_1 :: Optic Applicative (a, b) a\r\ntrav_1 = _1\r\n}}}\r\n\r\nand I wanted to move `cls ~=> Functor` into the `Optic` type itself.","type_of_failure":"OtherFailure","blocking":[]} >https://gitlab.haskell.org/ghc/ghc//issues/14983Have custom type errors imply Void20201030T21:57:01ZIcelandjackHave custom type errors imply VoidThis is a very minor issue, but `TypeError` (CustomTypeErrors) should entail a constraint like
```hs
import Data.Void
class (forall x. x) => No where
no :: Void
```
so users don't have to use `undefined` or `error ..`:
```hs
instance TypeError (Text "Can't show functions") => Show (a > b) where
show :: (a > b) > String
show = no & absurd
```This is a very minor issue, but `TypeError` (CustomTypeErrors) should entail a constraint like
```hs
import Data.Void
class (forall x. x) => No where
no :: Void
```
so users don't have to use `undefined` or `error ..`:
```hs
instance TypeError (Text "Can't show functions") => Show (a > b) where
show :: (a > b) > String
show = no & absurd
```https://gitlab.haskell.org/ghc/ghc//issues/14995QuantifiedConstraints: Incorrect pretty printing20190707T18:14:45ZIcelandjackQuantifiedConstraints: Incorrect pretty printingThis code from [OutsideIn(X)](https://www.microsoft.com/enus/research/wpcontent/uploads/2016/02/jfpoutsidein.pdf) compiles
```hs
{# Language FlexibleInstances, MultiParamTypeClasses, GADTs, QuantifiedConstraints #}
class C a
class B a b where op :: a > b
instance C a => B a [a] where op = undefined
data R a where
MkR :: C a => a > R a
k :: (C a => B a b) => R a > b
k (MkR x) = op x
```
but prettyprinting `k` prints `B a b => ..` instead of `(C a => B a b) => ..`
```
$ ghci ignoredotghci hs/228bug.hs
GHCi, version 8.5.20180128: http://www.haskell.org/ghc/ :? for help
[1 of 1] Compiling Main ( hs/228bug.hs, interpreted )
Ok, one module loaded.
*Main> :t k
k :: B a b => R a > b
*Main>
```This code from [OutsideIn(X)](https://www.microsoft.com/enus/research/wpcontent/uploads/2016/02/jfpoutsidein.pdf) compiles
```hs
{# Language FlexibleInstances, MultiParamTypeClasses, GADTs, QuantifiedConstraints #}
class C a
class B a b where op :: a > b
instance C a => B a [a] where op = undefined
data R a where
MkR :: C a => a > R a
k :: (C a => B a b) => R a > b
k (MkR x) = op x
```
but prettyprinting `k` prints `B a b => ..` instead of `(C a => B a b) => ..`
```
$ ghci ignoredotghci hs/228bug.hs
GHCi, version 8.5.20180128: http://www.haskell.org/ghc/ :? for help
[1 of 1] Compiling Main ( hs/228bug.hs, interpreted )
Ok, one module loaded.
*Main> :t k
k :: B a b => R a > b
*Main>
```https://gitlab.haskell.org/ghc/ghc//issues/15020PatternSynonyms: Problems with quantified constraints / foralls20200123T19:26:36ZIcelandjackPatternSynonyms: Problems with quantified constraints / forallsI couldn't find a way to implement `PLam2` as a simply bidirectional pattern synonym, I expected it to work but I recall a similar ticket. I couldn't find it though.
```hs
{# Language RankNTypes, PatternSynonyms, ViewPatterns #}
newtype Lam1 = Lam1 (forall xx mm. Monad mm => mm xx)
pattern PLam1 :: (forall xx mm. Monad mm => mm xx) > Lam1
pattern PLam1 a = Lam1 a

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

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

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

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

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

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

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

5  type E (c :: * > Constraint) = forall (a :: *). Eq a => c a
 ^^^
```
Note that GHC accepts the program when the `Eq a` constraint is removed.
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.6.3 
 Type  Bug 
 TypeOfFailure  OtherFailure 
 Priority  normal 
 Resolution  Unresolved 
 Component  Compiler 
 Test case  
 Differential revisions  
 BlockedBy  
 Related  
 Blocking  
 CC  
 Operating system  
 Architecture  
</details>
<! {"blocked_by":[],"summary":"GHC confused about type synonym kind with QuantifiedConstraints","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.6.3","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"{{{#!hs\r\n{# LANGUAGE KindSignatures, RankNTypes, ConstraintKinds, QuantifiedConstraints #}\r\nmodule Bug where\r\nimport Data.Constraint\r\n\r\ntype E (c :: * > Constraint) = forall (a :: *). Eq a => c a\r\n}}}\r\n\r\n{{{\r\nBug.hs:5:58: error:\r\n • Expected a type, but ‘c a’ has kind ‘Constraint’\r\n • In the type ‘forall (a :: *). Eq a => c a’\r\n In the type declaration for ‘E’\r\n \r\n5  type E (c :: * > Constraint) = forall (a :: *). Eq a => c a\r\n  ^^^\r\n}}}\r\n\r\nNote that GHC accepts the program when the `Eq a` constraint is removed.","type_of_failure":"OtherFailure","blocking":[]} >https://gitlab.haskell.org/ghc/ghc//issues/16140Cannot create type synonym for quantified constraint without ImpredicativeTypes20190707T18:01:19ZAshley YakeleyCannot create type synonym for quantified constraint without ImpredicativeTypes```hs
{# LANGUAGE KindSignatures, RankNTypes, ConstraintKinds, QuantifiedConstraints, FlexibleInstances, UndecidableInstances #}
module Bug where
type F1 (f :: * > *) = forall a. Eq (f a)
class (Functor f, F1 f) => C f
instance (Functor f, F1 f) => C f
type F2 f = (Functor f, F1 f)
```
```
Bug.hs:7:1: error:
• Illegal polymorphic type: F1 f
GHC doesn't yet support impredicative polymorphism
• In the type synonym declaration for ‘F2’

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

7  type F2 f = (Functor f, F1 f)
 ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
```
(GHC accepts the program with ImpredicativeTypes.)
`(Functor f, F1 f)` is allowed as a superclass constraint, and as an instance constraint, but a type synonym cannot be made for it.
Not sure if this really counts as a bug ("just switch on ImpredicativeTypes"), but I think it's worth discussing. I prefer to keep ImpredicativeTypes switched off, but if something can be a constraint, shouldn't I be able to create a type synonym of it?
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.6.3 
 Type  Bug 
 TypeOfFailure  OtherFailure 
 Priority  normal 
 Resolution  Unresolved 
 Component  Compiler 
 Test case  
 Differential revisions  
 BlockedBy  
 Related  
 Blocking  
 CC  
 Operating system  
 Architecture  
</details>
<! {"blocked_by":[],"summary":"Cannot create type synonym for quantified constraint without ImpredicativeTypes","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.6.3","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"{{{#!hs\r\n{# LANGUAGE KindSignatures, RankNTypes, ConstraintKinds, QuantifiedConstraints, FlexibleInstances, UndecidableInstances #}\r\nmodule Bug where\r\n\r\ntype F1 (f :: * > *) = forall a. Eq (f a)\r\nclass (Functor f, F1 f) => C f\r\ninstance (Functor f, F1 f) => C f\r\ntype F2 f = (Functor f, F1 f)\r\n}}}\r\n\r\n{{{\r\nBug.hs:7:1: error:\r\n • Illegal polymorphic type: F1 f\r\n GHC doesn't yet support impredicative polymorphism\r\n • In the type synonym declaration for ‘F2’\r\n \r\n7  type F2 f = (Functor f, F1 f)\r\n  ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^\r\n}}}\r\n\r\n(GHC accepts the program with ImpredicativeTypes.)\r\n\r\n`(Functor f, F1 f)` is allowed as a superclass constraint, and as an instance constraint, but a type synonym cannot be made for it.\r\n\r\nNot sure if this really counts as a bug (\"just switch on ImpredicativeTypes\"), but I think it's worth discussing. I prefer to keep ImpredicativeTypes switched off, but if something can be a constraint, shouldn't I be able to create a type synonym of it?","type_of_failure":"OtherFailure","blocking":[]} >https://gitlab.haskell.org/ghc/ghc//issues/16173Move `Data.Profunctor` from `profunctors` package to `base`20200709T23:56:57ZDmitrii KovanikovMove `Data.Profunctor` from `profunctors` package to `base``Contravariant` was added in GHC 8.6.
 https://hackage.haskell.org/package/base4.12.0.0/docs/DataFunctorContravariant.html
`Profunctor` also looks like fundamental abstraction to be worth considering adding to `base`.
Having both `Profunctor` and `Choice` typeclasses in the `base` library will also allow to write `microprism` package similar to `microlens`. Prisms often turns to be very useful since they allow to work nicely with sum types.
```hs
type Prism s t a b = forall p f. (Choice p, Applicative f) => p a (f b) > p s (f t)
```
Additional context for this ticket from Reddit:
 https://www.reddit.com/r/haskell/comments/8v53cb/announce_ghc_861alpha1_available/e1o1giy/
It was proposed on Reddit to use `QuantifiedConstraints` for `Profunctor`. I'm not quite fluent with `QuantifiedConstraints`, but I think this may looks like this (mostly copypasting code from `profunctors` package):
```hs
{# LANGUAGE QuantifiedConstraints #}
class (forall a . Functor (p a)) => Profunctor p where
{# MINIMAL dimap  (lmap, rmap) #}
dimap :: (a > b) > (c > d) > p b c > p a d
dimap f g = lmap f . rmap g
lmap :: (a > b) > p b c > p a c
lmap f = dimap f id
rmap :: (b > c) > p a b > p a c
rmap = dimap id
instance Profunctor (>) where
dimap ab cd bc = cd . bc . ab
lmap = flip (.)
rmap = (.)
```
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.6.3 
 Type  FeatureRequest 
 TypeOfFailure  OtherFailure 
 Priority  normal 
 Resolution  Unresolved 
 Component  Core Libraries 
 Test case  
 Differential revisions  
 BlockedBy  
 Related  
 Blocking  
 CC  andrewthad, ekmett 
 Operating system  
 Architecture  
</details>
<! {"blocked_by":[],"summary":"Move `Data.Profunctor` from `profunctors` package to `base`","status":"New","operating_system":"","component":"Core Libraries","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.6.3","keywords":["QuantifiedConstraints","base,","profunctor,"],"differentials":[],"test_case":"","architecture":"","cc":["andrewthad","ekmett"],"type":"FeatureRequest","description":"`Contravariant` was added in GHC 8.6. \r\n\r\n* https://hackage.haskell.org/package/base4.12.0.0/docs/DataFunctorContravariant.html\r\n\r\n`Profunctor` also looks like fundamental abstraction to be worth considering adding to `base`. \r\n\r\nHaving both `Profunctor` and `Choice` typeclasses in the `base` library will also allow to write `microprism` package similar to `microlens`. Prisms often turns to be very useful since they allow to work nicely with sum types.\r\n\r\n{{{#!hs\r\ntype Prism s t a b = forall p f. (Choice p, Applicative f) => p a (f b) > p s (f t)\r\n}}}\r\n\r\nAdditional context for this ticket from Reddit:\r\n\r\n* https://www.reddit.com/r/haskell/comments/8v53cb/announce_ghc_861alpha1_available/e1o1giy/\r\n\r\nIt was proposed on Reddit to use `QuantifiedConstraints` for `Profunctor`. I'm not quite fluent with `QuantifiedConstraints`, but I think this may looks like this (mostly copypasting code from `profunctors` package):\r\n\r\n{{{#!hs\r\n{# LANGUAGE QuantifiedConstraints #}\r\n\r\nclass (forall a . Functor (p a)) => Profunctor p where\r\n {# MINIMAL dimap  (lmap, rmap) #}\r\n\r\n dimap :: (a > b) > (c > d) > p b c > p a d\r\n dimap f g = lmap f . rmap g\r\n\r\n lmap :: (a > b) > p b c > p a c\r\n lmap f = dimap f id\r\n\r\n rmap :: (b > c) > p a b > p a c\r\n rmap = dimap id\r\n\r\ninstance Profunctor (>) where\r\n dimap ab cd bc = cd . bc . ab\r\n lmap = flip (.)\r\n rmap = (.)\r\n}}}","type_of_failure":"OtherFailure","blocking":[]} >`Contravariant` was added in GHC 8.6.
 https://hackage.haskell.org/package/base4.12.0.0/docs/DataFunctorContravariant.html
`Profunctor` also looks like fundamental abstraction to be worth considering adding to `base`.
Having both `Profunctor` and `Choice` typeclasses in the `base` library will also allow to write `microprism` package similar to `microlens`. Prisms often turns to be very useful since they allow to work nicely with sum types.
```hs
type Prism s t a b = forall p f. (Choice p, Applicative f) => p a (f b) > p s (f t)
```
Additional context for this ticket from Reddit:
 https://www.reddit.com/r/haskell/comments/8v53cb/announce_ghc_861alpha1_available/e1o1giy/
It was proposed on Reddit to use `QuantifiedConstraints` for `Profunctor`. I'm not quite fluent with `QuantifiedConstraints`, but I think this may looks like this (mostly copypasting code from `profunctors` package):
```hs
{# LANGUAGE QuantifiedConstraints #}
class (forall a . Functor (p a)) => Profunctor p where
{# MINIMAL dimap  (lmap, rmap) #}
dimap :: (a > b) > (c > d) > p b c > p a d
dimap f g = lmap f . rmap g
lmap :: (a > b) > p b c > p a c
lmap f = dimap f id
rmap :: (b > c) > p a b > p a c
rmap = dimap id
instance Profunctor (>) where
dimap ab cd bc = cd . bc . ab
lmap = flip (.)
rmap = (.)
```
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.6.3 
 Type  FeatureRequest 
 TypeOfFailure  OtherFailure 
 Priority  normal 
 Resolution  Unresolved 
 Component  Core Libraries 
 Test case  
 Differential revisions  
 BlockedBy  
 Related  
 Blocking  
 CC  andrewthad, ekmett 
 Operating system  
 Architecture  
</details>
<! {"blocked_by":[],"summary":"Move `Data.Profunctor` from `profunctors` package to `base`","status":"New","operating_system":"","component":"Core Libraries","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.6.3","keywords":["QuantifiedConstraints","base,","profunctor,"],"differentials":[],"test_case":"","architecture":"","cc":["andrewthad","ekmett"],"type":"FeatureRequest","description":"`Contravariant` was added in GHC 8.6. \r\n\r\n* https://hackage.haskell.org/package/base4.12.0.0/docs/DataFunctorContravariant.html\r\n\r\n`Profunctor` also looks like fundamental abstraction to be worth considering adding to `base`. \r\n\r\nHaving both `Profunctor` and `Choice` typeclasses in the `base` library will also allow to write `microprism` package similar to `microlens`. Prisms often turns to be very useful since they allow to work nicely with sum types.\r\n\r\n{{{#!hs\r\ntype Prism s t a b = forall p f. (Choice p, Applicative f) => p a (f b) > p s (f t)\r\n}}}\r\n\r\nAdditional context for this ticket from Reddit:\r\n\r\n* https://www.reddit.com/r/haskell/comments/8v53cb/announce_ghc_861alpha1_available/e1o1giy/\r\n\r\nIt was proposed on Reddit to use `QuantifiedConstraints` for `Profunctor`. I'm not quite fluent with `QuantifiedConstraints`, but I think this may looks like this (mostly copypasting code from `profunctors` package):\r\n\r\n{{{#!hs\r\n{# LANGUAGE QuantifiedConstraints #}\r\n\r\nclass (forall a . Functor (p a)) => Profunctor p where\r\n {# MINIMAL dimap  (lmap, rmap) #}\r\n\r\n dimap :: (a > b) > (c > d) > p b c > p a d\r\n dimap f g = lmap f . rmap g\r\n\r\n lmap :: (a > b) > p b c > p a c\r\n lmap f = dimap f id\r\n\r\n rmap :: (b > c) > p a b > p a c\r\n rmap = dimap id\r\n\r\ninstance Profunctor (>) where\r\n dimap ab cd bc = cd . bc . ab\r\n lmap = flip (.)\r\n rmap = (.)\r\n}}}","type_of_failure":"OtherFailure","blocking":[]} >https://gitlab.haskell.org/ghc/ghc//issues/16365Inconsistency in quantified constraint solving20190707T18:00:22ZRyan ScottInconsistency in quantified constraint solvingConsider the following program:
```hs
{# LANGUAGE ConstraintKinds #}
{# LANGUAGE ExistentialQuantification #}
{# LANGUAGE FlexibleContexts #}
{# LANGUAGE FlexibleInstances #}
{# LANGUAGE MultiParamTypeClasses #}
{# LANGUAGE QuantifiedConstraints #}
{# LANGUAGE TypeFamilies #}
{# LANGUAGE UndecidableInstances #}
module Bug where
import Data.Kind
import Data.Proxy
class C a where
m :: a > ()
data Dict c = c => Dict

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

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

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

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

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

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