Typechecker plugins: request for review and another workflow question

[Adam Gundry]

Thanks Eric!


On 16/11/14 19:33, Eric Seidel wrote:
> I've made a few changes based on your branch. Specifically I've
> removed the call to runTcPlugins inside solveFlats, and have replaced
> it with a specific runTcPluginsGiven that runs in a loop inside
> solveFlatsGiven much like your runTcPluginsFinal runs inside
> solveFlatsWanted. I think this is a bit cleaner given that you've
> split the wanteds-solving out already.
>
> The changes are at
https://github.com/gridaphobe/ghc/tree/wip/tc-plugins-els
> since I don't have commit access to GHC

I agree that it's better to split these out separately, if you and Iavor
are happy to work with only the unflattened constraints. I'm not
completely convinced by how solveFlatGivens/runTcPluginsGiven work now
though. It seems slightly odd that solveFlatGivens calls solveFlats and
runTcPluginsGiven with the same set of givens, even though solveFlats
might have simplified/discarded some.

Also, if I understand correctly, when a plugin generates new facts,
those will be added to the worklist directly, but also passed back in
the result Cts to be added to the worklist again. In the
solveFlatWanteds case, new facts are added to the worklist but not the
result Cts, which is fine.

Finally, I think the plugin should be allowed to "solve" given
constraints, just by discarding them (e.g. if the constraint is
something like "1 * x ~ x"). It's slightly odd that the interface
requires the plugin to provide an evidence term in this case, but the
evidence associated with the CtGiven (ctev_evtm) will do.

I'll put some commits together shortly to address these fine details.


> Iavor and I also have a question about your change to the last
> statement in solveFlatWanteds. You're putting the unsolved wanteds in
> a field called wc_flat, which suggests that they ought to be
> flattened. But the unsolved wanteds were just unflattened a few lines
> above! Is this a problem, or is the wc_flat field in need of a new
> name? :)

This is a slightly unfortunate clash of terminology. I believe wc_flat
is so named because the constraints are flat in the sense of "not
implications" rather than "contain no type family applications". This is
also the reason for the name "solveFlats".

Adam


-- 
Adam Gundry, Haskell Consultant
Well-Typed LLP, http://www.well-typed.com/