Opened 16 months ago

Last modified 9 months ago

#15147 new bug

Type checker plugin receives Wanteds that are not completely unflattened

Reported by: nfrisby Owned by:
Priority: normal Milestone: 8.10.1
Component: Compiler (Type checker) Version: 8.4.1
Keywords: TypeCheckerPlugins Cc: adamgundry
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: None/Unknown Test Case:
Blocked By: Blocking:
Related Tickets: Differential Rev(s):
Wiki Page:

Description

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.

Change History (24)

comment:1 Changed 16 months ago by nfrisby

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.

comment:2 Changed 16 months ago by nfrisby

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.

comment:3 Changed 16 months ago by adamgundry

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...

comment:4 Changed 16 months ago by simonpj

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.

comment:5 Changed 16 months ago by adamgundry

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?

comment:6 Changed 16 months ago by simonpj

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?)

comment:7 Changed 16 months ago by adamgundry

Keywords: TypeCheckerPlugins added; type checker plugins removed

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)?

comment:8 Changed 16 months ago by simonpj

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?

Last edited 16 months ago by simonpj (previous) (diff)

comment:9 Changed 16 months ago by adamgundry

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...

comment:10 Changed 16 months ago by 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.

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.)

comment:11 Changed 16 months ago by 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.

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

comment:12 in reply to:  11 Changed 16 months ago by adamgundry

Replying to 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 () ()))?

comment:13 in reply to:  10 Changed 16 months ago by adamgundry

Replying to 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.

comment:14 Changed 16 months ago by simonpj

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.

comment:15 Changed 15 months ago by nfrisby

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.

comment:16 Changed 15 months ago by simonpj

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.

comment:17 Changed 15 months ago by diatchki

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.

comment:18 Changed 15 months ago by goldfire

I agree: never unflatten, for simplicity and consistency.

comment:19 Changed 15 months ago by simonpj

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

comment:20 Changed 15 months ago by bgamari

Milestone: 8.6.18.8.1

These won't be addressed for GHC 8.6.

comment:21 Changed 9 months ago by nfrisby

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.

comment:22 Changed 9 months ago by simonpj

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 comment:16. Would you like to socialise it with other plugin authors and check they are happy?

comment:23 Changed 9 months ago by simonpj

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.

comment:24 Changed 9 months ago by osa1

Milestone: 8.8.18.10.1

Bumping milestones of low-priority tickets.

Note: See TracTickets for help on using tickets.