Gets rid of typing rule for record identifiers

[mikesol]

Description of the change

Allows records with constrained terms to typecheck.

Checklist:

• Added a file to CHANGELOG.d for this PR (see CHANGELOG.d/README.md)
• Added myself to CONTRIBUTORS.md (if this is my first contribution)
• Linked any existing issues or proposals that this pull request should close
• Updated or added relevant documentation
• Added a test for the contribution (if applicable)

[mikesol]

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

module Main where

import Prelude
import Effect.Console (log)

data X a = X

x :: forall a. X a
x = X

type Y = { x :: X Int }

test :: forall m. Monad m => m Y
test = pure { x: x }

type Z t = forall x. t x -> (forall a. t a) -> t x

class C t where c :: Z t

instance cA :: C Array where
  c x _ = x

test2 :: forall m. Monad m => m { ccc :: Z Array }
test2 = pure { ccc: (c :: Z Array) }

main = log "Done"

yields

 The type 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, appearing in the type
                                                           
           { ccc :: Array x6 -> (forall a. ...) -> Array x6
           }                                               
                                                           
       
       in the expression { ccc: c cA
                         }          
       in value declaration test2

[natefaubion]

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.

[natefaubion]

test2 :: forall m. Monad m => m { ccc :: Z Array }
test2 = pure { ccc: (c :: Z Array) }

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

[mikesol]

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?

[natefaubion]

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.

[mikesol]

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?

[natefaubion]

There is no way to specifically have the compiler infer:

{ 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".

[garyb]

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. 😄

[JordanMartinez]

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

[natefaubion]

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

[purefunctor]

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.

[mikesol]

Yikes, my brief forays into the compiler always land me in hornets nests!! I don't think I'm the right person to get this PR over the finishing line - as it's a breaking change, someone with a bit more knowledge of the ecosystem should make the call if this is a good path forward. Or maybe ask about it on the next survey in ~6 mo?

…

On Mon, 22 Aug 2022, 23.35 Gary Burgess, ***@***.***> wrote: You've stumbled into something that we've talked about for years here @mikesol <https://github.com/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. 😄 — Reply to this email directly, view it on GitHub <#4380 (comment)>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/AAEAIJQWAS6RTWXZ55DDO7TV2PQBZANCNFSM57FKB2JA> . You are receiving this because you were mentioned.Message ID: ***@***.***>

[purefunctor]

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.