Deep Subsumption

[mpickering]

The proposal has been accepted; the following discussion is mostly of historic interest.

---

The simplified subsumption proposal argued in favour of simplifying the subsumption judgement in GHC's type system, by removing:

• Covariance and contravariance of function types
• Deep skolemisation
• Deep instantiation.

The change was motivated by wanting to simplify both the implementation and language semantics, as well as being a stepping-stone to the implementation of Quick-look impredicativity.

Unfortunately, the breakage study failed to accurately predict how annoying this change would be to users. Some common patterns found in libraries now require eta-expansion, when the compiler used to automatically insert the appropriate lambdas.

This proposal suggests adding a new language extension, DeepSubsumption, enabled by default in the common case when the language is set to -XHaskell2010, which recovers the previous subsumption rules. This would allow users to opt-in to deep subsumption as it was before GHC-9.0.

Rendered

[serras]

As I stated in the “Simplified Subsumption” thread, I really wonder whether adding this back makes sense, once the ecosystem has already moved to 9.0. Do we expect libraries to support “ghc < 9 && >= 9.6”, to give an example?

[serras]

(Ok, I see now that at the end of the proposal my comment is added. Still, I think it’s worth discussing that particular point, what exactly we gain by reintroducing the change now)

[parsonsmatt]

I'd love this. Would immediately enable it and start using it again as soon as I could.

[phadej]

@serras, ecosystem has moved, but industrial users may well be on still ghc-8.x. Also these codebases are usually compatible with single GHC version only, so they very well could prefer DeepSubsumption over ImpredicativeTypes, if there were a choice.

[phadej]

There is no link to rendered version in the description.

[gbaz]

Also these codebases are usually compatible with single GHC version only, so they very well could prefer DeepSubsumption over ImpredicativeTypes, if there were a choice.

As I motivated in that proposal, I'd much prefer a feature that gives the functionality users want (type aliases able to abstract well over "floating" constraints) on purpose, rather than one that only gave it sort of accidentally, most of the time, due to some very quirky decisions.

[Gabriella439]

My understanding is that one reason (not the only reason) behind the simplified subsumption was to reduce the complexity of the compiler, but if you guarded the old logic behind a language pragma then wouldn't you need to preserve that complexity so long as that language pragma were supported?

There were other reasons for simplified subsumption, like semantic correctness, but as a language implementer I do appreciate the value of reduced implementation complexity and I feel that it would be a shame to reintroduce that complexity given that the cost of simplified subsumption seems to have been paid down by the community at this point.

Also, keep in mind that I don't know if the simplification to GHC's implementation materialized as a result of the simplified subsumption change, so I could be off base on this point and there might not be a downside to this proposal.

[Bodigrim]

I support the proposal, foremost because it is important to send a signal to the community that GHC cares and takes responsibility for the breakage caused, once it was recognized that the impact assessment was incomplete.

[Ericson2314]

Exactly agree with @Bodigrim. Even if we deprecate -XDeepSubsumption and remove it soon after, do what @gbaz says instead of this long term, etc. etc., it is right and proper to still do this now for community reasons.

I am squarely team "Haskell needs a lot of breaking changes", and I don't like how deep subsumption before and with this proposal messes up the operational semantics, but in order to make the amount of breaking changes I'd like to see happen politically feasible, we must always have nice and proper deprecation cycles.

[simonpj]

There were other reasons for simplified subsumption, like semantic correctness, but as a language implementer I do appreciate the value of reduced implementation complexity and I feel that it would be a shame to reintroduce that complexity given that the cost of simplified subsumption seems to have been paid down by the community at this point.

I'm happy to say that the implementation changes are

• modest (a couple of hundred lines)

and, crucially,

• highly localised, so the tax is paid in one place, rather than making lots of things more complicated.

You can see for yourself. Here's the patch: https://gitlab.haskell.org/ghc/ghc/-/merge_requests/8210. (It will need a substantial Note to explain it.)

The reasons to be cautious about DeepSubsumption (and why I think that Simplified Subumption was a good change, for all its pain) are laid out in Section 2.1

[goldfirere]

This proposal has rather little cost for those that don't use it, but it has potentially huge gain for those that do -- especially if simplified subsumption broke their API. So I'm personally going to listen more to people who say "yes, thank you, I'll use this" than those that say "is this really the best design? I won't use it". I'd also pay close attention to "I really want to use this, but the design doesn't fit my use case. Could we do X instead?"

Is it strange to have deep subsumption in a bunch of releases, then missing from a few, and then back? Yes, absolutely.

Is deep subsumption just plain wrong to begin with? I tend to think so.

But will this proposal make some people happy (and make their code better in their opinion)? I think so, and happiness is important. This is why I favor doing this.

[AntC2]

• We do not recommend that people use this feature [DeepSubsumption]. It makes the language more complicated and runtime performance less predictable.

It seems that where simplified subsumption broke stuff was gnarly bits inside packages. If a package continues to use DeepSubsumption, and I'm innocently importing/using it, will that cause "strange behaviour" in my calling program?

IOW will I have to understand these undesirable effects, even though my own code is simplified?

[simonpj]

It seems that where simplified subsumption broke stuff was gnarly bits inside packages

Yes, if a package uses gnarly things inside, but exports an API that doesn't have foralls to the right of arrows, the clients of that package are entirely unaffected by the package's choice of whether or not to use DeepSubsumption.

But if the package exports an API with forall to the right of an arrow, their clients must either use DeepSubsumption or be prepared to do judicious eta-expansion. Example 1 (from Section 3 of the proposal)

readFreqSumFile file = readFreqSumProd $ withFile file ReadMode fromHandle

This is in client code. Without DeepSubsumption they will have to write

readFreqSumFile file = readFreqSumProd $ withFile file ReadMode (\x -> fromHandle x)

[jberryman]

ecosystem has moved on

Curious has this actually been quantified?

Appreciate the proposal

[parsonsmatt]

Curious has this actually been quantified?

It would be very hard to do so - the entire reason why it was hard to do impact assessment is because we can still define these APIs for clients/end-users, it's the use-site that is broken. type SqlReadT m a = forall backend. SqlBackendCanRead backend => ReaderT backend m a compiles just fine with GHC 9.0, but any application that uses it will be broken.

Any company that has upgraded to GHC 9 has dealt with the migration. But I haven't deleted that type alias from the library, in part because we still support GHC 8.6, and in part because I've been hoping we'd be able to use it again.

[telser]

I added a small note to the proposal about the fact the extension will not be deprecated.

I definitely appreciate this and the points raised by others here that have made it clear to me this is the path that should be taken.

I've recommended acceptance to the committee.

This is great! Hope to see this work soon.

[mpickering]

Thanks Arnaud.

@mpickering Maybe you can implement Arnaud's typographical suggestions above.

Thanks @aspiwack, I have applied your two suggestions. Does this get merged now?

[aspiwack]

Not quite yet. It gets merged when the committee votes acceptance. I don't expect this to be controversial, I'll get back to you promptly.

I've asked the committee to vote on whether this should be backported to 9.2 or not, so I'll come back with the committee's recommendation for that as well.

[gridaphobe]

The User Guide says that -Wcompat is for warnings that will be enabled by default in the future. Is that the plan for -Wdeep-subsumption? If so, over what timeframe?

I also think it would be weird if we landed in a world where a language extension enabled a feature where all uses incur a warning. This proposal in particular seems to be motivated by pain felt by industrial users, who also tend to set -Werror to keep their code warning-free. Are we not just going to cause the same pain via the warnings?

[cdsmith]

I believe that -XPartialTypeSignatures is already a GHC extension that enables a feature, all of whose uses incur a warning. That said, I agree that it's weird, in that case as well as this one.

[gridaphobe]

@mpickering @simonpj I'm concerned by the requirement that clients must enable -XDeepSubsumption in order to gain the usability benefits. This is something we try to avoid. The language complexity cost should be paid by the library author, not the user.

Is there an alternative where a module M enables -XDeepSubsumption, and then either

1. all exported functions from M will have Deep Subsumption applied at call sites, or
2. specific functions (or specific arguments) can be marked as candidates for Deep Subsumption with some pragma?

[simonpj]

Is there an alternative where a module M enables -XDeepSubsumption, and then either

I'm sorry, but I have no idea how to achieve that, with reasonable complexity.

• We have no mechanism for exporting extensions along with particular functions
• Deep subsumption is a property of, well, the subsumption check, not of a particular function call

Doubtless these objections could be overcome, at the cost of a permanent tax on compiler complexity. But this proposal is intendended to be a mitigation of a mis-feature that users have (understandably) adopted. I'm content to have a couple of hundred lines of code in one place to support this mitigation. I am much, much, much less keen on investing in a brand new mechanism with unknown knock-on consequences (e.g. recompilation avoidance checks and hash summaries).

I agree this is less than ideal. It amounts to requiring libray authors to say "in your cabal file, if you depend directly on my library (i.e. call functions from it), then switch on -XDeepSubsumption". That doesn't sound too bad to me, although I accept that it is not as good as "do nothing".

[L-as]

What about when you want to use a library that uses it but don't want to enable it yourself? It's not like IHP, etc., are unusable, they're just less ergonomic.

[gridaphobe]

Is there an alternative where a module M enables -XDeepSubsumption, and then either

I'm sorry, but I have no idea how to achieve that, with reasonable complexity.

• We have no mechanism for exporting extensions along with particular functions
• Deep subsumption is a property of, well, the subsumption check, not of a particular function call

I’m not suggesting we export an extension, but attach a flag to the exported or annotated functions. The flag would

1. enable deep subsumption in a much more targeted way than a module-wide extension
2. be the responsibility of the library author to understand and apply to the relevant definitions

This feels rather like how we deal with OVERLAPPING or INLINE pragmas, both mechanically and in spirit, so it doesn’t seem like a new pattern to me.

I’m not sure about the implementation complexity of a pragma-based approach vs an extension-based approach. I can certainly imagine the pragma approach being significantly more involved and that might be reason enough to discard it.

But I wouldn’t go so far as to call deep subsumption a misfeature. It’s clearly serving a real use for advanced users in avoiding the need for explicit eta expands. We should try to solve that user-level problem in a good, integrated way.

[ChickenProp]

@gridaphobe it sounds like your suggestion would give a state of affairs where I might have two functions with the same type signature. And I try to call them with the same arguments. And one of these typechecks and the other doesn't, because of different extensions enabled in the modules they came from.

That seems pretty bad to me, if so.

[simonpj]

I’m not suggesting we export an extension, but attach a flag to the exported or annotated functions.

Yes, that's exactly what I'm concerned about. As I say above:

• We have no mechanism for exporting extensions along with particular functions. We do for instances, and it's a pervasive complication, affecting several data types, many functions, and recompilations avoidance hash-code generation. I am very un-keen to add all this complication to functions.

• Deep subsumption is a property of, well, the subsumption check, not of a particular function call. So even if we had a per-function flag, its not clear how to use it. Consider

  f (let v = ... in
     case v of
       True -> \y -> blah
       False -> g x)
  

  If f is one of these imported-and-labelled functions, we don't need to eta-expand f; we need to eta-expand the call to g, buried inside f's argument. I'm sure it's doable, but it would be a new and pervasive complication.

I can see three posssibilities:

1. Keep the status quo: no deep subsumption. That's the no-op, but it leave us with unhappy users.
2. Adopt the proposal. This continues to regard deep subsumption as a mis-feature (as did the committee when accepting the simple subsumption proposal), but puts in place a modest change to mitigate the effects of the change.
3. Adopt a new, and as yet unwritten, proposal that sees deep subsumption as a desirable feature (reversing the committee's earlier attitude), and puts in place language features to support it, perhaps along the lines you describe.

I think that (3) would be controversial. Speaking for myself I really do regard deep subsumption as a mis-feature, and I wish that I had not implemented it. (If I had not, we would not be having this conversation.) But I do not have a monopoly on truth and perhaps others would support (3).

Nevertheless I urge that we adopt (2) right now, and leave (3) for a subsequent conversation. No one is arguing against (2) -- the only debate is about whether we should go further. While it is not perfect, it gets us 80% of the way with 0% of the controversy. Moreover, we have a patch ready to go, just waiting for the commitee's blessing before it lands in a released GHC.

Nothing preclude someone proposing (3) as a separate proposal -- but adopting (2) allows us to offer immediate relief to users (which many of them have welcomed) while that debate takes place.

Would that be acceptable?

[parsonsmatt]

I'm totally fine with the language extension. The error message should be able to say whether or not deep subsumption would fix the issue and suggest that, and library authors can always say "For using this API, please enable DeepSubsumption"

[gridaphobe]

• We do for instances, and it's a pervasive complication, affecting several data types, many functions, and recompilations avoidance hash-code generation. I am very un-keen to add all this complication to functions.

Thanks, I did not realize how much complexity that added.

I can see three posssibilities:

1. Keep the status quo: no deep subsumption. That's the no-op, but it leave us with unhappy users.
2. Adopt the proposal. This continues to regard deep subsumption as a mis-feature (as did the committee when accepting the simple subsumption proposal), but puts in place a modest change to mitigate the effects of the change.
3. Adopt a new, and as yet unwritten, proposal that sees deep subsumption as a desirable feature (reversing the committee's earlier attitude), and puts in place language features to support it, perhaps along the lines you describe.

I think that (3) would be controversial. Speaking for myself I really do regard deep subsumption as a mis-feature, and I wish that I had not implemented it. (If I had not, we would not be having this conversation.) But I do not have a monopoly on truth and perhaps others would support (3).

I think we should distinguish between the user-visible behavior (I don't need to manually eta-expand my code to satisfy the typechecker) and the internal mechanism that drives the behavior (deep subsumption). Deep subsumption may be undesirable as an implementation strategy, but surely you agree that in an ideal world eta-expansion would not affect whether your program typechecks? We may not know how to achieve that in a satisfactory manner today, that's fine. I just don't want to write off the entire idea as undesirable.

I'm ok with accepting the proposal as-is to ease the pain felt by industrial users today.

[simonpj]

Deep subsumption may be undesirable as an implementation strategy, but surely you agree that in an ideal world eta-expansion would not affect whether your program typechecks?

Indeed! Impredicative polymoprhism is another example. Surely in an ideal world we would accept every single program that could be typed in System F. For example (\x. (x True, x "hello")) id should be typable, by inferring x :: forall a. a->a. But we don't know how to do that. I tried for 15 yrs, and at the end of that road found Quick Look. but even QL rejects that program. QL is a compromise: it accepts more programs than before, but not all the ones we could possibly want. (MLF goes further, at greater cost, but still doesn't get everything.)

Deep subsumption is more challenging still, because we'd have to go beyond System F to accept these programs without eta expansion! Absent type classes and evidence passing, one could imagine a system (more expresive than System F) in which we could accept deep-subsumptive programs without eta expansion. I don't know what that system is -- it's a research question -- and it'd be a radical chang to GHC's intermediate language. But the killer is that we do have evidence passing and type classes. With them, I don't know where to begin: so definitely a research question.

So yes, in an ideal world. But that ideal world is out of my immediate reach.

[aspiwack]

Dear all,

The committee has reach a conclusion, and this proposal is now accepted. As usual, I'll let @nomeata merge the PR.

[ChickenProp]

The proposal still says it's unresolved whether to backport to 9.2. Did the committee make a decision on that?

[aspiwack]

Oh! Thanks for flagging that. The committee is in favour of backporting to 9.2.

[mjrussell]

Im not sure how much feedback the committee gets on proposals like this after they've been accepted, but I just wanted to say that adding DeepSubsumption to GHC 9.2.4 had a significant & positive impact on upgrading a fairly large production codebase from 8.10.7 to 9.2.4. Now our team can take advantage of many of the benefits of 9.2 while we work on unwinding the DeepSubsumption required areas gradually from the codebase.

Everyone's efforts to advocate for this, get it merged into GHC and port the change to 9.2 made what is a tricky upgrade already due to breaking changes in libraries much smoother, so thank you very much!

[simonpj]

Im not sure how much feedback the committee gets on proposals like this after they've been accepted, but I just wanted to say that adding DeepSubsumption to GHC 9.2.4 had a significant & positive impact on upgrading a fairly large production codebase from 8.10.7 to 9.2.4. Now our team can take advantage of many of the benefits of 9.2 while we work on unwinding the DeepSubsumption required areas gradually from the codebase.

I'm delighted to hear this. Thanks for telling us!

[david-christiansen]

This has been implemented, right? Shouldn't it get the "Implemented" label?

[nomeata]

Thanks! (I thought I added it, but sometimes I close the tab to quickly :-))

[NorfairKing]

Feel free to ignore this message, I'm just leaving it here in case anyone else runs into a similar issue.

Could this be backported to GHC 9.0.2 ? I'm specifically asking because 9.0.2 is the default version in the latest NixOS release: https://search.nixos.org/packages?channel=22.05&show=ghc&from=0&size=50&sort=relevance&type=packages&query=ghc

Edit: To give more context. I'm trying to do a source-to-source transformation in this project: https://github.com/NorfairKing/dekking
The transformation involves transforming every expression a into something like id a.
I was under the assumption that that would be sound, but suddenly a bunch of code doesn't compile after this transformation.

Example:

data Example = Example {exampleString :: String}
  deriving (Show)


This type-checks:

exampleStringL :: Lens' Example String
exampleStringL = lens exampleString (\e s -> e {exampleString = s})


This doesn't:

exampleStringL :: Lens' Example String
exampleStringL = (id lens) exampleString (\e s -> e {exampleString = s}) 

Later edit:

It turns out -XImpredicativeTypes can get the second version to compile and is already in GHC 9.0.2.
That solves my problem. Feel free to ignore this comment.

[mpickering]

@NorfairKing There are not going to be any more releases in the 9.0 series, I would advise you upgrade to a nixpkgs snapshot which uses 9.2 as the compiler.