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 |