Skip to content

Goodbye `gen` 馃憢

Alistair O'Brien requested to merge ajob410/goodbye-gen into dev

Motivation and Context

Since !1905 (merged), type error messages contained peculiar gen#... type variables. These variables represented generated variables for existential or universally quantified variables that were introduced by our change to Bidirectional Type Checking.

However, printing these type variables in error messages often led to confusion as documented in this slack discussion: https://tezos-dev.slack.com/archives/CFX0B8Q3X/p1665043964832289.

This MR aims to remove the occurrences of gen type variables in the error messages.

Description

We remove gen type variables by defining a local mapping from type variables to string names.

The mapping (created per error) is stored in a mutable structure Type_var_name_tbl:

module Type_var_name_tbl : sig
  type t

  (** [create ()] creates a new type variable table. *)
  val create : unit -> t

  (** [clear t] clears the table [t]. *)
  val clear : t -> unit

  (** [name_of t tvar] returns the human readable name of [tvar] (potentially generating 
       a unique name for [tvar]). *)
  val name_of : t -> Type_var.t -> string

  module Exists : sig
    (** [clear ()] clears the table used for existential variables. *)
    val clear : unit -> unit

    (** [name_of tvar] returns the human readable name for the existential variable [tvar] *)
    val name_of : Type_var.t -> string
  end
end

The Type module now exposes two functions: pp and pp_with_tbl, the former is the original pp function (which displays gen type variables) and pp_with_tbl which uses a tbl to map type variables to names.

Generated names take the form: a, b, c, ..., z, a1, b1, ..., z1, .... The implementation of Type_var_name_tbl ensure generated names are unique (wrt to the passed table).

Types of changes

  • Bug fix (non-breaking change which fixes an issue)
  • New feature (non-breaking change which adds functionality)
  • Breaking change (fix or feature that would cause existing functionality to not work as expected)
  • Performance improvement (non-breaking change that improves performance)
  • None (change with no changelog)

Changelog

Improve pretty-printing of types in errors by removing occurrences of gen#... variables.

Checklist:

  • Changes follow the existing coding style (use dune @fmt to check).
  • Tests for the changes have been added (for bug fixes / feature).
  • Documentation has been updated.
  • Changelog description has been added (if appropriate).
  • Examples in changed behaviour have been added to the changelog (for breaking change / feature).
Edited by Alistair O'Brien

Merge request reports