Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Polymorphic record contracts should know which fields their row variables cannot contain #950

Closed
matthew-healy opened this issue Nov 28, 2022 · 1 comment

Comments

@matthew-healy
Copy link
Contributor

Consider the following program:

let f | forall r. { ; r } -> { x: Num; r } = fun r => %record_insert% "x" r 1 in f { x = 0 }

We know statically that the r row variable cannot contain the field x, and we return an error to that effect if we typecheck this code (by changing the end to (f { x = 0 } : _)).

However, after merging #949, the dynamic error for this is:

error: non mergeable terms
  ┌─ repl-input-1:1:78
  │
1 │ let f | forall r. { ; r } -> { x : Num; r } = fun r => %record_insert% "x" r 1 in (f { x = 0 })
  │                                                                              ^             ^ with this expression
  │                                                                              │              
  │                                                                              cannot merge this expression
  │
  = Both values have the same merge priority but they can't be combined

it should be possible to give a more detailed error message (e.g. "arguments to f cannot contain the field x"), by providing this information to the polymorphic record contract.

Radvendii added a commit that referenced this issue May 25, 2023
fixes #950 by calculating the fields disallowed in a parameterized tail
e.g. in `forall r. { x : Foo ; r }` `x` cannot be present in `r`
Radvendii added a commit that referenced this issue Jun 13, 2023
fixes #950 by calculating the fields disallowed in a parameterized tail
e.g. in `forall r. { x : Foo ; r }` `x` cannot be present in `r`
Radvendii added a commit that referenced this issue Jun 21, 2023
fixes #950 by calculating the fields disallowed in a parameterized tail
e.g. in `forall r. { x : Foo ; r }` `x` cannot be present in `r`
github-merge-queue bot pushed a commit that referenced this issue Jun 22, 2023
* blame caller when tail contains illegal fields

fixes #950 by calculating the fields disallowed in a parameterized tail
e.g. in `forall r. { x : Foo ; r }` `x` cannot be present in `r`

* make get_constraints() imperative and inline

* reorder match fields to reflect order they will be executed

* appease clippy

* recurse into record sub-types even if we are looking for enum tails

* NickelString has a From<Label> instance

* separate recursion from checking for constraints

* move constraint checking code to parser

we check for constraints in contract checking and type checking. by
moving it to the parser we only have to do it in one place.

also, removed constraint checking for enum rows, which doesn't seem to
have been doing anything and also we don't want it.
`[| 'x ; e |]` does not preclude `'x` showing up in `e`

added in VarKindDiscriminant for those places where we do actually just
want the enum type. This is mostly for error reporting.

* VarKindCellData -> Option<VarKind>

* update documentation

* fixup

* add tests

* address review comments
@Radvendii
Copy link
Member

Fixed in #1323

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
Development

No branches or pull requests

2 participants