Layout Unification
type:fixed
Related Issue:#1450 (closed)
Originally, LIGO's type checker would assume a default layout for records/variants that could not locally infer the layout.
This MR addresses this issue with the addition of layout unification, which propagates layout annotations in a sound and complete manner. To achieve this, we extend the syntax of layouts to:
layout l ::= comb | tree | ^l
where ^l
denotes an (existential) layout variable. These operate identically to existential type variables.
Layout variables that are never unified are elaborated to the default layout (tree
)
Debt
Since neither functorising nor parameterising Ast_typed
is permitted due to ppx_woo
and ppx_import
, layout variables were added directly to the Layout.t
type. This is a poor design choice since layout variables should only exist during the typing pass.
A hack of a pattern matching "view" is added for later passes (to avoid multiple assert false
s):
type view =
| L_comb
| L_tree
let view (t : t) : view =
match t with
| L_comb -> L_comb
| L_tree -> L_tree
| L_variable _lvar -> failwith "corner case: cannot view a layout variable"
Changelog details:
Add layout unification to LIGO's type checker, which fixes existing flaws in the propagation of layout annotations.