TypeFamilyDependencies accepts invalid injectivity annotation
Consider this code (depends on singletons-2.2):
{-# LANGUAGE TypeFamilies, DataKinds, PolyKinds, TypeOperators,
KindSignatures, TypeInType, TypeFamilyDependencies, UndecidableInstances #-}
module Bug where
import Data.Kind (Type)
import Data.Singletons.Prelude (Map, SndSym0)
import GHC.TypeLits (Nat)
data Payload = A | B
newtype NewType a = NewType Int
type NatList = [(Nat, Payload)]
type StripNatList (natList :: NatList) = Map SndSym0 natList
type family Family (natList :: NatList) = (r :: Type) | r -> natList where
Family '[] = ()
Family xs = NewType (StripNatList xs)
Why GHC is okay with injectivity annotation for Family
: r -> natList
?
These two types:
type Foo = Family '[ '(0, 'A), '(1, 'B)]
type Bar = Family '[ '(0, 'A), '(0, 'B)]
are obviously map to the same type:
*Bug Data.Singletons.Prelude> :kind! Foo
Foo :: *
= NewType ('A :$$$ '['B])
*Bug Data.Singletons.Prelude> :kind! Bar
Bar :: *
= NewType ('A :$$$ '['B])
If inline StripNatList
inside Family
definition:
type family Family (natList :: NatList) = (r :: Type) | r -> natList where
Family '[] = ()
Family xs = NewType (Map SndSym0 xs)
or change StripNatList
definition to type family:
type family StripNatList (natList :: NatList) where
StripNatList '[] = '[]
StripNatList ('(n, x) ': xs) = x ': StripNatList xs
Type family equation violates injectivity annotation.
compilation expectedly fails with Moreover, if I remove NewType
from Family
and change result kind:
type family Family (natList :: NatList) = (r :: [Payload]) | r -> natList where
Family xs = StripNatList xs
it fails with correct error regardless of StripNatList
definition.
Trac metadata
Trac field | Value |
---|---|
Version | 8.0.1 |
Type | Bug |
TypeOfFailure | OtherFailure |
Priority | high |
Resolution | Unresolved |
Component | Compiler (Type checker) |
Test case | |
Differential revisions | |
BlockedBy | |
Related | |
Blocking | |
CC | jstolarek |
Operating system | |
Architecture |