Opened 6 years ago
Last modified 16 months ago
#7842 new bug
Incorrect checking of let-bindings in recursive do
Reported by: | diatchki | Owned by: | |
---|---|---|---|
Priority: | normal | Milestone: | |
Component: | Compiler (Type checker) | Version: | 7.7 |
Keywords: | RecursiveDo | Cc: | |
Operating System: | Unknown/Multiple | Architecture: | Unknown/Multiple |
Type of failure: | GHC rejects valid program | Test Case: | |
Blocked By: | Blocking: | ||
Related Tickets: | Differential Rev(s): | ||
Wiki Page: |
Description
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')'
Change History (4)
comment:1 Changed 6 years ago by
comment:2 Changed 6 years ago by
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.
comment:3 Changed 5 years ago by
difficulty: | → Unknown |
---|
This ticket is listed on the page of tickets that SPJ is interested in.
comment:4 Changed 16 months ago by
Keywords: | RecursiveDo added |
---|
Another test case:
which gets renamed to:
Possible solution: At the moment, all statements are kept in order during segment glomming (
RnExpr.glomSegments
) but that seems overly restrictive. Let-statements inside anmdo
block should be able to get rearranged during segment glomming so that they can possibly be placed outside a recursive segment.