Support for ghc-9.2

[gelisam]

Creating a PR from the branch @junjihashimoto linked, to run CI, review the differences, and make a few adjustments.

[gelisam]

ghc-9.0 and ghc-9.2 both have LTSs by now, no need to use a nightly

[gelisam]

This looks suspicious. If the test has to be changed in order for the test to pass, that means the test is failing, no?

[gelisam]

I see that in ghc-9.2, the unmodified test fails with

    • Could not deduce (Foo (F a (G x x))) arising from a use of ‘foo’
      from the context: (F a b ~ G x y, x ~ y, Foo (F a b))
        bound by the type signature for:
                   f6 :: forall a b x y.
                         (F a b ~ G x y, y ~ x, x ~ y, Foo (F a b)) =>
                         ()
        at test/should-compile/InstanceConstraints/Test.hs:(44,1)-(50,8)
    • In the expression: foo @(F a (G x y))
      In an equation for ‘f6’: f6 = foo @(F a (G x y))

[gelisam]

The commit which introduces this test says:

test that substitutions also work with non-variables

the code only substitutes variables, but that's good enough because ghc
replaces nested calls to type families with fsk type variables whose
definition is in the type substitution.

The body of f6 is foo @(F a (G x y)), which requires a Foo (F a (G x y)) instance. The constraint F a b ~ G x y means that ghc could decide to simplify the requirement to Foo (F a (F a b)). This would allow the rewrite rule forall a b. F a (F a b) ~ F a b to fire, thus simplifying the requirement to Foo (F a b), which matches the given.

The difficulty is that ghc has no reason to choose to make that "simplification", because F a b is not in any way simpler than G x y. It is thus the job of typelevel-rewrite-rules to look at the available equality constraints and conclude that Foo (F a (G x y)) can be simplified to Foo (F a b).

In other words, this is a legitimate test. Changing the constraint from F a b ~ G x y to b ~ G x y completely changes the test:

1. b is simpler than G x y, so ghc is more likely to decide to make the simplification on its own, so the test no longer checks that typelevel-rewrite-rules is able to use the available equality constraints to look a few steps ahead.
2. Once ghc performs the simplification, we are left with Foo (F a b), which already matches the given without requiring typelevel-rewrite-rules to rewrite anything.

[gelisam]

Looking at the contents of typeSubst, the problem is clear: ghc-9.2 no longer replaces nested calls to type families with type variables named fskN. typelevel-rewrite-rules thus needs to work harder to determine whether rewrite rules should fire.

[junjihashimoto]

Thank you for your review.
The reason why hasktorch didn't generate an error was that this condition was not used by chance.

[gelisam]

I think we might also need to add a test where the expression to be substituted is inside a larger expression. Previously, with GHC separating all the sub-expressions, it was enough to check if the RHS of a fskN ~ F a b constraint matched the rewrite pattern, but it is now necessary to look deeper inside both the LHS and the RHS of F x (F a b) ~ G x (F a b).

[gelisam]

I need to remind myself [...] how we are currently distinguishing between ghc's unification variables and ours

The rewrite code is using two different substitution types:

type Subst = Map TyVar TypeTerm
type TypeSubst = [(TypeEq, TypeTerm)]

Beside the poor naming choice (both hold types, so the "Type" prefix doesn't clarify the difference between the two) and the accidental use of two different data structure, the main difference is the key type: TyVar is a type variable, while TypeEq can be any type... But the code assumes it's a type variable 🤦

The one which uses TyVar keys holds the replacements for the variables in the LHS of a rewrite rule, while the one which uses TypeEq keys holds the fsk1 ~ G x y constraints from GHC.

The fact that TypeEq allows arbitrary types as keys is what allows typelevel-rewrite-rules not to barf on ghc-9.2's F a b ~ G x y constraints: the key is now F a b. But that doesn't work because if the type expression to be rewritten contains an F a b, that part will be expanded to Fun "F" [Var "a", Var "b"] before the rewrite begins, and it is only at the leaves that the rewrite code checks whether "a" or "b" matches the key F a b. The substitution is thus not performed, and that's why the test fails on ghc-9.2.

[gelisam]

Taking a closer look, the data structure choice is not accidental at all! ghc simplifies the constraint F a b ~ G x y to two constraints, fsk1 ~ F a b and fsk1 ~ G x y. Normally an association list with duplicate keys just wastes space because Data.List.lookup stops after the first occurrence, but the rewrite code looks at all the possible substitutions. This has exponential cost, but has the benefit of being correct!

[gelisam]

It doesn't look like the rewrite code is carefully undoing the substitutions it performs when it encounters an fskN. If fsk1 ~ F a fsk2 and fsk2 ~ G x y, then when the rewrite code encounters Foo fsk1, it expands it to Foo (F a (G x y)), rewrites that to Foo (F a b), and then replaces the original Foo fsk1 with Foo (F a b). That seems to work fine, but I am now concerned that if ghc also knew that fsk2 ~ H u v, that information is now lost. So perhaps we should be more careful.

[gelisam]

Thinking about this further, there is no reason to expect that fsk2 ~ H u v should still hold. If the rewrite rules says that F a (F a b) should rewrite to F a, that's a claim about a property of F, it does not imply that the rewrite should be performed because F a b ~ F a. So I now think that the current code is correct, for pre-ghc-9.2 versions at least.

[gelisam]

sigh, why isn't CI running this time? This is my own PR!!

[sjoerdvisscher]

Hi, what's the status of this? I'd like to use it with ghc 9.6 and 9.8 :)

[gelisam]

Hi, what's the status of this?

I am not currently working on this, because my main goal was to get to a state where I could merge @junjihashimoto's ghc-9.0 PR. Once that succeeded, I put this MR on hold on order to focus on other priorities.

I'd like to use it with ghc 9.6 and 9.8 :)

Alas, this is a type-checker plugin, and is therefore tightly bound to the GHC internals, so some work is needed for each GHC version we want to support. Thus, even if I finished working on this ghc-9.2 branch, it would not help you much for ghc-9.6 nor for ghc-9.8. I can try to get this working with a more recent version of GHC, but probably not with all of ghc-9.2, ghc-9.6, and ghc-9.8. If you could only pick one GHC version, which one would you choose?

[sjoerdvisscher]

At the moment both 9.6 and 9.8 work equally well for me. Maybe with a slight preference for ghc 9.8 to be as future proof as possible. The use case is my proarrow library, to make working with monoidal categories, bicategories and double categories as easy as possible.

[junjihashimoto]

Hi, when ghc is 9.6, this patch is needed.
hasktorch@54d0871