Admin message

Due to a large amount of spam we do not allow new users to create repositories, they are "external" users. If you are a new user and want to create a repository, for example for forking GHC, open a new issue on ghc/ghc using the "get-verified" issue template

Won't use (forall xx. f xx) with -XQuantifiedConstraints
```hs {-# Language QuantifiedConstraints #-} {-# Language GADTs #-} {-# Language ConstraintKinds #-} data D c where D :: c => D c proof :: (forall xx. f xx) => D (f a) proof = D ``` Running this program with [wip/T2893](https://ghc.haskell.org/trac/ghc/ticket/2893#comment:28) gives ``` GHCi, version 8.5.20180128: http://www.haskell.org/ghc/ :? for help [1 of 1] Compiling Main ( 174-quantifiedconstraints.hs, interpreted ) 174-quantifiedconstraints.hs:9:9: error: • Could not deduce: f a arising from a use of ‘D’ from the context: forall xx. f xx bound by the type signature for: proof :: forall (f :: * -> Constraint) a. (forall xx. f xx) => D (f a) at 174-quantifiedconstraints.hs:8:1-37 • In the expression: D In an equation for ‘proof’: proof = D • Relevant bindings include proof :: D (f a) (bound at 174-quantifiedconstraints.hs:9:1) | 9 | proof = D | ^ ``` How can I instantiate `xx` to `a`? <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":"Won't use (forall xx. f xx) with -XQuantifiedConstraints","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.5","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"{{{#!hs\r\n{-# Language QuantifiedConstraints #-}\r\n{-# Language GADTs #-}\r\n{-# Language ConstraintKinds #-}\r\n\r\ndata D c where\r\n D :: c => D c\r\n\r\nproof :: (forall xx. f xx) => D (f a)\r\nproof = D\r\n}}}\r\n\r\nRunning this program with [https://ghc.haskell.org/trac/ghc/ticket/2893#comment:28 wip/T2893] gives\r\n\r\n{{{\r\nGHCi, version 8.5.20180128: http://www.haskell.org/ghc/ :? for help\r\n[1 of 1] Compiling Main ( 174-quantifiedconstraints.hs, interpreted )\r\n\r\n174-quantifiedconstraints.hs:9:9: error:\r\n • Could not deduce: f a arising from a use of ‘D’\r\n from the context: forall xx. f xx\r\n bound by the type signature for:\r\n proof :: forall (f :: * -> Constraint) a.\r\n (forall xx. f xx) =>\r\n D (f a)\r\n at 174-quantifiedconstraints.hs:8:1-37\r\n • In the expression: D\r\n In an equation for ‘proof’: proof = D\r\n • Relevant bindings include\r\n proof :: D (f a) (bound at 174-quantifiedconstraints.hs:9:1)\r\n |\r\n9 | proof = D\r\n | ^\r\n}}}\r\n\r\nHow can I instantiate `xx` to `a`?","type_of_failure":"OtherFailure","blocking":[]} -->
issue