[GHC] #7842: Incorrect checking of let-bindings in recursive do
#7842: Incorrect checking of let-bindings in recursive do --------------------------------------+------------------------------------- Reporter: diatchki | Owner: Type: bug | Status: new Priority: normal | Component: Compiler (Type checker) Version: 7.7 | Keywords: Os: Unknown/Multiple | Architecture: Unknown/Multiple Failure: GHC rejects valid program | Blockedby: Blocking: | Related: --------------------------------------+------------------------------------- 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')' }}} -- Ticket URL: http://hackage.haskell.org/trac/ghc/ticket/7842 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#7842: Incorrect checking of let-bindings in recursive do --------------------------------------+------------------------------------- Reporter: diatchki | Owner: Type: bug | Status: new Priority: normal | Component: Compiler (Type checker) Version: 7.7 | Keywords: Os: Unknown/Multiple | Architecture: Unknown/Multiple Failure: GHC rejects valid program | Blockedby: Blocking: | Related: --------------------------------------+------------------------------------- Comment(by parcs): Another test case: {{{ bug :: IO (Char,Bool) bug = mdo a <- return b let f = id b <- return a return (f 'a', f True) }}} which gets renamed to: {{{ finish rnSrc bug :: IO (Char, Bool) bug = mdo { rec { a <- return b; let f = id; -- 'f' can be placed outside the recursive block b <- return a }; return (f 'a', f True) } }}} Possible solution: At the moment, all statements are kept in order during segment glomming (`RnExpr.glomSegments`) but that seems overly restrictive. Let-statements inside an `mdo` block should be able to get rearranged during segment glomming so that they can possibly be placed outside a recursive segment. -- Ticket URL: http://hackage.haskell.org/trac/ghc/ticket/7842#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#7842: Incorrect checking of let-bindings in recursive do --------------------------------------+------------------------------------- Reporter: diatchki | Owner: Type: bug | Status: new Priority: normal | Component: Compiler (Type checker) Version: 7.7 | Keywords: Os: Unknown/Multiple | Architecture: Unknown/Multiple Failure: GHC rejects valid program | Blockedby: Blocking: | Related: --------------------------------------+------------------------------------- Comment(by wvv): First, it is needed to add extension: Rank2Types: {{{ {-# LANGUAGE RecursiveDo, Rank2Types #-} bug :: IO (Char,Bool) bug = mdo a <- return b let f = id let g :: (forall a. (a -> a) ) -> (Char, Bool) g f = (f 'a', f True) b <- return a return $ g f }}} but still error: {{{ Couldn't match type `a0' with `a' because type variable `a' would escape its scope This (rigid, skolem) type variable is bound by a type expected by the context: a -> a The following variables have types that mention a0 f :: a0 -> a0 (bound at test2.hs:34:8) Expected type: a -> a Actual type: a0 -> a0 In the first argument of `g', namely `f' In the second argument of `($)', namely `g f' In a stmt of an 'mdo' block: return $ g f }}} Code {{{ {-# LANGUAGE RecursiveDo, Rank2Types #-} bug :: IO (Char,Bool) bug = mdo let f = id let g :: (forall a. (a -> a) ) -> (Char, Bool) g f = (f 'a', f True) return $ g f }}} is OK. -- Ticket URL: http://hackage.haskell.org/trac/ghc/ticket/7842#comment:2 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
participants (2)
-
GHC -
GHC