GHC issueshttps://gitlab.haskell.org/ghc/ghc//issues20200716T21:57:58Zhttps://gitlab.haskell.org/ghc/ghc//issues/18464Tuple sections and impredicativity20200716T21:57:58ZSimon Peyton JonesTuple sections and impredicativityConsider `typecheck/should_run/tcrun042`
```
e :: a > (forall b. b > b > b) > (a, String, forall c. c > c > c)
e = (,"Hello" ++ "World",)
```
Currently the typing for tuple sections (in the `ExplicitTuples` case of `tcExpr`) makes the missing arguments into monotypes, so the program is rejected. With a bit more care we could do better. Not hard, but would need a little care.Consider `typecheck/should_run/tcrun042`
```
e :: a > (forall b. b > b > b) > (a, String, forall c. c > c > c)
e = (,"Hello" ++ "World",)
```
Currently the typing for tuple sections (in the `ExplicitTuples` case of `tcExpr`) makes the missing arguments into monotypes, so the program is rejected. With a bit more care we could do better. Not hard, but would need a little care.https://gitlab.haskell.org/ghc/ghc//issues/18324Impredicative types and donotation20200610T22:39:29ZSimon Peyton JonesImpredicative types and donotationThis ticket is about the interaction of Quick Look impredicativity and donotation.
Consider these definitions
```
t :: IO (forall a. a > a)
t = return id
p :: (forall a. a > a) > (Bool, Int)
p f = (f True, f 3)
 This typechecks (with QL)
foo1 = t >>= \x > return (p x)
 But this does *not* type check:
foo2 = do { x < t ; return (p x) }
```
Remember `(>>=) :: forall m a b. Monad m => m a > (a > m b) > m b`. Now, `foo1` works because Quick Look can work out how to instantiate `m` and `a` from the first argument `t`. Easy.
We just need to do the same for donotation, `foo2`. When #17582 finally lands (work in progress is !2960), this will happen automatically.This ticket is about the interaction of Quick Look impredicativity and donotation.
Consider these definitions
```
t :: IO (forall a. a > a)
t = return id
p :: (forall a. a > a) > (Bool, Int)
p f = (f True, f 3)
 This typechecks (with QL)
foo1 = t >>= \x > return (p x)
 But this does *not* type check:
foo2 = do { x < t ; return (p x) }
```
Remember `(>>=) :: forall m a b. Monad m => m a > (a > m b) > m b`. Now, `foo1` works because Quick Look can work out how to instantiate `m` and `a` from the first argument `t`. Easy.
We just need to do the same for donotation, `foo2`. When #17582 finally lands (work in progress is !2960), this will happen automatically.https://gitlab.haskell.org/ghc/ghc//issues/18126Implement Quick Look impredicativity20200917T08:22:01ZSimon Peyton JonesImplement Quick Look impredicativityThis ticket is to track progress on implementing ["A quick look at impredicativity"](https://www.microsoft.com/enus/research/publication/aquicklookatimpredicativity/).
The branch is `wip/T18126`. The MR for code review is !3220.
Still to do (in the future)
===============
* [ ] Donotation is not handled well (eg tcfail165). If we have `r :: IO (MVar (forall a. a>a))`, then
```
do { x < r ; ... }
```
should succeed with `x :: MVar (forall a. a>a)`, as we would if it was ``(>>=) r blah`. But currently we don't because we go via `tcSyntaxOp` (in `tcDoStmt`). This should get fixed automatically when we complete the work on rebindable syntax.
* [ ] Explicit lists don't work. E.g. if `ids :: [forall a.a>a]` then
```
x = [ids, ids]
```
fails. NB: works ok if the type is being *checked*; e.g. this is fine:
```
x :: [[forall a.a>a]]
x = [ids, ids]
```
The problem is in inference.
* [ ] Tuple sections fail; see `tcrun042` for example.
* [ ] Left and right sections fail. E.g. #8808, function `g2'`
* [ ] QL isn't applied in kinds at all. That is, we get no help with doing impredicative instantiation in types, only in terms. E.g. `dependent/should_fail/T15859a`.This ticket is to track progress on implementing ["A quick look at impredicativity"](https://www.microsoft.com/enus/research/publication/aquicklookatimpredicativity/).
The branch is `wip/T18126`. The MR for code review is !3220.
Still to do (in the future)
===============
* [ ] Donotation is not handled well (eg tcfail165). If we have `r :: IO (MVar (forall a. a>a))`, then
```
do { x < r ; ... }
```
should succeed with `x :: MVar (forall a. a>a)`, as we would if it was ``(>>=) r blah`. But currently we don't because we go via `tcSyntaxOp` (in `tcDoStmt`). This should get fixed automatically when we complete the work on rebindable syntax.
* [ ] Explicit lists don't work. E.g. if `ids :: [forall a.a>a]` then
```
x = [ids, ids]
```
fails. NB: works ok if the type is being *checked*; e.g. this is fine:
```
x :: [[forall a.a>a]]
x = [ids, ids]
```
The problem is in inference.
* [ ] Tuple sections fail; see `tcrun042` for example.
* [ ] Left and right sections fail. E.g. #8808, function `g2'`
* [ ] QL isn't applied in kinds at all. That is, we get no help with doing impredicative instantiation in types, only in terms. E.g. `dependent/should_fail/T15859a`.https://gitlab.haskell.org/ghc/ghc//issues/17332ImpredicativeTypes lets you pluck QuantifiedConstraints out of nowhere20200917T08:22:01ZRyan ScottImpredicativeTypes lets you pluck QuantifiedConstraints out of nowhereThis typechecks on GHC 8.6.5, 8.8.1, and HEAD:
```hs
{# LANGUAGE ConstraintKinds #}
{# LANGUAGE GADTs #}
{# LANGUAGE ImpredicativeTypes #}
{# LANGUAGE QuantifiedConstraints #}
module Bug where
import GHC.Exts
data Dict c = c => Dict
aux :: Dict (forall a. a)
aux = Dict
```
This is, to put it mildly, a bit concerning. Here is the most destructive use case I can find for this:
```hs
{# LANGUAGE ConstraintKinds #}
{# LANGUAGE GADTs #}
{# LANGUAGE ImpredicativeTypes #}
{# LANGUAGE MultiParamTypeClasses #}
{# LANGUAGE QuantifiedConstraints #}
{# LANGUAGE UndecidableInstances #}
{# LANGUAGE UndecidableSuperClasses #}
module Main where
data Dict c = c => Dict
aux :: Dict (forall a. a)
aux = Dict
class (forall a. a) => Bottom where
no :: a
sortOfUnsafeCoerce :: a > b
sortOfUnsafeCoerce
 Dict < aux
= no
main :: IO ()
main = print (sortOfUnsafeCoerce True :: Int)
```
I call this function `sortOfUnsafeCoerce` and not `unsafeCoerce` because I can't actually make it exhibit any sort of unsafety at runtime—it just panics in various ways:
```
$ /opt/ghc/8.8.1/bin/runghc Bug.hs
Bug.hs: Bug.hs: panic! (the 'impossible' happened)
(GHC version 8.8.1 for x86_64unknownlinux):
nameModule
system irred_a1uI
Call stack:
CallStack (from HasCallStack):
callStackDoc, called at compiler/utils/Outputable.hs:1159:37 in ghc:Outputable
pprPanic, called at compiler/basicTypes/Name.hs:249:3 in ghc:Name
Please report this as a GHC bug: https://www.haskell.org/ghc/reportabug
$ /opt/ghc/8.8.1/bin/ghc O0 Bug.hs
[1 of 1] Compiling Main ( Bug.hs, Bug.o )
ghc: panic! (the 'impossible' happened)
(GHC version 8.8.1 for x86_64unknownlinux):
StgCmmEnv: variable not found
irred_a1gL
local binds for:
no
$tc'Dict
$tcBottom
$tcDict
$trModule
$p1Bottom
$tcBottom1_r1HY
$tcBottom2_r1Iz
$tc'Dict1_r1IA
$tc'Dict2_r1IB
$tcDict1_r1IC
$tcDict2_r1ID
$krep_r1IE
$krep1_r1IF
$krep2_r1IG
$krep3_r1IH
$trModule1_r1II
$trModule2_r1IJ
$trModule3_r1IK
$trModule4_r1IL
$krep4_r1IM
$krep5_r1IN
Call stack:
CallStack (from HasCallStack):
callStackDoc, called at compiler/utils/Outputable.hs:1159:37 in ghc:Outputable
pprPanic, called at compiler/codeGen/StgCmmEnv.hs:149:9 in ghc:StgCmmEnv
Please report this as a GHC bug: https://www.haskell.org/ghc/reportabug
$ /opt/ghc/8.8.1/bin/ghc O Bug.hs
[1 of 1] Compiling Main ( Bug.hs, Bug.o )
ghc: panic! (the 'impossible' happened)
(GHC version 8.8.1 for x86_64unknownlinux):
piResultTys1
c_a1i0[tau:0]
[Bottom]
Call stack:
CallStack (from HasCallStack):
callStackDoc, called at compiler/utils/Outputable.hs:1159:37 in ghc:Outputable
pprPanic, called at compiler/types/Type.hs:1061:5 in ghc:Type
Please report this as a GHC bug: https://www.haskell.org/ghc/reportabug
```
I'm unclear if this is the same underlying issue as #17267, but I thought I would file a separate ticket just to be sure.This typechecks on GHC 8.6.5, 8.8.1, and HEAD:
```hs
{# LANGUAGE ConstraintKinds #}
{# LANGUAGE GADTs #}
{# LANGUAGE ImpredicativeTypes #}
{# LANGUAGE QuantifiedConstraints #}
module Bug where
import GHC.Exts
data Dict c = c => Dict
aux :: Dict (forall a. a)
aux = Dict
```
This is, to put it mildly, a bit concerning. Here is the most destructive use case I can find for this:
```hs
{# LANGUAGE ConstraintKinds #}
{# LANGUAGE GADTs #}
{# LANGUAGE ImpredicativeTypes #}
{# LANGUAGE MultiParamTypeClasses #}
{# LANGUAGE QuantifiedConstraints #}
{# LANGUAGE UndecidableInstances #}
{# LANGUAGE UndecidableSuperClasses #}
module Main where
data Dict c = c => Dict
aux :: Dict (forall a. a)
aux = Dict
class (forall a. a) => Bottom where
no :: a
sortOfUnsafeCoerce :: a > b
sortOfUnsafeCoerce
 Dict < aux
= no
main :: IO ()
main = print (sortOfUnsafeCoerce True :: Int)
```
I call this function `sortOfUnsafeCoerce` and not `unsafeCoerce` because I can't actually make it exhibit any sort of unsafety at runtime—it just panics in various ways:
```
$ /opt/ghc/8.8.1/bin/runghc Bug.hs
Bug.hs: Bug.hs: panic! (the 'impossible' happened)
(GHC version 8.8.1 for x86_64unknownlinux):
nameModule
system irred_a1uI
Call stack:
CallStack (from HasCallStack):
callStackDoc, called at compiler/utils/Outputable.hs:1159:37 in ghc:Outputable
pprPanic, called at compiler/basicTypes/Name.hs:249:3 in ghc:Name
Please report this as a GHC bug: https://www.haskell.org/ghc/reportabug
$ /opt/ghc/8.8.1/bin/ghc O0 Bug.hs
[1 of 1] Compiling Main ( Bug.hs, Bug.o )
ghc: panic! (the 'impossible' happened)
(GHC version 8.8.1 for x86_64unknownlinux):
StgCmmEnv: variable not found
irred_a1gL
local binds for:
no
$tc'Dict
$tcBottom
$tcDict
$trModule
$p1Bottom
$tcBottom1_r1HY
$tcBottom2_r1Iz
$tc'Dict1_r1IA
$tc'Dict2_r1IB
$tcDict1_r1IC
$tcDict2_r1ID
$krep_r1IE
$krep1_r1IF
$krep2_r1IG
$krep3_r1IH
$trModule1_r1II
$trModule2_r1IJ
$trModule3_r1IK
$trModule4_r1IL
$krep4_r1IM
$krep5_r1IN
Call stack:
CallStack (from HasCallStack):
callStackDoc, called at compiler/utils/Outputable.hs:1159:37 in ghc:Outputable
pprPanic, called at compiler/codeGen/StgCmmEnv.hs:149:9 in ghc:StgCmmEnv
Please report this as a GHC bug: https://www.haskell.org/ghc/reportabug
$ /opt/ghc/8.8.1/bin/ghc O Bug.hs
[1 of 1] Compiling Main ( Bug.hs, Bug.o )
ghc: panic! (the 'impossible' happened)
(GHC version 8.8.1 for x86_64unknownlinux):
piResultTys1
c_a1i0[tau:0]
[Bottom]
Call stack:
CallStack (from HasCallStack):
callStackDoc, called at compiler/utils/Outputable.hs:1159:37 in ghc:Outputable
pprPanic, called at compiler/types/Type.hs:1061:5 in ghc:Type
Please report this as a GHC bug: https://www.haskell.org/ghc/reportabug
```
I'm unclear if this is the same underlying issue as #17267, but I thought I would file a separate ticket just to be sure.https://gitlab.haskell.org/ghc/ghc//issues/16209GHC behaves differently when binding has separate or inlined type declaration20200716T17:16:14ZfghibelliniGHC behaves differently when binding has separate or inlined type declaration```hs
{# LANGUAGE RankNTypes #}
{# LANGUAGE ScopedTypeVariables #}
main = do
let a :: forall t. Functor t => t () = undefined
let g :: forall u. Functor u => u () = a
putStrLn "success"
```
fails with:
```
source_file.hs:6:44:
Couldn't match expected type ‘forall (u :: * > *).
Functor u =>
u ()’
with actual type ‘t0 ()’
When checking that: t0 ()
is more polymorphic than: forall (u :: * > *). Functor u => u ()
In the expression: a
```
but the following compiles successfully
```hs
{# LANGUAGE RankNTypes #}
{# LANGUAGE ScopedTypeVariables #}
main = do
let a :: forall t. Functor t => t () = undefined
let g :: forall u. Functor u => u ()
g = a
putStrLn "success"
```
On GHC 7.10 it works as described above. On 8.4.4 it fails even on the "functioning code".
```
a.hs:5:44: error:
• Cannot instantiate unification variable ‘a0’
with a type involving foralls:
forall (t :: * > *). Functor t => t ()
GHC doesn't yet support impredicative polymorphism
• In the expression: undefined
In a pattern binding:
a :: forall (t :: * > *). Functor t => t () = undefined
In the expression:
do let a :: forall t. Functor t => t () = undefined
let g :: forall u. Functor u => u ()
g = a
putStrLn "success"
``````hs
{# LANGUAGE RankNTypes #}
{# LANGUAGE ScopedTypeVariables #}
main = do
let a :: forall t. Functor t => t () = undefined
let g :: forall u. Functor u => u () = a
putStrLn "success"
```
fails with:
```
source_file.hs:6:44:
Couldn't match expected type ‘forall (u :: * > *).
Functor u =>
u ()’
with actual type ‘t0 ()’
When checking that: t0 ()
is more polymorphic than: forall (u :: * > *). Functor u => u ()
In the expression: a
```
but the following compiles successfully
```hs
{# LANGUAGE RankNTypes #}
{# LANGUAGE ScopedTypeVariables #}
main = do
let a :: forall t. Functor t => t () = undefined
let g :: forall u. Functor u => u ()
g = a
putStrLn "success"
```
On GHC 7.10 it works as described above. On 8.4.4 it fails even on the "functioning code".
```
a.hs:5:44: error:
• Cannot instantiate unification variable ‘a0’
with a type involving foralls:
forall (t :: * > *). Functor t => t ()
GHC doesn't yet support impredicative polymorphism
• In the expression: undefined
In a pattern binding:
a :: forall (t :: * > *). Functor t => t () = undefined
In the expression:
do let a :: forall t. Functor t => t () = undefined
let g :: forall u. Functor u => u ()
g = a
putStrLn "success"
```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/10709Using ($) allows sneaky impredicativity on its left20190707T18:34:32ZRichard Eisenbergrae@richarde.devUsing ($) allows sneaky impredicativity on its leftObserve the following shady interaction with GHCi:
```
GHCi, version 7.10.1: http://www.haskell.org/ghc/ :? for help
Prelude> import GHC.IO
Prelude GHC.IO> import Control.Monad
Prelude GHC.IO Control.Monad> :t mask
mask :: forall b. ((forall a. IO a > IO a) > IO b) > IO b
Prelude GHC.IO Control.Monad> :t replicateM 2 . mask
<interactive>:1:16:
Couldn't match type ‘a’ with ‘(forall a2. IO a2 > IO a2) > IO a1’
‘a’ is a rigid type variable bound by
the inferred type of it :: a > IO [a1] at Top level
Expected type: a > IO a1
Actual type: ((forall a. IO a > IO a) > IO a1) > IO a1
In the second argument of ‘(.)’, namely ‘mask’
In the expression: replicateM 2 . mask
Prelude GHC.IO Control.Monad> :t (replicateM 2 . mask) undefined
<interactive>:1:17:
Cannot instantiate unification variable ‘a0’
with a type involving foralls: (forall a1. IO a1 > IO a1) > IO a
Perhaps you want ImpredicativeTypes
In the second argument of ‘(.)’, namely ‘mask’
In the expression: replicateM 2 . mask
Prelude GHC.IO Control.Monad> :t (replicateM 2 . mask) $ undefined
(replicateM 2 . mask) $ undefined :: forall a. IO [a]
```
Due to the way that GHC processes `($)`, it allows this form of impredicativity on the LHS of `($)`. This case is inspired by https://github.com/ghc/nofib/blob/master/smp/threads006/Main.hs which contains the line
```
tids < replicateM nthreads . mask $ \_ > forkIO $ return ()
```
I think that line should be rejected.
The problem stems from the treatment of `OpenKind` as described in `Note [OpenTypeKind accepts foralls]` in TcMType.
Unrelated work changes this behavior by rejecting the nofib program. The point of this ticket is to provoke discussion about what is right and what is wrong here, not to request a fix.
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  7.10.1 
 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":"Using ($) allows sneaky impredicativity on its left","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"OwnedBy","contents":"goldfire"},"version":"7.10.1","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"Observe the following shady interaction with GHCi:\r\n\r\n{{{\r\nGHCi, version 7.10.1: http://www.haskell.org/ghc/ :? for help\r\nPrelude> import GHC.IO\r\nPrelude GHC.IO> import Control.Monad\r\nPrelude GHC.IO Control.Monad> :t mask\r\nmask :: forall b. ((forall a. IO a > IO a) > IO b) > IO b\r\nPrelude GHC.IO Control.Monad> :t replicateM 2 . mask\r\n\r\n<interactive>:1:16:\r\n Couldn't match type ‘a’ with ‘(forall a2. IO a2 > IO a2) > IO a1’\r\n ‘a’ is a rigid type variable bound by\r\n the inferred type of it :: a > IO [a1] at Top level\r\n Expected type: a > IO a1\r\n Actual type: ((forall a. IO a > IO a) > IO a1) > IO a1\r\n In the second argument of ‘(.)’, namely ‘mask’\r\n In the expression: replicateM 2 . mask\r\nPrelude GHC.IO Control.Monad> :t (replicateM 2 . mask) undefined\r\n\r\n<interactive>:1:17:\r\n Cannot instantiate unification variable ‘a0’\r\n with a type involving foralls: (forall a1. IO a1 > IO a1) > IO a\r\n Perhaps you want ImpredicativeTypes\r\n In the second argument of ‘(.)’, namely ‘mask’\r\n In the expression: replicateM 2 . mask\r\nPrelude GHC.IO Control.Monad> :t (replicateM 2 . mask) $ undefined\r\n(replicateM 2 . mask) $ undefined :: forall a. IO [a]\r\n}}}\r\n\r\nDue to the way that GHC processes `($)`, it allows this form of impredicativity on the LHS of `($)`. This case is inspired by https://github.com/ghc/nofib/blob/master/smp/threads006/Main.hs which contains the line\r\n\r\n{{{\r\n tids < replicateM nthreads . mask $ \\_ > forkIO $ return ()\r\n}}}\r\n\r\nI think that line should be rejected.\r\n\r\nThe problem stems from the treatment of `OpenKind` as described in `Note [OpenTypeKind accepts foralls]` in TcMType.\r\n\r\nUnrelated work changes this behavior by rejecting the nofib program. The point of this ticket is to provoke discussion about what is right and what is wrong here, not to request a fix.","type_of_failure":"OtherFailure","blocking":[]} >Observe the following shady interaction with GHCi:
```
GHCi, version 7.10.1: http://www.haskell.org/ghc/ :? for help
Prelude> import GHC.IO
Prelude GHC.IO> import Control.Monad
Prelude GHC.IO Control.Monad> :t mask
mask :: forall b. ((forall a. IO a > IO a) > IO b) > IO b
Prelude GHC.IO Control.Monad> :t replicateM 2 . mask
<interactive>:1:16:
Couldn't match type ‘a’ with ‘(forall a2. IO a2 > IO a2) > IO a1’
‘a’ is a rigid type variable bound by
the inferred type of it :: a > IO [a1] at Top level
Expected type: a > IO a1
Actual type: ((forall a. IO a > IO a) > IO a1) > IO a1
In the second argument of ‘(.)’, namely ‘mask’
In the expression: replicateM 2 . mask
Prelude GHC.IO Control.Monad> :t (replicateM 2 . mask) undefined
<interactive>:1:17:
Cannot instantiate unification variable ‘a0’
with a type involving foralls: (forall a1. IO a1 > IO a1) > IO a
Perhaps you want ImpredicativeTypes
In the second argument of ‘(.)’, namely ‘mask’
In the expression: replicateM 2 . mask
Prelude GHC.IO Control.Monad> :t (replicateM 2 . mask) $ undefined
(replicateM 2 . mask) $ undefined :: forall a. IO [a]
```
Due to the way that GHC processes `($)`, it allows this form of impredicativity on the LHS of `($)`. This case is inspired by https://github.com/ghc/nofib/blob/master/smp/threads006/Main.hs which contains the line
```
tids < replicateM nthreads . mask $ \_ > forkIO $ return ()
```
I think that line should be rejected.
The problem stems from the treatment of `OpenKind` as described in `Note [OpenTypeKind accepts foralls]` in TcMType.
Unrelated work changes this behavior by rejecting the nofib program. The point of this ticket is to provoke discussion about what is right and what is wrong here, not to request a fix.
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  7.10.1 
 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":"Using ($) allows sneaky impredicativity on its left","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"OwnedBy","contents":"goldfire"},"version":"7.10.1","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"Observe the following shady interaction with GHCi:\r\n\r\n{{{\r\nGHCi, version 7.10.1: http://www.haskell.org/ghc/ :? for help\r\nPrelude> import GHC.IO\r\nPrelude GHC.IO> import Control.Monad\r\nPrelude GHC.IO Control.Monad> :t mask\r\nmask :: forall b. ((forall a. IO a > IO a) > IO b) > IO b\r\nPrelude GHC.IO Control.Monad> :t replicateM 2 . mask\r\n\r\n<interactive>:1:16:\r\n Couldn't match type ‘a’ with ‘(forall a2. IO a2 > IO a2) > IO a1’\r\n ‘a’ is a rigid type variable bound by\r\n the inferred type of it :: a > IO [a1] at Top level\r\n Expected type: a > IO a1\r\n Actual type: ((forall a. IO a > IO a) > IO a1) > IO a1\r\n In the second argument of ‘(.)’, namely ‘mask’\r\n In the expression: replicateM 2 . mask\r\nPrelude GHC.IO Control.Monad> :t (replicateM 2 . mask) undefined\r\n\r\n<interactive>:1:17:\r\n Cannot instantiate unification variable ‘a0’\r\n with a type involving foralls: (forall a1. IO a1 > IO a1) > IO a\r\n Perhaps you want ImpredicativeTypes\r\n In the second argument of ‘(.)’, namely ‘mask’\r\n In the expression: replicateM 2 . mask\r\nPrelude GHC.IO Control.Monad> :t (replicateM 2 . mask) $ undefined\r\n(replicateM 2 . mask) $ undefined :: forall a. IO [a]\r\n}}}\r\n\r\nDue to the way that GHC processes `($)`, it allows this form of impredicativity on the LHS of `($)`. This case is inspired by https://github.com/ghc/nofib/blob/master/smp/threads006/Main.hs which contains the line\r\n\r\n{{{\r\n tids < replicateM nthreads . mask $ \\_ > forkIO $ return ()\r\n}}}\r\n\r\nI think that line should be rejected.\r\n\r\nThe problem stems from the treatment of `OpenKind` as described in `Note [OpenTypeKind accepts foralls]` in TcMType.\r\n\r\nUnrelated work changes this behavior by rejecting the nofib program. The point of this ticket is to provoke discussion about what is right and what is wrong here, not to request a fix.","type_of_failure":"OtherFailure","blocking":[]} >Richard Eisenbergrae@richarde.devRichard Eisenbergrae@richarde.devhttps://gitlab.haskell.org/ghc/ghc//issues/9730Polymorphism and type classes20200917T08:22:01ZmjaskelPolymorphism and type classesLet us define some typeclasses
```hs
class A a where
class B b where
class C c where
```
I often use `RankNTypes` and write a type `forall a. A a => a` to mean that only the members of type class `A` have been used to construct its elements.
If I have a function that converts programs written only with members of `A` into a programs written only with members of `B`, and an analogous one to convert from `B` to `C`, I would expect to be able to compose them
```hs
a2b :: (forall a. A a => a) > (forall b. B b => b)
a2b = undefined
b2c :: (forall b. B b => b) > (forall c. C c => c)
b2c = undefined
a2c :: (forall a. A a => a) > (forall c. C c => c)
a2c = b2c . a2b
```
However, I get many types error of the form:
```
Cannot instantiate unification variable ‘b0’
with a type involving foralls: forall b. B b => b
Perhaps you want ImpredicativeTypes
```
Every `forall` is under a function type, but I enable `ImpredicativeTypes` anyway, and I get the following error:
```
Could not deduce (B (forall b. B b => b))
arising from a use of ‘a2b’
from the context (C c)
bound by the type signature for
a2c :: C c => (forall a. A a => a) > c
```
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  7.8.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":"Polymorphism and type classes","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"7.8.3","keywords":["ImpredicativeTypes","Polymorphism,","Typeclass,"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"Let us define some typeclasses\r\n\r\n{{{#!hs\r\nclass A a where\r\n\r\nclass B b where\r\n\r\nclass C c where\r\n}}}\r\n\r\nI often use `RankNTypes` and write a type `forall a. A a => a` to mean that only the members of type class `A` have been used to construct its elements. \r\n\r\nIf I have a function that converts programs written only with members of `A` into a programs written only with members of `B`, and an analogous one to convert from `B` to `C`, I would expect to be able to compose them\r\n\r\n{{{#!hs\r\na2b :: (forall a. A a => a) > (forall b. B b => b)\r\na2b = undefined\r\n\r\nb2c :: (forall b. B b => b) > (forall c. C c => c)\r\nb2c = undefined\r\n\r\na2c :: (forall a. A a => a) > (forall c. C c => c)\r\na2c = b2c . a2b\r\n}}}\r\n\r\n\r\nHowever, I get many types error of the form: \r\n\r\n{{{\r\nCannot instantiate unification variable ‘b0’\r\n with a type involving foralls: forall b. B b => b\r\n Perhaps you want ImpredicativeTypes\r\n}}}\r\n\r\nEvery `forall` is under a function type, but I enable `ImpredicativeTypes` anyway, and I get the following error:\r\n\r\n{{{\r\n Could not deduce (B (forall b. B b => b))\r\n arising from a use of ‘a2b’\r\n from the context (C c)\r\n bound by the type signature for\r\n a2c :: C c => (forall a. A a => a) > c\r\n}}}\r\n","type_of_failure":"OtherFailure","blocking":[]} >Let us define some typeclasses
```hs
class A a where
class B b where
class C c where
```
I often use `RankNTypes` and write a type `forall a. A a => a` to mean that only the members of type class `A` have been used to construct its elements.
If I have a function that converts programs written only with members of `A` into a programs written only with members of `B`, and an analogous one to convert from `B` to `C`, I would expect to be able to compose them
```hs
a2b :: (forall a. A a => a) > (forall b. B b => b)
a2b = undefined
b2c :: (forall b. B b => b) > (forall c. C c => c)
b2c = undefined
a2c :: (forall a. A a => a) > (forall c. C c => c)
a2c = b2c . a2b
```
However, I get many types error of the form:
```
Cannot instantiate unification variable ‘b0’
with a type involving foralls: forall b. B b => b
Perhaps you want ImpredicativeTypes
```
Every `forall` is under a function type, but I enable `ImpredicativeTypes` anyway, and I get the following error:
```
Could not deduce (B (forall b. B b => b))
arising from a use of ‘a2b’
from the context (C c)
bound by the type signature for
a2c :: C c => (forall a. A a => a) > c
```
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  7.8.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":"Polymorphism and type classes","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"7.8.3","keywords":["ImpredicativeTypes","Polymorphism,","Typeclass,"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"Let us define some typeclasses\r\n\r\n{{{#!hs\r\nclass A a where\r\n\r\nclass B b where\r\n\r\nclass C c where\r\n}}}\r\n\r\nI often use `RankNTypes` and write a type `forall a. A a => a` to mean that only the members of type class `A` have been used to construct its elements. \r\n\r\nIf I have a function that converts programs written only with members of `A` into a programs written only with members of `B`, and an analogous one to convert from `B` to `C`, I would expect to be able to compose them\r\n\r\n{{{#!hs\r\na2b :: (forall a. A a => a) > (forall b. B b => b)\r\na2b = undefined\r\n\r\nb2c :: (forall b. B b => b) > (forall c. C c => c)\r\nb2c = undefined\r\n\r\na2c :: (forall a. A a => a) > (forall c. C c => c)\r\na2c = b2c . a2b\r\n}}}\r\n\r\n\r\nHowever, I get many types error of the form: \r\n\r\n{{{\r\nCannot instantiate unification variable ‘b0’\r\n with a type involving foralls: forall b. B b => b\r\n Perhaps you want ImpredicativeTypes\r\n}}}\r\n\r\nEvery `forall` is under a function type, but I enable `ImpredicativeTypes` anyway, and I get the following error:\r\n\r\n{{{\r\n Could not deduce (B (forall b. B b => b))\r\n arising from a use of ‘a2b’\r\n from the context (C c)\r\n bound by the type signature for\r\n a2c :: C c => (forall a. A a => a) > c\r\n}}}\r\n","type_of_failure":"OtherFailure","blocking":[]} >https://gitlab.haskell.org/ghc/ghc//issues/8808ImpredicativeTypes type checking fails depending on syntax of arguments20200917T08:22:01ZguestImpredicativeTypes type checking fails depending on syntax of argumentsg1 and g2 below type check, but g1', g2', and g2'' don't even though the types are exactly the same.
```
{# LANGUAGE ImpredicativeTypes, NoMonomorphismRestriction #}
module Test where
f1 :: Maybe (forall a. [a] > [a]) > Maybe ([Int], [Char])
f1 (Just g) = Just (g [3], g "hello")
f1 Nothing = Nothing
f2 :: [forall a. [a] > [a]] > Maybe ([Int], [Char])
f2 [g] = Just (g [3], g "hello")
f2 [] = Nothing
g1 = (f1 . Just) reverse
g1' = f1 (Just reverse)
g2 = f2 [reverse]
g2' = f2 ((:[]) reverse)
g2'' = f2 (reverse : [])
```
Compiling it with HEAD gives these errors:
```
[1 of 1] Compiling Test ( test.hs, test.o )
test.hs:12:16:
Couldn't match expected type ‛forall a. [a] > [a]’
with actual type ‛[a2] > [a2]’
In the first argument of ‛Just’, namely ‛reverse’
In the first argument of ‛f1’, namely ‛(Just reverse)’
test.hs:15:17:
Couldn't match expected type ‛forall a. [a] > [a]’
with actual type ‛[a0] > [a0]’
In the first argument of ‛: []’, namely ‛reverse’
In the first argument of ‛f2’, namely ‛((: []) reverse)’
test.hs:16:12:
Couldn't match expected type ‛forall a. [a] > [a]’
with actual type ‛[a1] > [a1]’
In the first argument of ‛(:)’, namely ‛reverse’
In the first argument of ‛f2’, namely ‛(reverse : [])’
```
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  7.8.1rc1 
 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":"ImpredicativeTypes type checking fails depending on syntax of arguments","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"7.8.1rc1","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"g1 and g2 below type check, but g1', g2', and g2'' don't even though the types are exactly the same.\r\n{{{\r\n{# LANGUAGE ImpredicativeTypes, NoMonomorphismRestriction #}\r\nmodule Test where\r\nf1 :: Maybe (forall a. [a] > [a]) > Maybe ([Int], [Char])\r\nf1 (Just g) = Just (g [3], g \"hello\")\r\nf1 Nothing = Nothing\r\n\r\nf2 :: [forall a. [a] > [a]] > Maybe ([Int], [Char])\r\nf2 [g] = Just (g [3], g \"hello\")\r\nf2 [] = Nothing\r\n\r\ng1 = (f1 . Just) reverse\r\ng1' = f1 (Just reverse)\r\n\r\ng2 = f2 [reverse]\r\ng2' = f2 ((:[]) reverse)\r\ng2'' = f2 (reverse : [])\r\n}}}\r\nCompiling it with HEAD gives these errors:\r\n{{{\r\n[1 of 1] Compiling Test ( test.hs, test.o )\r\n\r\ntest.hs:12:16:\r\n Couldn't match expected type ‛forall a. [a] > [a]’\r\n with actual type ‛[a2] > [a2]’\r\n In the first argument of ‛Just’, namely ‛reverse’\r\n In the first argument of ‛f1’, namely ‛(Just reverse)’\r\n\r\ntest.hs:15:17:\r\n Couldn't match expected type ‛forall a. [a] > [a]’\r\n with actual type ‛[a0] > [a0]’\r\n In the first argument of ‛: []’, namely ‛reverse’\r\n In the first argument of ‛f2’, namely ‛((: []) reverse)’\r\n\r\ntest.hs:16:12:\r\n Couldn't match expected type ‛forall a. [a] > [a]’\r\n with actual type ‛[a1] > [a1]’\r\n In the first argument of ‛(:)’, namely ‛reverse’\r\n In the first argument of ‛f2’, namely ‛(reverse : [])’\r\n}}}","type_of_failure":"OtherFailure","blocking":[]} >g1 and g2 below type check, but g1', g2', and g2'' don't even though the types are exactly the same.
```
{# LANGUAGE ImpredicativeTypes, NoMonomorphismRestriction #}
module Test where
f1 :: Maybe (forall a. [a] > [a]) > Maybe ([Int], [Char])
f1 (Just g) = Just (g [3], g "hello")
f1 Nothing = Nothing
f2 :: [forall a. [a] > [a]] > Maybe ([Int], [Char])
f2 [g] = Just (g [3], g "hello")
f2 [] = Nothing
g1 = (f1 . Just) reverse
g1' = f1 (Just reverse)
g2 = f2 [reverse]
g2' = f2 ((:[]) reverse)
g2'' = f2 (reverse : [])
```
Compiling it with HEAD gives these errors:
```
[1 of 1] Compiling Test ( test.hs, test.o )
test.hs:12:16:
Couldn't match expected type ‛forall a. [a] > [a]’
with actual type ‛[a2] > [a2]’
In the first argument of ‛Just’, namely ‛reverse’
In the first argument of ‛f1’, namely ‛(Just reverse)’
test.hs:15:17:
Couldn't match expected type ‛forall a. [a] > [a]’
with actual type ‛[a0] > [a0]’
In the first argument of ‛: []’, namely ‛reverse’
In the first argument of ‛f2’, namely ‛((: []) reverse)’
test.hs:16:12:
Couldn't match expected type ‛forall a. [a] > [a]’
with actual type ‛[a1] > [a1]’
In the first argument of ‛(:)’, namely ‛reverse’
In the first argument of ‛f2’, namely ‛(reverse : [])’
```
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  7.8.1rc1 
 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":"ImpredicativeTypes type checking fails depending on syntax of arguments","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"7.8.1rc1","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"g1 and g2 below type check, but g1', g2', and g2'' don't even though the types are exactly the same.\r\n{{{\r\n{# LANGUAGE ImpredicativeTypes, NoMonomorphismRestriction #}\r\nmodule Test where\r\nf1 :: Maybe (forall a. [a] > [a]) > Maybe ([Int], [Char])\r\nf1 (Just g) = Just (g [3], g \"hello\")\r\nf1 Nothing = Nothing\r\n\r\nf2 :: [forall a. [a] > [a]] > Maybe ([Int], [Char])\r\nf2 [g] = Just (g [3], g \"hello\")\r\nf2 [] = Nothing\r\n\r\ng1 = (f1 . Just) reverse\r\ng1' = f1 (Just reverse)\r\n\r\ng2 = f2 [reverse]\r\ng2' = f2 ((:[]) reverse)\r\ng2'' = f2 (reverse : [])\r\n}}}\r\nCompiling it with HEAD gives these errors:\r\n{{{\r\n[1 of 1] Compiling Test ( test.hs, test.o )\r\n\r\ntest.hs:12:16:\r\n Couldn't match expected type ‛forall a. [a] > [a]’\r\n with actual type ‛[a2] > [a2]’\r\n In the first argument of ‛Just’, namely ‛reverse’\r\n In the first argument of ‛f1’, namely ‛(Just reverse)’\r\n\r\ntest.hs:15:17:\r\n Couldn't match expected type ‛forall a. [a] > [a]’\r\n with actual type ‛[a0] > [a0]’\r\n In the first argument of ‛: []’, namely ‛reverse’\r\n In the first argument of ‛f2’, namely ‛((: []) reverse)’\r\n\r\ntest.hs:16:12:\r\n Couldn't match expected type ‛forall a. [a] > [a]’\r\n with actual type ‛[a1] > [a1]’\r\n In the first argument of ‛(:)’, namely ‛reverse’\r\n In the first argument of ‛f2’, namely ‛(reverse : [])’\r\n}}}","type_of_failure":"OtherFailure","blocking":[]} >https://gitlab.haskell.org/ghc/ghc//issues/7026Impredicative implicit parameters20200917T08:22:01ZAshley YakeleyImpredicative implicit parametersThere doesn't seem to be a way to make impredicative implicit parameters work in 7.4.2:
```
{# LANGUAGE ImplicitParams, ImpredicativeTypes #}
module Bug where
f1 :: Maybe ((?a :: Bool) => Char)
f1 = Just 'C'
f2 :: Maybe ((?a :: Bool) => Bool)
f2 = Just ?a
```
```
$ ghc c Bug.hs
Bug.hs:5:15:
Couldn't match expected type `(?a::Bool) => Char'
with actual type `Char'
In the first argument of `Just', namely 'C'
In the expression: Just 'C'
In an equation for `f1': f1 = Just 'C'
Bug.hs:8:15:
Unbound implicit parameter (?a::(?a::Bool) => Bool)
arising from a use of implicit parameter `?a'
In the first argument of `Just', namely `?a'
In the expression: Just ?a
In an equation for `f2': f2 = Just ?a
```
I believe this used to work?
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  7.4.2 
 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":"Impredicative implicit parameters","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"7.4.2","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"There doesn't seem to be a way to make impredicative implicit parameters work in 7.4.2:\r\n\r\n{{{\r\n{# LANGUAGE ImplicitParams, ImpredicativeTypes #}\r\nmodule Bug where\r\n\r\n f1 :: Maybe ((?a :: Bool) => Char)\r\n f1 = Just 'C'\r\n\r\n f2 :: Maybe ((?a :: Bool) => Bool)\r\n f2 = Just ?a\r\n}}}\r\n\r\n\r\n{{{\r\n$ ghc c Bug.hs \r\n\r\nBug.hs:5:15:\r\n Couldn't match expected type `(?a::Bool) => Char'\r\n with actual type `Char'\r\n In the first argument of `Just', namely 'C'\r\n In the expression: Just 'C'\r\n In an equation for `f1': f1 = Just 'C'\r\n\r\nBug.hs:8:15:\r\n Unbound implicit parameter (?a::(?a::Bool) => Bool)\r\n arising from a use of implicit parameter `?a'\r\n In the first argument of `Just', namely `?a'\r\n In the expression: Just ?a\r\n In an equation for `f2': f2 = Just ?a\r\n}}}\r\n\r\nI believe this used to work?","type_of_failure":"OtherFailure","blocking":[]} >There doesn't seem to be a way to make impredicative implicit parameters work in 7.4.2:
```
{# LANGUAGE ImplicitParams, ImpredicativeTypes #}
module Bug where
f1 :: Maybe ((?a :: Bool) => Char)
f1 = Just 'C'
f2 :: Maybe ((?a :: Bool) => Bool)
f2 = Just ?a
```
```
$ ghc c Bug.hs
Bug.hs:5:15:
Couldn't match expected type `(?a::Bool) => Char'
with actual type `Char'
In the first argument of `Just', namely 'C'
In the expression: Just 'C'
In an equation for `f1': f1 = Just 'C'
Bug.hs:8:15:
Unbound implicit parameter (?a::(?a::Bool) => Bool)
arising from a use of implicit parameter `?a'
In the first argument of `Just', namely `?a'
In the expression: Just ?a
In an equation for `f2': f2 = Just ?a
```
I believe this used to work?
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  7.4.2 
 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":"Impredicative implicit parameters","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"7.4.2","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"There doesn't seem to be a way to make impredicative implicit parameters work in 7.4.2:\r\n\r\n{{{\r\n{# LANGUAGE ImplicitParams, ImpredicativeTypes #}\r\nmodule Bug where\r\n\r\n f1 :: Maybe ((?a :: Bool) => Char)\r\n f1 = Just 'C'\r\n\r\n f2 :: Maybe ((?a :: Bool) => Bool)\r\n f2 = Just ?a\r\n}}}\r\n\r\n\r\n{{{\r\n$ ghc c Bug.hs \r\n\r\nBug.hs:5:15:\r\n Couldn't match expected type `(?a::Bool) => Char'\r\n with actual type `Char'\r\n In the first argument of `Just', namely 'C'\r\n In the expression: Just 'C'\r\n In an equation for `f1': f1 = Just 'C'\r\n\r\nBug.hs:8:15:\r\n Unbound implicit parameter (?a::(?a::Bool) => Bool)\r\n arising from a use of implicit parameter `?a'\r\n In the first argument of `Just', namely `?a'\r\n In the expression: Just ?a\r\n In an equation for `f2': f2 = Just ?a\r\n}}}\r\n\r\nI believe this used to work?","type_of_failure":"OtherFailure","blocking":[]} >https://gitlab.haskell.org/ghc/ghc//issues/4295Review higherrank and impredicative types20200917T08:22:01ZSimon Peyton JonesReview higherrank and impredicative typesThe ticket is a placeholder to remind me to work through the test cases for impredicative and higher rank types in the new typechecker. For now, I'm marking many of them as `expect_broken` on this ticket, although I think many of them really should fail.
 tc150
 tc194
 tcfail198
 tcfail174
 tcfail165
 tcfail145
 tcfail104
 tc211
 indexedtypes/should_compile/T4120
 simpl017
 Many tests in `boxy/` (see also #1330 for Church2)
 #2193
 #2846
 #4347
 [Lennart's blog post](http://augustss.blogspot.com/2011/07/impredicativepolymorphismusecasein.html) has an interesting use case of impredicative polymorphism; it worked in 7.0, but alas not in the new typechecker.The ticket is a placeholder to remind me to work through the test cases for impredicative and higher rank types in the new typechecker. For now, I'm marking many of them as `expect_broken` on this ticket, although I think many of them really should fail.
 tc150
 tc194
 tcfail198
 tcfail174
 tcfail165
 tcfail145
 tcfail104
 tc211
 indexedtypes/should_compile/T4120
 simpl017
 Many tests in `boxy/` (see also #1330 for Church2)
 #2193
 #2846
 #4347
 [Lennart's blog post](http://augustss.blogspot.com/2011/07/impredicativepolymorphismusecasein.html) has an interesting use case of impredicative polymorphism; it worked in 7.0, but alas not in the new typechecker.8.0.1Simon Peyton JonesSimon Peyton Joneshttps://gitlab.haskell.org/ghc/ghc//issues/1330Impredicativity bug: Church2 test gives a rather confusing error with the HEAD20200917T08:22:01ZIan Lynagh <igloo@earth.li>Impredicativity bug: Church2 test gives a rather confusing error with the HEADThe Church2 test gives a rather confusing error with the HEAD:
```
Church2.hs:27:14:
Couldn't match expected type `CNat'
against inferred type `(a > a) > a > a'
Expected type: CNat > CNat
Inferred type: CNat > CNat
In the first argument of `n', namely `(mul m)'
In the expression: n (mul m) n1
```
In particular the lines
```
Expected type: CNat > CNat
Inferred type: CNat > CNat
```
are confusing, and I'm not sure why it's giving two expected/inferred pairs of types.
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  6.7 
 Type  Bug 
 TypeOfFailure  OtherFailure 
 Priority  normal 
 Resolution  Unresolved 
 Component  Compiler (Type checker) 
 Test case  
 Differential revisions  
 BlockedBy  
 Related  
 Blocking  
 CC  
 Operating system  Unknown 
 Architecture  Unknown 
</details>
<! {"blocked_by":[],"summary":"Church2 test gives a rather confusing error with the HEAD","status":"New","operating_system":"Unknown","component":"Compiler (Type checker)","related":[],"milestone":"6.8 branch","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"6.7","keywords":[],"differentials":[],"test_case":"","architecture":"Unknown","cc":[""],"type":"Bug","description":"The Church2 test gives a rather confusing error with the HEAD:\r\n{{{\r\nChurch2.hs:27:14:\r\n Couldn't match expected type `CNat'\r\n against inferred type `(a > a) > a > a'\r\n Expected type: CNat > CNat\r\n Inferred type: CNat > CNat\r\n In the first argument of `n', namely `(mul m)'\r\n In the expression: n (mul m) n1\r\n}}}\r\nIn particular the lines\r\n{{{\r\n Expected type: CNat > CNat\r\n Inferred type: CNat > CNat\r\n}}}\r\nare confusing, and I'm not sure why it's giving two expected/inferred pairs of types.","type_of_failure":"OtherFailure","blocking":[]} >The Church2 test gives a rather confusing error with the HEAD:
```
Church2.hs:27:14:
Couldn't match expected type `CNat'
against inferred type `(a > a) > a > a'
Expected type: CNat > CNat
Inferred type: CNat > CNat
In the first argument of `n', namely `(mul m)'
In the expression: n (mul m) n1
```
In particular the lines
```
Expected type: CNat > CNat
Inferred type: CNat > CNat
```
are confusing, and I'm not sure why it's giving two expected/inferred pairs of types.
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  6.7 
 Type  Bug 
 TypeOfFailure  OtherFailure 
 Priority  normal 
 Resolution  Unresolved 
 Component  Compiler (Type checker) 
 Test case  
 Differential revisions  
 BlockedBy  
 Related  
 Blocking  
 CC  
 Operating system  Unknown 
 Architecture  Unknown 
</details>
<! {"blocked_by":[],"summary":"Church2 test gives a rather confusing error with the HEAD","status":"New","operating_system":"Unknown","component":"Compiler (Type checker)","related":[],"milestone":"6.8 branch","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"6.7","keywords":[],"differentials":[],"test_case":"","architecture":"Unknown","cc":[""],"type":"Bug","description":"The Church2 test gives a rather confusing error with the HEAD:\r\n{{{\r\nChurch2.hs:27:14:\r\n Couldn't match expected type `CNat'\r\n against inferred type `(a > a) > a > a'\r\n Expected type: CNat > CNat\r\n Inferred type: CNat > CNat\r\n In the first argument of `n', namely `(mul m)'\r\n In the expression: n (mul m) n1\r\n}}}\r\nIn particular the lines\r\n{{{\r\n Expected type: CNat > CNat\r\n Inferred type: CNat > CNat\r\n}}}\r\nare confusing, and I'm not sure why it's giving two expected/inferred pairs of types.","type_of_failure":"OtherFailure","blocking":[]} >8.0.1Simon Peyton JonesSimon Peyton Jones