GHC issueshttps://gitlab.haskell.org/ghc/ghc/-/issues2023-08-08T13:08:41Zhttps://gitlab.haskell.org/ghc/ghc/-/issues/23796TemplateHaskell typechecking regression in HEAD2023-08-08T13:08:41ZRyan ScottTemplateHaskell typechecking regression in HEAD_(Originally observed in a `head.hackage` CI job [here](https://gitlab.haskell.org/ghc/head.hackage/-/jobs/1632860).)_
The `what4-1.4` Hackage library currently fails to build with GHC HEAD + `head.hackage`. Here is a minimized example ..._(Originally observed in a `head.hackage` CI job [here](https://gitlab.haskell.org/ghc/head.hackage/-/jobs/1632860).)_
The `what4-1.4` Hackage library currently fails to build with GHC HEAD + `head.hackage`. Here is a minimized example of the issue:
```hs
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TemplateHaskell #-}
module Bug where
good :: (forall a. a -> a) -> b -> b
good = \g x -> g x
bad :: (forall a. a -> a) -> b -> b
bad = $([| \g x -> g x |])
```
This compiles with GHC 9.8 and earlier, but fails to typecheck with GHC HEAD at commit b938950d98945f437f1e28b15a0a3629bfe336c2:
```
$ ghc-head Bug.hs
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
Bug.hs:9:8: error: [GHC-83865]
• Couldn't match type: b -> b
with: forall a. a -> a
Expected: (forall a. a -> a) -> b -> b
Actual: (b -> b) -> b -> b
• In the expression: \ g_a24j x_a24k -> g_a24j x_a24k
In an equation for ‘bad’: bad = (\ g_a24j x_a24k -> g_a24j x_a24k)
• Relevant bindings include
bad :: (forall a. a -> a) -> b -> b (bound at Bug.hs:9:1)
|
9 | bad = $([| \g x -> g x |])
| ^^^^^^^^^^^^^^^^^^^
```
I think both of these should be accepted, as the only difference between `good` and `bad` is the presence of a Template Haskell splice.
While I haven't had time to bisect the issue just yet, my first hunch is to suspect commit !10911 (`Look through TH splices in splitHsApps`).9.10.1https://gitlab.haskell.org/ghc/ghc/-/issues/23692ApplicativeDo breaks typechecking2023-07-25T14:22:12ZSergey VinokurovApplicativeDo breaks typechecking## Summary
When enabling the `ApplicativeDo` extension the provided program ceases to typecheck. It does work in 9.4.5 and does work if I move `putStrLn` around or remove it entirely, which is surprising. Removing `ApplicativeDo` extens...## Summary
When enabling the `ApplicativeDo` extension the provided program ceases to typecheck. It does work in 9.4.5 and does work if I move `putStrLn` around or remove it entirely, which is surprising. Removing `ApplicativeDo` extension also helps but I'd like to get its effects in `parseCommandLine` function (omitted here for brevity).
## Steps to reproduce
Compile the following program.
Original program:
```haskell
{-# LANGUAGE ApplicativeDo #-}
module Main (main) where
import Control.Monad
data Command
= PolyCmd
| VanillaCmd
data CommonConfig = CommonConfig
{ ccVerbose :: Bool
}
parseCommandline :: IO (CommonConfig, Command)
parseCommandline = undefined
locateHelper :: FilePath -> IO (Maybe FilePath)
locateHelper = undefined
complexWrapper :: IO a -> IO a
complexWrapper = undefined
vanillaRun :: IO ()
vanillaRun = pure ()
polyRun :: (forall a. IO a -> IO a) -> IO ()
polyRun f = f $ pure ()
main :: IO ()
main = do
(config, cmd) <- parseCommandline
when (ccVerbose config) $
putStrLn "OK"
let wrapper :: IO a -> IO a
wrapper act = do
complexWrapper act
case cmd of
VanillaCmd -> wrapper vanillaRun
PolyCmd -> polyRun wrapper
```
```
$ ghc -c Main.hs
Main.hs:42:27: error: [GHC-25897]
• Couldn't match type ‘a’ with ‘()’
Expected: IO a -> IO a
Actual: IO () -> IO ()
‘a’ is a rigid type variable bound by
a type expected by the context:
forall a. IO a -> IO a
at Main.hs:42:27-33
• In the first argument of ‘polyRun’, namely ‘wrapper’
In the expression: polyRun wrapper
In a case alternative: PolyCmd -> polyRun wrapper
|
42 | PolyCmd -> polyRun wrapper
| ^^^^^^^
```
However this one does typecheck
```haskell
{-# LANGUAGE ApplicativeDo #-}
module Main (main) where
import Control.Monad
data Command
= PolyCmd
| VanillaCmd
data CommonConfig = CommonConfig
{ ccVerbose :: Bool
}
parseCommandline :: IO (CommonConfig, Command)
parseCommandline = undefined
locateHelper :: FilePath -> IO (Maybe FilePath)
locateHelper = undefined
complexWrapper :: IO a -> IO a
complexWrapper = undefined
vanillaRun :: IO ()
vanillaRun = pure ()
polyRun :: (forall a. IO a -> IO a) -> IO ()
polyRun f = f $ pure ()
main :: IO ()
main = do
(config, cmd) <- parseCommandline
let wrapper :: IO a -> IO a
wrapper act = do
when (ccVerbose config) $
putStrLn "OK"
complexWrapper act
case cmd of
VanillaCmd -> wrapper vanillaRun
PolyCmd -> polyRun wrapper
```
Commenting out `ApplicativeDo` also makes the original program typecheck.
## Expected behavior
Original program typechecks successfully with `ApplicativeDo` extension enabled.
## Environment
* GHC version used: 9.6.2
Optional:
* Operating System: Linux
* System Architecture: x86_64https://gitlab.haskell.org/ghc/ghc/-/issues/23145Incorrect non-exhaustive pattern match warning with higher rank types2023-05-24T07:01:31ZJaro ReindersIncorrect non-exhaustive pattern match warning with higher rank types## Summary
I was experimenting with some very impredicative types when I got a seemingly redundant warning.
## Steps to reproduce
```haskell
{-# LANGUAGE ImpredicativeTypes #-}
data Freer c0 f a = Pure (c0 a) | forall x. Freer (f x) (...## Summary
I was experimenting with some very impredicative types when I got a seemingly redundant warning.
## Steps to reproduce
```haskell
{-# LANGUAGE ImpredicativeTypes #-}
data Freer c0 f a = Pure (c0 a) | forall x. Freer (f x) (forall c. c x -> Freer c f a)
bind :: (forall c. Freer c f a) -> (forall c. c a -> Freer c f b) -> (forall c. Freer c f b)
bind (Pure x) k = k x
bind (Freer op k) k' = Freer op (kcompose k' k)
kcompose :: (forall c. c y -> Freer c f z) -> (forall c. c x -> Freer c f y) -> (forall c. c x -> Freer c f z)
kcompose k1 k2 x =
case k2 x of
Pure y -> k1 y
Freer op k3 -> Freer op (kcompose k1 k3)
```
This gave me the warning:
```
Pattern match(es) are non-exhaustive
In an equation for ‘bind’:
Patterns of type ‘forall (c :: k -> *). Freer c f a’,
‘forall (c :: k -> *). c a -> Freer c f b’ not matched:
_ _
```
## Expected behavior
I expected no warnings.
## Environment
* GHC version used: 9.4.4https://gitlab.haskell.org/ghc/ghc/-/issues/23067Error when combining ambiguous and higher rank types2023-03-04T09:40:04ZJaro ReindersError when combining ambiguous and higher rank types## Summary
I just encountered this error in my experiments. I don't believe this should be an error.
## Steps to reproduce
```haskell
{-# LANGUAGE AllowAmbiguousTypes #-}
foo :: (forall a. Show a => Int) -> Int
foo f = 10
bar :: for...## Summary
I just encountered this error in my experiments. I don't believe this should be an error.
## Steps to reproduce
```haskell
{-# LANGUAGE AllowAmbiguousTypes #-}
foo :: (forall a. Show a => Int) -> Int
foo f = 10
bar :: forall a. Show a => Int
bar = 5
main = print (foo bar)
```
```
T.hs:9:19: error:
• Could not deduce (Show a0) arising from a use of ‘bar’
from the context: Show a
bound by a type expected by the context:
forall a. Show a => Int
at T.hs:9:19-21
The type variable ‘a0’ is ambiguous
These potential instances exist:
instance Show Ordering -- Defined in ‘GHC.Show’
instance Show a => Show (Maybe a) -- Defined in ‘GHC.Show’
instance Show Integer -- Defined in ‘GHC.Show’
...plus 23 others
...plus 13 instances involving out-of-scope types
(use -fprint-potential-instances to see them all)
• In the first argument of ‘foo’, namely ‘bar’
In the first argument of ‘print’, namely ‘(foo bar)’
In the expression: print (foo bar)
|
9 | main = print (foo bar)
| ^^^
```
It seems GHC tries to instantiate `bar`, while it should just be passed uninstantiated.
## Expected behavior
GHC should accept the program without error.
## Environment
* GHC version used: 9.4.4https://gitlab.haskell.org/ghc/ghc/-/issues/21474Warn on uses of Rank2Types2022-05-04T18:32:45ZBen GamariWarn on uses of Rank2TypesLong ago we deprecated `Rank2Types` in favor of `RankNTypes`. However, strangely, we don't appear to warn in this case. This should be fixed.Long ago we deprecated `Rank2Types` in favor of `RankNTypes`. However, strangely, we don't appear to warn in this case. This should be fixed.Ben GamariBen Gamarihttps://gitlab.haskell.org/ghc/ghc/-/issues/21077GHC 9.2.1 typechecking regression with RankNTypes, TemplateHaskell, and compo...2023-08-04T17:02:49ZRyan ScottGHC 9.2.1 typechecking regression with RankNTypes, TemplateHaskell, and compound expressions_(Originally spun off from https://gitlab.haskell.org/ghc/ghc/-/issues/21038#note_407457)_
The `crux-llvm` library (specifically, [this code](https://github.com/GaloisInc/crucible/blob/e1308319eef8e0fcb55ed04df7eb2e9d5e87aac5/crux-llvm/..._(Originally spun off from https://gitlab.haskell.org/ghc/ghc/-/issues/21038#note_407457)_
The `crux-llvm` library (specifically, [this code](https://github.com/GaloisInc/crucible/blob/e1308319eef8e0fcb55ed04df7eb2e9d5e87aac5/crux-llvm/src/Crux/LLVM/Overrides.hs#L149-L153)) typechecks on GHC 9.0.2 and earlier, but fails to typecheck with GHC 9.2.1. I made an attempt to minimize the issue in #21038, but after trying again with that patch, I discovered that `crux-llvm` _still_ does not typecheck. It turns out that my minimization of the issue was a bit too minimal. Here is an example that better illustrates what is going on:
```hs
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TemplateHaskell #-}
module Bug where
data Foo = MkFoo () (forall a. a -> a)
worksOnAllGHCs1 :: Foo
worksOnAllGHCs1 = MkFoo () (\x -> x)
worksOnAllGHCs2 :: Foo
worksOnAllGHCs2 = MkFoo () $ \x -> x
worksOnAllGHCs42 :: Foo
worksOnAllGHCs42 = (MkFoo ()) $ \x -> x
doesn'tWorkOnGHC9'2 :: Foo
doesn'tWorkOnGHC9'2 = $([| MkFoo () |]) $ \x -> x
```
As the names suggest, all of the things functions will typecheck on GHC 9.0.2 and earlier. The `worksOnAllGHCs{1,2,3}` functions will typecheck on GHC 9.2.1, but `doesn'tWorkOnGHC9'2` will not:
```
$ ghc-9.2.1 Bug.hs
[1 of 1] Compiling Bug ( Bug.hs, Bug.o, Bug.dyn_o )
Bug.hs:17:24: error:
• Couldn't match type: forall a. a -> a
with: p0 -> p0
Expected: (p0 -> p0) -> Foo
Actual: (forall a. a -> a) -> Foo
• In the first argument of ‘($)’, namely ‘(MkFoo ())’
In the expression: (MkFoo ()) $ \ x -> x
In an equation for ‘doesn'tWorkOnGHC9'2’:
doesn'tWorkOnGHC9'2 = (MkFoo ()) $ \ x -> x
|
17 | doesn'tWorkOnGHC9'2 = $([| MkFoo () |]) $ \x -> x
| ^^^^^^^^^^^^^^^^
```
The commit which introduced this regression is 9632f413dc90f39bc64586c064805f515a672ca0 (`Implement Quick Look impredicativity`).
Note that unlike the example in #21038, the expression being spliced isn't a simple identifier (i.e., a "head", to use Quick Look terminology), but rather a compound expression. @simonpj suggests [the following fix](https://gitlab.haskell.org/ghc/ghc/-/issues/21038#note_407705):
> Ah yes. Hmm. Reflecting on this, I think the Right Thing is *to treat a splice that is run in the renamer (i.e. an untyped TH splice) as using the "HsExpansion" mechanism*. See `Note [Handling overloaded and rebindable constructs]` in GHC.Tc.Rename.Expr.
>
> That is, the splice `$(expr)` turns into `HsExpanded $(expr) <result-of-running-splice>`. After all, it really *is* an expansion! Then the stuff in the type checker will deal smoothly with application chains. See `Note [Looking through HsExpanded]` in GHC.Tc.Gen.Head.
>
> In principle that should be pretty easy. But `Note [Delaying modFinalizers in untyped splices]` in GHC.Rename.Splice is a painful wart that will hurt us here.
>
> * Where might we store these modFinalizdrs in the HsExpanded? Maybe in the first (original expression) field?
> * Actually I think I favour separating them out entirely into a new extension constructor for `HsExpr GhcRn`. Currenlty we have
>
> ```
> type instance XXExpr GhcRn = HsExpansion (HsExpr GhcRn) (HsExpr GhcRn)
> type instance XXExpr GhcTc = XXExprGhcTc
> ```
>
> We could instead have
>
> ```
> type instance XXExpr GhcRn = XXExprGhcRn
>
> data XXExprGhcRn = ExpansionRn (HsExpansion (HsExpr GhcRn) (HsExpr GhcRn))
> | AddModFinalizedrs ThModFinalizers (HsExpr GhcRn)
> ```
>
> In exchange we can get rid of `HsSpliced` altogether.
> * We still need to call `addModFinalizersWithLclEnv` on those finalisers; so it looks as if we'd need to make `splitHsApps` monadic. That's a pain, but not actually difficult.
>
> I'm not certain of this. But *something* along these lines seems like the right solution.Ryan ScottRyan Scotthttps://gitlab.haskell.org/ghc/ghc/-/issues/21038GHC 9.2.1 typechecking regression with RankNTypes and TemplateHaskell2022-02-14T13:59:23ZRyan ScottGHC 9.2.1 typechecking regression with RankNTypes and TemplateHaskellWhile porting some code over to use GHC 9.2.1, I noticed a typechecking regression that doesn't appear to be explained in the 9.2.1 release notes. Here is a minimal example:
```hs
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TemplateHaskell...While porting some code over to use GHC 9.2.1, I noticed a typechecking regression that doesn't appear to be explained in the 9.2.1 release notes. Here is a minimal example:
```hs
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TemplateHaskell #-}
module Bug where
data Foo = MkFoo (forall a. a -> a)
worksOnAllGHCs1 :: Foo
worksOnAllGHCs1 = MkFoo (\x -> x)
worksOnAllGHCs2 :: Foo
worksOnAllGHCs2 = MkFoo $ \x -> x
worksOnAllGHCs3 :: Foo
worksOnAllGHCs3 = $([| MkFoo |]) (\x -> x)
doesn'tWorkOnGHC9'2 :: Foo
doesn'tWorkOnGHC9'2 = $([| MkFoo |]) $ \x -> x
```
All four of these top-level functions will typecheck on GHC 9.0.2 and earlier. On GHC 9.2.1 and HEAD, `worksOnAllGHCs{1,2,3}` functions will typecheck, but the `doesn'tWorkOnGHC9'2` function will not typecheck:
```
$ ghc-9.2.1 Bug.hs
[1 of 1] Compiling Bug ( Bug.hs, Bug.o, Bug.dyn_o )
Bug.hs:17:24: error:
• Couldn't match type: forall a. a -> a
with: p0 -> p0
Expected: (p0 -> p0) -> Foo
Actual: (forall a. a -> a) -> Foo
• In the first argument of ‘($)’, namely ‘(MkFoo)’
In the expression: (MkFoo) $ \ x -> x
In an equation for ‘doesn'tWorkOnGHC9'2’:
doesn'tWorkOnGHC9'2 = (MkFoo) $ \ x -> x
|
17 | doesn'tWorkOnGHC9'2 = $([| MkFoo |]) $ \x -> x
| ^^^^^^^^^^^^^
```
I'm unclear why using a Template Haskell splice would affect typechecking like this, so I believe this is a bug.9.2.2Ryan ScottRyan Scotthttps://gitlab.haskell.org/ghc/ghc/-/issues/20737Warn when an equality constraint comes into scope without -XMonoLocalBinds2021-11-27T14:04:12ZRichard Eisenbergrae@richarde.devWarn when an equality constraint comes into scope without -XMonoLocalBindsAs imagined in https://gitlab.haskell.org/ghc/ghc/-/issues/20485#note_393506, we might have an equality given come into scope even without a pattern match:
```haskell
{-# LANGUAGE TypeFamilies, RankNTypes #-}
module A where
higher :: fo...As imagined in https://gitlab.haskell.org/ghc/ghc/-/issues/20485#note_393506, we might have an equality given come into scope even without a pattern match:
```haskell
{-# LANGUAGE TypeFamilies, RankNTypes #-}
module A where
higher :: forall a. (forall b. (a ~ F b) => ...) -> ...
```
```haskell
import A
x = higher (\ ... -> ...)
```
The lambda argument to `higher` has an equality given in scope without `MonoLocalBinds`. This should produce the warning introduced by !7042.https://gitlab.haskell.org/ghc/ghc/-/issues/19140panic: No skolem info when trying to use variable with polymorphic kind as Ty...2020-12-31T13:44:07ZJakob Brünkerpanic: No skolem info when trying to use variable with polymorphic kind as Type/Constraint## Summary
In a quantified constraint in the context for an instance declaration, when trying to use a type variable with a polymorphic kind as either a `Type` or a `Constraint`, ghc will panic.
## Steps to reproduce
Each of the follo...## Summary
In a quantified constraint in the context for an instance declaration, when trying to use a type variable with a polymorphic kind as either a `Type` or a `Constraint`, ghc will panic.
## Steps to reproduce
Each of the following three instances trigger the error
```haskell
{-# LANGUAGE ExplicitForAll , PolyKinds #-}
instance (forall (a :: k) . a) => Show b
instance (forall (a :: k) . Show a) => Show b
instance (forall (a :: k) . a -> a) => Show b
```
Error:
```
ghc: panic! (the 'impossible' happened)
(GHC version 9.0.0.20201227:
No skolem info:
[k_aEZ[sk:1]]
Call stack:
CallStack (from HasCallStack):
callStackDoc, called at compiler/GHC/Utils/Outputable.hs:1230:37 in ghc:GHC.Utils.Outputable
pprPanic, called at compiler/GHC/Tc/Errors.hs:2810:17 in ghc:GHC.Tc.Errors
```
## Expected behavior
8.10 has the expected behavior: show the following type error
```
Bug.hs:3:29: error:
• Expected a constraint, but ‘a’ has kind ‘k’
• In the instance declaration for ‘Show b’
|
3 | instance (forall (a :: k) . a) => Show b
| ^
Bug.hs:4:34: error:
• Expected a type, but ‘a’ has kind ‘k’
• In the first argument of ‘Show’, namely ‘a’
In the instance declaration for ‘Show b’
|
4 | instance (forall (a :: k) . Show a) => Show b
| ^
Bug.hs:5:29: error:
• Expected a constraint, but ‘a -> a’ has kind ‘*’
• In the instance declaration for ‘Show b’
|
5 | instance (forall (a :: k) . a -> a) => Show b
| ^^^^^^
Failed, no modules loaded.
```
## Environment
* GHC version used: 9.0.0.20201227
Optional:
* Operating System: Ubuntu inside WSL2 inside Windows 10
* System Architecture: x86_649.2.1https://gitlab.haskell.org/ghc/ghc/-/issues/18855GHC 9.0+ regression in checking program with higher-rank kinds2020-12-15T21:46:27ZRyan ScottGHC 9.0+ regression in checking program with higher-rank kindsGHC 8.10.2 typechecks the following program:
```hs
{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE StandaloneKindSignatures #-}
{...GHC 8.10.2 typechecks the following program:
```hs
{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE StandaloneKindSignatures #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
module Bug where
import Data.Kind
type TyFun :: Type -> Type -> Type
data TyFun a b
type (~>) :: Type -> Type -> Type
type a ~> b = TyFun a b -> Type
infixr 0 ~>
type Apply :: (a ~> b) -> a -> b
type family Apply f x
type Nat :: Type
data Nat = Z | S Nat
type Vec :: Type -> Nat -> Type
data Vec :: Type -> Nat -> Type where
VNil :: Vec a Z
VCons :: a -> Vec a n -> Vec a (S n)
type ElimVec :: forall a.
forall (p :: forall (k :: Nat). Vec a k ~> Type)
-> forall (n :: Nat).
forall (v :: Vec a n)
-> Apply p VNil
-> (forall (m :: Nat).
forall (x :: a) (xs :: Vec a m) ->
Apply p xs ~> Apply p (VCons x xs))
-> Apply p v
type family ElimVec p v pVNil pVCons where
forall a (p :: forall (k :: Nat). Vec a k ~> Type)
(pVNil :: Apply p VNil)
(pVCons :: forall (m :: Nat).
forall (x :: a) (xs :: Vec a m) ->
Apply p xs ~> Apply p (VCons x xs)).
ElimVec p VNil pVNil pVCons = pVNil
forall a (p :: forall (k :: Nat). Vec a k ~> Type)
(pVNil :: Apply p VNil)
(pVCons :: forall (m :: Nat).
forall (x :: a) (xs :: Vec a m) ->
Apply p xs ~> Apply p (VCons x xs)) l x xs.
ElimVec p (VCons x (xs :: Vec a l)) pVNil pVCons =
Apply (pVCons x xs) (ElimVec @a p @l xs pVNil pVCons)
```
However, GHC 9.0.1-alpha1 and HEAD reject it:
```
$ ~/Software/ghc-9.0.1-alpha1/bin/ghc Bug.hs
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
Bug.hs:40:26: error:
• Couldn't match kind ‘k1’ with ‘m’
Expected kind ‘Vec a k1’, but ‘xs’ has kind ‘Vec a m’
because kind variable ‘m’ would escape its scope
This (rigid, skolem) kind variable is bound by
‘forall (m :: Nat).
forall (x :: a) (xs :: Vec a m) ->
Apply p xs ~> Apply p (VCons x xs)’
at Bug.hs:(38,18)-(40,51)
• In the second argument of ‘Apply’, namely ‘xs’
In the first argument of ‘(~>)’, namely ‘Apply p xs’
In a standalone kind signature for ‘ElimVec’:
forall a.
forall (p :: forall (k :: Nat). Vec a k ~> Type) ->
forall (n :: Nat).
forall (v :: Vec a n) ->
Apply p VNil
-> (forall (m :: Nat).
forall (x :: a) (xs :: Vec a m) ->
Apply p xs ~> Apply p (VCons x xs))
-> Apply p v
|
40 | Apply p xs ~> Apply p (VCons x xs))
| ^^
Bug.hs:41:25: error:
• Couldn't match kind ‘k0’ with ‘n’
Expected kind ‘Vec a k0’, but ‘v’ has kind ‘Vec a n’
because kind variable ‘n’ would escape its scope
This (rigid, skolem) kind variable is bound by
‘forall (n :: Nat).
forall (v :: Vec a n) ->
Apply p VNil
-> (forall (m :: Nat).
forall (x :: a) (xs :: Vec a m) ->
Apply p xs ~> Apply p (VCons x xs))
-> Apply p v’
at Bug.hs:(35,17)-(41,25)
• In the second argument of ‘Apply’, namely ‘v’
In a standalone kind signature for ‘ElimVec’:
forall a.
forall (p :: forall (k :: Nat). Vec a k ~> Type) ->
forall (n :: Nat).
forall (v :: Vec a n) ->
Apply p VNil
-> (forall (m :: Nat).
forall (x :: a) (xs :: Vec a m) ->
Apply p xs ~> Apply p (VCons x xs))
-> Apply p v
|
41 | -> Apply p v
| ^
```9.0.1https://gitlab.haskell.org/ghc/ghc/-/issues/18455SPECIALISE instance pragmas allow nested `forall`s/contexts2020-09-21T16:34:56ZRyan ScottSPECIALISE instance pragmas allow nested `forall`s/contextsGHC rejects nested `forall`s and contexts in instance declarations, like so:
```hs
class C a
instance forall a. forall b. C (Either a b)
```
```
Bug.hs:6:20: error:
Instance head cannot contain nested ‘forall’s or contexts
In a...GHC rejects nested `forall`s and contexts in instance declarations, like so:
```hs
class C a
instance forall a. forall b. C (Either a b)
```
```
Bug.hs:6:20: error:
Instance head cannot contain nested ‘forall’s or contexts
In an instance declaration
|
6 | instance forall a. forall b. C (Either a b)
| ^^^^^^^^^^^^^^^^^^^^^^^^
```
However, GHC permits nested `forall`s in `SPECIALISE instance` pragmas, like in the following example:
```hs
instance C (Either a b) where
{-# SPECIALISE instance forall a. forall b. C (Either a b) #-}
```
This seems inconsistent. If we reject nested `forall`s in the former, we should reject them in the latter as well.9.0.1https://gitlab.haskell.org/ghc/ghc/-/issues/18432Inferred type variable check is defeated by nested foralls2020-10-31T06:53:59ZRyan ScottInferred type variable check is defeated by nested forallsGHC HEAD will reject the following program:
```hs
{-# LANGUAGE DefaultSignatures #-}
{-# LANGUAGE RankNTypes #-}
module Bug where
class C a where
m :: forall b. forall c. a -> b -> c -> c
default m :: forall {b}. forall c...GHC HEAD will reject the following program:
```hs
{-# LANGUAGE DefaultSignatures #-}
{-# LANGUAGE RankNTypes #-}
module Bug where
class C a where
m :: forall b. forall c. a -> b -> c -> c
default m :: forall {b}. forall c. a -> b -> c -> c
m _ _ = id
```
```
$ ~/Software/ghc5/inplace/bin/ghc-stage2 Bug.hs
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
Bug.hs:7:3: error:
A default type signature cannot contain inferred type variables
In a class method signature for ‘m’
|
7 | default m :: forall {b}. forall c. a -> b -> c -> c
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
```
However, a simple change to the default signature will evade this check and cause the program to typecheck successfully:
```hs
default m :: forall b. forall {c}. a -> b -> c -> c
```
This seems inconsistent to me.9.0.1https://gitlab.haskell.org/ghc/ghc/-/issues/18412Monotype check for case branches should not recur through arrows2020-07-20T07:57:36ZRichard Eisenbergrae@richarde.devMonotype check for case branches should not recur through arrowsConsider this module:
```hs
{-# LANGUAGE RankNTypes #-}
module Bug where
hr :: (forall a. a -> a) -> ()
hr _ = ()
foo x = case x of () -> hr
bar x = case x of True -> hr
False -> hr
```
On HEAD, `foo` is accepted ...Consider this module:
```hs
{-# LANGUAGE RankNTypes #-}
module Bug where
hr :: (forall a. a -> a) -> ()
hr _ = ()
foo x = case x of () -> hr
bar x = case x of True -> hr
False -> hr
```
On HEAD, `foo` is accepted while `bar` is rejected. (This is not a change from previous behavior.) The reason is that GHC requires `case` branches (when there are more than 1; and when the result of the `case` is being inferred, not checked) to have monotypes, lest it be left with the task of finding the most general supertype of a bunch of polytypes. However, now that we have simplified subsumption, it is draconian to propagate the monotype check past arrows. I thus claim that `bar` should be accepted.https://gitlab.haskell.org/ghc/ghc/-/issues/18191GADT constructors and the forall-or-nothing rule2020-06-24T19:10:55ZRyan ScottGADT constructors and the forall-or-nothing ruleTypes that adhere to the `forall`-or-nothing rule must explicitly bind all of their type variables if there is an outermost `forall`. The converse is that if the type lacks an outermost `forall`, then any type variables that are not expl...Types that adhere to the `forall`-or-nothing rule must explicitly bind all of their type variables if there is an outermost `forall`. The converse is that if the type lacks an outermost `forall`, then any type variables that are not explicitly bound become implicitly quantified. Here is an example of the converse in action:
```hs
f :: (forall a. a -> b -> a)
f x _ = x
```
Because of the outermost parentheses, the type signature for `f` lacks an outer `forall`. As a result, the `b` is implicitly quantified. It's as if you had written `forall b. (forall a. a -> b -> a)`.
GADT constructors allegedly adhere to the `forall`-or-nothing rule, but they have strange behavior _vis-à-vis_ types that begin with outermost parentheses. Consider this example:
```hs
data T where
MkT :: (forall a. a -> b -> T)
```
Should this be rejected? Because of the outermost parentheses, `(forall a. a -> b -> T)` is effectively equivalent to `forall b. (forall a. a -> b -> T)`. Moreover, since GADT constructors [do not allow nested `forall`s](https://gitlab.haskell.org/ghc/ghc/commit/039fa1b994a8b0d6be25eb1bc711904db9661db2), it would be reasonable to expect this to be rejected with a "`GADT constructor type signature cannot contain nested ‘forall’s or contexts`" error.
As it turns out, `MkT` _is_ rejected, but for all the wrong reasons. Here is the actual error that you get:
```
error: Not in scope: type variable ‘b’
|
6 | MkT :: (forall a. a -> b -> T)
| ^
```
For some reason, `b` is not in scope, even though the `forall`-or-nothing rule would dictate that `b` be implicitly quantified. But that's not all. Here is another fishy example:
```hs
data S a where
MkS :: (forall a. S a)
```
Again, the `forall`-or-nothing rule would suggest that `(forall a. S a)` is effectively equivalent to `forall. (forall a. S a)`, and because of the nested `forall`s, GHC ought to reject this. But in reality, GHC _accepts_ this program! (In fact, a user specifically requested that a program like this be accepted in #14320. As the person who authored a fix for that issue, I can only blame myself for my lack of foresight.)
The reason for both of these oddities is quite simple: GHC eagerly strips away parentheses when constructing GADT constructor types in the parser, in [`mkGadtDecl`](https://gitlab.haskell.org/ghc/ghc/-/blob/568d7279a80cf945271f0659f11a94eea3f1433d/compiler/GHC/Parser/PostProcess.hs#L666-701):
```hs
mkGadtDecl names ty
= (ConDeclGADT { con_g_ext = noExtField
, con_names = names
, con_forall = L l $ isLHsForAllTy ty'
, con_qvars = mkHsQTvs tvs
, con_mb_cxt = mcxt
, con_args = args
, con_res_ty = res_ty
, con_doc = Nothing }
, anns1 ++ anns2)
where
(ty'@(L l _),anns1) = peel_parens ty []
(tvs, rho) = splitLHsForAllTyInvis ty'
(mcxt, tau, anns2) = split_rho rho []
split_rho (L _ (HsQualTy { hst_ctxt = cxt, hst_body = tau })) ann
= (Just cxt, tau, ann)
split_rho (L l (HsParTy _ ty)) ann
= split_rho ty (ann++mkParensApiAnn l)
split_rho tau ann
= (Nothing, tau, ann)
(args, res_ty) = split_tau tau
-- See Note [GADT abstract syntax] in GHC.Hs.Decls
split_tau (L _ (HsFunTy _ (L loc (HsRecTy _ rf)) res_ty))
= (RecCon (L loc rf), res_ty)
split_tau tau
= (PrefixCon [], tau)
peel_parens (L l (HsParTy _ ty)) ann = peel_parens ty
(ann++mkParensApiAnn l)
peel_parens ty ann = (ty, ann)
```
`peel_parens` looks through parentheses that surround an outer `forall`, and is therefore the main culprit. (`split_rho` also looks through parentheses that surround the context, although this doesn't pertain to the `forall-or-nothing rule directly.)
What should we do here? One option is to keep GHC's current behavior. I'm not a huge fan of this idea, since this means we'd have to maintain something that deviates from the `forall`-or-nothing rule in an unusual way. On the other hand, changing the current behavior would mean breaking the test case from #14320.
Another option is to make GADT constructor types more faithfully implement the `forall`-or-nothing by removing the use of `peel_parens` and replacing `splitLHsForAllTyInvis` with a function that does not look through parentheses. If we do this, however, that raises some further questions, since this would be rejected for having nested `forall`s:
```hs
data S a where
MkS :: (forall a. S a)
```
But this would not be rejected for having nested contexts:
```hs
data U a where
MkU :: (Show a => U a)
```
Which is a bit odd. We could further clamp down by changing `mkGadtDecl` so that `split_rho` does not look through parentheses either. Is this a step too far?
I originally noticed this when implementing #16762, but this could be fixed independently of that issue.9.0.1https://gitlab.haskell.org/ghc/ghc/-/issues/18127Impredicativity checking is fooled by a type synonym2020-05-06T10:27:48ZRyan ScottImpredicativity checking is fooled by a type synonymConsider the following functions, which all instantiate `undefined` impredicatively:
```hs
{-# LANGUAGE RankNTypes #-}
module Bug where
a :: (forall a. a) -> ()
a = undefined
b :: (Show a => a) -> ()
b = undefined
type C = forall a. ...Consider the following functions, which all instantiate `undefined` impredicatively:
```hs
{-# LANGUAGE RankNTypes #-}
module Bug where
a :: (forall a. a) -> ()
a = undefined
b :: (Show a => a) -> ()
b = undefined
type C = forall a. a
c :: C -> ()
c = undefined
type D a = Show a => a
d :: D a -> ()
d = undefined
```
`a`, `b`, and `c` will each fail to typecheck:
```
[1 of 1] Compiling Bug ( Bug.hs, interpreted )
Bug.hs:5:5: error:
• Cannot instantiate unification variable ‘a1’
with a type involving polytypes: (forall a. a) -> ()
GHC doesn't yet support impredicative polymorphism
• In the expression: undefined
In an equation for ‘a’: a = undefined
|
5 | a = undefined
| ^^^^^^^^^
Bug.hs:8:5: error:
• Cannot instantiate unification variable ‘a2’
with a type involving polytypes: (Show a => a) -> ()
GHC doesn't yet support impredicative polymorphism
• In the expression: undefined
In an equation for ‘b’: b = undefined
• Relevant bindings include
b :: (Show a => a) -> () (bound at Bug.hs:8:1)
|
8 | b = undefined
| ^^^^^^^^^
Bug.hs:12:5: error:
• Cannot instantiate unification variable ‘a0’
with a type involving polytypes: C -> ()
GHC doesn't yet support impredicative polymorphism
• In the expression: undefined
In an equation for ‘c’: c = undefined
|
12 | c = undefined
| ^^^^^^^^^
```
Curiously, there is no error message for `d`. In fact, if you comment out `a`, `b`, and `c`, then `d` will typecheck! This is concerning, as `d` is just a variant of `b` with an extra type synonym thrown into the mix.
Why is it that `c`, which also uses a type synonym, is rejected, but `d` is accepted? It's ultimately because of [`GHC.Tc.Utils.Unify.preCheck`](https://gitlab.haskell.org/ghc/ghc/-/blob/fd7ea0fee92a60f9658254cc4fe3abdb4ff299b1/compiler/GHC/Tc/Utils/Unify.hs#L2233-2298), which powers GHC's impredicative instantiation checks. This part of `preCheck` is suspicious:
```hs
preCheck dflags ty_fam_ok tv ty
= fast_check ty
where
...
fast_check :: TcType -> MetaTyVarUpdateResult ()
...
fast_check (TyConApp tc tys)
| bad_tc tc = MTVU_Bad
| otherwise = mapM fast_check tys >> ok
...
bad_tc :: TyCon -> Bool
bad_tc tc
| not (impredicative_ok || isTauTyCon tc) = True
| not (ty_fam_ok || isFamFreeTyCon tc) = True
| otherwise = False
```
If `bad_tc` returns `True`, then that results in a `TyConApp` being flagged as impredicative. `bad_tc` first checks if `impredicative_ok` is `True` (i.e., if `ImpredicativeTypes` is enabled), and since that isn't the case in the program above, it checks `isTauTyCon tc`. For type synonyms like `C` and `D`, this checks if the RHS of the type synonym is a tau type, as defined by the [`isTauTy`](https://gitlab.haskell.org/ghc/ghc/-/blob/fd7ea0fee92a60f9658254cc4fe3abdb4ff299b1/compiler/GHC/Core/Type.hs#L1860-1870) function:
```hs
-- @isTauTy@ tests if a type has no foralls
isTauTy :: Type -> Bool
isTauTy ty | Just ty' <- coreView ty = isTauTy ty'
isTauTy (TyVarTy _) = True
isTauTy (LitTy {}) = True
isTauTy (TyConApp tc tys) = all isTauTy tys && isTauTyCon tc
isTauTy (AppTy a b) = isTauTy a && isTauTy b
isTauTy (FunTy _ a b) = isTauTy a && isTauTy b
isTauTy (ForAllTy {}) = False
isTauTy (CastTy ty _) = isTauTy ty
isTauTy (CoercionTy _) = False -- Not sure about this
```
However, `isTauTy` only checks if a type contains `forall`s, not contexts! As a result, `C` is flagged as impredicative, but `D a` is not.
I wonder if the definition of `isTauTy` should be expanded to detect higher-rank contexts in addition to higher-rank `forall`s? In other words, should the following change be applied?
```diff
diff --git a/compiler/GHC/Core/Type.hs b/compiler/GHC/Core/Type.hs
index 1e7af2d8cf..3cf4231480 100644
--- a/compiler/GHC/Core/Type.hs
+++ b/compiler/GHC/Core/Type.hs
@@ -1864,6 +1864,7 @@ isTauTy (TyVarTy _) = True
isTauTy (LitTy {}) = True
isTauTy (TyConApp tc tys) = all isTauTy tys && isTauTyCon tc
isTauTy (AppTy a b) = isTauTy a && isTauTy b
+isTauTy (FunTy InvisArg _ _) = False
isTauTy (FunTy _ a b) = isTauTy a && isTauTy b
isTauTy (ForAllTy {}) = False
isTauTy (CastTy ty _) = isTauTy ty
```
This change suffices to make `d` be flagged as impredicative, and it passes GHC's test suite to boot. But then again, I'm unclear on the origins of the term "tau type"—perhaps it's permissible for tau types to have higher-rank contexts? If so, this suggests that we'd need to implement a variant of `isTauTy` that checked for both contexts and `forall`s.9.0.1https://gitlab.haskell.org/ghc/ghc/-/issues/18008Regression with PartialTypeSignatures in 8.102020-09-03T16:47:28ZadamRegression with PartialTypeSignatures in 8.10This is a regression in 8.10, the code was fine in 8.8.2.
```haskell
-- Bug.hs
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE PartialTypeSignatures #-}
module Bug where
import Control.Exception
data WrappedException = Wra...This is a regression in 8.10, the code was fine in 8.8.2.
```haskell
-- Bug.hs
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE PartialTypeSignatures #-}
module Bug where
import Control.Exception
data WrappedException = WrappedException
deriving (Show)
fromSomeException :: SomeException -> WrappedException
fromSomeException _ = WrappedException
instance Exception WrappedException
fun :: IO () -> (forall e. (Exception e) => e -> IO ()) -> _ -- If I say IO () here it works
fun someComputation reportException =
try someComputation >>= \x -> case x of
Left someException -> reportException (fromSomeException someException) -- or if I turn on TypeApplications and put @_ as the first argument here
Right _ -> pure ()
```
Problem:
```
$ ghc --version
The Glorious Glasgow Haskell Compilation System, version 8.10.1
$ ghc Bug.hs -fforce-recomp
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
Bug.hs:18:27: error:
• Couldn't match kind ‘Constraint’ with ‘*’
When matching types
WrappedException :: *
Exception e0 :: Constraint
Expected type: WrappedException -> e0 -> IO ()
Actual type: Exception e0 => e0 -> IO ()
• The function ‘reportException’ is applied to one argument,
but its type ‘Exception e0 => e0 -> IO ()’ has none
In the expression:
reportException (fromSomeException someException)
In a case alternative:
Left someException
-> reportException (fromSomeException someException)
|
18 | Left someException -> reportException (fromSomeException someException)
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
```8.10.2https://gitlab.haskell.org/ghc/ghc/-/issues/18005Sufficiently higher-rank record selectors fail to typecheck2020-04-04T14:46:34ZRyan ScottSufficiently higher-rank record selectors fail to typecheckThere are certain situations where record selectors with higher-rank types will fail to typecheck unless the user enables `ImpredicativeTypes`. Here is one example, adapted from https://gitlab.haskell.org/ghc/ghc/-/merge_requests/2600#no...There are certain situations where record selectors with higher-rank types will fail to typecheck unless the user enables `ImpredicativeTypes`. Here is one example, adapted from https://gitlab.haskell.org/ghc/ghc/-/merge_requests/2600#note_257654:
```hs
{-# LANGUAGE RankNTypes #-}
module Bug where
type S = Int -> (forall a. a -> a) -> Int
data T = MkT {unT :: S}
| Dummy
```
This will fail to compile on GHC 8.0.2 or later:
```
$ /opt/ghc/8.10.1/bin/ghc Bug.hs
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
Bug.hs:6:15: error:
• Cannot instantiate unification variable ‘a0’
with a type involving polytypes: Int -> (forall a. a -> a) -> Int
GHC doesn't yet support impredicative polymorphism
• In the expression: Control.Exception.Base.recSelError "unT"#
In a case alternative:
_ -> Control.Exception.Base.recSelError "unT"#
|
6 | data T = MkT {unT :: S}
| ^^^
```
Here is a similar example involving `PatternSynonyms`, adapted from https://gitlab.haskell.org/ghc/ghc/-/merge_requests/2600#note_255078:
```hs
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ViewPatterns #-}
module Bug where
type S = Int -> (forall a. a -> a) -> Int
newtype T = MkT S
unT' :: T -> S
unT' (MkT x) = x
pattern MkT' :: S -> T
pattern MkT' {unT} <- (unT' -> unT)
```
```
$ /opt/ghc/8.10.1/bin/ghc Bug.hs
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
Bug.hs:14:15: error:
• Cannot instantiate unification variable ‘a0’
with a type involving polytypes: Int -> (forall a. a -> a) -> Int
GHC doesn't yet support impredicative polymorphism
• In the expression: Control.Exception.Base.recSelError "unT"#
In a case alternative:
_ -> Control.Exception.Base.recSelError "unT"#
In the declaration for pattern synonym ‘MkT'’
|
14 | pattern MkT' {unT} <- (unT' -> unT)
| ^^^
```
The underlying cause behind both of these failures is the same. GHC generates `HsBinds` for `unT` that look roughly like this:
```hs
unT :: T -> S
unT (MkT x) = x
unT _ = recSelError "unT'"#
```
Note that the type of `recSelError` is `forall r (a :: TYPE r). Addr# -> a`. Therefore, when used in the right-hand side of `unT`, GHC attempts to instantiate `a` with `Int -> (forall a. a -> a) -> Int`. But this requires `ImpredicativeTypes`, so GHC rejects it.
There's no real reason why a user should have to explicitly enable `ImpredicativeTypes` in order to make this program typecheck, however. GHC could just as well generate the following `HsBinds`:
```hs
unT :: T -> S
unT (MkT x) = x
unT _ = recSelError @_ @S "unT"#
```
And then GHC could enable `ImpredicativeTypes` (and `RankNTypes`) internally when typechecking `unT`. This is very similar to a trick that is used in `TcDeriv`—see [`Note [Newtype-deriving instances]`](https://gitlab.haskell.org/ghc/ghc/-/blob/30a63e79c65b023497af4fe2347149382c71829d/compiler/typecheck/TcGenDeriv.hs#L1600-1653).
Fixing this is a prerequisite for #17775, since simplified subsumption makes this bug even more likely to occur than it does currently. See the discussion beginning at https://gitlab.haskell.org/ghc/ghc/-/merge_requests/2600#note_255078.9.0.1https://gitlab.haskell.org/ghc/ghc/-/issues/17923Core Lint error when compiling singletons (HEAD only), possibly due to nested...2020-04-16T15:28:15ZRyan ScottCore Lint error when compiling singletons (HEAD only), possibly due to nested forallsI originally observed this bug in `head.hackage` when compiling the `singletons-2.6` library with GHC HEAD. Minimizing the issue is tricky, and the smallest reproducer I've managed to create is still pretty long. Here it is:
<details>
...I originally observed this bug in `head.hackage` when compiling the `singletons-2.6` library with GHC HEAD. Minimizing the issue is tricky, and the smallest reproducer I've managed to create is still pretty long. Here it is:
<details>
```hs
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilyDependencies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
{-# OPTIONS_GHC -Wall #-}
module Bug where
import Data.Kind
import qualified Data.Text as T
import Data.Text (Text)
import Data.Proxy
import GHC.TypeLits
import Unsafe.Coerce
type SingFunction1 f = forall t. Sing t -> Sing (f `Apply` t)
singFun1 :: forall f. SingFunction1 f -> Sing f
singFun1 f = SLambda f
-- type SingFunction2 f = forall t1 t2. Sing t1 -> Sing t2 -> Sing (f `Apply` t1 `Apply` t2)
type SingFunction2 f = forall t1. Sing t1 -> forall t2. Sing t2 -> Sing (f `Apply` t1 `Apply` t2)
singFun2 :: forall f. SingFunction2 f -> Sing f
singFun2 f = SLambda (\x -> singFun1 (f x))
-- type SingFunction3 f = forall t1 t2 t3. Sing t1 -> Sing t2 -> Sing t3 -> Sing (f `Apply` t1 `Apply` t2 `Apply` t3)
type SingFunction3 f = forall t1. Sing t1 -> forall t2. Sing t2 -> forall t3. Sing t3 -> Sing (f `Apply` t1 `Apply` t2 `Apply` t3)
singFun3 :: forall f. SingFunction3 f -> Sing f
singFun3 f = SLambda (\x -> singFun2 (f x))
type family Sing :: k -> Type
data SomeSing :: Type -> Type where
SomeSing :: Sing (a :: k) -> SomeSing k
data TyFun :: Type -> Type -> Type
type a ~> b = TyFun a b -> Type
infixr 0 ~>
type family Apply (f :: a ~> b) (x :: a) :: b
type SameKind (a :: k) (b :: k) = (() :: Constraint)
class SingKind k where
type Demote k = (r :: Type) | r -> k
fromSing :: Sing (a :: k) -> Demote k
toSing :: Demote k -> SomeSing k
class SingI a where
sing :: Sing a
data SList :: forall a. [a] -> Type where
SNil :: SList '[]
SCons :: Sing x -> Sing xs -> SList (x:xs)
type instance Sing = SList
data SSymbol (n :: Symbol) = KnownSymbol n => SSym
type instance Sing = SSymbol
instance KnownSymbol n => SingI n where
sing = SSym
instance SingKind Symbol where
type Demote Symbol = Text
fromSing (SSym :: Sing n) = T.pack (symbolVal (Proxy :: Proxy n))
toSing s = case someSymbolVal (T.unpack s) of
SomeSymbol (_ :: Proxy n) -> SomeSing (SSym :: Sing n)
newtype SLambda (f :: k1 ~> k2) =
SLambda { applySing :: forall t. Sing t -> Sing (Apply f t) }
type instance Sing = SLambda
type family ((f :: b ~> c) . (g :: a ~> b)) (x :: a) :: c where
(f . g) x = f `Apply` (g `Apply` x)
data (.@#@$) :: (b ~> c) ~> (a ~> b) ~> a ~> c
data (.@#@$$) :: (b ~> c) -> (a ~> b) ~> a ~> c
data (.@#@$$$) :: (b ~> c) -> (a ~> b) -> a ~> c
type instance Apply (.@#@$) f = (.@#@$$) f
type instance Apply ((.@#@$$) f) g = f .@#@$$$ g
type instance Apply (f .@#@$$$ g) x = (f . g) x
(%.) :: Sing f -> Sing g -> Sing x -> Sing ((f . g) x)
(sF %. sG) sX = sF `applySing` (sG `applySing` sX)
class PSemigroup a where
type (x :: a) <> (y :: a) :: a
data (<>@#@$) :: a ~> a ~> a
data (<>@#@$$) :: a -> a ~> a
type instance Apply (<>@#@$) x = (<>@#@$$) x
type instance Apply ((<>@#@$$) x) y = x <> y
class SSemigroup a where
(%<>) :: forall (x :: a) (y :: a). Sing x -> Sing y -> Sing (x <> y)
instance PSemigroup Symbol where
type a <> b = AppendSymbol a b
instance SSemigroup Symbol where
sa %<> sb =
let a = fromSing sa
b = fromSing sb
ex = someSymbolVal $ T.unpack $ a <> b
in case ex of
SomeSymbol (_ :: Proxy ab) -> unsafeCoerce (SSym :: Sing ab)
type family Foldr1 (f :: a ~> a ~> a) (l :: [a]) :: a where
Foldr1 _ '[x] = x
Foldr1 f (x:y:ys) = f `Apply` x `Apply` (Foldr1 f (y:ys))
data Foldr1Sym0 :: (a ~> a ~> a) ~> [a] ~> a
data Foldr1Sym1 :: (a ~> a ~> a) -> [a] ~> a
type instance Apply Foldr1Sym0 f = Foldr1Sym1 f
type instance Apply (Foldr1Sym1 f) l = Foldr1 f l
sFoldr1 :: Sing f -> Sing l -> Sing (Foldr1 f l)
sFoldr1 _ (sX `SCons` SNil) = sX
sFoldr1 sF (sX `SCons` sXs@(_ `SCons` _)) = sF `applySing` sX `applySing` (sFoldr1 sF sXs)
sFoldr1 _ _ = error "empty list"
type family Lambda_6989586621679111672_aqvf ss_aqvc a_6989586621679111668_aqvd t_aqvi t_aqvj where
Lambda_6989586621679111672_aqvf ss_aqvc a_6989586621679111668_aqvd s_aqvg r_aqvh = Apply (Apply (.@#@$) s_aqvg) (Apply (Apply (.@#@$) (Apply ShowCharSym0 ",")) r_aqvh)
type Lambda_6989586621679111672Sym4 ss6989586621679111670 a_69895866216791116686989586621679111671 t6989586621679111676 t6989586621679111677 =
Lambda_6989586621679111672_aqvf ss6989586621679111670 a_69895866216791116686989586621679111671 t6989586621679111676 t6989586621679111677
data Lambda_6989586621679111672Sym3 ss6989586621679111670 a_69895866216791116686989586621679111671 t6989586621679111676 t6989586621679111677
type instance Apply (Lambda_6989586621679111672Sym3 t6989586621679111676 a_69895866216791116686989586621679111671 ss6989586621679111670) t6989586621679111677 = Lambda_6989586621679111672_aqvf t6989586621679111676 a_69895866216791116686989586621679111671 ss6989586621679111670 t6989586621679111677
data Lambda_6989586621679111672Sym2 ss6989586621679111670 a_69895866216791116686989586621679111671 t6989586621679111676
type instance Apply (Lambda_6989586621679111672Sym2 a_69895866216791116686989586621679111671 ss6989586621679111670) t6989586621679111676 = Lambda_6989586621679111672Sym3 a_69895866216791116686989586621679111671 ss6989586621679111670 t6989586621679111676
data Lambda_6989586621679111672Sym1 ss6989586621679111670 a_69895866216791116686989586621679111671
type instance Apply (Lambda_6989586621679111672Sym1 ss6989586621679111670) a_69895866216791116686989586621679111671 = Lambda_6989586621679111672Sym2 ss6989586621679111670 a_69895866216791116686989586621679111671
data Lambda_6989586621679111672Sym0 ss6989586621679111670
type instance Apply Lambda_6989586621679111672Sym0 ss6989586621679111670 = Lambda_6989586621679111672Sym1 ss6989586621679111670
type Show_tupleSym2 (a6989586621679111664 :: [(~>) Symbol Symbol]) (a6989586621679111665 :: Symbol) =
Show_tuple a6989586621679111664 a6989586621679111665
data Show_tupleSym1 (a6989586621679111664 :: [(~>) Symbol Symbol]) :: (~>) Symbol Symbol
type instance Apply (Show_tupleSym1 a6989586621679111664) a6989586621679111665 = Show_tuple a6989586621679111664 a6989586621679111665
data Show_tupleSym0 :: (~>) [(~>) Symbol Symbol] ((~>) Symbol Symbol)
type instance Apply Show_tupleSym0 a6989586621679111664 = Show_tupleSym1 a6989586621679111664
type ShowStringSym2 (a6989586621679111686 :: Symbol) (a6989586621679111687 :: Symbol) =
ShowString a6989586621679111686 a6989586621679111687
data ShowStringSym1 (a6989586621679111686 :: Symbol) :: (~>) Symbol Symbol
type instance Apply (ShowStringSym1 a6989586621679111686) a6989586621679111687 = ShowString a6989586621679111686 a6989586621679111687
data ShowStringSym0 :: (~>) Symbol ((~>) Symbol Symbol)
type instance Apply ShowStringSym0 a6989586621679111686 = ShowStringSym1 a6989586621679111686
type ShowCharSym2 (a6989586621679111696 :: Symbol) (a6989586621679111697 :: Symbol) =
ShowChar a6989586621679111696 a6989586621679111697
data ShowCharSym1 (a6989586621679111696 :: Symbol) :: (~>) Symbol Symbol
type instance Apply (ShowCharSym1 a6989586621679111696) a6989586621679111697 = ShowChar a6989586621679111696 a6989586621679111697
data ShowCharSym0 :: (~>) Symbol ((~>) Symbol Symbol)
type instance Apply ShowCharSym0 a6989586621679111696 = ShowCharSym1 a6989586621679111696
type family Show_tuple (a_aqv6 :: [(~>) Symbol Symbol]) (a_aqv7 :: Symbol) :: Symbol where
Show_tuple ss_aqvc a_6989586621679111668_aqvd = Apply (Apply (Apply (.@#@$) (Apply ShowCharSym0 "(")) (Apply (Apply (.@#@$) (Apply (Apply Foldr1Sym0 (Apply (Apply Lambda_6989586621679111672Sym0 ss_aqvc) a_6989586621679111668_aqvd)) ss_aqvc)) (Apply ShowCharSym0 ")"))) a_6989586621679111668_aqvd
type family ShowString (a_aqvs :: Symbol) (a_aqvt :: Symbol) :: Symbol where
ShowString a_6989586621679111682_aqvw a_6989586621679111684_aqvx = Apply (Apply (<>@#@$) a_6989586621679111682_aqvw) a_6989586621679111684_aqvx
type family ShowChar (a_aqvC :: Symbol) (a_aqvD :: Symbol) :: Symbol where
ShowChar a_6989586621679111692_aqvG a_6989586621679111694_aqvH = Apply (Apply (<>@#@$) a_6989586621679111692_aqvG) a_6989586621679111694_aqvH
sShow_tuple ::
forall (t_aqvI :: [(~>) Symbol Symbol]) (t_aqvJ :: Symbol).
Sing t_aqvI
-> Sing t_aqvJ
-> Sing (Show_tuple t_aqvI t_aqvJ)
sShowString ::
forall (t_aqvM :: Symbol) (t_aqvN :: Symbol).
Sing t_aqvM
-> Sing t_aqvN
-> Sing (ShowString t_aqvM t_aqvN)
sShowChar ::
forall (t_aqvQ :: Symbol) (t_aqvR :: Symbol).
Sing t_aqvQ
-> Sing t_aqvR
-> Sing (ShowChar t_aqvQ t_aqvR)
sShow_tuple
(sSs :: Sing ss_aqvc)
(sA_6989586621679111668 :: Sing a_6989586621679111668_aqvd)
= (applySing
((applySing
((applySing ((singFun3 @(.@#@$)) (%.)))
((applySing ((singFun2 @ShowCharSym0) sShowChar))
(sing :: Sing "("))))
((applySing
((applySing ((singFun3 @(.@#@$)) (%.)))
((applySing
((applySing ((singFun2 @Foldr1Sym0) sFoldr1))
((singFun2
@(Apply (Apply Lambda_6989586621679111672Sym0 ss_aqvc) a_6989586621679111668_aqvd))
(\ sS sR
-> case ((,) sS) sR of {
(,) (_ :: Sing s_aqvg) (_ :: Sing r_aqvh)
-> (applySing ((applySing ((singFun3 @(.@#@$)) (%.))) sS))
((applySing
((applySing ((singFun3 @(.@#@$)) (%.)))
((applySing
((singFun2 @ShowCharSym0) sShowChar))
(sing :: Sing ","))))
sR) }))))
sSs)))
((applySing ((singFun2 @ShowCharSym0) sShowChar))
(sing :: Sing ")")))))
sA_6989586621679111668
sShowString
(sA_6989586621679111682 :: Sing a_6989586621679111682_aqvw)
(sA_6989586621679111684 :: Sing a_6989586621679111684_aqvx)
= (applySing
((applySing ((singFun2 @(<>@#@$)) (%<>))) sA_6989586621679111682))
sA_6989586621679111684
sShowChar
(sA_6989586621679111692 :: Sing a_6989586621679111692_aqvG)
(sA_6989586621679111694 :: Sing a_6989586621679111694_aqvH)
= (applySing
((applySing ((singFun2 @(<>@#@$)) (%<>))) sA_6989586621679111692))
sA_6989586621679111694
instance SingI (ShowStringSym0 :: (~>) Symbol ((~>) Symbol Symbol)) where
sing = (singFun2 @ShowStringSym0) sShowString
```
</details>
This passes Core Lint on GHC 8.8.3 and 8.10.1-rc1, but not on HEAD:
<details>
```
$ ~/Software/ghc5/inplace/bin/ghc-stage2 -dcore-lint Bug.hs -fprint-explicit-kinds
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
*** Core Lint errors : in result of Simplifier ***
Bug.hs:174:34: warning:
Kind application error in type ‘Sing @Symbol t_X5’
Function kind = forall k. k -> *
Arg kinds = [(Symbol, *), (t_X5, Symbol ~> Symbol)]
Fun: Symbol
(t_X5, Symbol ~> Symbol)
In the RHS of sShow_tuple :: forall (t_aqvI :: [Symbol ~> Symbol])
(t_aqvJ :: Symbol).
Sing @[Symbol ~> Symbol] t_aqvI
-> Sing @Symbol t_aqvJ -> Sing @Symbol (Show_tuple t_aqvI t_aqvJ)
In the body of lambda with binder t_aqvI_a29K :: [Symbol ~> Symbol]
In the body of lambda with binder t_aqvJ_a29L :: Symbol
In the body of lambda with binder ds_X1 :: Sing
@[Symbol ~> Symbol] t_aqvI_a29K
In the body of lambda with binder ds_X2 :: Sing @Symbol t_aqvJ_a29L
In the body of letrec with binders x_s2zK :: forall {t :: Symbol}.
Sing @Symbol t -> Sing @Symbol ((<>) @Symbol "(" t)
In the RHS of x_s2zL :: Sing
@(Symbol ~> Symbol)
((.@#@$$$)
@Symbol
@Symbol
@Symbol
(Foldr1
@(TyFun Symbol Symbol -> *)
(Lambda_6989586621679111672Sym2
@{[Symbol ~> Symbol]}
@{Symbol}
@{TyFun
(Symbol ~> Symbol)
((Symbol ~> Symbol) ~> (Symbol ~> Symbol))}
t_aqvI_a29K
t_aqvJ_a29L)
t_aqvI_a29K)
(ShowCharSym1 ")"))
In the RHS of x_s2zI :: Sing
@(TyFun Symbol Symbol -> *)
(Foldr1
@(TyFun Symbol Symbol -> *)
(Lambda_6989586621679111672Sym2
@{[Symbol ~> Symbol]}
@{Symbol}
@{TyFun
(Symbol ~> Symbol)
((Symbol ~> Symbol) ~> (Symbol ~> Symbol))}
t_aqvI_a29K
t_aqvJ_a29L)
t_aqvI_a29K)
In the RHS of x_s2zH :: forall {t :: Symbol ~> Symbol}.
Sing @(Symbol ~> Symbol) t
-> forall {t :: Symbol ~> Symbol}.
Sing @(Symbol ~> Symbol) t
-> Sing
@(Symbol ~> Symbol)
(Apply
@(Symbol ~> Symbol)
@(Symbol ~> Symbol)
(Apply
@(Symbol ~> Symbol)
@(TyFun (Symbol ~> Symbol) (Symbol ~> Symbol) -> *)
(Apply
@Symbol
@(TyFun
(Symbol ~> Symbol)
(TyFun (Symbol ~> Symbol) (Symbol ~> Symbol) -> *)
-> *)
(Apply
@[Symbol ~> Symbol]
@(TyFun
Symbol
((Symbol ~> Symbol)
~> ((Symbol ~> Symbol) ~> (Symbol ~> Symbol)))
-> *)
(Lambda_6989586621679111672Sym0
@{TyFun
[Symbol ~> Symbol]
(TyFun
Symbol
((Symbol ~> Symbol)
~> ((Symbol ~> Symbol)
~> (Symbol ~> Symbol)))
-> *)})
t_aqvI_a29K)
t_aqvJ_a29L)
t)
t)
In the body of lambda with binder t_X3 :: Symbol ~> Symbol
In the body of lambda with binder x_X4 :: Sing
@(Symbol ~> Symbol) t_X3
In the body of lambda with binder t_X5 :: Symbol ~> Symbol
In the body of letrec with binders $dKnownSymbol_s2zD :: [Char]
In the body of letrec with binders $dSingI_s2zE :: SSymbol ","
In the body of lambda with binder sR_aMu :: Sing
@(Symbol ~> Symbol) t_X5
In the RHS of x_s2zG :: Sing
@(Symbol ~> Symbol)
((.@#@$$$) @Symbol @Symbol @Symbol (ShowCharSym1 ",") t_X5)
In the body of letrec with binders x_s2zF :: forall {t :: Symbol}.
Sing @Symbol t -> Sing @Symbol ((<>) @Symbol "," t)
In the type of a binder: x_s2zF
In the type ‘forall {t :: Symbol}.
Sing @Symbol t -> Sing @Symbol ((<>) @Symbol "," t)’
Substitution: [TCvSubst
In scope: InScope {t_X3 t_X5 t_X6 t_aqvI_a29K t_aqvJ_a29L}
Type env: [X5 :-> t_X6]
Co env: []]
Bug.hs:174:34: warning:
Kind application error in type ‘(<>) @Symbol "," t_X5’
Function kind = forall a. a -> a -> a
Arg kinds = [(Symbol, *), (",", Symbol), (t_X5, Symbol ~> Symbol)]
Fun: Symbol
(t_X5, Symbol ~> Symbol)
In the RHS of sShow_tuple :: forall (t_aqvI :: [Symbol ~> Symbol])
(t_aqvJ :: Symbol).
Sing @[Symbol ~> Symbol] t_aqvI
-> Sing @Symbol t_aqvJ -> Sing @Symbol (Show_tuple t_aqvI t_aqvJ)
In the body of lambda with binder t_aqvI_a29K :: [Symbol ~> Symbol]
In the body of lambda with binder t_aqvJ_a29L :: Symbol
In the body of lambda with binder ds_X1 :: Sing
@[Symbol ~> Symbol] t_aqvI_a29K
In the body of lambda with binder ds_X2 :: Sing @Symbol t_aqvJ_a29L
In the body of letrec with binders x_s2zK :: forall {t :: Symbol}.
Sing @Symbol t -> Sing @Symbol ((<>) @Symbol "(" t)
In the RHS of x_s2zL :: Sing
@(Symbol ~> Symbol)
((.@#@$$$)
@Symbol
@Symbol
@Symbol
(Foldr1
@(TyFun Symbol Symbol -> *)
(Lambda_6989586621679111672Sym2
@{[Symbol ~> Symbol]}
@{Symbol}
@{TyFun
(Symbol ~> Symbol)
((Symbol ~> Symbol) ~> (Symbol ~> Symbol))}
t_aqvI_a29K
t_aqvJ_a29L)
t_aqvI_a29K)
(ShowCharSym1 ")"))
In the RHS of x_s2zI :: Sing
@(TyFun Symbol Symbol -> *)
(Foldr1
@(TyFun Symbol Symbol -> *)
(Lambda_6989586621679111672Sym2
@{[Symbol ~> Symbol]}
@{Symbol}
@{TyFun
(Symbol ~> Symbol)
((Symbol ~> Symbol) ~> (Symbol ~> Symbol))}
t_aqvI_a29K
t_aqvJ_a29L)
t_aqvI_a29K)
In the RHS of x_s2zH :: forall {t :: Symbol ~> Symbol}.
Sing @(Symbol ~> Symbol) t
-> forall {t :: Symbol ~> Symbol}.
Sing @(Symbol ~> Symbol) t
-> Sing
@(Symbol ~> Symbol)
(Apply
@(Symbol ~> Symbol)
@(Symbol ~> Symbol)
(Apply
@(Symbol ~> Symbol)
@(TyFun (Symbol ~> Symbol) (Symbol ~> Symbol) -> *)
(Apply
@Symbol
@(TyFun
(Symbol ~> Symbol)
(TyFun (Symbol ~> Symbol) (Symbol ~> Symbol) -> *)
-> *)
(Apply
@[Symbol ~> Symbol]
@(TyFun
Symbol
((Symbol ~> Symbol)
~> ((Symbol ~> Symbol) ~> (Symbol ~> Symbol)))
-> *)
(Lambda_6989586621679111672Sym0
@{TyFun
[Symbol ~> Symbol]
(TyFun
Symbol
((Symbol ~> Symbol)
~> ((Symbol ~> Symbol)
~> (Symbol ~> Symbol)))
-> *)})
t_aqvI_a29K)
t_aqvJ_a29L)
t)
t)
In the body of lambda with binder t_X3 :: Symbol ~> Symbol
In the body of lambda with binder x_X4 :: Sing
@(Symbol ~> Symbol) t_X3
In the body of lambda with binder t_X5 :: Symbol ~> Symbol
In the body of letrec with binders $dKnownSymbol_s2zD :: [Char]
In the body of letrec with binders $dSingI_s2zE :: SSymbol ","
In the body of lambda with binder sR_aMu :: Sing
@(Symbol ~> Symbol) t_X5
In the RHS of x_s2zG :: Sing
@(Symbol ~> Symbol)
((.@#@$$$) @Symbol @Symbol @Symbol (ShowCharSym1 ",") t_X5)
In the body of letrec with binders x_s2zF :: forall {t :: Symbol}.
Sing @Symbol t -> Sing @Symbol ((<>) @Symbol "," t)
In the type of a binder: x_s2zF
In the type ‘forall {t :: Symbol}.
Sing @Symbol t -> Sing @Symbol ((<>) @Symbol "," t)’
Substitution: [TCvSubst
In scope: InScope {t_X3 t_X5 t_X6 t_aqvI_a29K t_aqvJ_a29L}
Type env: [X5 :-> t_X6]
Co env: []]
*** Offending Program ***
<elided>
```
</details>
(The full Core Lint error has been elided due to its sheer length.)
One interesting observation about this program is that the Core Lint error only occurs if `SingFunction2` and `SingFunction3` are defined like so:
```hs
type SingFunction2 f = forall t1. Sing t1 -> forall t2. Sing t2 -> Sing (f `Apply` t1 `Apply` t2)
type SingFunction3 f = forall t1. Sing t1 -> forall t2. Sing t2 -> forall t3. Sing t3 -> Sing (f `Apply` t1 `Apply` t2 `Apply` t3)
```
If they are instead defined without nested `forall`s, like so:
```hs
type SingFunction2 f = forall t1 t2. Sing t1 -> Sing t2 -> Sing (f `Apply` t1 `Apply` t2)
type SingFunction3 f = forall t1 t2 t3. Sing t1 -> Sing t2 -> Sing t3 -> Sing (f `Apply` t1 `Apply` t2 `Apply` t3)
```
Then the Core Lint error does not occur.9.0.1https://gitlab.haskell.org/ghc/ghc/-/issues/17768ApplicativeDo breaks compilation with polymorphic bindings2023-07-25T14:21:43ZKirill Elaginkirelagin@gmail.comApplicativeDo breaks compilation with polymorphic bindings## Summary
A valid code that uses a let binding with an explicit Rank2 type stops compiling when `ApplicativeDo` is enabled.
## Steps to reproduce
```haskell
{-# LANGUAGE ApplicativeDo, Rank2Types #-}
module Test where
type M = fora...## Summary
A valid code that uses a let binding with an explicit Rank2 type stops compiling when `ApplicativeDo` is enabled.
## Steps to reproduce
```haskell
{-# 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:3-4: 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:3-8
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/17213Rank-n-types without -XRankNTypes2020-07-14T17:14:18ZKrzysztof GogolewskiRank-n-types without -XRankNTypesConsider two modules:
```
{-# LANGUAGE RankNTypes #-}
module X where
foo :: (forall a. a -> a) -> Int
foo = foo
```
```
module Y where
import X
g = foo
```
Note that `Y` does not use `RankNTypes`.
Currently, `g` is accepted. However...Consider two modules:
```
{-# LANGUAGE RankNTypes #-}
module X where
foo :: (forall a. a -> a) -> Int
foo = foo
```
```
module Y where
import X
g = foo
```
Note that `Y` does not use `RankNTypes`.
Currently, `g` is accepted. However, the inferred type of `g` is `(forall a. a -> a) -> Int`, which cannot be written. We should not allow a value if writing its type requires an additional extension.
Reporting on behalf of Simon PJ.8.10.1