path: root/dev/doc/univpoly.txt

Notes on universe polymorphism and primitive projections, M. Sozeau
===================================================================

The new implementation of universe polymorphism and primitive
projections introduces a few changes to the API of Coq. First and
foremost, the term language changes, as global references now carry a
universe level substitution:

type 'a puniverses = 'a * Univ.Instance.t
type pconstant = constant puniverses
type pinductive = inductive puniverses
type pconstructor = constructor puniverses

type constr = ...
  | Const of puniverses
  | Ind of pinductive
  | Constr of pconstructor
  | Proj of constant * constr


Universes
=========

  Universe instances (an array of levels) gets substituted when
unfolding definitions, are used to typecheck and are unified according
to the rules in the ITP'14 paper on universe polymorphism in Coq.  

type Level.t = Set | Prop | Level of int * dirpath (* hashconsed *)
type Instance.t = Level.t array
type Universe.t = Level.t list (* hashconsed *)

The universe module defines modules and abstract types for levels,
universes etc.. Structures are hashconsed (with a hack to take care
of the fact that deserialization breaks sharing). 

  Definitions (constants, inductives) now carry around not only 
constraints but also the universes they introduced (a Univ.UContext.t).
There is another kind of contexts [Univ.ContextSet.t], the latter has 
a set of universes, while the former has serialized the levels in an
array, and is used for polymorphic objects. Both have "reified" 
constraints depending on global and local universes. 

  A polymorphic definition is abstract w.r.t. the variables in this
context, while a monomorphic one (or template polymorphic) just adds the
universes and constraints to the global universe context when it is put
in the environment. No other universes than the global ones and the
declared local ones are needed to check a declaration, hence the kernel
does not produce any constraints anymore, apart from module
subtyping.... There are hence two conversion functions now: [check_conv]
and [infer_conv]: the former just checks the definition in the current env
(in which we usually push_universe_context of the associated context),
and [infer_conv] which produces constraints that were not implied by the
ambient constraints. Ideally, that one could be put out of the kernel,
but currently module subtyping needs it. 

 Inference of universes is now done during refinement, and the evar_map
carries the incrementally built universe context, starting from the
global universe constraints (see [Evd.from_env]). [Evd.conversion] is a
wrapper around [infer_conv] that will do the bookkeeping for you, it
uses [evar_conv_x]. There is a universe substitution being built
incrementally according to the constraints, so one should normalize at
the end of a proof (or during a proof) with that substitution just like
we normalize evars. There are some nf_* functions in
library/universes.ml to do that. Additionally, there is a minimization
algorithm in there that can be applied at the end of a proof to simplify
the universe constraints used in the term. It is heuristic but
validity-preserving. No user-introduced universe (i.e. coming from a
user-written anonymous Type) gets touched by this, only the fresh
universes generated for each global application. Using

val pf_constr_of_global : Globnames.global_reference -> (constr -> tactic) -> tactic

Is the way to make a constr out of a global reference in the new API.
If they constr is polymorphic, it will add the necessary constraints to
the evar_map. Even if a constr is not polymorphic, we have to take care
of keeping track of its universes. Typically, using:

  mkApp (coq_id_function, [| A; a |]) 

and putting it in a proof term is not enough now. One has to somehow
show that A's type is in cumululativity relation with id's type
argument, incurring a universe constraint. To do this, one can simply
call Typing.resolve_evars env evdref c which will do some infer_conv to
produce the right constraints and put them in the evar_map. Of course in
some cases you might know from an invariant that no new constraint would
be produced and get rid of it. Anyway the kernel will tell you if you
forgot some. As a temporary way out, [Universes.constr_of_global] allows
you to make a constr from any non-polymorphic constant, but it will fail
on polymorphic ones.

Other than that, unification (w_unify and evarconv) now take account of universes and
produce only well-typed evar_maps.

Some syntactic comparisons like the one used in [change] have to be
adapted to allow identification up-to-universes (when dealing with 
polymorphic references), [make_eq_univs_test] is there to help. 
In constr, there are actually many new comparison functions to deal with
that:
 
(** [equal a b] is true if [a] equals [b] modulo alpha, casts,
   and application grouping *)
val equal : constr -> constr -> bool

(** [eq_constr_univs u a b] is [true] if [a] equals [b] modulo alpha, casts,
   application grouping and the universe equalities in [u]. *)
val eq_constr_univs : constr Univ.check_function

(** [leq_constr_univs u a b] is [true] if [a] is convertible to [b] modulo 
    alpha, casts, application grouping and the universe inequalities in [u]. *)
val leq_constr_univs : constr Univ.check_function

(** [eq_constr_universes a b] [true, c] if [a] equals [b] modulo alpha, casts,
   application grouping and the universe equalities in [c]. *)
val eq_constr_universes : constr -> constr -> bool Univ.universe_constrained

(** [leq_constr_universes a b] [true, c] if [a] is convertible to [b] modulo
    alpha, casts, application grouping and the universe inequalities in [c]. *)
val leq_constr_universes : constr -> constr -> bool Univ.universe_constrained

(** [eq_constr_univs a b] [true, c] if [a] equals [b] modulo alpha, casts,
   application grouping and ignoring universe instances. *)
val eq_constr_nounivs : constr -> constr -> bool

The [_univs] versions are doing checking of universe constraints
according to a graph, while the [_universes] are producing (non-atomic) 
universe constraints. The non-atomic universe constraints include the
[ULub] constructor: when comparing [f (* u1 u2 *) c] and [f (* u1' u2'
*) c] we add ULub constraints on [u1, u1'] and [u2, u2']. These are
treated specially: as unfolding [f] might not result in these
unifications, we need to keep track of the fact that failure to satisfy
them does not mean that the term are actually equal. This is used in
unification but probably not necessary to the average programmer. 

Another issue for ML programmers is that tables of constrs now usually
need to take a [constr Univ.in_universe_context_set] instead, and
properly refresh the universes context when using the constr, e.g. using 
Clenv.refresh_undefined_univs clenv or: 

(** Get fresh variables for the universe context.
    Useful to make tactics that manipulate constrs in universe contexts polymorphic. *)
val fresh_universe_context_set_instance : universe_context_set -> 
  universe_level_subst * universe_context_set

The substitution should be applied to the constr(s) under consideration, 
and the context_set merged with the current evar_map with:

val merge_context_set : rigid -> evar_map -> Univ.universe_context_set -> evar_map

The [rigid] flag here should be [Evd.univ_flexible] most of the
time. This means the universe levels of polymorphic objects in the
constr might get instantiated instead of generating equality constraints 
(Evd.univ_rigid does that).

On this issue, I recommend forcing commands to take [global_reference]s
only, the user can declare his specialized terms used as hints as
constants and this is cleaner. Alas, backward-compatibility-wise,
this is the only solution I found. In the case of global_references
only, it's just a matter of using [Evd.fresh_global] /
[pf_constr_of_global] to let the system take care of universes.


The universe graph
==================

To accomodate universe polymorphic definitions, the graph structure in
kernel/univ.ml was modified. The new API forces every universe to be
declared before it is mentionned in any constraint. This forces to
declare every universe to be >= Set or > Set. Every universe variable
introduced during elaboration is >= Set. Every _global_ universe is now
declared explicitly > Set, _after_ typechecking the definition. In
polymorphic definitions Type@{i} ranges over Set and any other universe
j. However, at instantiation time for polymorphic references, one can
try to instantiate a universe parameter with Prop as well, if the
instantiated constraints allow it. The graph invariants ensure that
no universe i can be set lower than Set, so the chain of universes
always bottoms down at Prop < Set.

Modules
=======

One has to think of universes in modules as being globally declared, so
when including a module (type) which declares a type i (e.g. through a
parameter), we get back a copy of i and not some fresh universe.

Projections
===========

  | Proj of constant * constr

Projections are always applied to a term, which must be of a record type
(i.e. reducible to an inductive type [I params]). Type-checking,
reduction and conversion are fast (not as fast as they could be yet)
because we don't keep parameters around. As you can see, it's currently
a [constant] that is used here to refer to the projection, that will
change to an abstract [projection] type in the future. Basically a
projection constant records which inductive it is a projection for, the
number of params and the actual position in the constructor that must be
projected. For compatibility reason, we also define an eta-expanded form
(accessible from user syntax @f). The constant_entry of a projection has
both informations. Declaring a record (under [Set Primitive
Projections]) will generate such definitions. The API to declare them is
not stable at the moment, but the inductive type declaration also knows
about the projections, i.e. a record inductive type decl contains an
array of terms representing the projections. This is used to implement
eta-conversion for record types (with at least one field and having all
projections definable). The canonical value being [Build_R (pn x)
... (pn x)]. Unification and conversion work up to this eta rule. The
records can also be universe polymorphic of course, and we don't need to
keep track of the universe instance for the projections either.
Projections are reduced _eagerly_ everywhere, and introduce a new Zproj
constructor in the abstract machines that obeys both the delta (for the
constant opacity) and iota laws (for the actual reduction). Refolding
works as well (afaict), but there is a slight hack there related to
universes (not projections). 

For the ML programmer, the biggest change is that pattern-matchings on
kind_of_term require an additional case, that is handled usually exactly
like an [App (Const p) arg].

There are slight hacks related to hints is well, to use the primitive
projection form of f when one does [Hint Resolve f]. Usually hint
resolve will typecheck the term, resulting in a partially applied
projection (disallowed), so we allow it to take
[constr_or_global_reference] arguments instead and special-case on
projections. Other tactic extensions might need similar treatment. 

WIP
===

- [vm_compute] does not deal with universes and projections correctly,
except when it goes to a normal form with no projections or polymorphic
constants left (the most common case). E.g. Ring with Set Universe
Polymorphism and Set Primitive Projections work (at least it did at some
point, I didn't recheck yet).  

- [native_compute] works with universes and projections.


Incompatibilities
=================

Old-style universe polymorphic definitions were implemented by taking
advantage of the fact that elaboration (i.e., pretyping and unification)
were _not_ universe aware, so some of the constraints generated during
pretypechecking would be forgotten. In the current setting, this is not
possible, as unification ensures that the substitution is built is
entirely well-typed, even w.r.t universes. This means that some terms
that type-checked before no longer do, especially projections of the
pair:

@fst ?x ?y : prod ?x ?y : Type (max(Datatypes.i, Datatypes.j)).

The "template universe polymorphic" variables i and j appear during
typing without being refreshed, meaning that they can be lowered (have
upper constraints) with user-introduced universes. In most cases this
won't work, so ?x and ?y have to be instantiated earlier, either from
the type of the actual projected pair term (some t : prod A B) or the
typing constraint. Adding the correct type annotations will always fix 
this.


Unification semantics
=====================

In Ltac, matching with:

- a universe polymorphic constant [c] matches any instance of the
  constant.
- a variable ?x already bound to a term [t] (non-linear pattern) uses 
  strict equality of universes (e.g., Type@{i} and Type@{j} are not
  equal).

In tactics:

- [change foo with bar], [pattern foo] will unify all instances of [foo]
  (and convert them with [bar]). This might incur unifications of
  universes. [change] uses conversion while [pattern] only does
  syntactic matching up-to unification of universes.
- [apply], [refine] use unification up to universes.