[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
      Resolution:                    |             Keywords:  TypeFamilies
Operating System:  Unknown/Multiple  |         Architecture:
                                     |  Unknown/Multiple
 Type of failure:  Other             |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:                    |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------

Comment (by simonpj):

 Your analysis is right. We have something like
 {{{
 test = replace @ 'Z
                @ '[Int]
                @ '[Int]
                @ Int
                (Test.$WLZ
                 `cast` ((Length (Sym (Test.D:R:Remove[0] <Int>_N
 <'[]>_N)))_R
                         :: (Length '[] :: *) ~R# (Length (Remove 'Z
 '[Int]) :: *)))
                (Test.$WLS @ '[] @ Int Test.$WLZ)
                (Test.$WIZ @ Int @ '[])
                (Test.$WVInL @ Int @ '[])
                (Test.$WVInL @ Int @ '[] (GHC.Types.I# 2#)))
 }}}
 where the RHS of `replace` has various occurrences of `Remove n as`.  If
 we inline `replace`
 for this call site, those occurrences become `Remove 'Z '[Int]`, which
 you'd like to
 see reduced to `'[]`.   But the rule matcher does not match modulo
 function reduction.

 Perhaps it should. But it't not clear to me how.  Suppose we have an axiom
 {{{
 ax :: F Int ~ Bool
 }}}
 and we have a call
 {{{
 ...(f @(Maybe (F Int)) e1 e2)...
 }}}
 Perhaps, before (or somehow during) the matching of a rule for `f`, we
 should
 transform to
 {{{
 ...(f @(Maybe Bool) e1 e2)...
 }}}
 But that isn't well typed; we'd need to do some `liftCoSubst` kind of
 thing.  Suppose
 {{{
     f :: forall a. ty<a>
 and
     co :: s1 ~ s2   -- s2 is a normalised version of s1
 }}}
 Then perhaps we can rewrite
 {{{
    f @s1
 ===>
    f @s2 |> ty[sym co/a]
 }}}
 Perhaps something like this (maybe a bit more; e.g. on binder types)
 can replace the handful of
 uses of `topNormaliseType_maybe` in the simplifier.  Or, more generally,
 perhaps we can do this normalisation in `simplType`.  It would make sense
 for the simplifier to aggressively normalise types, as inlining happens,
 just
 as it normalises terms.

 Why do fundeps work?  I think it's because the function appliation does
 not
 appear nested inside `replace`, but rather is passed as an argument to
 `replace`,
 and hence can be normalised in the caller.

 I wonder if other people have tripped over this lack of normalisation
 in types in the simplifier?

 I don't think this would be hard to try out.

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