Desugaring introduces

21 Feb 2015

      Hi devs,

before I file a bug, I'd like to double check on a strange desugaring
behaviour with RankNTypes and RebindableSyntax.

Here is the snippet
{{{
{-# LANGUAGE RankNTypes, RebindableSyntax #-}
{-# LANGUAGE ImpredicativeTypes #-}

import qualified Prelude as P

(>>=) :: a -> ((forall b . b) -> c) -> c
a >>= f = f P.undefined
return a = a
fail s = P.undefined

t1 = 'd' >>= (\_ -> 'k')

t2 = do _ <- 'd'
        'k'

main = P.putStrLn [t1, t2]
}}}

Without ImpredicativeTypes I get this error:
{{{
rebindtest.hs:13:9:
    Cannot instantiate unification variable ‘t0’
    with a type involving foralls: forall b. b
      Perhaps you want ImpredicativeTypes
    In a stmt of a 'do' block: _ <- 'd'
    In the expression:
      do { _ <- 'd';
           'k' }
    In an equation for ‘t2’:
        t2
          = do { _ <- 'd';
                 'k' }
}}}

t1 is supposed to be the desugaring of t2. Strangely t2 only compiles
with ImpredicativeTypes. Why? Isn't desugaring a purely syntactic
transformation (esp. with RebindableSyntax)?

Any hints welcome!

Cheers,

    Gabor

Desugaring introduces

Gabor Greif