Desugaring introduces

[Adam Gundry]

Hi Gabor,

Interesting! While in principle it is true that t1 is the desugaring of
t2, GHC does typechecking before desugaring (even with RebindableSyntax)
in the interests of generating error messages that reflect what the user
actually wrote. The typechecker probably should treat t1 and t2
identically, but in practice this may be difficult to ensure. In this
case, I suspect the typechecking rules for do-notation assume that (>>=)
has a more usual type.

The user's guide section on RebindableSyntax says

> In all cases (apart from arrow notation), the static semantics should
> be that of the desugared form, even if that is a little unexpected.

so on that basis you're probably justified in reporting this as a bug.

Hope this helps,

Adam


On 21/02/15 11:42, Gabor Greif wrote:
> 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


-- 
Adam Gundry, Haskell Consultant
Well-Typed LLP, http://www.well-typed.com/