Check role declarations arity during type checking by kl0tl · Pull Request #4157 · purescript/purescript · GitHub
Skip to content

Check role declarations arity during type checking - #4157

Merged
JordanMartinez merged 5 commits into
purescript:masterfrom
kl0tl:check-role-declarations-arity-during-typechecking
Nov 16, 2021
Merged

Check role declarations arity during type checking#4157
JordanMartinez merged 5 commits into
purescript:masterfrom
kl0tl:check-role-declarations-arity-during-typechecking

Conversation

@kl0tl

@kl0tl kl0tl commented Jul 16, 2021 •
edited
Loading

Copy link
Copy Markdown
Member

Description of the change

As Jordan noticed in #4121 (comment) we incorrectly infer the arity of foreign data types whose kind contains parens (and type synonyms) while checking their role declaration arity. We ought to check role declarations arity during type checking, so that parens and type synonyms are desugared away.

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)

@kl0tl kl0tl mentioned this pull request Jul 16, 2021
Merged
4 of 5 tasks
@rhendric

rhendric commented Jul 16, 2021

Copy link
Copy Markdown
Member

@kl0tl
kl0tl force-pushed the check-role-declarations-arity-during-typechecking branch from 3d2134d to c66ae6d Compare July 16, 2021 23:56
kl0tl
kl0tl commented Jul 16, 2021
View reviewed changes
Comment thread tests/purs/failing/CoercibleRoleMismatch1.out Outdated

in role declaration for [33mIdentity[0m
in type constructor [33mIdentity[0m
in data binding group Identity

@kl0tl kl0tl Jul 16, 2021

Copy link
Copy Markdown
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Having foreign data type declarations depend on their role declaration in the binding group desugaring step would complicate self cycles detection, but this leaks in error messages since we do display that role declarations of data types belong to a binding group here. Is there a reason for not eliminating the hint for singleton binding groups?

@rhendric rhendric Jul 17, 2021

Copy link
Copy Markdown
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I might even go further and suggest that it should be eliminated whenever another hint narrows down the error to one declaration. Maybe there should be a hint category for top-level declarations or something?

@kl0tl kl0tl Jul 17, 2021

Copy link
Copy Markdown
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I introduced a category for declaration hints.

@kl0tl

kl0tl commented Jul 16, 2021

Copy link
Copy Markdown
Member Author

I applied your suggestion. This was slightly more involved than expected because we need to know all the role declarations of data binding groups when inferring roles of mutually recursive data types, but it is nice to remove declared roles from the environment and to position RoleMismatch errors accurately!

This was referenced Jul 17, 2021
Merged
Merged
@JordanMartinez

JordanMartinez commented Jul 21, 2021

Copy link
Copy Markdown
Contributor

This now has a merge conflict:

<<<<<<< check-role-declarations-arity-during-typechecking
  go d@(ExternDataDeclaration _ name kind) = do
    elabKind <- withFreshSubstitution $ checkKindDeclaration moduleName kind
    env <- getEnv
    let qualName = Qualified (Just moduleName) name
        roles = nominalRolesForKind elabKind
    putEnv $ env { types = M.insert qualName (elabKind, ExternData roles) (types env) }
    return d
=======
  go d@(ExternDataDeclaration (ss, _) name kind) = do
    warnAndRethrow (addHint (ErrorInForeignImportData name) . addHint (positionedError ss)) $ do
      elabKind <- withFreshSubstitution $ checkKindDeclaration moduleName kind
      env <- getEnv
      let qualName = Qualified (Just moduleName) name
      -- If there's an explicit role declaration, just trust it
      let roles = fromMaybe (nominalRolesForKind elabKind) $ M.lookup qualName (roleDeclarations env)
      putEnv $ env { types = M.insert qualName (elabKind, ExternData roles) (types env) }
      return d
>>>>>>> master

@JordanMartinez

JordanMartinez commented Jul 23, 2021

Copy link
Copy Markdown
Contributor

CI builds again. Any other feedback on this PR?

JordanMartinez
JordanMartinez suggested changes Nov 13, 2021
View reviewed changes

@JordanMartinez JordanMartinez left a comment

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I think this is good to go aside from the one issue raised below.

Comment thread src/Language/PureScript/TypeChecker/Roles.hs

@JordanMartinez JordanMartinez Nov 13, 2021

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I think this error message could be improved to indicate which type parameter's role was wrong in a declaration with 2+ role annotations. For example, looking at this error message

... the source spans indicates the entire role declaration. They do not indicate which role declaration has the issue.

If I have the following example,

data Foo a b c d = Foo a b c

type role Foo representational phantom representational phantom

and b is the one with the bad role, the error message wouldn't tell me which of the four values above is wrong.

@JordanMartinez JordanMartinez Nov 16, 2021

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

On second thought, the issue above is a separate issue. This PR AFAICT accomplishes its goal of checking for arity. I'll retract this.

@JordanMartinez
JordanMartinez merged commit 375bcdc into purescript:master Nov 16, 2021
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@rhendric rhendric rhendric left review comments
+1 more reviewer
@JordanMartinez JordanMartinez JordanMartinez approved these changes
Reviewers whose approvals may not affect merge requirements

Assignees

No one assigned

Labels

None yet

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

3 participants

@kl0tl @rhendric @JordanMartinez