and then realised that no flattening at all means also no flattening of [W]anteds.
Now, let's say I have a type family called "Magic" for which I want to write a constraint solver plugin; and some type family "Foo" and "Bar"
And then lets say we start out with an original [W]anted: Foo (Magic 8) ~ Bar 42
Then if I understand flattening correctly, that would get flattened to:
[w] Magic 8 ~ fmv1
[w] fmv1 ~ 42
[w] Foo fmv1 ~ fmv2
[w] fmv2 ~ Bar fmv1
Correct?
So currently, with flattened wanted, all a constraint solver plugin has to do is look for [w]anted where the head of the type family application is "Magic", [w] Magic 8 ~ fmv1.
Then perhaps do some substitution for fmv1 to get back [w] Magic 8 ~ 42, use its internal solving rules to reduce Magic 8 to 42, and conclude what "[w] 42 ~ 42" can be solved by reflexivity.
But in a version without flattening, all we would see is:
[W]
Foo (Magic 8) ~ Foo 42
And all I can do is to traverse the entire [W]anted, look for type family applications of "Magic" an then improve to:
[W] Foo 42 ~ Bar 42
Now... I can't declare that [W]anted solved, because i have no idea what Foo and Bar do (they might also be type families that can only be solved through constraint solver plugins).
A) A set of contradictions
B) A set of solved [W] constraints + A set of new [W] constraints
With the above API, the only way to move forward is to: 1) declare "[w] Foo (Magic 8) ~ Bar 42" solved, while at the same time emitting a new wanted "[w] Foo 42 ~ Bar 42"
But it's basically the same wanted... so I would like a function of type "updateWantedType :: Ct -> TcPredType -> Ct" (which I don't think exists in the current GHC API)
But you might think the above way of working with the constraint solver as a plugin write, where we "solve" a wanted, only to emit an "improved" wanted, is _not_ the way things should work.
If that's the case, how do you envision plugin writers interacting with the solver?
Note that the above way of interacting with the constraint solver, "solving" + emitting "improved", is something I already sorta do, but in a different context:
In "ghc-typelits-natnormalise", when asked to solve [w] "a + Foo b ~ Foo b + c", I solve it, but then immediately emitting "[w] a ~ c".
-- Christiaan