[GHC] #14279: Type families interfere with specialisation rewrite rules

[GHC]

#14279: Type families interfere with specialisation rewrite rules
-------------------------------------+-------------------------------------
           Reporter:  IvanTimokhin   |             Owner:  (none)
               Type:  bug            |            Status:  new
           Priority:  normal         |         Milestone:
          Component:  Compiler       |           Version:  8.2.1
           Keywords:                 |  Operating System:  Unknown/Multiple
       Architecture:                 |   Type of failure:  Other
  Unknown/Multiple                   |
          Test Case:                 |        Blocked By:
           Blocking:                 |   Related Tickets:
Differential Rev(s):                 |         Wiki Page:
-------------------------------------+-------------------------------------
 Consider the attached file, in particular the function
 {{{#!hs
 vinr :: Length as -> VSum bs -> VSum (as ++ bs)
 }}}
 its specialised version
 {{{#!hs
 vinr0 :: Length '[] -> VSum as -> VSum as
 }}}
 and the rewrite rule
 {{{#!hs
 {-# RULES "vinr/0" vinr = vinr0 #-}
 }}}

 According to
 [https://downloads.haskell.org/~ghc/latest/docs/html/users_guide/glasgow_exts.html#specialisation
 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`):

 {{{#!hs
 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.

-- 
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/14279>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler