id,summary,reporter,owner,description,type,status,priority,milestone,component,version,resolution,keywords,cc,os,architecture,failure,difficulty,testcase,blockedby,blocking,related
6088,GeneralizedNewtypeDeriving + TypeFamilies + Equality constraints,Lemming,,"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)
}}}
",feature request,closed,normal,,Compiler (Type checker),7.4.1,fixed,,,Unknown/Multiple,Unknown/Multiple,GHC rejects valid program,Unknown,indexed-types/should_compile/T6088,,,3046