Opened 5 years ago

Last modified 3 years 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: | 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 (3)

### comment:1 Changed 5 years ago by

### comment:2 Changed 5 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 3 years ago by

difficulty: | → Unknown |
---|

This ticket is listed on the page of tickets that SPJ is interested in.

**Note:**See TracTickets for help on using tickets.

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 an`mdo`

block should be able to get rearranged during segment glomming so that they can possibly be placed outside a recursive segment.