GitLab

Marge Bot pushed to branch master at Glasgow Haskell Compiler / GHC

Commits:

40764930

by sheaf at 2026-06-12T14:54:43-04:00

Add type family performance test for #26426

Some GHC versions produced large numbers of coercions after typechecking
and desugaring when compiling the program in #26426:

Version | Typechecker time | Typechecker allocations | Coercions
-------:|-----------------:|------------------------:|---------:
9.6     |   47 ms          |  48 MB                  |    110k
9.8     | 1000 ms          | 486 MB                  | 10,437k
9.10    |  922 ms          | 489 MB                  | 10,436k
9.12    |  906 ms          | 482 MB                  | 10,437k
9.14    |   63 ms          |  55 MB                  |    333k
10.0    |   47 ms          |  64 MB                  |     35k

The improvement 9.12 -> 9.14 was due to commit 22d11fa818fae2c95c494fc0fac1f8cb4c6e7cb6,
while the improvement 9.14 -> 10.0 was due to commit 0b7df6db9e46df40e86fbff1a66dc10440b99db5.

As the behaviour of GHC seems better than it's ever been on this program,
we declare victory, adding this performance test to ensure we don't
regress on this program.

On the way, we update Note [Combining equalities] in GHC.Tc.SolveR.Equality
with the explanation of the 9.12 -> 9.14 improvement (getting rid of an
exponential blowup in coercion sizes), and we update
Note [Exploiting closed type families] in GHC.Tc.Solver.FunDeps with
the explanation of the 9.14 -> 10.0 improvement (bringing down coercion
size growth from cubic to quadratic).

4 changed files:

compiler/GHC/Tc/Solver/Equality.hs
compiler/GHC/Tc/Solver/FunDeps.hs
+ testsuite/tests/perf/compiler/T26426.hs
testsuite/tests/perf/compiler/all.T

Changes:

compiler/GHC/Tc/Solver/Equality.hs

@@ -2980,15 +2980,30 @@ But it's not so simple:
     we kick out g1. Now we have two constraints
         [W] g1        : F a ~ a Int  (arising from (F a ~ a Int))
         [W] g2{rw:g1} : F a ~ a Int  (arising from (F alpha ~ F a))
 -   If we end up with g2 in the inert set (not g1) we'll get a very confusing
 -   error message that we can solve (F a ~ a Int)
 -       arising from F a ~ F a
 +   If we solve `g1` from `g2` we end up with
 +     g1 := g2
 +     [W] g2{} : F a ~ a Int  (arising from (F alpha ~ F a))
 +   and hence (since alpha := a) we report that we can't solve (F a ~ a Int)
 +   arising from (F a ~ F a), which is extremely confusing. Moreover, it seems
 +   wrong to "solve" `g1` using `g2` when `g2` has itself been rewritten by `g1`!
     TL;DR: Better to hang on to `g1` (with no rewriters), in preference
     to `g2` (which has a rewriter).
     See (WRW11) in Note [Wanteds rewrite Wanteds: rewriter-sets]
     in GHC.Tc.Types.Constraint.
++
 +   Note that the decision to prefer a constraint without rewriters over one that
 +   has rewriters can also have a /huge/ effect on performance. For instance, it
 +   avoids an **exponential** blow-up in the size of coercions produced when
 +   typechecking in T26426. In that program, we have coercions of the form:
++
 +     co_i :: TaggedTypes as `Append` TaggedTypes '[ty]
 +          ~# TaggedTypes (as `Append` '[ty])
++
 +   and each 'co_{i+1}' contains the previous 'co_i' twice. Without preferring
 +   Wanteds with no rewriters, we essentially end up inlining 'co_i' into 'co_{i+1}',
 +   which results in exponentially-sized proof terms, growing like O(2^i).
  -}
  tryInertEqs :: EqCt -> SolverStage ()

compiler/GHC/Tc/Solver/FunDeps.hs

@@ -1198,6 +1198,56 @@ Key point: equations that are not relevant do not need to be considered for fund
    and [W] I alpha ~ Int |> g2
    Here we definiteily want to take advantage of injectivity.
 +(CF6) This machinery can also have a significant positive effect on the size of
 +  proof terms. For example (simplification of T26426):
++
 +      type family (++) a b where { '[] ++ ys = ys; (x:xs) ++ ys = x : (xs ++ ys) }
 +      type family MapId a where { MapId '[] = '[]; MapId (x:xs) = x : MapId xs }
++
 +      app :: (MapId xs ++ MapId ys ~ MapId (xs ++ ys)) => Proxy xs -> Proxy ys -> Proxy (xs ++ ys)
++
 +      test :: Proxy [ty_1, ..., ty_n]
 +      test =   Proxy @'[ty_1]
 +         `app` Proxy @'[ty_2]
 +         ...
 +         `app` Proxy @'[ty_n]
++
 +  Every `app` call gives rise to a Wanted of the form:
++
 +    [W] MapId acc_i ++ MapId '[ty_i] ~ MapId (acc_i ++ '[ty_i])
++
 +  while the overall result type gives us a Wanted of the form
++
 +    [W] acc_n ++ '[ty_n] ~ [ty_1, ..., ty_n]
++
 +  By using (CFFA) on this result Wanted, we deduce that we must have
++
 +    acc_n ~ [ty_1, ..., ty_{n-1}]
++
 +  which is a flat list. Repeating the process, (CFFA) allows us to deduce that
++
 +    acc_i ~ [ty_1, ..., ty_{i-1}]
++
 +  for all i. This allows the other Wanteds to be solved directly, giving rise to
 +  proof terms with the typical triangular O(n^2) shape
++
 +    co_i = (O(i) proof that MapId acc_i ++ MapId '[ty_i] ~ acc_{i+1})
 +         ; (O(i) proof that acc_{i+1} ~ MapId (acc_i ++ '[ty_i]))
++
 +  However, /without/ (CFFA), 'acc_i' is not unified with a flat list but is left
 +  as the nested application:
++
 +    acc_i ~ (... (('[ty_1] ++ '[ty_2]) ++ '[ty_3]) ... ++ '[ty_{i-1}])
++
 +  This means that 'MapId acc_i' is stuck until we reduce the above, which takes
 +  O(i^2) type family reduction steps, instead of O(i). The same applies to
 +  the other proof term involving 'MapId (acc_i ++ '[ty_i])'.
 +  Consequently, without (CFFA) the overall coercion size blows up to O(n^3).
++
 +  The takeaway is that (CFFA) allows us to push in the (flat) result type,
 +  instead of relying on recursively built sub-proof terms, which brings down
 +  coercion sizes (in certain situations) from O(n^3) to O(n^2).
++
  Note [Cache-caused loops]
  ~~~~~~~~~~~~~~~~~~~~~~~~~
  It is very dangerous to cache a rewritten wanted family equation as 'solved' in

testsuite/tests/perf/compiler/T26426.hs

 +{-# LANGUAGE DataKinds #-}
 +{-# LANGUAGE TypeFamilies #-}
 +module T26426 (
 +  someTypes
 +) where
++
 +import Data.Kind (Type)
 +import GHC.TypeLits (Symbol)
++
 +type family Append (left :: [k]) (right :: [k]) :: [k] where
 +  Append '[] right = right
 +  Append (a : rest) right = a : Append rest right
++
 +type family TaggedTypes (tags :: [(Symbol, Type)]) :: [Type] where
 +  TaggedTypes '[] = '[]
 +  TaggedTypes ('(_, typ) : rest) = typ : TaggedTypes rest
++
 +data Types (types :: [(Symbol, Type)]) = Types
++
 +mkTypes :: forall sym val. val -> Types '[ '(sym, val) ]
 +mkTypes _ = Types
++
 +appendTypes ::
 +  -- This constraint is the one that causes the issue. If the next line is commented
 +  -- out, then this module compiles quickly
 +  Append (TaggedTypes left) (TaggedTypes right) ~ TaggedTypes (Append left right) =>
 +  Types left -> Types right -> Types (Append left right)
 +appendTypes _ _ = Types
++
 +someTypes ::
 +  Types
 +    [ '("01", Int)
 +    , '("02", Int)
 +    , '("03", Int)
 +    , '("04", Int)
 +    , '("05", Int)
 +    , '("06", Int)
 +    , '("07", Int)
 +    , '("08", Int)
 +    , '("09", Int)
 +    , '("10", Int)
 +    , '("11", Int)
 +    , '("12", Int)
 +    , '("13", Int)
 +    , '("14", Int)
 +    , '("15", Int)
 +    , '("16", Int)
 +    ]
++
 +someTypes =
 +  mkTypes @"01"  1 `appendTypes`
 +  mkTypes @"02"  2 `appendTypes`
 +  mkTypes @"03"  3 `appendTypes`
 +  mkTypes @"04"  4 `appendTypes`
 +  mkTypes @"05"  5 `appendTypes`
 +  mkTypes @"06"  6 `appendTypes`
 +  mkTypes @"07"  7 `appendTypes`
 +  mkTypes @"08"  8 `appendTypes`
 +  mkTypes @"09"  9 `appendTypes`
 +  mkTypes @"10" 10 `appendTypes`
 +  mkTypes @"11" 11 `appendTypes`
 +  mkTypes @"12" 12 `appendTypes`
 +  mkTypes @"13" 13 `appendTypes`
 +  mkTypes @"14" 14 `appendTypes`
 +  mkTypes @"15" 15 `appendTypes`
 +  mkTypes @"16" 16

testsuite/tests/perf/compiler/all.T

@@ -87,6 +87,13 @@ test('T783',
        ],
        compile,[''])
 +test ('T26426'
 +     , [ only_ways(['normal'])
 +       , collect_compiler_stats('bytes allocated',4) ]
 +     , compile
 +     , ['']
 +     )
++
  test('T5321Fun',
       [ only_ways(['normal']),  # no optimisation for this one
         collect_compiler_runtime(2),