[GHC] #12114: GHC rejects injective type family

[GHC]

#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