GHC: Ticket #7842: Incorrect checking of let-bindings in recursive do
http://ghc.haskell.org/trac/ghc/ticket/7842
<p>
I have run into a problem with the type-checking of recursive do blocks, which reduces to the following example:
</p>
<pre class="wiki">{-# 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')
</pre><p>
This program is rejected with the errors shown below. The problem appears to be that somehow <tt>f</tt> has become monomorphic, despite its type-signature. This seems to happen only when <tt>f</tt> is part of a <tt>let</tt> block that is also involved in the recursion.
</p>
<p>
Here is the error reported by GHC 7.7.20130215:
</p>
<pre class="wiki">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')'
</pre>en-usGHChttp://ghc.haskell.org/trac/ghc/chrome/site/ghc_logo.png
http://ghc.haskell.org/trac/ghc/ticket/7842
Trac 1.0.1parcsTue, 07 May 2013 01:19:20 GMT
http://ghc.haskell.org/trac/ghc/ticket/7842#comment:1
http://ghc.haskell.org/trac/ghc/ticket/7842#comment:1
<p>
Another test case:
</p>
<pre class="wiki">bug :: IO (Char,Bool)
bug = mdo
a <- return b
let f = id
b <- return a
return (f 'a', f True)
</pre><p>
which gets renamed to:
</p>
<pre class="wiki">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) }
</pre><p>
Possible solution: At the moment, all statements are kept in order during segment glomming (<tt>RnExpr.glomSegments</tt>) but that seems overly restrictive. Let-statements inside an <tt>mdo</tt> block should be able to get rearranged during segment glomming so that they can possibly be placed outside a recursive segment.
</p>
TicketwvvFri, 21 Jun 2013 19:16:11 GMT
http://ghc.haskell.org/trac/ghc/ticket/7842#comment:2
http://ghc.haskell.org/trac/ghc/ticket/7842#comment:2
<p>
First, it is needed to add extension: Rank2Types:
</p>
<pre class="wiki">{-# 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
</pre><p>
but still error:
</p>
<pre class="wiki"> 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
</pre><p>
Code
</p>
<pre class="wiki">{-# 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
</pre><blockquote>
<p>
is OK.
</p>
</blockquote>
Ticket