GeneralizedNewtypeDeriving + TypeFamilies + Equality constraints
I have the following module that uses generalized newtype deriving:
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
class C a
newtype A n = A Int
class Pos n
instance (Pos n) => C (A n)
newtype B n = B (A n)
deriving (C)
This module can be compiled, and GHCi shows me what generalized newtype deriving generated for B:
*Main> :info B
newtype B n = B (A n) -- Defined at NewtypeSuperclass.hs:13:9
instance Pos n => C (B n) -- Defined at NewtypeSuperclass.hs:14:14
This is what I expected.
Now I want to translate the Pos type class to an equality constraint on a type function value:
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE EmptyDataDecls #-}
class C a
newtype A n = A Int
type family Pos n
data True
instance (Pos n ~ True) => C (A n)
newtype B n = B (A n)
deriving (C)
Now I get the compiler error:
Couldn't match type `Pos n' with `True'
arising from the 'deriving' clause of a data type declaration
When deriving the instance for (C (B n))
It seems that the equality constraint disallows generalized newtype deriving. Is this an implementation issue or is there a deep theoretic problem? I would certainly prefer to obtain something like:
*Main> :info B
newtype B n = B (A n)
instance (Pos n ~ True) => C (B n)
Trac metadata
| Trac field | Value |
|---|---|
| Version | 7.4.1 |
| Type | FeatureRequest |
| TypeOfFailure | OtherFailure |
| Priority | normal |
| Resolution | Unresolved |
| Component | Compiler (Type checker) |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | |
| Operating system | |
| Architecture |