Type checker plugin receives Wanteds that are not completely unflattened

changed milestone to %8.6.1

changed weight to 5

added Tbug Trac import typechecker labels

Looking at -ddump-tc-trace, the compiler flattens the wanteds and then zonks them before passing them to the plugin. However, the zonking pass makes a substitution that re-introduces the fsk var.

Actually, I'm starting to suspect that my plugin would be best off if GHC neither unflattened nor zonked the wanteds before invoking the plugin. Does that sound unreasonable? If not, let me know and I'll try to prepare a feature request ticket. Perhaps we could add an option to the API for a plugin to request that sort of treatment. Thanks.

I'm also seeing this trying to port uom-plugin to 8.4. Unfortunately I've got the details of how this works in GHC pretty well paged out, and I think the code may have evolved a bit since I worked on it.

The original thinking was to avoid bothering typechecker plugins with the complications of flattening and zonking, on the basis that sets (well, lists) of constraints are a simpler model to work with. But perhaps in practice the plugin interface is so low level that we would be better off doing as little as possible before handing constraints over to the plugin. Assuming we can make it relatively easy for the plugin to flatten/zonk if it wants to, that is...

I am surprised about those fsks. But if you want it in unflattened form then rather than fix the bug we can just refrain from flattening.

Would you like to send an email to ghc-devs to propose this change, explaining why? I'm fully open to whatever would be easiest for plugin authors.

Well, it rather depends on the plugin: my uom-plugin and other existing plugins were designed to work on the basis of receiving fully unflattened constraints, and at the time that seemed the simplest thing to get working. Of course it depends on what the plugin is doing as to which is simplest, so I can well understand nfrisby having an opposite preference in his case.

As I say, I don't mind terribly if the interface changes to supply unflattened constraints, provided there is a way to properly flatten them again in the plugin monad. That seems like it would require resolving this issue anyway, though?

Providing a way to flatten inside the plugin would be tricky I think. Better either to supply flattened or unflattened constraints. (I suppose we could offer both, with the plugin advertising which it wanted?)

In that case perhaps we should indeed offer both by adding a new field to TcPlugin with a boolean (or a more informative new data type)?

added plugins label

I've looked at why the plugin is seeing flattened givens. It has been this way for some time.

Currently, when we go "under" an implication constraint we flatten the Givens; and we only unflatten them when we've finished with that implication. When calling a plugin, we have Givens from a whole stack of enclosing implications, and none of them will be unflattened.

See the inert_fsks field of InertSet; and TcSMonad.unflattenGivens which uses that field to guide unflattening. You can see that unflattenGivens is called by nestImplicTcS which goes under an implication.

It's quite awkward to unflatten them, in fact... even accessing the unflattening info for the stack of implications would require extra plumbing.

Humph. How bad would it be just to document the status quo? Or to make it consistent by not unflattening the Wanteds either?

Originally plugins would see flattened givens but unflattened wanteds (https://ghc.haskell.org/trac/ghc/wiki/Plugins/TypeChecker#Callingpluginsfromthetypechecker). The issue here is that the wanteds are now sometimes not fully unflattened, isn't it?

If we were to provide only flattened wanteds, that might well be more consistent, but we're back to plugins needing to implement unflattening themselves...

My plugin is responsible for reducing some type families. Receiving flattened Wanteds appeals to me because all of the tyfam applications (except those under forall? hmmm) would be FunEq constraints, so I wouldn't have to seek them out in the types.

So perhaps if there were a separate mechanism for the plugin to declare a custom "reducer" for a type family, that might eliminate my interest in flattened Wanteds.

Another related quality of life improvement would be easier access to the unflattening substitution, e.g. without having to manually assemble the FunEq constraints. I'm not sure yet, but I think I'll eventually want to only unflatten certain "relevant" type families (and maybe other applications containing applications of those type families). (This is for givens too, not just Wanteds.)

The issue here is that the wanteds are now sometimes not fully unflattened, isn't it?

No, the reported issue (in the Description) is that a Given CFunEqCan remains. I believe that all Wanted CFunEqCans are removed.

It's inconsistent, I know, but hard to fix -- except by leaving the Wanted CFunEqCans too. Which might be useful for some...

Replying to [ticket:15147#comment:154250 simonpj]:

The issue here is that the wanteds are now sometimes not fully unflattened, isn't it?

No, the reported issue (in the Description) is that a Given CFunEqCan remains. I believe that all Wanted CFunEqCans are removed.

Perhaps I'm misunderstanding something, but as the Description shows, the plugin is being called with

 [WD] hole{co_a4or} {3}:: (F x_a4o6[tau:2] fsk_a4oc[fsk:0] :: *)
                           ~# (p_a4o2[sk:2] :: *) (CNonCanonical)

including the flatten-skolem fsk_a4oc. Shouldn't that be unflattened to give

 (F x_a4o6[tau:2] (G () ()) :: *) ~# (p_a4o2[sk:2] :: *)

aka (p ~ F x (G () ()))?

Replying to [ticket:15147#comment:154228 nfrisby]:

My plugin is responsible for reducing some type families. Receiving flattened Wanteds appeals to me because all of the tyfam applications (except those under forall? hmmm) would be FunEq constraints, so I wouldn't have to seek them out in the types.

So perhaps if there were a separate mechanism for the plugin to declare a custom "reducer" for a type family, that might eliminate my interest in flattened Wanteds.

I've wanted such a thing as well (some discussion here). It's not completely obvious what the right design is, though, because GHC's current type family reduction implementation is pure so it doesn't fit nicely with TcPluginM.

Perhaps I'm misunderstanding something

I didn't express it very clearly. As it stands, the Given CFunEqCan's remain, and hence so do the fsks. The Wanted CFunEqCans are removed (currently) along with the fmvs.

So yes, currently Wanteds can contain fsks, whose definition is given by a CFunEqCan. I would have thought that most plugins would not find it hard to deal with that.

That way of saying it clarifies the expectations for me. And doesn't seem too burdensome for the plugin author.

Thus I think this ticket could be resolved by updating the documentation. (Though I still would like for a plugin to be able to request the flattened Wanteds. Separate ticket?)

In particular this sentence in the User Guide

"[The plugin] will be invoked at two points in the constraint solving process: after simplification of given constraints, and after unflattening of wanted constraints."

would benefit from some elaboration. Specifically, "unflattening of wanted constraints" is somewhat ambiguous: until you spelled it out, I was thinking that if a constraint is flattened, it doesn't have any flattening variables in it. However, I'm inferring here that the jargon is used to mean that "unflattening a wanted constraint" only eliminates fmvs, possibly leaving fsks behind? That's what I've been confused about (until now, I think). Thanks.

To me it seems odd that we unflatten the Wanted CFunEqCans but not the Given ones. Indeed, it's not entirely clear how you can decide if a type-function call is in which class.

'''So perhaps it'd be more consistent to do no un-flattening whatsoever?''' (The alternative, of unflattening everything, is not easy to implement.) Since the plugins have to deal with flattened Givens, it's probably no harder to deal with unflattened Wanteds too.

I'd be interested in opinions.

Meanwhile, would you like to suggest concrete alternative wording for the user manual? I can fill in the blanks if you have any.

I agree with Simon here, I think it'd be more consistent if the plugins were always given the flattened constraints, as it seems simpler and more consistent.

Also, is it the case that un-flattening only substitutes in the variables that it introduces by flattening, and not all constraints that are in a similar form? More concretely, if I a programmer wrote x ~ F a, G x ~ G Int, then would un-flattening rewrite this to G (F a) ~ G Int or would it leave it as is? If the latter, then plugins should already be prepared to deal with this case, as it would be quite odd if the one form worked but the other didn't.

I agree: never unflatten, for simplicity and consistency.

if I a programmer wrote x ~ F a, G x ~ G Int, then would un-flattening rewrite this to G (F a) ~ G Int or would it leave it as is?

If these were Wanteds, un-flattening would not rewrite to G (F a) ~ G Int. (Wanteds do not rewrite Wanteds.) But if they were Givens, which we don't un-unflatten, we'd end up with

[G] F a ~ fsk1     CFunEqCan
[G] G fsk1 ~ fsk2  CFunEqCan
[G] G Int ~ fsk3   CFunEqCan
[G] fsk2 ~ fsk3    CTyEqCan
[G] x ~ fsk1       CTyEqCan

If we didn't unflatten Wanteds either, we'd get

[W] F a ~ fuv1     CFunEqCan
[W] G x ~ fuv2     CFunEqCan    -- NB: not rewritten by [W] x~fuv1
[W] G Int ~ fsk3   CFunEqCan
[W] x ~ fuv1       CTyEqCan
[W] fuv2 ~ fuv3    CTyEqCan

changed milestone to %8.8.1

These won't be addressed for GHC 8.6.

I now believe my work-in-progress plugin could be simpler, if a few parts of the plugin API changed. One of those is if the fsks and fmvs were both left in place in both Givens and in Wanteds; no extra unflattening before invoking plugins.

I have a related request: directly provide the list of all in-scope variables bound by the enclosing and current implications. This would include the flattening variables with their definitions (preferably in a topological order), instead of having to partition their defining constraints from the passed in Cts. In particular, it's awkward that some fsks are defined as an alias of another by a CTyEqCan, not by a CFunEq -- there is no CFunEq for such fsks, just the CTyEqCan. I'm not sure when this happens, but I'm definitely seeing it in GHC 8.6.2.

That list would also include skolem binders pretty easily -- the fsk, fmv, and skolem lists are already in data structures (implication, inert cans). Ideally the list would also include unification variables, but I don't think their list is maintained anywhere currently, so I imagine their might be a good reason for that.

But. If I had the unflattened constraints as-is from GHC, and a list of all in-scope type variables (incl covars?), my life as plugin author would be much easier. That would let me replace my type and coercion traversing code with just calls to the subst functions. My final ingredient for this wishlist would be for the subst* functions to indicate if they ever applied the passed-in substitution: I need to know if a substitution actually applied to a constraint. I could ask for free vars before substing, but that incurs a redundant traversal.

One of those is if the fsks and fmvs were both left in place in both Givens and in Wanteds; no extra unflattening before invoking plugins.

Great! That sounds in line with the proposal in ticket:15147#comment:154628. Would you like to socialise it with other plugin authors and check they are happy?

I have a related request: directly provide the list of all in-scope variables bound by the enclosing and current implications

It's not quite readily available, because we simply recurse in the solver, without putting the skolems anywhere accessible.

The right place would be in the InertSet (in TcSMonad). There is already a field for the flatten-skolems (fsks); you'd just need to add a field for the ordinary skolems. Not hard.

The fmv are more like unification variables; you can easily find them from the RHS of CFunEqCan wanteds/deriveds.

If you want to offer a patch, I'm sure Richard and I can offer guidance. I think we should concentrate on what GHC can easily do; we don't want to impose substantial overheads for the benefit of plugins that may not exist in the common case.

changed milestone to %8.10.1

Bumping milestones of low-priority tickets.

added typechecker plugins label

removed typechecker label

added Pnormal label

removed milestone

I think this can be closed, as the constraint solver no longer performs flattening?

Trac field	Value
Version	8.4.1
Type	Bug
TypeOfFailure	OtherFailure
Priority	normal
Resolution	Unresolved
Component	Compiler (Type checker)
Test case
Differential revisions
BlockedBy
Related
Blocking
CC	adamgundry
Operating system
Architecture

Type checker plugin receives Wanteds that are not completely unflattened

Child items ...

Activity