Typechecker plugins: request for review and another workflow question

[Adam Gundry]

I think we're converging on a reasonable story about the way to call
plugins for givens and for wanteds; it's a shame they don't quite match
up, but I think that is probably unavoidable and relatively harmless.

On 17/11/14 17:11, Eric Seidel wrote:
> Ah, good catch on both accounts, thanks!
> 
> Re "solving" givens: although the interface requires the plugins to
> provide an evidence term, the end result would be that the given is
> discarded entirely, correct? If so, we should probably caution plugin
> authors not to solve any givens they can't easily re-derive later, but
> perhaps this is obvious.. Apart from that concern, it seems reasonable,
> and could potentially reduce the amount of work GHC has to do. 

Yes, that's right, it makes sense to discard a given only if it can be
re-derived (and hence is providing no new information). This happens in
the vanilla constraint solver, for example reflexive given equations are
discarded. When reporting errors, it's nice to omit obviously boring
constraints!

> Ping me if you want to offload any work, I'm also very keen to get this
> landed before the 7.10 branch!

I'd be very grateful if you could try out my latest commit to
wip/tc-plugins-amg and tell me if it makes sense or if I'm doing
something silly. The code could do with a bit of tidying up, including
cleaning up the diff to master, which I'll try to get done tomorrow,
unless you want to jump in first. ;-)

Cheers,

Adam


> On Mon, Nov 17, 2014, at 08:36, Adam Gundry wrote:
>> 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/