Skip to content

Layout Unification

Alistair O'Brien requested to merge ajob410/layout-variables into dev

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 falses):

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.

Merge request reports