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.

Sign up for GitHub

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
+15 −4
Open

Support for ghc-9.2 #35

Show file tree
Hide file tree
Changes from 3 commits
Commits
Show all changes
4 commits
Select commit Hold shift + click to select a range
10f6831
Upper limit relaxation of ghc
junjihashimoto Apr 19, 2022
1a1e489
Fix a test for ghc9.2
junjihashimoto May 16, 2022
4176e10
Update package.yml
junjihashimoto Oct 21, 2022
e5d98e7
rename CI config file
gelisam Mar 15, 2023
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 1 addition & 1 deletion package.yaml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -25,7 +25,7 @@ dependencies:
library:
source-dirs: src
dependencies:
- ghc >= 8.10.2 && <9.1
- ghc >= 8.10.2 && <9.4
- containers >= 0.6.2.1
- term-rewriting >= 0.3.0.1
- transformers >= 0.5.6.2
Expand Down
13 changes: 12 additions & 1 deletion src/TypeLevel/Rewrite/Internal/Lookup.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -6,8 +6,13 @@ import Data.Tuple (swap)

-- GHC API
import GHC (DataCon, TyCon, dataConTyCon)
#if MIN_VERSION_ghc(9,0,0)
#if MIN_VERSION_ghc(9,2,0)
import GHC.Iface.Load (cannotFindModule)
import GHC.Tc.Plugin (getTopEnv)
#elif MIN_VERSION_ghc(9,0,0)
import GHC.Driver.Finder (cannotFindModule)
#endif
#if MIN_VERSION_ghc(9,0,0)
import GHC (Module, ModuleName, mkModuleName)
import GHC.Plugins (mkDataOcc, mkTcOcc)
import GHC.Utils.Panic (panicDoc)
Expand Down Expand Up @@ -35,9 +40,15 @@ lookupModule moduleNameStr = do
Found _ module_ -> do
pure module_
findResult -> do
#if MIN_VERSION_ghc(9,2,0)
hscEnv <- getTopEnv
panicDoc ("TypeLevel.Lookup.lookupModule " ++ show moduleNameStr)
$ cannotFindModule hscEnv moduleName findResult
#else
dynFlags <- unsafeTcPluginTcM getDynFlags
panicDoc ("TypeLevel.Lookup.lookupModule " ++ show moduleNameStr)
$ cannotFindModule dynFlags moduleName findResult
#endif

-- 'TcPluginM.lookupM' unfortunately fails with a very unhelpful error message
-- when we look up a name which doesn't exist:
Expand Down
2 changes: 1 addition & 1 deletion test/should-compile/InstanceConstraints/Test.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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.

, y ~ x
, x ~ y
, Foo (F a b)
Expand Down
2 changes: 1 addition & 1 deletion typelevel-rewrite-rules.cabal
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -48,7 +48,7 @@ library
build-depends:
base >=4.12 && <5
, containers >=0.6.2.1
, ghc >=8.10.2 && <9.1
, ghc >=8.10.2 && <9.4
, ghc-prim >=0.5.3
, term-rewriting >=0.3.0.1
, transformers >=0.5.6.2
Expand Down