GHC issueshttps://gitlab.haskell.org/ghc/ghc//issues20200625T10:02:38Zhttps://gitlab.haskell.org/ghc/ghc//issues/17768ApplicativeDo breaks compilation with a rank2 let20200625T10:02:38ZKirill Elaginkirelagin@gmail.comApplicativeDo breaks compilation with a rank2 let## Summary
A valid code that uses a let binding with an explicit Rank2 type stops compiling when `ApplicativeDo` is enabled.
## Steps to reproduce
```
{# LANGUAGE ApplicativeDo, Rank2Types #}
module Test where
type M = forall m. Monad m => m () > m ()
runM :: M > IO ()
runM m = m $ pure ()
q :: IO ()
q = do
() < pure ()
let
m :: M
m = id
() < pure ()
runM m
 pure ()
```
Note that the example is very fragile. It will start to compile if you either:
* Remove `ApplicativeDo`
* Uncomment the last `pure`
* Remove one of the `pure`
* Reorder the `pure`s and `let`
The error is:
```
foo.hs:14:34: error:
• Ambiguous type variable ‘m0’ arising from a use of ‘m’
prevents the constraint ‘(Monad m0)’ from being solved.
<...>
• In the first argument of ‘return’, namely ‘m’
In the expression:
do () < pure ()
let m :: M
m = id
() < pure ()
runM m
In an equation for ‘q’:
q = do () < pure ()
let m :: M
....
() < pure ()
runM m

14  () < pure ()
 ^^
foo.hs:19:8: error:
• Couldn't match type ‘m’ with ‘m0’
‘m’ is a rigid type variable bound by
a type expected by the context:
M
at foo.hs:19:38
Expected type: m () > m ()
Actual type: m0 () > m0 ()
• In the first argument of ‘runM’, namely ‘m’
In a stmt of a 'do' block: runM m
In the expression:
do () < pure ()
let m :: M
m = id
() < pure ()
runM m
• Relevant bindings include
m :: m0 () > m0 () (bound at foo.hs:17:5)

19  runM m
```
The renamer outputs:
```
= do join (m_aXe < do () < pure ()
let m_aXe :: Test.M
m_aXe = id
return m_aXe 
() < pure ())
Test.runM m_aXe
```
which I couldn’t make sense of, but it looks like it is getting deshugared to something like:
```
q2 :: IO ()
q2 = let {m :: M; m = id} in return m >>= runM
```
which doesn’t compile indeed.
## Expected behavior
Code that compiles without `ApplicativeDo` should compile with `ApplicativeDo`.
## Environment
* GHC version used: 8.6.5, 8.8.2
Optional:
* Operating System:
* System Architecture:## Summary
A valid code that uses a let binding with an explicit Rank2 type stops compiling when `ApplicativeDo` is enabled.
## Steps to reproduce
```
{# LANGUAGE ApplicativeDo, Rank2Types #}
module Test where
type M = forall m. Monad m => m () > m ()
runM :: M > IO ()
runM m = m $ pure ()
q :: IO ()
q = do
() < pure ()
let
m :: M
m = id
() < pure ()
runM m
 pure ()
```
Note that the example is very fragile. It will start to compile if you either:
* Remove `ApplicativeDo`
* Uncomment the last `pure`
* Remove one of the `pure`
* Reorder the `pure`s and `let`
The error is:
```
foo.hs:14:34: error:
• Ambiguous type variable ‘m0’ arising from a use of ‘m’
prevents the constraint ‘(Monad m0)’ from being solved.
<...>
• In the first argument of ‘return’, namely ‘m’
In the expression:
do () < pure ()
let m :: M
m = id
() < pure ()
runM m
In an equation for ‘q’:
q = do () < pure ()
let m :: M
....
() < pure ()
runM m

14  () < pure ()
 ^^
foo.hs:19:8: error:
• Couldn't match type ‘m’ with ‘m0’
‘m’ is a rigid type variable bound by
a type expected by the context:
M
at foo.hs:19:38
Expected type: m () > m ()
Actual type: m0 () > m0 ()
• In the first argument of ‘runM’, namely ‘m’
In a stmt of a 'do' block: runM m
In the expression:
do () < pure ()
let m :: M
m = id
() < pure ()
runM m
• Relevant bindings include
m :: m0 () > m0 () (bound at foo.hs:17:5)

19  runM m
```
The renamer outputs:
```
= do join (m_aXe < do () < pure ()
let m_aXe :: Test.M
m_aXe = id
return m_aXe 
() < pure ())
Test.runM m_aXe
```
which I couldn’t make sense of, but it looks like it is getting deshugared to something like:
```
q2 :: IO ()
q2 = let {m :: M; m = id} in return m >>= runM
```
which doesn’t compile indeed.
## Expected behavior
Code that compiles without `ApplicativeDo` should compile with `ApplicativeDo`.
## Environment
* GHC version used: 8.6.5, 8.8.2
Optional:
* Operating System:
* System Architecture:https://gitlab.haskell.org/ghc/ghc//issues/16245GHC panic (No skolem info) with RankNTypes and strange scoping20200922T11:06:17ZRyan ScottGHC panic (No skolem info) with RankNTypes and strange scopingThe following program panics with GHC 8.6.3 and HEAD:
```hs
{# LANGUAGE ConstraintKinds #}
{# LANGUAGE DataKinds #}
{# LANGUAGE PolyKinds #}
{# LANGUAGE QuantifiedConstraints #}
module Bug where
import Data.Kind
type Const a b = a
type SameKind (a :: k) (b :: k) = (() :: Constraint)
class (forall (b :: k). SameKind a b) => C (k :: Const Type a)
```
```
$ /opt/ghc/8.6.3/bin/ghc Bug.hs
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
Bug.hs:11:36: error:ghc: panic! (the 'impossible' happened)
(GHC version 8.6.3 for x86_64unknownlinux):
No skolem info:
[k1_a1X4[sk:1]]
Call stack:
CallStack (from HasCallStack):
callStackDoc, called at compiler/utils/Outputable.hs:1160:37 in ghc:Outputable
pprPanic, called at compiler/typecheck/TcErrors.hs:2891:5 in ghc:TcErrors
```
As with #16244, I imagine that the real culprit is that `SameKind a b` would force `a :: k`, which would be illscoped.
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.6.3 
 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":"GHC panic (No skolem info) with QuantifiedConstraints and strange scoping","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.6.3","keywords":["QuantifiedConstraints","TypeInType,"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"The following program panics with GHC 8.6.3 and HEAD:\r\n\r\n{{{#!hs\r\n{# LANGUAGE ConstraintKinds #}\r\n{# LANGUAGE DataKinds #}\r\n{# LANGUAGE PolyKinds #}\r\n{# LANGUAGE QuantifiedConstraints #}\r\nmodule Bug where\r\n\r\nimport Data.Kind\r\n\r\ntype Const a b = a\r\ntype SameKind (a :: k) (b :: k) = (() :: Constraint)\r\nclass (forall (b :: k). SameKind a b) => C (k :: Const Type a)\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:11:36: error:ghc: panic! (the 'impossible' happened)\r\n (GHC version 8.6.3 for x86_64unknownlinux):\r\n No skolem info:\r\n [k1_a1X4[sk:1]]\r\n Call stack:\r\n CallStack (from HasCallStack):\r\n callStackDoc, called at compiler/utils/Outputable.hs:1160:37 in ghc:Outputable\r\n pprPanic, called at compiler/typecheck/TcErrors.hs:2891:5 in ghc:TcErrors\r\n}}}\r\n\r\nAs with #16244, I imagine that the real culprit is that `SameKind a b` would force `a :: k`, which would be illscoped.","type_of_failure":"OtherFailure","blocking":[]} >The following program panics with GHC 8.6.3 and HEAD:
```hs
{# LANGUAGE ConstraintKinds #}
{# LANGUAGE DataKinds #}
{# LANGUAGE PolyKinds #}
{# LANGUAGE QuantifiedConstraints #}
module Bug where
import Data.Kind
type Const a b = a
type SameKind (a :: k) (b :: k) = (() :: Constraint)
class (forall (b :: k). SameKind a b) => C (k :: Const Type a)
```
```
$ /opt/ghc/8.6.3/bin/ghc Bug.hs
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
Bug.hs:11:36: error:ghc: panic! (the 'impossible' happened)
(GHC version 8.6.3 for x86_64unknownlinux):
No skolem info:
[k1_a1X4[sk:1]]
Call stack:
CallStack (from HasCallStack):
callStackDoc, called at compiler/utils/Outputable.hs:1160:37 in ghc:Outputable
pprPanic, called at compiler/typecheck/TcErrors.hs:2891:5 in ghc:TcErrors
```
As with #16244, I imagine that the real culprit is that `SameKind a b` would force `a :: k`, which would be illscoped.
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.6.3 
 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":"GHC panic (No skolem info) with QuantifiedConstraints and strange scoping","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.6.3","keywords":["QuantifiedConstraints","TypeInType,"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"The following program panics with GHC 8.6.3 and HEAD:\r\n\r\n{{{#!hs\r\n{# LANGUAGE ConstraintKinds #}\r\n{# LANGUAGE DataKinds #}\r\n{# LANGUAGE PolyKinds #}\r\n{# LANGUAGE QuantifiedConstraints #}\r\nmodule Bug where\r\n\r\nimport Data.Kind\r\n\r\ntype Const a b = a\r\ntype SameKind (a :: k) (b :: k) = (() :: Constraint)\r\nclass (forall (b :: k). SameKind a b) => C (k :: Const Type a)\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:11:36: error:ghc: panic! (the 'impossible' happened)\r\n (GHC version 8.6.3 for x86_64unknownlinux):\r\n No skolem info:\r\n [k1_a1X4[sk:1]]\r\n Call stack:\r\n CallStack (from HasCallStack):\r\n callStackDoc, called at compiler/utils/Outputable.hs:1160:37 in ghc:Outputable\r\n pprPanic, called at compiler/typecheck/TcErrors.hs:2891:5 in ghc:TcErrors\r\n}}}\r\n\r\nAs with #16244, I imagine that the real culprit is that `SameKind a b` would force `a :: k`, which would be illscoped.","type_of_failure":"OtherFailure","blocking":[]} >https://gitlab.haskell.org/ghc/ghc//issues/15598RebindableSyntax with RankNTypes and type class method call yields panic.20200617T03:35:55ZRoman BorschelRebindableSyntax with RankNTypes and type class method call yields panic.The following program in a file `ghcpanic.hs`
```hs
{# LANGUAGE
GADTSyntax
, RankNTypes
, RebindableSyntax
#}
import Prelude hiding ((>>=))
data InfDo where
InfDo :: String > (forall a. a > InfDo) > InfDo
prog :: InfDo
prog = do
_ < show (42 :: Int)
prog
where
(>>=) = InfDo
main :: IO ()
main = let x = prog in x `seq` return ()
```
when loaded into GHCi yields
```
λ> main
ghc: panic! (the 'impossible' happened)
(GHC version 8.4.3 for x86_64unknownlinux):
nameModule
system $dShow_abfY
Call stack:
CallStack (from HasCallStack):
callStackDoc, called at compiler/utils/Outputable.hs:1150:37 in ghc:Outputable
pprPanic, called at compiler/basicTypes/Name.hs:241:3 in ghc:Name
```
and separate compilation yields
```
$ ghc ghcpanic.hs
[1 of 1] Compiling Main ( ghcpanic.hs, ghcpanic.o )
ghc: panic! (the 'impossible' happened)
(GHC version 8.4.3 for x86_64unknownlinux):
StgCmmEnv: variable not found
$dShow_a1qI
local binds for:
$tcInfDo
$trModule
$tcInfDo1_r1th
$tcInfDo2_r1tH
$trModule1_r1tI
$trModule2_r1tJ
$trModule3_r1tK
$trModule4_r1tL
sat_s1E4
Call stack:
CallStack (from HasCallStack):
callStackDoc, called at compiler/utils/Outputable.hs:1150:37 in ghc:Outputable
pprPanic, called at compiler/codeGen/StgCmmEnv.hs:149:9 in ghc:StgCmmEnv
```
The problem disappears when either the rank2 type is removed from `InfDo` or when the call to `show` is replaced by a static string.
Besides 8.4.3, also reproduced with 8.6.0.20180714.
I believe it is somewhat related to [https://ghc.haskell.org/trac/ghc/ticket/14963](https://ghc.haskell.org/trac/ghc/ticket/14963)The following program in a file `ghcpanic.hs`
```hs
{# LANGUAGE
GADTSyntax
, RankNTypes
, RebindableSyntax
#}
import Prelude hiding ((>>=))
data InfDo where
InfDo :: String > (forall a. a > InfDo) > InfDo
prog :: InfDo
prog = do
_ < show (42 :: Int)
prog
where
(>>=) = InfDo
main :: IO ()
main = let x = prog in x `seq` return ()
```
when loaded into GHCi yields
```
λ> main
ghc: panic! (the 'impossible' happened)
(GHC version 8.4.3 for x86_64unknownlinux):
nameModule
system $dShow_abfY
Call stack:
CallStack (from HasCallStack):
callStackDoc, called at compiler/utils/Outputable.hs:1150:37 in ghc:Outputable
pprPanic, called at compiler/basicTypes/Name.hs:241:3 in ghc:Name
```
and separate compilation yields
```
$ ghc ghcpanic.hs
[1 of 1] Compiling Main ( ghcpanic.hs, ghcpanic.o )
ghc: panic! (the 'impossible' happened)
(GHC version 8.4.3 for x86_64unknownlinux):
StgCmmEnv: variable not found
$dShow_a1qI
local binds for:
$tcInfDo
$trModule
$tcInfDo1_r1th
$tcInfDo2_r1tH
$trModule1_r1tI
$trModule2_r1tJ
$trModule3_r1tK
$trModule4_r1tL
sat_s1E4
Call stack:
CallStack (from HasCallStack):
callStackDoc, called at compiler/utils/Outputable.hs:1150:37 in ghc:Outputable
pprPanic, called at compiler/codeGen/StgCmmEnv.hs:149:9 in ghc:StgCmmEnv
```
The problem disappears when either the rank2 type is removed from `InfDo` or when the call to `show` is replaced by a static string.
Besides 8.4.3, also reproduced with 8.6.0.20180714.
I believe it is somewhat related to [https://ghc.haskell.org/trac/ghc/ticket/14963](https://ghc.haskell.org/trac/ghc/ticket/14963)https://gitlab.haskell.org/ghc/ghc//issues/11540ghc accepts nonstandard type without language extension20200602T16:30:57Zlennart@augustsson.netghc accepts nonstandard type without language extensionGhc accepts this
```
f :: Eq a => Eq b => a > b > Bool
f a b = a==a && b==b
```
The nested contexts should require some language extension.
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  7.8.4 
 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 accepts nonstandard type without language extension","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"7.8.4","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"Ghc accepts this\r\n{{{\r\nf :: Eq a => Eq b => a > b > Bool\r\nf a b = a==a && b==b\r\n}}}\r\nThe nested contexts should require some language extension.\r\n","type_of_failure":"OtherFailure","blocking":[]} >Ghc accepts this
```
f :: Eq a => Eq b => a > b > Bool
f a b = a==a && b==b
```
The nested contexts should require some language extension.
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  7.8.4 
 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 accepts nonstandard type without language extension","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"7.8.4","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"Ghc accepts this\r\n{{{\r\nf :: Eq a => Eq b => a > b > Bool\r\nf a b = a==a && b==b\r\n}}}\r\nThe nested contexts should require some language extension.\r\n","type_of_failure":"OtherFailure","blocking":[]} >https://gitlab.haskell.org/ghc/ghc//issues/10450Poor type error message when an argument is insufficently polymorphic20190707T18:35:52ZsjcjoostenPoor type error message when an argument is insufficently polymorphicWhen pattern matching, "let/where" and "case" have different behaviours.
Currently, this is accepted (a version using 'where' instead of 'let' typechecks too):
```hs
{# LANGUAGE RankNTypes, ScopedTypeVariables #}
module Main where
data Phantom x = Phantom Int deriving Show
foo :: forall y. (forall x. (Phantom x)) > Phantom y
foo (Phantom x) = Phantom (x+1)
 trying to map foo over a list, this is the only way I can get it to work
typeAnnotatedMap :: (forall x. [Phantom x])
> [Phantom y]
typeAnnotatedMap intList = case intList of
[] > []
_ > let (phead:ptail) = intList
in foo phead : typeAnnotatedMap ptail
```
The following are not accepted:
```hs
typeAnnotatedMap1 :: (forall x. [Phantom x])
> [Phantom y]
typeAnnotatedMap1 intList = case intList of
[] > []
(phead:ptail) > foo phead : typeAnnotatedMap1 ptail
typeAnnotatedMap2 :: (forall x. [Phantom x])
> [Phantom y]
typeAnnotatedMap2 [] = []
typeAnnotatedMap2 (phead:ptail) = foo phead : typeAnnotatedMap2 ptail
```
The current type error is something like:
```
Couldn't match type ‘x0’ with ‘x’
because type variable ‘x’ would escape its scope
This (rigid, skolem) type variable is bound by
a type expected by the context: [Phantom x]
```
More helpful would be something like:
```
Your pattern match bound the following types to a shared skolem variable:
ptail :: [Phantom x0] (bound at rankNtest.hs:11:25)
phead :: Phantom x0 (bound at rankNtest.hs:11:19)
You may have intended to use a "let" or "where" patternmatch instead.
```When pattern matching, "let/where" and "case" have different behaviours.
Currently, this is accepted (a version using 'where' instead of 'let' typechecks too):
```hs
{# LANGUAGE RankNTypes, ScopedTypeVariables #}
module Main where
data Phantom x = Phantom Int deriving Show
foo :: forall y. (forall x. (Phantom x)) > Phantom y
foo (Phantom x) = Phantom (x+1)
 trying to map foo over a list, this is the only way I can get it to work
typeAnnotatedMap :: (forall x. [Phantom x])
> [Phantom y]
typeAnnotatedMap intList = case intList of
[] > []
_ > let (phead:ptail) = intList
in foo phead : typeAnnotatedMap ptail
```
The following are not accepted:
```hs
typeAnnotatedMap1 :: (forall x. [Phantom x])
> [Phantom y]
typeAnnotatedMap1 intList = case intList of
[] > []
(phead:ptail) > foo phead : typeAnnotatedMap1 ptail
typeAnnotatedMap2 :: (forall x. [Phantom x])
> [Phantom y]
typeAnnotatedMap2 [] = []
typeAnnotatedMap2 (phead:ptail) = foo phead : typeAnnotatedMap2 ptail
```
The current type error is something like:
```
Couldn't match type ‘x0’ with ‘x’
because type variable ‘x’ would escape its scope
This (rigid, skolem) type variable is bound by
a type expected by the context: [Phantom x]
```
More helpful would be something like:
```
Your pattern match bound the following types to a shared skolem variable:
ptail :: [Phantom x0] (bound at rankNtest.hs:11:25)
phead :: Phantom x0 (bound at rankNtest.hs:11:19)
You may have intended to use a "let" or "where" patternmatch instead.
```https://gitlab.haskell.org/ghc/ghc//issues/8346Rank 1 type signature still requires RankNTypes20200505T12:51:27ZTinctoriusRank 1 type signature still requires RankNTypesWhen trying to figure out which type variable names are \*actually\* bound in `ScopedTypeVariables`, I tried floating `forall`s into the covariant argument of the function type. Essentially, I ran into the problem that programs like the following are rejected:
```hs
{# LANGUAGE ExplicitForAll #}
tuple :: forall a. a > (forall b. b > (a, b))
tuple = (,)
```
The message is as follows:
```
Main.hs:2:10:
Illegal polymorphic or qualified type: forall b. b > (a, b)
Perhaps you intended to use XRankNTypes or XRank2Types
In the type signature for `tuple':
tuple :: forall a. a > (forall b. b > (a, b))
```
As far as I know, the rank of a type is defined by how deep quantifiers are nested in contravariant parts of that type. Or something like that. Also, as far as I know, `forall a. a > (forall b. b > (a, b))` is equivalent to `forall a b. a > b > (a, b)`, and more importantly, both are rank1 polymorphic. There should be no need to use extensions that allow higherranked polymorphism.
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  7.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":"Rank 1 type signature still requires RankNTypes","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"7.6.3","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"When trying to figure out which type variable names are *actually* bound in `ScopedTypeVariables`, I tried floating `forall`s into the covariant argument of the function type. Essentially, I ran into the problem that programs like the following are rejected:\r\n\r\n{{{\r\n#!hs\r\n{# LANGUAGE ExplicitForAll #}\r\ntuple :: forall a. a > (forall b. b > (a, b))\r\ntuple = (,)\r\n}}}\r\n\r\nThe message is as follows:\r\n{{{\r\nMain.hs:2:10:\r\n Illegal polymorphic or qualified type: forall b. b > (a, b)\r\n Perhaps you intended to use XRankNTypes or XRank2Types\r\n In the type signature for `tuple':\r\n tuple :: forall a. a > (forall b. b > (a, b))\r\n}}}\r\n\r\nAs far as I know, the rank of a type is defined by how deep quantifiers are nested in contravariant parts of that type. Or something like that. Also, as far as I know, `forall a. a > (forall b. b > (a, b))` is equivalent to `forall a b. a > b > (a, b)`, and more importantly, both are rank1 polymorphic. There should be no need to use extensions that allow higherranked polymorphism.","type_of_failure":"OtherFailure","blocking":[]} >When trying to figure out which type variable names are \*actually\* bound in `ScopedTypeVariables`, I tried floating `forall`s into the covariant argument of the function type. Essentially, I ran into the problem that programs like the following are rejected:
```hs
{# LANGUAGE ExplicitForAll #}
tuple :: forall a. a > (forall b. b > (a, b))
tuple = (,)
```
The message is as follows:
```
Main.hs:2:10:
Illegal polymorphic or qualified type: forall b. b > (a, b)
Perhaps you intended to use XRankNTypes or XRank2Types
In the type signature for `tuple':
tuple :: forall a. a > (forall b. b > (a, b))
```
As far as I know, the rank of a type is defined by how deep quantifiers are nested in contravariant parts of that type. Or something like that. Also, as far as I know, `forall a. a > (forall b. b > (a, b))` is equivalent to `forall a b. a > b > (a, b)`, and more importantly, both are rank1 polymorphic. There should be no need to use extensions that allow higherranked polymorphism.
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  7.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":"Rank 1 type signature still requires RankNTypes","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"7.6.3","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"When trying to figure out which type variable names are *actually* bound in `ScopedTypeVariables`, I tried floating `forall`s into the covariant argument of the function type. Essentially, I ran into the problem that programs like the following are rejected:\r\n\r\n{{{\r\n#!hs\r\n{# LANGUAGE ExplicitForAll #}\r\ntuple :: forall a. a > (forall b. b > (a, b))\r\ntuple = (,)\r\n}}}\r\n\r\nThe message is as follows:\r\n{{{\r\nMain.hs:2:10:\r\n Illegal polymorphic or qualified type: forall b. b > (a, b)\r\n Perhaps you intended to use XRankNTypes or XRank2Types\r\n In the type signature for `tuple':\r\n tuple :: forall a. a > (forall b. b > (a, b))\r\n}}}\r\n\r\nAs far as I know, the rank of a type is defined by how deep quantifiers are nested in contravariant parts of that type. Or something like that. Also, as far as I know, `forall a. a > (forall b. b > (a, b))` is equivalent to `forall a b. a > b > (a, b)`, and more importantly, both are rank1 polymorphic. There should be no need to use extensions that allow higherranked polymorphism.","type_of_failure":"OtherFailure","blocking":[]} >