Be lazier about reducing type-function applications

Consider this:

f :: F 20 -> F 20
f x = x

That ought to typecheck in a trice, right? But if F is a type function, GHC currently (8.0) eagerly reduces F 20 to normal form. Let's say F 20 unltimately reduces to Int, after a long time. Then we get

   f = \x . (x |> g1) |> g2
where
   g1 :: F 20 ~ Int
   g2 :: Int ~ F 20

Here both g1 and g2 are big coercions. So we waste time reducing F 20 and we generate giant coercions by doing so. Maybe the optimiser gets rid of them again; more probably not. But it's clearly stupid.

This is one reason that the program in #5030 (closed) typechecks so slowly. We have

cnst :: Integer -> Either (Immediate DummyCPU) (RegVar DummyCPU)
cnst x = Left (Const x)

and there is absolutely no need to reduce either argument of the Either to normal form.

Richard and I have ideas about how to fix this, but I'm recording it in a ticket.

Relevant performance tests are T3064 and T5030 in compiler/perf. Doubtless many others too.

changed weight to 5

added Tbug Trac import labels

changed the description

Here is the basic idea we had: keep CFunEqCans in a lower-priority wing of the work-list, and then solve them only when necessary.

When we see a type function application like F 20 in a type, we flatten it to produce a flatten-unification-variable, fuv, and a constraint [W] F 20 ~ fuv. It is this constraint that would be de-prioritized. If the program can be type-checked without ever solving the CFunEqCan, then we do not need to reduce the type function.

When a CFunEqCan comes up as the work item, we try to solve it only if it is active. An active CFunEqCan involves an fuv that:

1. Is an argument to the class in an inert class constraint, OR
2. Is an argument to the type family in an active CFunEqCan, OR
3. Is at the top level of an inert equality

If a CFunEqCan is not active (that is, if it's passive), then just throw it right into the inert set without trying to solve. The inert set will have a new place to store passive CFunEqCans; if it were to become active (by one of the conditions above becoming satisfied), then it must get kicked out.

We think that an efficient way of implementing this scheme is by reference counting, essentially, where each fuv is mapped (in some data structure in the TcSEnv) to a count of places where it is active. When the count drops to zero, the associated CFunEqCan becomes passive. We would then have to increment and decrement counters when adding to and kicking out from the inert set.

Note that we have to be careful to making the refcount wibbles as efficient as possible, because they will happen a lot. For example, we can't just get the free variables of a constraint and then look for fuvs, as that would allocate space to store the fv set. Instead, we must write a new function that extracts only fuvs.

It remains to be seen if this will be a real performance improvement, as there will be a cost everyone has to pay to speed up the type family case.

mentioned in commit 1f09b246

added Pnormal label

marked this issue as related to #18965

added TypeFamilies compiler perf labels