search

tweag / nickel

Better configuration for less
https://nickel-lang.org/
MIT License
2.43k stars 93 forks source link

Record row polymorphism can be destructive #2014

Closed cydparser closed 3 months ago

cydparser commented 3 months ago

Describe the bug

A function with type forall tail. { a : Number ; tail } -> { a : Number ; tail } can remove the record tail from the returned value.

To Reproduce

Evaluate the following expression:

let f : forall tail. { a : Number ; tail } -> { a : Number ; tail }
  = fun o => o
  in f { a = 1, b = ".." }

The result is { a = 1, }.

Expected behavior

I expect a result of { a = 1, b = ".." }.

Environment

yannham commented 3 months ago

This hasn't been caught earlier, which is embarrassing. This bug was already present in 1.7. It seems to be related to the contract elision optimization (which avoids some dynamic check when a function is statically typed), because turning the type annotation to a | works as expected.

Having fields that mysteriously disappear from your record silently is surely not going to be fun to debug. Thanks a lot for catching this, will include a fix in the imminent 1.8 release.

yannham commented 3 months ago

I confirm that static contract elision is the culprit. It simplifies the signature in the example to the contract forall tail. Dyn -> {a: Number; tail}, which has an unseal operation after the function returns but doesn't have the symmetric sealing operation anymore. Contracts optimizations are too aggressive (we can't just throw an entire record type just because it's in positive position). A fix in on the way.