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
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/
Gabor You don't say which version of GHC you are using. I assume 7.8. Yes, you should really get the same behaviour with the surgared and desugared versions. Happily, with HEAD (and 7.6) it compiles fine without ImpredicativeTypes. Simon | -----Original Message----- | From: ghc-devs [mailto:ghc-devs-bounces@haskell.org] On Behalf Of Gabor | Greif | Sent: 21 February 2015 11:42 | To: ghc-devs | Subject: Desugaring introduces | | 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 | _______________________________________________ | ghc-devs mailing list | ghc-devs@haskell.org | http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
Yes, I am using 7.8.
I'll also try HEAD now...
... and it works! :-)
Thanks, I am happy now.
Cheers,
Gabor
PS: Would it be worth adding this as a regression test?
On 2/23/15, Simon Peyton Jones
Gabor
You don't say which version of GHC you are using. I assume 7.8.
Yes, you should really get the same behaviour with the surgared and desugared versions.
Happily, with HEAD (and 7.6) it compiles fine without ImpredicativeTypes.
Simon
| -----Original Message----- | From: ghc-devs [mailto:ghc-devs-bounces@haskell.org] On Behalf Of Gabor | Greif | Sent: 21 February 2015 11:42 | To: ghc-devs | Subject: Desugaring introduces | | 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 | _______________________________________________ | ghc-devs mailing list | ghc-devs@haskell.org | http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
participants (3)
-
Adam Gundry -
Gabor Greif -
Simon Peyton Jones