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 |