matchActualFunTy: FRR phase 2

This MR started off as a fix for #26072 (closed). It grew to contain a fair amount of fixes related to linear types, although some of those were eventually split off to separate MRs (in particular !14761 (closed)).

Motivation

At its core, the change to fix #26072 (closed) is quite straightforward: change the hasFixedRuntimeRep_syntactic call in matchActualFunTy into a hasFixedRuntimeRep call.

The problem is that this change alone causes GHC to panic in cases such as T17021; this is due to eta-expansion of data constructors for linear types as explained in Note [Typechecking data constructors].

Relation to deep subsumption

After discussing with Simon, we came up with a new story: instead of eta-expanding data constructors on their own, we eta-expand applications of data constructors inside tcApp, more precisely in tcCheckResultTy, the same place that deep subsumption is done (which already deals with eta-expansion). For example, in tc_sub_type_deep, when ty_actual ~ (a %1 -> b) and ty_expected ~ (a %Many -> b), we eta-expand.

To get this right, I had to restructure tc_sub_type_deep to deal with several situations it didn't deal with before (unrelated to linear types), as seen in #26225 (closed). Relatedly, I had to change the Infer case of tcCheckResultTy, to deal with #26225 (comment 628947) (and the corresponding issue with LinearTypes).

I also had to make a few changes to qlUnify to avoid it aggressively unifying types when doing a sub-type check would suffice.

This allows us to get rid of workarounds such as having two different types for a data constructor, with dataConWrapperType and dataConNonlinearType. This also fits in nicely with the "valid hole fits" approach, as that precisely does a subsumption check.

Changes to the simple optimiser

After that, I had to modify the simple optimiser to ensure that it can inline newtype constructors, because we rely on the pushCoercionIntoLambda logic to fire for representation-polymorphism checking, and that can only happen if the newtype constructor was unfolded into a lambda.

Changes to WpFun

Previous iterations of this MR struggled with the fact that the lambda abstractions introduced by WpFun change the evaluation semantics. After wrestling with this for a long time, we decided to simply not introduce WpFuns to deal with multiplicity subsumption, and instead use an unsafe One ~# Many "submultiplicity coercion". This improves compiler performance as the simplifier doesn't have to chew through so many lambdas.

TODOs

TODOs:

• Rebase over !14760 (closed) !14761 (closed) !14764 (closed).
• Investigate runtime regression in T10359. This was due to a change in inlining thresholds, which is fixed in !14701 (closed).
• Clean up the changes to wrapFamInstBody which avoid introducing a rep-poly lambda abstraction, and change the commit in which "Wrinkle [Unlifted newtypes with wrappers]" is added (currently it's in the "push coercion into lambda" commit).
• Fix AppIsHNF by being more careful about strictness when desugaring WpFun.
• Explain the new desugaring of WpFun (in Note [Desugaring WpFun]).
• Shore up the rule matching engine to be able to deal with cases/lets in various position to avoid massive perf regressions ("T3294 T4801").
• Figure out how to change the Core Lint checks to accept e.g. T17021.
• Investigate and fix Core Lint linearity failures in "LinearConstructors EtaExpandDataCon".
• Fix the simplifier falling over in T21650_{a,b}, now that the typechecker accepts these programs.
• Remove ad-hoc logic surrounding ConLikeTc. It should go back to how it was pre-9.0 (HsConLikeOut).
• Get rid of all the code related to the old approach for eta expansion of data constructors.
• Update Note [Polymorphisation of linear fields].
• Update Note [Typechecking data constructors].
• Update Note [The need for deep instantiation].
• Update Note [Multiplicity in deep subsumption].
• Write a Note to explain the changes to qlUnify.
• Figure out a better way to do representation polymorphism checking in tc_sub_type_deep.
• Update the comments around tcDeepSplitSigmaTy_maybe.
• There are a few tests which print out linear types for data constructors instead of normal Many arrows. This might be a regression, as we want to avoid printing linear arrows to the user unless we absolutely need to (or -XLinearTypes is enabled). Tests: ExplicitSpecificity2 T7627 TypeAppData T11721 T12550 T14796 ListTuplePunsPpr.
• Address TODO in commit for the new story of rep-poly unlifted newtypes.