Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Support for ghc-9.2 #35

Open
wants to merge 4 commits into
base: main
Choose a base branch
from
Open

Support for ghc-9.2 #35

wants to merge 4 commits into from

Conversation

gelisam
Copy link
Owner

@gelisam gelisam commented Mar 15, 2023

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

.github/workflows/ci.yml Outdated Show resolved Hide resolved
.github/workflows/ci.yml Outdated Show resolved Hide resolved
package.yaml Outdated Show resolved Hide resolved
stack.yaml Outdated
@@ -1,7 +1,7 @@
resolver: nightly-2020-12-10
resolver: nightly-2021-07-22
Copy link
Owner Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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

@@ -42,7 +42,7 @@ f5 :: forall a b x y
f5 = foo @(F a x)

f6 :: forall a b x y
. ( F a b ~ G x y
. ( b ~ G x y
Copy link
Owner Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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

Copy link
Owner Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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))

Copy link
Owner Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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.

Copy link
Owner Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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.

Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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

Copy link
Owner Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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).

Copy link
Owner Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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.

Copy link
Owner Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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!

Copy link
Owner Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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.

Copy link
Owner Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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
Copy link
Owner Author

gelisam commented Mar 15, 2023

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

According to my experiments in #36, renaming the CI config file
mysteriously allows CI to start running again!
@gelisam gelisam mentioned this pull request Mar 16, 2023
@sjoerdvisscher
Copy link

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

@gelisam
Copy link
Owner Author

gelisam commented Jan 18, 2024

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
Copy link

sjoerdvisscher commented Jan 19, 2024

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
Copy link
Collaborator

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

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

3 participants