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

Previous Topic Next Topic
 
classic Classic list List threaded Threaded
5 messages Options
Reply | Threaded
Open this post in threaded view
|

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

Michael Karg
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
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
Reply | Threaded
Open this post in threaded view
|

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

Gabor Greif-2
The same bug has bitten git-annex too. IIRC.

Cheers,

    Gabor

Em domingo, 29 de maio de 2016, Michael Karg <[hidden email]> 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
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
Reply | Threaded
Open this post in threaded view
|

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

Adam Gundry-2
In reply to this post by Michael Karg
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/
_______________________________________________
ghc-devs mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
Reply | Threaded
Open this post in threaded view
|

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

Oleg Grenrus
In reply to this post by Gabor Greif-2
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 <[hidden email]> wrote:

The same bug has bitten git-annex too. IIRC.

Cheers,

    Gabor

Em domingo, 29 de maio de 2016, Michael Karg <[hidden email]> 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
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs


_______________________________________________
ghc-devs mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs

signature.asc (859 bytes) Download Attachment
Reply | Threaded
Open this post in threaded view
|

Re: 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 <[hidden email]>:
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 <[hidden email]> wrote:

The same bug has bitten git-annex too. IIRC.

Cheers,

    Gabor

Em domingo, 29 de maio de 2016, Michael Karg <[hidden email]> 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
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs



_______________________________________________
ghc-devs mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs