Deciding type equality for two flat types (aka contracts aka opaque types)

[yannham]

Contracts (and more generally, even if that may be meaningless at runtime, any valid term) can appear inside a type annotation. The semantics, as far as the typechecker is concerned, is that those terms are seen as black-box opaque types, which can only unify with themselves. For example:

let FooContract = ... in
{
  x : FooContract = let bar = (5 | FooContract) in bar
}

This typechecks, because the contract application 5 | FooContract ensures to either fail with a contract error or that 5 satisfies FooContract. Thus, indeed, bar : FooContract.

However, the current check is very fragile, and even unsound:

• unifying two flat types requires them to be variables, or fails otherwise (see #701). This is far too limiting for many use-cases.

• if they are variables, it just compares their names. But names may be shadowed, so this is unsound. For example, the following passes:

    let FooContract = Str in
    let foo : FooContract = (let FooContract = Num in (5 | FooContract)) in
    foo
  

  This typechecks, but fails at runtime with a contract error (ouch).

This situation leads to the following question: how should we decide type equality between two contracts (flat types)? For variables, we must have a way to check that they refer to the same definition. We may also want to support more complex expressions, like contract application: Nullable Str should be unifiable with Nullable Str. On the other hand, we probably don't want to do general substitution and allow let BarContract = FooContract to be equal to FooContract, because this is a slippery slope that could lead to arbitrary computations being run during typechecking.

[yannham]

Type equality for contracts

After a bit more thinking, here is a proposal for type equality on contracts.

Aliases

One basic case that I think we want to handle is aliases, which come in handy for parametrized contracts. We want to be able to equate Alias with e.g. Foo "bar" "baz" if Alias has been defined as such: let Alias = Foo "bar" "baz" in .... This should be a common.

We probably also want to equate different aliases with the same definition: Alias type_eq Alias' if let Alias' = Foo "bar" "baz" in ..., or let Alias' = Alias in .

Recursion

We don't want follow all variables links blindly, as it could be non terminating:

{
  Foo = Bar,
  Bar = Foo,
}

Though because we just follows variables, and don't apply functions, we can detect cycles while walking the graph.

Beside infinite loops, type equality ought to stay reasonably cheap, as it is performed during typechecking, potentially many times. A pragmatic approach could just be to set an arbitrary gas limit, on the number of variable links that the type equality may follow. Doing so, we won't have to worry about loops again.

Equality on terms

The terms inside a type may be arbitrarily complex. Do we want or need to compare e.g. primops applications ? or switch ? Those are quite unlikely to appear inside an annotation (they may appear inside contract definitions). We don't want to try to syntactically compare functions either. In general, the spirit of this proposal is to try to be able to equates aliases or simple constructs that may appear inlined inside an annotation (applications and records, mostly) in a structural way. We would first test for physical equality (both as an optimization and to detect two variables pointing to the same contract definition in the AST), and if the comparison fails, we do a simple structural recursion, unfolding applications, records, and variables with a limited number of gas. For anything more complex, we return false.

Summary

Let MAX_GAS be a small integer. We decide type equality on two contracts A and B with gas consumption gas >= 0, written type_eq A B gas, as follow:

• if A and B are physically equal (corresponds to the same node of the AST), then type_eq A B 0.
• Usual (Nickel's ==) equality for primitive values: booleans, numbers, strings, null with consumption 0.
• Structural equality for application, records and arrays. For example, if A = headA argA, then type_eq A B (gas+gas') iff B = headB argB, type_eq headA headB gas, type_eq argA argB gas'.
• if A = x where x is a variable bound to term X, then type_eq A B (gas+1) if type_eq X B gas.
• If A is not a variable and B = y, same as above.

We say that the two contracts A and B satisfies type equality if there exists gas such that type_eq A B gas with gas <= MAX_GAS (in fact, such a gas is unique because the steps above define a deterministic algorithm).

[yannham]

Closed by #766 and related PRs.