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

[Adam Gundry]

Hi Michael,

I think that GHC 8 is correct to reject this program without
ImpredicativeTypes (and if you enable ImpredicativeTypes, all bets are
off). Previous versions incorrectly accepted such programs, because they
didn't look through type synonyms. If you expand the type of the second
createResolver, you get

    ((String -> forall state . State state -> IO String), Dummy)

which has a quantified type in the first argument of the pair (i.e. it
requires impredicativity). See ticket #10194 for more details.

All the best,

Adam


On 29/05/16 17:47, Michael Karg wrote:
> 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)
> -}


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