[GHC] #15147: Type checker plugin receives Wanteds that are not completely unflattened
#15147: Type checker plugin receives Wanteds that are not completely unflattened -------------------------------------+------------------------------------- Reporter: nfrisby | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.6.1 Component: Compiler | Version: 8.4.1 (Type checker) | Keywords: type checker | Operating System: Unknown/Multiple plugins | Architecture: | Type of failure: None/Unknown Unknown/Multiple | Test Case: | Blocked By: Blocking: | Related Tickets: Differential Rev(s): | Wiki Page: -------------------------------------+------------------------------------- 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#Callingpluginsfrom... section. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15147 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#15147: Type checker plugin receives Wanteds that are not completely unflattened -------------------------------------+------------------------------------- Reporter: nfrisby | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.6.1 Component: Compiler (Type | Version: 8.4.1 checker) | Keywords: type checker Resolution: | plugins Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (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. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15147#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#15147: Type checker plugin receives Wanteds that are not completely unflattened -------------------------------------+------------------------------------- Reporter: nfrisby | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.6.1 Component: Compiler (Type | Version: 8.4.1 checker) | Keywords: type checker Resolution: | plugins Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (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. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15147#comment:2 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#15147: Type checker plugin receives Wanteds that are not completely unflattened -------------------------------------+------------------------------------- Reporter: nfrisby | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.6.1 Component: Compiler (Type | Version: 8.4.1 checker) | Keywords: type checker Resolution: | plugins Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (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... -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15147#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#15147: Type checker plugin receives Wanteds that are not completely unflattened -------------------------------------+------------------------------------- Reporter: nfrisby | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.6.1 Component: Compiler (Type | Version: 8.4.1 checker) | Keywords: type checker Resolution: | plugins Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (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. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15147#comment:4 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#15147: Type checker plugin receives Wanteds that are not completely unflattened -------------------------------------+------------------------------------- Reporter: nfrisby | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.6.1 Component: Compiler (Type | Version: 8.4.1 checker) | Keywords: type checker Resolution: | plugins Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (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? -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15147#comment:5 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#15147: Type checker plugin receives Wanteds that are not completely unflattened -------------------------------------+------------------------------------- Reporter: nfrisby | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.6.1 Component: Compiler (Type | Version: 8.4.1 checker) | Keywords: type checker Resolution: | plugins Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (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?) -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15147#comment:6 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#15147: Type checker plugin receives Wanteds that are not completely unflattened -------------------------------------+------------------------------------- Reporter: nfrisby | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.6.1 Component: Compiler (Type | Version: 8.4.1 checker) | Keywords: Resolution: | TypeCheckerPlugins Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by adamgundry): * keywords: type checker plugins => TypeCheckerPlugins Comment: 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)? -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15147#comment:7 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#15147: Type checker plugin receives Wanteds that are not completely unflattened -------------------------------------+------------------------------------- Reporter: nfrisby | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.6.1 Component: Compiler (Type | Version: 8.4.1 checker) | Keywords: Resolution: | TypeCheckerPlugins Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (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? -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15147#comment:8 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#15147: Type checker plugin receives Wanteds that are not completely unflattened -------------------------------------+------------------------------------- Reporter: nfrisby | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.6.1 Component: Compiler (Type | Version: 8.4.1 checker) | Keywords: Resolution: | TypeCheckerPlugins Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by adamgundry): Originally plugins would see flattened givens but unflattened wanteds (https://ghc.haskell.org/trac/ghc/wiki/Plugins/TypeChecker#Callingpluginsfrom...). 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... -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15147#comment:9 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#15147: Type checker plugin receives Wanteds that are not completely unflattened -------------------------------------+------------------------------------- Reporter: nfrisby | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.6.1 Component: Compiler (Type | Version: 8.4.1 checker) | Keywords: Resolution: | TypeCheckerPlugins Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (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.) -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15147#comment:10 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#15147: Type checker plugin receives Wanteds that are not completely unflattened -------------------------------------+------------------------------------- Reporter: nfrisby | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.6.1 Component: Compiler (Type | Version: 8.4.1 checker) | Keywords: Resolution: | TypeCheckerPlugins Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (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... -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15147#comment:11 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#15147: Type checker plugin receives Wanteds that are not completely unflattened -------------------------------------+------------------------------------- Reporter: nfrisby | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.6.1 Component: Compiler (Type | Version: 8.4.1 checker) | Keywords: Resolution: | TypeCheckerPlugins Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by adamgundry): Replying to [comment:11 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 () ()))`? -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15147#comment:12 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#15147: Type checker plugin receives Wanteds that are not completely unflattened -------------------------------------+------------------------------------- Reporter: nfrisby | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.6.1 Component: Compiler (Type | Version: 8.4.1 checker) | Keywords: Resolution: | TypeCheckerPlugins Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by adamgundry): Replying to [comment:10 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 ([wiki:Plugins/TypeChecker#Underdiscussion:Definingtypefamilies 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`. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15147#comment:13 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#15147: Type checker plugin receives Wanteds that are not completely unflattened -------------------------------------+------------------------------------- Reporter: nfrisby | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.6.1 Component: Compiler (Type | Version: 8.4.1 checker) | Keywords: Resolution: | TypeCheckerPlugins Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (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. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15147#comment:14 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#15147: Type checker plugin receives Wanteds that are not completely unflattened -------------------------------------+------------------------------------- Reporter: nfrisby | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.6.1 Component: Compiler (Type | Version: 8.4.1 checker) | Keywords: Resolution: | TypeCheckerPlugins Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (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. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15147#comment:15 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#15147: Type checker plugin receives Wanteds that are not completely unflattened -------------------------------------+------------------------------------- Reporter: nfrisby | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.6.1 Component: Compiler (Type | Version: 8.4.1 checker) | Keywords: Resolution: | TypeCheckerPlugins Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (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. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15147#comment:16 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#15147: Type checker plugin receives Wanteds that are not completely unflattened -------------------------------------+------------------------------------- Reporter: nfrisby | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.6.1 Component: Compiler (Type | Version: 8.4.1 checker) | Keywords: Resolution: | TypeCheckerPlugins Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (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. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15147#comment:17 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#15147: Type checker plugin receives Wanteds that are not completely unflattened -------------------------------------+------------------------------------- Reporter: nfrisby | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.6.1 Component: Compiler (Type | Version: 8.4.1 checker) | Keywords: Resolution: | TypeCheckerPlugins Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by goldfire): I agree: never unflatten, for simplicity and consistency. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15147#comment:18 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#15147: Type checker plugin receives Wanteds that are not completely unflattened -------------------------------------+------------------------------------- Reporter: nfrisby | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.6.1 Component: Compiler (Type | Version: 8.4.1 checker) | Keywords: Resolution: | TypeCheckerPlugins Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (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 }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15147#comment:19 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#15147: Type checker plugin receives Wanteds that are not completely unflattened -------------------------------------+------------------------------------- Reporter: nfrisby | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.8.1 Component: Compiler (Type | Version: 8.4.1 checker) | Keywords: Resolution: | TypeCheckerPlugins Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (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 {{{Ct}}}s. 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. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15147#comment:21 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#15147: Type checker plugin receives Wanteds that are not completely unflattened -------------------------------------+------------------------------------- Reporter: nfrisby | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.8.1 Component: Compiler (Type | Version: 8.4.1 checker) | Keywords: Resolution: | TypeCheckerPlugins Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (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? -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15147#comment:22 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#15147: Type checker plugin receives Wanteds that are not completely unflattened -------------------------------------+------------------------------------- Reporter: nfrisby | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.8.1 Component: Compiler (Type | Version: 8.4.1 checker) | Keywords: Resolution: | TypeCheckerPlugins Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (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. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15147#comment:23 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
participants (1)
-
GHC