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

[Michael Karg]

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 <oleg.grenrus at iki.fi>:

> 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 <ggreif at gmail.com> wrote:
>
> The same bug has bitten git-annex too. IIRC.
>
> Cheers,
>
>     Gabor
>
> Em domingo, 29 de maio de 2016, Michael Karg <mgoremeier at gmail.com>
> 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 at haskell.org
> http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
>
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/ghc-devs/attachments/20160529/822ad090/attachment.html>