#12114: GHC rejects injective type family -------------------------------------+------------------------------------- Reporter: MikeIzbicki | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.0.1 (Type checker) | Keywords: | Operating System: Unknown/Multiple Architecture: | Type of failure: None/Unknown Unknown/Multiple | Test Case: | Blocked By: Blocking: | Related Tickets: Differential Rev(s): | Wiki Page: -------------------------------------+------------------------------------- The following injective type family fails to compile in GHC 8.0 {{{ type family Snoc (xs :: [k]) (y::k) = r | r -> xs y where Snoc '[] y = '[y] Snoc (x ': xs) y = x ': (Snoc xs y) }}} The error message is {{{ • Type family equations violate injectivity annotation: forall k (y :: k). Snoc '[] y = '[y] -- Defined at FAlgebra.hs:49:5 forall k (xs :: [k]) (x :: k) (y :: k). Snoc (x : xs) y = x : Snoc xs y -- Defined at FAlgebra.hs:52:5 • In the equations for closed type family ‘Snoc’ In the type family declaration for ‘Snoc’ }}} I think the problem is related to injectivity rule 5 from [this page](https://ghc.haskell.org/trac/ghc/wiki/InjectiveTypeFamilies) being too conservative. In particular, if you substitute `'[]` for `Snoc xs y` in the RHS of the second rule, then the two rules will unify but have different LHSs. This substitution is invalid, however, because the `Snoc` type family will never result in an empty list. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12114 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler