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

[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 <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 <mailto: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/e51c3a36/attachment-0001.html>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 842 bytes
Desc: Message signed with OpenPGP using GPGMail
URL: <http://mail.haskell.org/pipermail/ghc-devs/attachments/20160529/e51c3a36/attachment-0001.sig>