Opened 5 months ago

Last modified 4 months ago

#15147 new bug

Type checker plugin receives Wanteds that are not completely unflattened

Reported by: nfrisby Owned by:
Priority: normal Milestone: 8.8.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 (20)

comment:1 Changed 5 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 5 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 5 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 5 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 5 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 5 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 5 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 5 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 5 months ago by simonpj (previous) (diff)

comment:9 Changed 5 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 5 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 5 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 5 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 5 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 5 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 4 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 4 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 4 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 4 months ago by goldfire

I agree: never unflatten, for simplicity and consistency.

comment:19 Changed 4 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 4 months ago by bgamari

Milestone: 8.6.18.8.1

These won't be addressed for GHC 8.6.

Note: See TracTickets for help on using tickets.