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 <[email protected]>: > 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 <[email protected]> wrote: > > The same bug has bitten git-annex too. IIRC. > > Cheers, > > Gabor > > Em domingo, 29 de maio de 2016, Michael Karg <[email protected]> > 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 > [email protected] > http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs > > >
_______________________________________________ ghc-devs mailing list [email protected] http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
