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 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.

comment:2 Changed 4 years ago 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.

comment:3 Changed 3 years ago by thomie

difficulty: Unknown

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

Note: See TracTickets for help on using tickets.