Need ImpredicativeTypes for GeneralizedNewtypeDeriving?
Nathan Howell posts this code:
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE RankNTypes #-}
-- Uncomment to compile on GHC 7.8
-- {-# LANGUAGE ImpredicativeTypes #-}
module Repro where
import Control.Monad.Trans.Cont
import Control.Monad.Trans.State.Lazy
newtype AnyContT m a = AnyContT { unAnyContT :: forall r . ContT r m a }
class MonadAnyCont b m where
anyContToM :: (forall r . (a -> b r) -> b r) -> m a
instance MonadAnyCont b (AnyContT m) where
anyContToM _ = error "foo"
data DecodeState = DecodeState
newtype DecodeAST a = DecodeAST { unDecodeAST :: AnyContT (StateT DecodeState IO) a }
deriving (MonadAnyCont IO)
Compiling on HEAD produces
[1 of 1] Compiling Repro ( repro.hs, interpreted )
repro.hs:24:13:
Cannot instantiate unification variable ‛b0’
with a type involving foralls:
(forall r. (a1 -> IO r) -> IO r) -> DecodeAST a1
Perhaps you want ImpredicativeTypes
In the expression:
GHC.Prim.coerce
(anyContToM ::
(forall (r :: *). (a -> IO r) -> IO r)
-> AnyContT (StateT DecodeState IO) a) ::
forall (a :: *).
(forall (r :: *). (a -> IO r) -> IO r) -> DecodeAST a
In an equation for ‛anyContToM’:
anyContToM
= GHC.Prim.coerce
(anyContToM ::
(forall (r :: *). (a -> IO r) -> IO r)
-> AnyContT (StateT DecodeState IO) a) ::
forall (a :: *).
(forall (r :: *). (a -> IO r) -> IO r) -> DecodeAST a
Failed, modules loaded: none.
Two questions:
- Should we require users to specify !ImpredicativeTypes here? Or, should the !GeneralizedNewtypeDeriving mechanism (which sometimes is impredicative) just assume the extension?
- Can we improve the error message?
I'd like to note that the original example really does require impredicativity -- the question is whether and how to bother the user with this technicality.
Small program note: I've done a lot of stuff with !GeneralizedNewtypeDeriving lately but am on holiday until Jan. 6, so don't expect responses!
Trac metadata
Trac field | Value |
---|---|
Version | 7.7 |
Type | Bug |
TypeOfFailure | OtherFailure |
Priority | normal |
Resolution | Unresolved |
Component | Compiler |
Test case | |
Differential revisions | |
BlockedBy | |
Related | |
Blocking | |
CC | |
Operating system | |
Architecture |