`std.contract.from_validator` is hard to use in statically typed code

[jneem]

std.contract.from_validator takes an argument of type Dyn -> [| 'Ok, 'Error { message | String | optional, notes | Array String | optional, } |], but it's annoying to produce a literal of that type. For example, consider

let
  IsZero = std.contract.from_validator (fun x => if x == 0 then 'Ok else 'Error { message = "blah" }
in
0 | IsZero

This runs ok, but as soon as I wrap it in (...) : _ it errors with

2 │   IsZero = std.contract.from_validator (fun x => if x == 0 then 'Ok else 'Error { message = "blah" })
  │                                                  ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ this expression
  │
  = Expected an expression of an enum type with the enum row `'Error { message | String | optional, notes | Array String | optional, }`
  = Found an expression of an enum type with the enum row `'Error { message : String }`
  = Could not match the two declarations of `Error`

Maybe this is another situation where we can use subtyping?

A work-around is to annotate the record type, like {message = "blah"} | { message, notes | optional } but that's a bit verbose. Also, I'm a little surprised that this annotation passes the typechecker despite not supplying a type for notes.

[yannham]

The rationale was that I expected people would use from_validator more in untyped code than in typed code, and thus that the well-typed alternative without optional values would be more cumbersome most of the time (that is, you have to always specify both message and notes, and it's also not forward-compatible with adding more fields in the future).

However, I do agree that it's annoying to use in statically typed code. The issue is that {message | String | optional, notes | Array String | optional} is currently not representable in the type system. That would be the first step: add optional fields. Then, it would indeed not be very hard to extend subtyping - especially now that we have the base implementation - such that {message : String} <: {message ?: String, notes ?: Array String}, and thus we could probably just change the type annotation of from_validator without breaking backward compatibility (or only in specific, easy-to-fix cases). Or implement something that is described in the original "merge type and term syntax RFC", which is that we could extract a static type from a contract when they have a specific form - in this case without even changing the contract annotation, it would be statically understood as {message ?: String, notes ?: Array String}. But that's a lot of non trivial steps to get there.

Another simpler solution is to have a statically typed variant from_validator_typed: Dyn -> [| 'Ok, 'Error { message : String, notes : Array String} |]. I think it's not the first time that it makes sense to have a dynamically typed wrapper and a statically typed wrapper of the same operator; we would just have to find a good naming scheme for where to put and find them easily and consistently.

As an aside, the easiest right now to just disable typechecking on such contract definitions is probably to write let IsZero | Dyn and call it a day, even if it's still annoying and verbose.

[yannham]

Also, I'm a little surprised that this annotation passes the typechecker despite not supplying a type for notes.

Note that by fundamental design of Nickel, a contract annotation disables the typechecker for the annotated term. So basically let = foo | "glorbug" 5 = null in [] passes the typechecker, although it doesn't make any sense. In particular, as long as the types match, the typechecker probably happily accepts let id : "glorbug" 5 -> "glorbug" 5 = fun x => x in (id foo : _) because it can prove that both contracts "glorbug" 5 are equal. As long as you don't actually try to destruct foo in a statically typed context, contracts are just opaque types for the typechecker, and it can compute equality in most basic cases.

[jneem]

Oh I see. For some reason I thought that annotating let x | Number = foo would let the typechecker assume that x: Number, not just make it ignore x's type altogether...

[yannham]

It's not really that it ignores x's type - if you use x elsewhere, it will be considered a Number. But it doesn't statically check that x has the type it says it has. If you want the latter, you can just use a standard type annotation.

[jneem]

Ok, so then I'm confused again that {message = "blah"} | { message, notes | optional } was enough to satisfy the typechecker, because that annotation is not the same as the expected type. Why am I not required to write

{message = "blah"} | { message | optional | String, notes | optional | Array String }

[yannham]

Ah, I didn't understand your question properly then, sorry. It shouldn't work, indeed. Could you provide the full example? One possibility that I see is the recent bug over contract equality that has been fixed in 1.8.1. It's the same code used for contract deduplication and to check for contract equality during typechecking, which used to equate any records that have the same fields basically.

[jneem]

It seems to have been the contract equality thing indeed. Updating to latest master raises an error as expected. Sorry about the noise!