GHC issueshttps://gitlab.haskell.org/ghc/ghc/-/issues2020-01-23T19:20:59Zhttps://gitlab.haskell.org/ghc/ghc/-/issues/15034Desugaring `mdo` moves a `let` where it shouldn't be2020-01-23T19:20:59ZparsonsmattDesugaring `mdo` moves a `let` where it shouldn't beConsider the following program:
```hs
{-# LANGUAGE RecursiveDo #-}
module Main where
a :: String
a = "hello"
test :: IO ()
test = mdo
putStrLn a
let a = 3 :: Int
print a
```
With both GHC 8.2.2 and GHC 8.4...Consider the following program:
```hs
{-# LANGUAGE RecursiveDo #-}
module Main where
a :: String
a = "hello"
test :: IO ()
test = mdo
putStrLn a
let a = 3 :: Int
print a
```
With both GHC 8.2.2 and GHC 8.4.1, it fails with the following error:
```hs
/home/matt/Projects/ghc-repro/src/Main.hs:10:5: error:
• Couldn't match type ‘Int’ with ‘[Char]’
Expected type: String
Actual type: Int
• In a stmt of an 'mdo' block:
rec putStrLn a
let a = (3 :: Int)
In the expression:
mdo rec putStrLn a
let a = ...
print a
In an equation for ‘test’:
test
= mdo rec putStrLn a
let ...
print a
|
10 | putStrLn a
| ^^^^^^^^^^
```
I would expect it to succeed, with `a` shadowing the top-level definition. The desugared output in the error message tells us what is wrong: it is grouping `putStrLn a; let a = ...` together!
If I alter the program to be:
```hs
a :: String
a = "hello"
test :: IO ()
test = do
rec putStrLn a
let a = 3 :: Int
print a
```
Then it does the Right Thing.
Looking at the [Haskell Prime wiki entry for Recursive Do](https://prime.haskell.org/wiki/RecursiveDo), this seems to be the relevant bit:
> That is, a variable used before it is bound is treated as recursively defined, while in a Haskell 98 do-statement it would be treated as shadowed.
I have a more complicated reproduction involving `ST` types and complaints of skolem type variables escaping scope:
```hs
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE RecursiveDo #-}
module Main where
import Control.Monad.ST
theThing :: ST s ()
theThing = pure ()
weirdlyLocal :: ST s ()
weirdlyLocal = theThing
runSTIO :: (forall s. ST s a) -> IO a
runSTIO x = pure (runST x)
thisWorks :: IO ()
thisWorks = mdo
let weirdlyLocal = theThing
runSTIO weirdlyLocal
runSTIO weirdlyLocal
thisBreaks :: IO ()
thisBreaks = mdo
runSTIO weirdlyLocal
let weirdlyLocal = theThing
runSTIO weirdlyLocal
thisIsFine :: IO ()
thisIsFine = mdo
runSTIO weirdlyLocal
let asdf = theThing
runSTIO asdf
```
This demonstrates an even more bizarre behavior! If I move the `let` up to the top, then it no longer gets included in a `rec`, and it compiles fine. If I move it under the first statement, then I get this error:
```hs
/home/matt/Projects/ghc-repro/src/Main.hs:25:13: error:
• Couldn't match type ‘s0’ with ‘s’
because type variable ‘s’ would escape its scope
This (rigid, skolem) type variable is bound by
a type expected by the context:
forall s. ST s ()
at src/Main.hs:25:5-24
Expected type: ST s ()
Actual type: ST s0 ()
• In the first argument of ‘runSTIO’, namely ‘weirdlyLocal’
In a stmt of an 'mdo' block: runSTIO weirdlyLocal
In a stmt of an 'mdo' block:
rec runSTIO weirdlyLocal
let weirdlyLocal = theThing
• Relevant bindings include
weirdlyLocal :: ST s0 () (bound at src/Main.hs:26:9)
|
25 | runSTIO weirdlyLocal
| ^^^^^^^^^^^^
/home/matt/Projects/ghc-repro/src/Main.hs:27:13: error:
• Couldn't match type ‘s0’ with ‘s’
because type variable ‘s’ would escape its scope
This (rigid, skolem) type variable is bound by
a type expected by the context:
forall s. ST s ()
at src/Main.hs:27:5-24
Expected type: ST s ()
Actual type: ST s0 ()
• In the first argument of ‘runSTIO’, namely ‘weirdlyLocal’
In a stmt of an 'mdo' block: runSTIO weirdlyLocal
In the expression:
mdo rec runSTIO weirdlyLocal
let weirdlyLocal = ...
runSTIO weirdlyLocal
• Relevant bindings include
weirdlyLocal :: ST s0 () (bound at src/Main.hs:26:9)
|
27 | runSTIO weirdlyLocal
| ^^^^^^^^^^^^
```
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ------------ |
| Version | 8.2.2 |
| 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":"Desugaring `mdo` moves a `let` where it shouldn't be","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"8.6.1","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.2.2","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"Consider the following program:\r\n\r\n{{{#!hs\r\n{-# LANGUAGE RecursiveDo #-}\r\n\r\nmodule Main where\r\n\r\na :: String\r\na = \"hello\"\r\n\r\ntest :: IO ()\r\ntest = mdo\r\n putStrLn a\r\n let a = 3 :: Int\r\n print a\r\n}}}\r\n\r\nWith both GHC 8.2.2 and GHC 8.4.1, it fails with the following error:\r\n\r\n{{{#!hs\r\n/home/matt/Projects/ghc-repro/src/Main.hs:10:5: error:\r\n • Couldn't match type ‘Int’ with ‘[Char]’\r\n Expected type: String\r\n Actual type: Int\r\n • In a stmt of an 'mdo' block:\r\n rec putStrLn a\r\n let a = (3 :: Int)\r\n In the expression:\r\n mdo rec putStrLn a\r\n let a = ...\r\n print a\r\n In an equation for ‘test’:\r\n test\r\n = mdo rec putStrLn a\r\n let ...\r\n print a\r\n |\r\n10 | putStrLn a\r\n | ^^^^^^^^^^\r\n}}}\r\n\r\nI would expect it to succeed, with `a` shadowing the top-level definition. The desugared output in the error message tells us what is wrong: it is grouping `putStrLn a; let a = ...` together!\r\n\r\nIf I alter the program to be:\r\n\r\n{{{#!hs\r\na :: String\r\na = \"hello\"\r\n\r\ntest :: IO ()\r\ntest = do\r\n rec putStrLn a\r\n let a = 3 :: Int\r\n print a\r\n}}}\r\n\r\nThen it does the Right Thing.\r\n\r\nLooking at the [https://prime.haskell.org/wiki/RecursiveDo Haskell Prime wiki entry for Recursive Do], this seems to be the relevant bit:\r\n\r\n> That is, a variable used before it is bound is treated as recursively defined, while in a Haskell 98 do-statement it would be treated as shadowed.\r\n\r\nI have a more complicated reproduction involving `ST` types and complaints of skolem type variables escaping scope:\r\n\r\n{{{#!hs\r\n{-# LANGUAGE RankNTypes #-}\r\n{-# LANGUAGE RecursiveDo #-}\r\n\r\nmodule Main where\r\n\r\nimport Control.Monad.ST\r\n\r\ntheThing :: ST s ()\r\ntheThing = pure ()\r\n\r\nweirdlyLocal :: ST s ()\r\nweirdlyLocal = theThing\r\n\r\nrunSTIO :: (forall s. ST s a) -> IO a\r\nrunSTIO x = pure (runST x)\r\n\r\nthisWorks :: IO ()\r\nthisWorks = mdo\r\n let weirdlyLocal = theThing\r\n runSTIO weirdlyLocal\r\n runSTIO weirdlyLocal\r\n\r\nthisBreaks :: IO ()\r\nthisBreaks = mdo\r\n runSTIO weirdlyLocal\r\n let weirdlyLocal = theThing\r\n runSTIO weirdlyLocal\r\n\r\nthisIsFine :: IO ()\r\nthisIsFine = mdo\r\n runSTIO weirdlyLocal\r\n let asdf = theThing\r\n runSTIO asdf\r\n}}}\r\n\r\nThis demonstrates an even more bizarre behavior! If I move the `let` up to the top, then it no longer gets included in a `rec`, and it compiles fine. If I move it under the first statement, then I get this error:\r\n\r\n{{{#!hs\r\n/home/matt/Projects/ghc-repro/src/Main.hs:25:13: error:\r\n • Couldn't match type ‘s0’ with ‘s’\r\n because type variable ‘s’ would escape its scope\r\n This (rigid, skolem) type variable is bound by\r\n a type expected by the context:\r\n forall s. ST s ()\r\n at src/Main.hs:25:5-24\r\n Expected type: ST s ()\r\n Actual type: ST s0 ()\r\n • In the first argument of ‘runSTIO’, namely ‘weirdlyLocal’\r\n In a stmt of an 'mdo' block: runSTIO weirdlyLocal\r\n In a stmt of an 'mdo' block:\r\n rec runSTIO weirdlyLocal\r\n let weirdlyLocal = theThing\r\n • Relevant bindings include\r\n weirdlyLocal :: ST s0 () (bound at src/Main.hs:26:9)\r\n |\r\n25 | runSTIO weirdlyLocal\r\n | ^^^^^^^^^^^^\r\n\r\n/home/matt/Projects/ghc-repro/src/Main.hs:27:13: error:\r\n • Couldn't match type ‘s0’ with ‘s’\r\n because type variable ‘s’ would escape its scope\r\n This (rigid, skolem) type variable is bound by\r\n a type expected by the context:\r\n forall s. ST s ()\r\n at src/Main.hs:27:5-24\r\n Expected type: ST s ()\r\n Actual type: ST s0 ()\r\n • In the first argument of ‘runSTIO’, namely ‘weirdlyLocal’\r\n In a stmt of an 'mdo' block: runSTIO weirdlyLocal\r\n In the expression:\r\n mdo rec runSTIO weirdlyLocal\r\n let weirdlyLocal = ...\r\n runSTIO weirdlyLocal\r\n • Relevant bindings include\r\n weirdlyLocal :: ST s0 () (bound at src/Main.hs:26:9)\r\n |\r\n27 | runSTIO weirdlyLocal\r\n | ^^^^^^^^^^^^\r\n}}}\r\n\r\n","type_of_failure":"OtherFailure","blocking":[]} -->https://gitlab.haskell.org/ghc/ghc/-/issues/11117mdo blocks in error messages are shown modified2019-07-07T18:31:53ZJoachim Breitnermail@joachim-breitner.demdo blocks in error messages are shown modified```hs
{-# LANGUAGE RecursiveDo #-}
main = mdo
Just x <- return (Right x)
return ()
```
gives
```
MdoTypeError.hs:3:3:
Couldn't match expected type ‘Either a0 b0’
with actual type ‘Maybe b0’
Relevant bindings...```hs
{-# LANGUAGE RecursiveDo #-}
main = mdo
Just x <- return (Right x)
return ()
```
gives
```
MdoTypeError.hs:3:3:
Couldn't match expected type ‘Either a0 b0’
with actual type ‘Maybe b0’
Relevant bindings include x :: b0 (bound at MdoTypeError.hs:3:8)
In the pattern: Just x
In a stmt of an 'mdo' block: Just x <- return (Right x)
In a stmt of an 'mdo' block: rec { Just x <- return (Right x) }
```
Note that the error message mentions `rec` even though that is not what the user entered. In other instances, we are careful to show the code more similar to the original (e.g. `do`-notation instead of `>>=`). This should also be done here.
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ------------ |
| Version | 7.8.3 |
| Type | Bug |
| TypeOfFailure | OtherFailure |
| Priority | low |
| Resolution | Unresolved |
| Component | Compiler |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"mdo blocks in error messages are shown modified","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"7.8.3","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"{{{#!hs\r\n{-# LANGUAGE RecursiveDo #-}\r\nmain = mdo\r\n Just x <- return (Right x)\r\n return ()\r\n}}}\r\n\r\ngives\r\n\r\n{{{\r\nMdoTypeError.hs:3:3:\r\n Couldn't match expected type ‘Either a0 b0’\r\n with actual type ‘Maybe b0’\r\n Relevant bindings include x :: b0 (bound at MdoTypeError.hs:3:8)\r\n In the pattern: Just x\r\n In a stmt of an 'mdo' block: Just x <- return (Right x)\r\n In a stmt of an 'mdo' block: rec { Just x <- return (Right x) }\r\n}}}\r\n\r\nNote that the error message mentions `rec` even though that is not what the user entered. In other instances, we are careful to show the code more similar to the original (e.g. `do`-notation instead of `>>=`). This should also be done here.","type_of_failure":"OtherFailure","blocking":[]} -->https://gitlab.haskell.org/ghc/ghc/-/issues/7842Incorrect checking of let-bindings in recursive do2019-07-07T18:47:51ZIavor S. DiatchkiIncorrect checking of let-bindings in recursive doI have run into a problem with the type-checking of recursive do blocks, which reduces to the following example:
```
{-# LANGUAGE RecursiveDo #-}
module Bug where
bug :: (Int -> IO Int) -> IO (Bool, Char)
bug m =
mdo i <- m i1 -...I have run into a problem with the type-checking of recursive do blocks, which reduces to the following example:
```
{-# LANGUAGE RecursiveDo #-}
module Bug where
bug :: (Int -> IO Int) -> IO (Bool, Char)
bug m =
mdo i <- m i1 -- RECURSION
let i1 :: Int
i1 = i -- RECURSION
-- This appears to be monomorphic, despite the type signature.
f :: b -> b
f x = x
return (f True, f 'a')
```
This program is rejected with the errors shown below. The problem appears to be that somehow `f` has become monomorphic, despite its type-signature. This seems to happen only when `f` is part of a `let` block that is also involved in the recursion.
Here is the error reported by GHC 7.7.20130215:
```
Bug.hs:15:23:
Couldn't match expected type `Char' with actual type `Bool'
In the return type of a call of `f'
In the expression: f 'a'
In the first argument of `return', namely `(f True, f 'a')'
Bug.hs:15:25:
Couldn't match expected type `Bool' with actual type `Char'
In the first argument of `f', namely 'a'
In the expression: f 'a'
In the first argument of `return', namely `(f True, f 'a')'
```
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 7.7 |
| 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":"Incorrect checking of let-bindings in recursive do","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"7.7","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"I have run into a problem with the type-checking of recursive do blocks, which reduces to the following example:\r\n\r\n{{{\r\n{-# LANGUAGE RecursiveDo #-}\r\nmodule Bug where\r\n\r\nbug :: (Int -> IO Int) -> IO (Bool, Char)\r\nbug m =\r\n mdo i <- m i1 -- RECURSION\r\n\r\n let i1 :: Int\r\n i1 = i -- RECURSION\r\n\r\n -- This appears to be monomorphic, despite the type signature.\r\n f :: b -> b\r\n f x = x\r\n\r\n return (f True, f 'a')\r\n}}}\r\n\r\nThis program is rejected with the errors shown below. The problem appears to be that somehow `f` has become monomorphic, despite its type-signature. This seems to happen only when `f` is part of a `let` block that is also involved in the recursion.\r\n\r\nHere is the error reported by GHC 7.7.20130215:\r\n\r\n{{{\r\nBug.hs:15:23:\r\n Couldn't match expected type `Char' with actual type `Bool'\r\n In the return type of a call of `f'\r\n In the expression: f 'a'\r\n In the first argument of `return', namely `(f True, f 'a')'\r\n\r\nBug.hs:15:25:\r\n Couldn't match expected type `Bool' with actual type `Char'\r\n In the first argument of `f', namely 'a'\r\n In the expression: f 'a'\r\n In the first argument of `return', namely `(f True, f 'a')'\r\n}}}","type_of_failure":"OtherFailure","blocking":[]} -->