Type checker plugin receives Wanteds that are not completely unflattened
With the following, a plugin will receive a wanted constraint that includes a fsk
flattening skolem.
-- "Reduced" via the plugin
type family F u v where {}
type family G a b where {}
data D p where
DC :: (p ~ F x (G () ())) => D p
(Please ignore the apparent ambiguity regarding x
; the goal is for the plugin to eliminate any ambiguity.)
A do-nothing plugin that merely logs its inputs gives the following for the ambiguity check on DC.
given
[G] $d~_a4oh {0}:: (p_a4o2[sk:2] :: *)
~ (p_a4o2[sk:2] :: *) (CDictCan)
[G] $d~~_a4oi {0}:: (p_a4o2[sk:2] :: *)
~~ (p_a4o2[sk:2] :: *) (CDictCan)
[G] co_a4od {0}:: (G () () :: *)
~# (fsk_a4oc[fsk:0] :: *) (CFunEqCan)
[G] co_a4of {0}:: (F x_a4o3[sk:2] fsk_a4oc[fsk:0] :: *)
~# (fsk_a4oe[fsk:0] :: *) (CFunEqCan)
[G] co_a4og {1}:: (fsk_a4oe[fsk:0] :: *)
~# (p_a4o2[sk:2] :: *) (CTyEqCan)
derived
wanted
[WD] hole{co_a4or} {3}:: (F x_a4o6[tau:2] fsk_a4oc[fsk:0] :: *)
~# (p_a4o2[sk:2] :: *) (CNonCanonical)
untouchables [fsk_a4oe[fsk:0], fsk_a4oc[fsk:0], x_a4o3[sk:2], p_a4o2[sk:2]]
Note the fsk_a4oc[fsk:0]
tyvar in the Wanted constraint, which is why I'm opening this ticket. Its presence contradicts the "The wanteds will be unflattened and zonked" claim from https://ghc.haskell.org/trac/ghc/wiki/Plugins/TypeChecker#Callingpluginsfromthetypechecker section.
Trac metadata
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 |
No child items are currently assigned. Use child items to break down this issue into smaller parts.
Link issues together to show that they're related or that one is blocking others. Learn more.
Activity
- nfrisby changed weight to 5
changed weight to 5
- nfrisby added Tbug Trac import typechecker labels
added Tbug Trac import typechecker labels
- Author
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. - Author
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.
- Developer
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...
- Developer
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.
- Developer
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?
- Developer
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?)
- Developer
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)? - Adam Gundry added plugins label
added plugins label
- Developer
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 ofInertSet
; andTcSMonad.unflattenGivens
which uses that field to guide unflattening. You can see thatunflattenGivens
is called bynestImplicTcS
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?
- Developer
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...
- Author
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.)
- Developer
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 WantedCFunEqCans
are removed.It's inconsistent, I know, but hard to fix -- except by leaving the Wanted
CFunEqCans
too. Which might be useful for some... - Developer
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 WantedCFunEqCans
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 () ()))
? - Developer
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
. - Developer
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.
- Author
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.
- Developer
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.
- Developer
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 toG (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. - Developer
I agree: never unflatten, for simplicity and consistency.
- Developer
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
- Ben Gamari changed milestone to %8.8.1
changed milestone to %8.8.1
- Maintainer
These won't be addressed for GHC 8.6.
- Author
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
Ct
s. In particular, it's awkward that some fsks are defined as an alias of another by aCTyEqCan
, not by aCFunEq
-- there is noCFunEq
for such fsks, just theCTyEqCan
. 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 thesubst*
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. - Developer
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?
- Developer
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
(inTcSMonad
). 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.
- Ömer Sinan Ağacan changed milestone to %8.10.1
changed milestone to %8.10.1
- Maintainer
Bumping milestones of low-priority tickets.
- Ben Gamari added typechecker plugins label
added typechecker plugins label
- Ben Gamari removed typechecker label
removed typechecker label
- Ben Gamari added Pnormal label
added Pnormal label
- Ben Gamari removed milestone
removed milestone
- Developer
I think this can be closed, as the constraint solver no longer performs flattening?