New GeneralisedNewtypeDeriving needs help with higher rank types
Consider
{-# LANGUAGE RankNTypes, GeneralizedNewtypeDeriving #-}
module Foo where
class C a where
op :: (forall b. b -> a) -> a
newtype T x = MkT x deriving( C )
With the new "coerce" implementation of GND, this fails:
Foo.hs:7:31:
Cannot instantiate unification variable ‛b0’
with a type involving foralls: (forall b. b -> T x) -> T x
Perhaps you want ImpredicativeTypes
In the expression:
GHC.Prim.coerce (op :: (forall (b :: *). b -> x) -> x) ::
(forall (b :: *). b -> T x) -> T x
In an equation for ‛op’:
op
= GHC.Prim.coerce (op :: (forall (b :: *). b -> x) -> x) ::
(forall (b :: *). b -> T x) -> T x
We want to coerce betweeen
(forall b. b -> x) -> x ~R (forall b. b -> T x) -> T x
There are two difficulties with the new coerce
approach:
- Regarded as source code, instance declaration
instance C x => C (T x) where
op = coerce (op :: (forall b. b -> x) -> x)
requires impredicative instantiation.
- We probably don't have a decomposition rule for
Coercible (forall a. t1) (forall a. t2)
There is no difficulty in principle here, but it's not quite obvious what the best approach to a fix is. But it would be good to fix before release; we don't want to break conduit
Trac metadata
Trac field | Value |
---|---|
Version | 7.6.3 |
Type | Bug |
TypeOfFailure | OtherFailure |
Priority | normal |
Resolution | Unresolved |
Component | Compiler |
Test case | |
Differential revisions | |
BlockedBy | |
Related | |
Blocking | |
CC | goldfire, nomeata |
Operating system | |
Architecture |