It looks like there are a couple regressions when removing this check, ie:

moduleMainwhereimportPreludeimportEffect.Console (log)dataXa =Xx::foralla.Xax =XtypeY={x::XInt}test::forallm.Monadm=>mYtest = pure { x: x }typeZt=forallx.tx-> (foralla.ta)->txclassCtwhere c::ZtinstancecA ::CArraywhere  c x _ = xtest2::forallm.Monadm=>m{ccc::ZArray}test2 = pure { ccc: (c::ZArray) }main = log"Done"

yields

 Thetype variable x, bound at                  tests/purs/passing/1110.purs:16:12 - 16:51 (line 16, column 12 - line 16, column 51)                has escaped its scope, appearingin thetype                                                                      { ccc :: Array x6 -> (forall a. ...) -> Array x6           }in the expression { ccc: c cA                         }in value declaration test2

That's correct, this check is not benign. I would expect there to be failures because it is no longer inferring polytypes in records. This test specifically tests what the rule is meant to support.

test2::forallm.Monadm=>m{ccc::ZArray}test2 = pure { ccc: (c::ZArray) }

I think this is an expected failure, not dissimilar fromrunST $ ..., as the polytype would have to be threaded through the record constructor and the call topure. It may work if you annotate the record as a whole, rather than justc.

If the rule currently provides inference for polytypes for records & if the PR causes a regression, maybe this PR isn't a good candidate for merging?

We don’t infer polytypes in records other than the special case of bare identifiers. I personally think this special case causes far more trouble than it’s worth.

I'm in a bit over my head as it's a part of the compiler I don't know well, but is there any way to avoid the regression while achieving the desired behavior?

There is no way to specifically have the compilerinfer:

{ wat: mempty }

{ wat :: forall a. Monoid a => a }

Given our current approach. Generally we do not infer polymorphism. We only let generalize at the top level. This is a special case for records which doesn't otherwise exist in any other construct in the language.

The way to fix this would be to push more information down as part of checking, so it could check this field as being polymorphic. This would require a better treatment of first-class polymorphism like QuickLook or "dynamic order elaboration".

You've stumbled into something that we've talked about for years here@mikesol, I'm not sure if you're aware of that / would pick it up from what Nate is saying. The fact that it will break some existing things is perhaps partially why nobody has gotten too much into it despite it being an occasional topic for a long time, but it doesn't necessarily mean we shouldn't do it.

I think the first time I remember a discussion about it was Phil saying he thought we should restrict record properties to monotypes in like 2014 when I met up with him in person. 😄

Just to clarify, this is a breaking change, right? As some code that currently compiles would likely no longer compile?

That's correct, this is necessarily a breaking change.

An adjacent change to this is#4376. Constructors were made to infer into monotypes to align with the typing rule here. In my changeset, I just hoisted up this predicate and added a special case for singleton constructors.

If we follow through with this change, we should also free the special case done for constructors in#835. Constructors inferring to monotypes instead of polytypes is currently a blocker for visible type applications. There's#4376 of course, which effectively just defers the hoisting for constructors.