record type modify functions are changed with pretty-printer roundtrip

[ceedubs]

If you edit the modify function for a record field, then save it without making any changes, it gets changed and the type is no longer recognized as a record type.

This means that if you work on a project by loading all of it into your scratch file, then all of your record types keep becoming non-record types.

Raw transcript

Click to view raw transcript

```` ```ucm:hide .> builtins.merge ``` Define a simple record type: ```unison unique type User = { id : Nat, name : Text } ``` ```ucm:hide .> add ``` It should now pretty-print as a record: ```ucm .> view User ``` But the `modify` function on record fields is changed with a pretty-printer roundtrip. This shouldn't prompt me to update: ```ucm .> edit User.id.modify .> load scratch.u ``` If I go ahead and do the update, then my type is no longer treated as a record: ```ucm .> update .> view User ``` ````

Transcript with output

Define a simple record type:

unique type User = {
  id : Nat,
  name : Text
}

  I found and typechecked these definitions in scratch.u. If you
  do an `add` or `update`, here's how your codebase would
  change:

    ⍟ These new definitions are ok to `add`:

      unique type User
      User.id          : User -> Nat
      User.id.modify   : (Nat ->{g} Nat) -> User ->{g} User
      User.id.set      : Nat -> User -> User
      User.name        : User -> Text
      User.name.modify : (Text ->{g} Text) -> User ->{g} User
      User.name.set    : Text -> User -> User

It should now pretty-print as a record:

.> view User

  unique type User = { id : Nat, name : Text }

But the modify function on record fields is changed with a pretty-printer roundtrip. This shouldn't prompt me to update:

.> edit User.id.modify

  ☝️

  I added these definitions to the top of
  /home/cody/code/unison/scratch.u

    User.id.modify : (Nat ->{g} Nat) -> User ->{g} User
    User.id.modify f = cases User id name -> User (f id) name

  You can edit them there, then do `update` to replace the
  definitions currently in this namespace.

.> load scratch.u

  I found and typechecked these definitions in scratch.u. If you
  do an `add` or `update`, here's how your codebase would
  change:

    ⍟ These names already exist. You can `update` them to your
      new definition:

      User.id.modify : (Nat ->{g} Nat) -> User ->{g} User

If I go ahead and do the update, then my type is no longer treated as a record:

.> update

  ⍟ I've updated these names to your new definition:

    User.id.modify : (Nat ->{g} Nat) -> User ->{g} User

.> view User

  unique type User = User Nat Text

[ChrisPenner]

We discovered that the pretty-printed type signature:

User.id.modify : (Nat ->{g} Nat) -> User ->{g} User
User.id.modify f = cases User id name -> User (f id) name

Has a different type signature than the generated 'modify'.

Entering any of the following will match the generated modify:

User.id.modify : (Nat ->{g} Nat) -> {} User ->{g} User
User.id.modify f = cases User id name -> User (f id) name

Or

User.id.modify : (Nat -> Nat) -> User -> User
User.id.modify f = cases User id name -> User (f id) name

Or

User.id.modify f = cases User id name -> User (f id) name

Possible courses of action:

• Change the pretty-printer so it doesn't alter the type signature
• Change the 'record field' detector so it accepts either
• Change the generated 'modify' function to match what is pretty-printed.

[ChrisPenner]

I write this:

foo1 f = cases Rec a -> Rec (f a)

Unison correctly infers as:

foo1 : (Nat ->{g} Nat) -> {} Rec ->{g} Rec

We edit foo1, it prints as:

foo1 : (Nat ->{g} Nat) -> Rec ->{g} Rec
foo1 f = cases Rec a -> Rec (f a)

Which infers as

foo1 : (Nat ->{g} Nat) -> {h} Rec ->{g} Rec

So we have a mismatch where the pretty-printer elides the empty ability list, the typechecker infers it as the polymorphic ability, but it's should simplify it down to the empty ability list at some point. It should simplify it to the empty ability list wherever possible while maintaining subtyping to be as general, and simple as possible.

[pchiusano]

@dolio See the above example - it seems we're somehow inferring a signature with an ability variable in strictly positive position (like inferring forall g . Nat ->{g} Nat instead of just Nat ->{} Nat). Where does it happen that we strip out useless ability variables? Is that just before pretty-printing, or do we do it for all inferred types coming out of the typechecker? If we're only doing it before pretty-printing, that might explain this.

If we infer a type, t with universally quantified ability variables, I believe we want to normalize that to t' where t' has the maximal number of ability variables replaced with {} while still being a subtype of the original t.

[pchiusano]

Also, note that if we implemented https://github.com/unisonweb/unison/issues/3753, we would just never infer a needless ability variable in the first place, so this situation wouldn't come up.

[ceedubs]

To anyone else who keeps getting bitten by this, here is an awk script that comments out all of the .modify functions in a scratch file.

[ceedubs]

@tstat @aryairani and I narrowed this down a bit. It's not really specific to records. Any function of the following form won't round-trip currently:

foo : (Nat ->{g} Nat) -> {} Nat ->{g} Text
foo _ n = Nat.toText n

The empty ability list on the second argument is elided, resulting in issues.

[aryairani]

Are the current type signature simplifying rules documented somewhere @pchiusano @dolio (I'd like them to be) and/or can you point us to the spot in the code where the changes happen? (Meaning the ones that hide effects to make the signature more digestible.)

I also like #3753; whatever approach we go with, we want to be careful about functions that could use abilities in a partial application (e.g. List.notMap : (a ->{g} b) -> [a] ->{g} [b] -> b).

But regardless, I'm pretty sure we always want signatures to round trip.

[aryairani]

The original issue as stated now seems to work. I'm not clear on whether there's a subsequent issue that needs follow up. @ceedubs WDYT?

Current transcript output / unison version: 5a7ce7d (built on 2024-04-25)

Define a simple record type:

unique type User = {
  id : Nat,
  name : Text
}

  Loading changes detected in scratch.u.

  I found and typechecked these definitions in scratch.u. If you
  do an `add` or `update`, here's how your codebase would
  change:

    ⍟ These new definitions are ok to `add`:

      type User
      User.id          : User -> Nat
      User.id.modify   : (Nat ->{g} Nat) -> User ->{g} User
      User.id.set      : Nat -> User -> User
      User.name        : User -> Text
      User.name.modify : (Text ->{g} Text) -> User ->{g} User
      User.name.set    : Text -> User -> User

It should now pretty-print as a record:

.> view User

  type User = { id : Nat, name : Text }

But the modify function on record fields is changed with a pretty-printer roundtrip. This shouldn't prompt me to update:

.> edit User.id.modify

  ☝️

  I added 1 definitions to the top of scratch.u

  You can edit them there, then run `update` to replace the
  definitions currently in this namespace.

.> load scratch.u

  Loading changes detected in scratch.u.

  I found and typechecked the definitions in scratch.u. This
  file has been previously added to the codebase.

User.id.modify : (Nat ->{g} Nat) -> User ->{g} User
User.id.modify f = cases User id name -> User (f id) name

If I go ahead and do the update, then my type is no longer treated as a record:

.> update

  Okay, I'm searching the branch for code that needs to be
  updated...

  Done.

.> view User

  type User = { id : Nat, name : Text }

[ceedubs]

Yeah this was fixed quite some time ago. #4232 is still horribly annoying when update or edit.namespace bring a lot of definitions into your scratch file, but that's a separate issue.