TypeFamilyDependencies:为什么接受这个注入性注释？

Question

考虑一下这段代码(需要单例-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 List = [Payload]
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)    

我不明白为什么GHC可以使用注入性注释Family:r -> natList.

这两种类型:

type Foo = Family '[ '(0, 'A), '(1, 'B)]
type Bar = Family '[ '(0, 'A), '(0, 'B)]

显然是映射到相同的类型:

*Bug Data.Singletons.Prelude> :kind! Foo
Foo :: *
= NewType ('A :$$$ '['B])
*Bug Data.Singletons.Prelude> :kind! Bar
Bar :: *
= NewType ('A :$$$ '['B])

为什么这不被拒绝？