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 |