Deep dive for leak check/higher ranked fn ptr subtyping

[BoxyUwU]

Summary

I would like to have a deep dive to discuss

• subtyping of higher ranked fn ptrs and how its currently causing (soundness) problems
• the coherence leak check future compat lint which is highly related to the fn ptr subtyping and whether it is desirable to keep saying we will break the things it lints on
• potentially decide on whether relax leak-check rust#112999 is something we are comfortable doing and don't think it will break code that we want to work, although it is fine if we don't actually do this as my primary goal is to hopefully spread knowledge of the above two points which can be used in making decisions on the FCP in relax leak-check rust#112999

Rationale

rust-lang/rust#112999 has an FCP and it does relatively complicated changes to a future compat lint that atleast myself am rather unclear on whether its accurately stating breakage we want or not. Personally I tend to see this future compat lint as "buggy" rather than something we actually we want to turn into a hard error.

We also have an open soundness bug rust-lang/rust#97156 that is highly related to the changes that rust-lang/rust#112999 is making, some of the solutions to the soundness bug are even going in the opposite direction than rust-lang/rust#112999 and the future compat lint and explicitly wanting to allow those impls.

[BoxyUwU]

This deep dive will be taking place on 28/8/2023. It was scheduled here

[BoxyUwU]

this took place but imo did not have a satisfactory ending so not closing this

[BoxyUwU]

Things to cover in a future deep dive:

• Why is it okay for coherence to mistakenly believe types implement traits when they actually don't.
• Why do we think it will never cause issues in the future (assuming its currently okay) for intercrate mode to mistakenly believe types implement traits when they actually don't.
  • There have been some vague talkings of using intercrate mode for other things than coherence, just as a "the solver will only return Yes/No when its actually Yes/No"
• Current type equality of higher ranked fn ptrs causes soundness bugs in type_id and type_name: TypeId exposes equality-by-subtyping vs normal-form-syntactic-equality unsoundness. rust#97156. Some of the proposed solutions would actually make less fn ptrs types equal to each other which is the opposite of what this PR is trying to do. Are we comfortable with coherence and elsewhere having such a large difference (or any difference) in what counts as equality between two types.
  • Do we want to attempt alternate solutions for this soundness bug, i.e. adding a new trait like Sized which every type parameter is implicitly bounded by, that is not implemented for types syntactically containing higher ranked fn ptrs so that it is simply not possible to call type_id/type_name on them. (I have absolutely no idea how this would be possible to do in a backwards compatible way...) We should avoid making complex decisions about equality of higher ranked types without ensuring it will interact nicely with however TypeId exposes equality-by-subtyping vs normal-form-syntactic-equality unsoundness. rust#97156 is solved.
• the following issue: generalization is incomplete for aliases trait-system-refactor-initiative#8, details complexities surrounding generalization and aliases. One such issue involves aliases that are inside of types with binders and make use of the bound vars. One of the potential solutions detailed involves making universe errors in coherence be ambiguity not hard errors. This is effectively equivalent to making the coherence leak check lint a hard error. How does this potential solution interact with this PR, would we want to pick one of the other solutions for generalizing aliases under binders correctly if this PR goes through.
• Why these specific rules for what """implied bounds""" we consider the fn ptrs to have? Is there a logical justification for them specifically? They are completely inconsistent with what implied bounds we judge fn ptrs and fn signatures to have elsewhere.