Opened 2 years ago

Last modified 2 years ago

#14279 new bug

Type families interfere with specialisation rewrite rules

Reported by: IvanTimokhin Owned by:
Priority: normal Milestone:
Component: Compiler Version: 8.2.1
Keywords: TypeFamilies Cc:
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: Other Test Case:
Blocked By: Blocking:
Related Tickets: Differential Rev(s):
Wiki Page:

Description

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.

Attachments (1)

test.hs (1.6 KB) - added by IvanTimokhin 2 years ago.

Download all attachments as: .zip

Change History (6)

Changed 2 years ago by IvanTimokhin

Attachment: test.hs added

comment:1 Changed 2 years ago by RyanGlScott

Keywords: TypeFamilies added

comment:2 Changed 2 years ago 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.

comment:3 Changed 2 years ago by goldfire

I argue that (related to my musings in #14119), patterns -- such as that LHS of rules -- should not mention type families at all. In other words, we should change any F ty in rule LHS to a fresh type variable a and then require F ty ~ a. Which, as it turns out, is precisely what's done in my Constrained Type Families paper.

comment:4 Changed 2 years ago by simonpj

But the LHS of the rule does not mention a type family, so comment:3 is irrelevant to this particular ticket. Here is the rule:

==================== Tidy Core rules ====================
"vinr/0"
    forall (@ (as :: [*])).
      vinr @ '[] @ as
      = (vinr0 @ as)
        `cast` (<Length '[]>_R
                ->_R <VSum as>_R
                ->_R (VSum (Sym (D:R:++[0] <as>_N)))_R
                :: Coercible
                     (Length '[] -> VSum as -> VSum as)
                     (Length '[] -> VSum as -> VSum ('[] ++ as)))

The trouble is that type family appears in the term we are matching the rule against. And it appears in the form Remove 'Z '[Int]. We can reduce that to '[], which matches the rule. But we don't: hence my suggestions in comment:2.

comment:5 Changed 2 years ago by goldfire

Ah yes. The unreduced type family is in the target, not the rule. I was skimming too quickly.

In agreement with comment:2, I argue this is very much like my new flatten_args (see Phab:D3848). GHC's flattener is a component of its constraint solver that essentially implements a strongly-typed rewrite system, where the equations of the rewrite system are 1) type family equations, 2) assumed equalities (e.g., from GADTs), and 3) filled-in metavariables. Of course, a RULE is just an equation to be used in a rewrite system, just the same. The problem is that the two rewrite system implementations are utterly distinct within GHC, where it seems like they should be combined somehow. And, following on from comment:2, the new logic in my Phab:D3848 patch would need to be applied here, too.

Interesting. I think this is doable, but I don't think it's done lightly (unlike Simon's conclusion above).

Note: See TracTickets for help on using tickets.