GHC cannot infer injectivity on type family operating on GHC.TypeLits' Nat, but can for equivalent type family operating on user-defined Nat kind

The following does not work:

{-# LANGUAGE DataKinds, PolyKinds, TypeFamilies, TypeOperators, UndecidableInstances #-}

import GHC.TypeLits (Nat, type (-))

type family Replicate (n :: Nat) (a :: k) = (r :: [k]) | r -> n where
    Replicate 0 a = '[]
    Replicate n a = a ': Replicate (n - 1) a

It fails to compile with the following error:

error:
    • Type family equation violates injectivity annotation.
      Type variable ‘n’ cannot be inferred from the right-hand side.
      In the type family equation:
        forall (k :: BOX) (n :: Nat) (a :: k).
          Replicate n a = a : Replicate (n - 1) a
    • In the equations for closed type family ‘Replicate’
      In the type family declaration for ‘Replicate’
Failed, modules loaded: none.

However, the following does:

{-# LANGUAGE DataKinds, PolyKinds, TypeFamilies, TypeOperators, UndecidableInstances #-}

data Nat = Zero | Succ Nat

type family Replicate (n :: Nat) (a :: k) = (r :: [k]) | r -> n where
    Replicate Zero a = '[]
    Replicate (Succ n) a = a ': Replicate n a

Sure GHC.TypeLits' built-in Nat type is isomorphic to the one defined above, and thus GHC should be able to infer injectivity for Replicate?

Trac metadata

Trac field	Value
Version	7.10.2
Type	Bug
TypeOfFailure	OtherFailure
Priority	normal
Resolution	Unresolved
Component	Compiler
Test case
Differential revisions
BlockedBy
Related
Blocking
CC
Operating system
Architecture