Re: Rank2Types example not typechecking w/ GHC8. Bug or feature?

29 May 2016

      Hi all,

thank you for the quick response.
Since ImpredicativeTypes is not a road I want to go down, a newtype instead
of a type synonym seems like the best bet for that particular case.

Avoiding impredicativity "by accident" makes complete sense to me. I just
thought to bring up the example on the list, since there's a clear change
from GHC7 regarding which programs are accepted and which are not.

Thx again + enjoy the rest of the weekend
M.

2016-05-29 20:20 GMT+02:00 Oleg Grenrus :
...
The non-outer variant works, because then there aren’t higher rank types
at all, i.e. `state` of `Handler` is free to flow outwards.
There is two ways to fix issue: Either use `newtype` or use
`ImpredicativeTypes`
—
{-# LANGUAGE RankNTypes #-}
module TestTypes where
data State a        = State a
data Dummy          = Dummy
newtype Handler result = Handler { runHandler :: forall state . State
state -> IO result }
type Resolver       = String -> Handler String
eventRouter :: Resolver -> String -> IO ()
eventRouter resolver event =
    runHandler (resolver event) state >> return ()
  where
    state :: State ()
    state = undefined
{-
-- does type check
createResolver :: Resolver
createResolver = \event state -> return "result"
processor :: IO ()
processor =
    getLine >>= eventRouter resolver >> processor
  where
    resolver = createResolver
-}
eventConsumer :: Resolver -> String -> IO ()
eventConsumer = undefined
{-
rank2.hs:34:17: error:
    • Cannot instantiate unification variable ‘a0’
      with a type involving foralls: Resolver -> String -> IO ()
        GHC doesn't yet support impredicative polymorphism
    • In the expression: undefined
      In an equation for ‘eventConsumer’: eventConsumer = undefined
-}
-- does not type check when the rank 2 type isn't the "outermost" one?
createResolver :: (Resolver, Dummy)
createResolver = (\event -> Handler $ \state -> return "result", Dummy)
processor :: IO ()
processor =
    getLine >>= eventConsumer resolver >> processor
  where
    resolver :: Resolver
    resolver = fst (createResolver :: (Resolver, Dummy))
{-
    • Couldn't match type ‘t’ with ‘Resolver’
      ‘t’ is a rigid type variable bound by
        the inferred type of resolver :: t at TestTypes.hs:41:5
      Expected type: (t, Dummy)
        Actual type: (Resolver, Dummy)
-}
---
On 29 May 2016, at 21:02, Gabor Greif  wrote:
The same bug has bitten git-annex too. IIRC.
Cheers,
Gabor
Em domingo, 29 de maio de 2016, Michael Karg 
escreveu:
...
Hi devs,
could you please have a look at the following code snippet (modeled after
a real-world app of mine)? There's a rank2type involved, and it doesn't
type-check anymore when the type is e.g. part of a tuple, whereas
everything's fine when it's the "outermost" type.
With GHC7.10 both variants type-check. Could anyone shed some light on
what's behind this? Is the way the types are used in the snippet considered
dispreferred or wrong under GHC8?
Thanks for having a look and hopefully pointing me to a page/ticket/...
providing insight,
Michael
--------
{-# LANGUAGE Rank2Types #-}
module TestTypes where
data State a        = State a
data Dummy          = Dummy
type Handler result = forall state . State state -> IO result
type Resolver       = String -> Handler String
eventRouter :: Resolver -> String -> IO ()
eventRouter resolver event =
    resolver event state >> return ()
  where
    state :: State ()
    state = undefined
{-
-- does type check
createResolver :: Resolver
createResolver = \event state -> return "result"
processor :: IO ()
processor =
    getLine >>= eventRouter resolver >> processor
  where
    resolver = createResolver
-}
-- does not type check when the rank 2 type isn't the "outermost" one?
createResolver :: (Resolver, Dummy)
createResolver = (\event state -> return "result", Dummy)
processor :: IO ()
processor =
    getLine >>= eventConsumer resolver >> processor
  where
    (resolver, _) = createResolver
{-
    • Couldn't match type ‘t’ with ‘Resolver’
      ‘t’ is a rigid type variable bound by
        the inferred type of resolver :: t at TestTypes.hs:41:5
      Expected type: (t, Dummy)
        Actual type: (Resolver, Dummy)
-}
_______________________________________________
ghc-devs mailing list
ghc-devs@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs