rewrite Given and Derived constraints too

[gelisam]

the rewrite rules are morally givens, and givens should be used to simplify givens, wanteds, and deriveds.

[gelisam]

afterwards, check if #3 is accepted or if yet more work is needed

[gelisam]

A useful tutorial on rewriting givens: https://youtu.be/sE1qWyQWWVY?t=1502

[gelisam]

@tscholak, can you paste your repro example?

[gelisam]

Here is the example @tscholak found:

type family F a b

type FLaw a b = F a (F a b) ~ F a b

f :: forall a b. Foo (F a (F a b)) => ()
f = foo @(F a b)

[gelisam]

Hmm, we tried calling applyRules on the givens, but that led the typechecker into an infinite loop as ghc immediately undid our changes.

The code on which the plugin runs is:

f7 :: forall a b. Foo (F a (F a b)) => ()
f7 = foo @(F a b)

I would expect the plugin to receive

[G] Foo (F a (F a b))
[W] Foo (F a b)

or

[G] Foo fsk1
[G] F a b ~ fsk0
[G] F a fsk0 ~ fsk1
[W] Foo fsk0

and in both cases, I would expect the plugin to rewrite the first given to [G] Foo (F a b). What happens instead is that my plugin sees

[G] Foo fsk0
[G] F a b ~ fsk0
[G] F a fsk0 ~ fsk1
[W] Foo (F a0 (F a0 b0))

And the plugin rewrites the first given to [G] Foo (F a b), which ghc rewrites right back to [G] Foo fsk0.

There are two related mysteries:

1. Since f7 is given Foo (F a (F a b)), why is the first given equivalent to Foo (F a b) instead?
2. If the first given is already equivalent to Foo (F a b), why is the plugin trying to rewrite it to Foo (F a b)?

[gelisam]

I improved the pretty-printer, and now I get:

[G] Foo (F a (F a b))  -- rewritten to Foo (F a b)
[G] F a b ~ F a b
[G] F a (F a b) ~ F a (F a b)

So mystery 1 is solved (my old pretty printer is apparently not very good), and mystery 2 is solved as well (it's a genuine rewrite). But now we're left with a new mystery: why does ghc rewrite Foo (F a b) back to Foo (F a (F a b))? My guess is that it doesn't; I am probably accidentally rewriting Foo (F a (F a b)) to a non-canonical version of itself, which ghc immediately canonicalize, and then my plugin runs again on the same input.