Type families interfere with specialisation rewrite rules

Consider the attached file, in particular the function

vinr :: Length as -> VSum bs -> VSum (as ++ bs)

its specialised version

vinr0 :: Length '[] -> VSum as -> VSum as

and the rewrite rule

{-# RULES "vinr/0" vinr = vinr0 #-}

According to the relevant section of GHC user guide, vinr should be replaced with vinr0 whenever the types match. However, the resulting Core for test contains the following (compiled with ghc -O2):

Test.test1
  = case extractIdx
           @ 'Z @ '[Int] @ Int (Test.$WIZ @ Int @ '[]) Test.test2
    of {
      Left other_aZf ->
        Test.$wvinl @ Length @ '[Int] @ (Remove 'Z '[Int]) other_aZf;
      Right x_aZg ->
        vinr
          @ (Remove 'Z '[Int])
          @ '[Int]
          (Test.$WLZ
           `cast` ((Length (Sym (Test.D:R:Remove[0] <Int>_N <'[]>_N)))_R
                   :: (Length '[] :: *) ~R# (Length (Remove 'Z '[Int]) :: *)))
          (Test.VInL
             @ '[Int]
             @ Int
             @ '[]
             @~ (<'[Int]>_N :: ('[Int] :: [*]) GHC.Prim.~# ('[Int] :: [*]))
             x_aZg)
    }

So the rule never fires, and vinr is still there, even though it is directly applied to LZ :: Length '[].

My dilettante analysis is that, for some reason, GHC keeps the Remove 'Z '[Int] as-is, not evaluating it to '[], and, since the types don't match //syntactically//, doesn't apply the rule. In particular, if I replace type families with classes with functional dependencies, the rule fires as expected.

Trac metadata

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