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

compilation expectedly fails with Type family equation violates injectivity annotation.

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