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/