GHC issueshttps://gitlab.haskell.org/ghc/ghc/-/issues2023-07-25T14:22:12Zhttps://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/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/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/11540ghc accepts non-standard type without language extension2020-06-02T16:30:57Zlennart@augustsson.netghc accepts non-standard type without language extensionGhc accepts this
```
f :: Eq a => Eq b => a -> b -> Bool
f a b = a==a && b==b
```
The nested contexts should require some language extension.
<details><summary>Trac metadata</summary>
| Trac field | Value |
| -----...Ghc accepts this
```
f :: Eq a => Eq b => a -> b -> Bool
f a b = a==a && b==b
```
The nested contexts should require some language extension.
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ------------ |
| Version | 7.8.4 |
| Type | Bug |
| TypeOfFailure | OtherFailure |
| Priority | normal |
| Resolution | Unresolved |
| Component | Compiler |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"ghc accepts non-standard type without language extension","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"7.8.4","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"Ghc accepts this\r\n{{{\r\nf :: Eq a => Eq b => a -> b -> Bool\r\nf a b = a==a && b==b\r\n}}}\r\nThe nested contexts should require some language extension.\r\n","type_of_failure":"OtherFailure","blocking":[]} -->https://gitlab.haskell.org/ghc/ghc/-/issues/8346Rank 1 type signature still requires RankNTypes2020-05-05T12:51:27ZTinctoriusRank 1 type signature still requires RankNTypesWhen trying to figure out which type variable names are \*actually\* bound in `ScopedTypeVariables`, I tried floating `forall`s into the covariant argument of the function type. Essentially, I ran into the problem that programs like the ...When trying to figure out which type variable names are \*actually\* bound in `ScopedTypeVariables`, I tried floating `forall`s into the covariant argument of the function type. Essentially, I ran into the problem that programs like the following are rejected:
```hs
{-# LANGUAGE ExplicitForAll #-}
tuple :: forall a. a -> (forall b. b -> (a, b))
tuple = (,)
```
The message is as follows:
```
Main.hs:2:10:
Illegal polymorphic or qualified type: forall b. b -> (a, b)
Perhaps you intended to use -XRankNTypes or -XRank2Types
In the type signature for `tuple':
tuple :: forall a. a -> (forall b. b -> (a, b))
```
As far as I know, the rank of a type is defined by how deep quantifiers are nested in contravariant parts of that type. Or something like that. Also, as far as I know, `forall a. a -> (forall b. b -> (a, b))` is equivalent to `forall a b. a -> b -> (a, b)`, and more importantly, both are rank-1 polymorphic. There should be no need to use extensions that allow higher-ranked polymorphism.
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ------------ |
| Version | 7.6.3 |
| Type | Bug |
| TypeOfFailure | OtherFailure |
| Priority | normal |
| Resolution | Unresolved |
| Component | Compiler |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"Rank 1 type signature still requires RankNTypes","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"7.6.3","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"When trying to figure out which type variable names are *actually* bound in `ScopedTypeVariables`, I tried floating `forall`s into the covariant argument of the function type. Essentially, I ran into the problem that programs like the following are rejected:\r\n\r\n{{{\r\n#!hs\r\n{-# LANGUAGE ExplicitForAll #-}\r\ntuple :: forall a. a -> (forall b. b -> (a, b))\r\ntuple = (,)\r\n}}}\r\n\r\nThe message is as follows:\r\n{{{\r\nMain.hs:2:10:\r\n Illegal polymorphic or qualified type: forall b. b -> (a, b)\r\n Perhaps you intended to use -XRankNTypes or -XRank2Types\r\n In the type signature for `tuple':\r\n tuple :: forall a. a -> (forall b. b -> (a, b))\r\n}}}\r\n\r\nAs far as I know, the rank of a type is defined by how deep quantifiers are nested in contravariant parts of that type. Or something like that. Also, as far as I know, `forall a. a -> (forall b. b -> (a, b))` is equivalent to `forall a b. a -> b -> (a, b)`, and more importantly, both are rank-1 polymorphic. There should be no need to use extensions that allow higher-ranked polymorphism.","type_of_failure":"OtherFailure","blocking":[]} -->https://gitlab.haskell.org/ghc/ghc/-/issues/10450Poor type error message when an argument is insufficently polymorphic2019-07-07T18:35:52ZsjcjoostenPoor type error message when an argument is insufficently polymorphicWhen pattern matching, "let/where" and "case" have different behaviours.
Currently, this is accepted (a version using 'where' instead of 'let' type-checks too):
```hs
{-# LANGUAGE RankNTypes, ScopedTypeVariables #-}
module Main where
...When pattern matching, "let/where" and "case" have different behaviours.
Currently, this is accepted (a version using 'where' instead of 'let' type-checks too):
```hs
{-# LANGUAGE RankNTypes, ScopedTypeVariables #-}
module Main where
data Phantom x = Phantom Int deriving Show
foo :: forall y. (forall x. (Phantom x)) -> Phantom y
foo (Phantom x) = Phantom (x+1)
-- trying to map foo over a list, this is the only way I can get it to work
typeAnnotatedMap :: (forall x. [Phantom x])
-> [Phantom y]
typeAnnotatedMap intList = case intList of
[] -> []
_ -> let (phead:ptail) = intList
in foo phead : typeAnnotatedMap ptail
```
The following are not accepted:
```hs
typeAnnotatedMap1 :: (forall x. [Phantom x])
-> [Phantom y]
typeAnnotatedMap1 intList = case intList of
[] -> []
(phead:ptail) -> foo phead : typeAnnotatedMap1 ptail
typeAnnotatedMap2 :: (forall x. [Phantom x])
-> [Phantom y]
typeAnnotatedMap2 [] = []
typeAnnotatedMap2 (phead:ptail) = foo phead : typeAnnotatedMap2 ptail
```
The current type error is something like:
```
Couldn't match type ‘x0’ with ‘x’
because type variable ‘x’ would escape its scope
This (rigid, skolem) type variable is bound by
a type expected by the context: [Phantom x]
```
More helpful would be something like:
```
Your pattern match bound the following types to a shared skolem variable:
ptail :: [Phantom x0] (bound at rankNtest.hs:11:25)
phead :: Phantom x0 (bound at rankNtest.hs:11:19)
You may have intended to use a "let" or "where" pattern-match instead.
```