Improve destructuring existential types

Make destructuring existentials less arcane by allowing them to be destructured via type patterns (typ_pat in ast.ml). This allows the following code for example:

val mk_square : unit -> {'n 'm, 'n = 'm. vector('n, dec, vector('m, dec, bit))}

function test (() : unit) -> unit = {
  let matrix as vector('width, _, 'height) = mk_square ();
  _prove(constraint('width = 'height));
  ()
}

where 'width we become 'n from mk_square, and 'height becomes 'm. The old syntax

let vector as 'length  = ...
or even
let 'vector = ...

still works under this new scheme in a uniform way, so this is backwards compatible

The way this works is when a kind identifier in a type pattern is bound against a type, e.g. 'height being bound against vector('m, dec, bit) in the example, then we get a constraint that 'height is equal to the first and only n-expression in the type, in this case 'm. If the type has two or more n-expressions (or zero) then this is a type error.

0 files changed, 0 insertions, 0 deletions