[GHC] #15034: Desugaring `mdo` moves a `let` where it shouldn't be
#15034: Desugaring `mdo` moves a `let` where it shouldn't be -------------------------------------+------------------------------------- Reporter: parsonsmatt | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.6.1 Component: Compiler | Version: 8.2.2 Keywords: | Operating System: Unknown/Multiple Architecture: | Type of failure: None/Unknown Unknown/Multiple | Test Case: | Blocked By: Blocking: | Related Tickets: Differential Rev(s): | Wiki Page: -------------------------------------+------------------------------------- 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 [https://prime.haskell.org/wiki/RecursiveDo Haskell Prime wiki entry for Recursive Do], 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 | ^^^^^^^^^^^^ }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15034 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
Looking at the Haskell Prime wiki entry for Recursive Do, this seems to be the relevant bit: That is, a variable used before it is bound is
#15034: Desugaring `mdo` moves a `let` where it shouldn't be -------------------------------------+------------------------------------- Reporter: parsonsmatt | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.6.1 Component: Compiler | Version: 8.2.2 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by simonpj): treated as recursively defined, while in a Haskell 98 do-statement it would be treated as shadowed. So it looks as if GHC is following the specification. Are you proposing a different specification? And if so, what is it? -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15034#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#15034: Desugaring `mdo` moves a `let` where it shouldn't be -------------------------------------+------------------------------------- Reporter: parsonsmatt | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.6.1 Component: Compiler | Version: 8.2.2 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by parsonsmatt): I should have used a less minimal example, I think I didn't adequately demonstrate the problem :) I ran into this while working on a DSL for database definitions, and I'm using `RecursiveDo` to allow table references out of order. I am also using an `ST` token trick to ensure that field references don't escape their table. Here's a snippet of the DSL: {{{#!hs example :: Schema example = mdo let theUsual = derive @[Eq, Ord, Show] table_ "Dog" $ do owner <- field "owner" userRef field "name" (typ @String) foreignKey userRef "fk_dog_user" [owner] derive @[Eq, Ord, Show] userRef <- table "User" $ do field "name" (typ @String) field "age" (typ @Int) ! "do people use attribute?" ! "i hope so" theUsual table_ "Friend" $ do _ <- field "foobar" (typ @Int) name <- field "name" (typ @Int) ugh <- field "ugh" (typ @Int) unique "FriendName" name primary ugh theUsual }}} This works fine. However, if I move `theUsual` definition to below the `table_ "Dog"` block: {{{#!hs example = mdo table_ "Dog" $ do owner <- field "owner" userRef field "name" (typ @String) foreignKey userRef "fk_dog_user" [owner] derive @[Eq, Ord, Show] let theUsual = derive @[Eq, Ord, Show] userRef <- table "User" $ do field "name" (typ @String) field "age" (typ @Int) ! "do people use attribute?" ! "i hope so" theUsual table_ "Friend" $ do _ <- field "foobar" (typ @Int) name <- field "name" (typ @Int) ugh <- field "ugh" (typ @Int) unique "FriendName" name primary ugh theUsual }}} I get the following error: {{{ /home/matt/Projects/mesa-verde/src/MesaVerde/Internal.hs:59:9: 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. EntityDefine s () at src/MesaVerde/Internal.hs:(51,5)-(59,16) Expected type: EntityDefine s () Actual type: EntityDefine s0 () • In a stmt of a 'do' block: theUsual In the second argument of ‘($)’, namely ‘do _ <- field "foobar" (typ @Int) name <- field "name" (typ @Int) ugh <- field "ugh" (typ @Int) unique "FriendName" name ....’ In a stmt of an 'mdo' block: table_ "Friend" $ do _ <- field "foobar" (typ @Int) name <- field "name" (typ @Int) ugh <- field "ugh" (typ @Int) unique "FriendName" name .... • Relevant bindings include ugh :: FieldRef s (bound at src/MesaVerde/Internal.hs:54:9) name :: FieldRef s (bound at src/MesaVerde/Internal.hs:53:9) theUsual :: EntityDefine s0 () (bound at src/MesaVerde/Internal.hs:41:9) | 59 | theUsual | ^^^^^^^^ }}} It seems that it is floating `theUsual` into one of the blocks, causing the phantom type to infer as local to one of the blocks, and only allows it to be used in one block at a time. Switching to `do` instead of `mdo` fixes the problem (though it also forbids circular references, which I need). -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15034#comment:2 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#15034: Desugaring `mdo` moves a `let` where it shouldn't be -------------------------------------+------------------------------------- Reporter: parsonsmatt | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.6.1 Component: Compiler | Version: 8.2.2 Resolution: | Keywords: RecursiveDo Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by simonpj): * keywords: => RecursiveDo Comment: That is indeed odd. Are you sure your example is right in comment:2? You don't even use `theUsual` before its definition in the "However, when I move..." version. The `weiddlyLocal` example in the Description is more comprehensible. After dependency analysis we get {{{ thisWorks :: IO () thisWorks = do let weirdlyLocal1 = theThing runSTIO weirdlyLocal1 runSTIO weirdlyLocal1 thisBreaks :: IO () thisBreaks = do rec { runSTIO weirdlyLocal2 ; let weirdlyLocal2 = theThing runSTIO weirdlyLocal2 } }}} I've made the recursive block explicit. No `rec` is needed in the first example, and we get {{{ weirdlyLocal1 :: forall s. ST s () }}} But in the second example we have recursion, and like all reduction (at least without type signatures) in Haskell, it is monomorphic. So in the recursive block we get {{{ weirdlyLocal2 :: ST s0 () }}} where `s0` is some monomorphic type. So `weirdlyLocal2` is not polymoprhic enough to give to `runSTIO`, hence breakage. Another way to think of it is to imagine typing this: {{{ thisBreaks = do weirdlyLocal2 <- mfix (\wl2 -> do { runSTIO wl2 ; let weirdlyLocal2 = theThing ; return weirdlyLocal2 }) runSTIO weirdlyLocal2 } }}} Here you can see that the lambda-bound `wl2` would get a monormorphic type. I don't think anyone has studied how to do ''polymorphic'' recursion in `mdo`. But it'd be interesting to try. Trac #7842 is another report of the same problem. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15034#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#15034: Desugaring `mdo` moves a `let` where it shouldn't be -------------------------------------+------------------------------------- Reporter: parsonsmatt | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.6.1 Component: Compiler | Version: 8.2.2 Resolution: | Keywords: RecursiveDo Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by parsonsmatt):
That is indeed odd. Are you sure your example is right in comment:2? You don't even use theUsual before its definition in the "However, when I move..." version.
Yes. [https://github.com/parsonsmatt/mesa- verde/blob/81d2fb68ec87ff3f97eed1463f86f5f7e0b77240/src/MesaVerde/Internal.hs This is a repository] containing all of the code and definitions. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15034#comment:4 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
participants (1)
-
GHC