BreakOut 2020 12 03 MetaCoq

WG on MetaCoq

• tHole or (tMeta?) in TemplateCoq to ease term construction

  • Not a full treatment of evars, but a convenience tool, as with _ in coq.
  • What's the cleanest way? tHole : Ast.t?
  • Does the unquote operation just have to create a fresh evar and then call some typecheck this function? If yes: which one?
  • The monad tmInferInstance could then probably be implemented with these tHoles.
  • Is it possible in the Extractable monad?

  Discussion

  We can have a specific tEvar (hole_evar, []) that is understood by unquoting specially. We need to change the Denoter.denote_term function to 1) carry the current environment when going under binders, 2) create an evar (with an evar as its type) when facing (tEvar (hole_evar, [])), 3) let typechecking try to fill it. Currently Denoter.denote_term does not call Typing.solve_evars to do 3). Maybe it should, or be left for the user to do (I'm not sure Ltac/Ltac2 has the right API for that), as it might be unecessary when we know that the denotation has to be well-typed.

  @mattam82: I'll try it quickly

• Status of completeness of type checking (Meven and Jakob)

  • Bidirectional type-checking version of typing. Easy part of the equivalence done, other direction difficult for cases (Coq incompleteness bug). Paranoid version of Typing would be useful.
  • TypeChecker completeness straightforward w.r.t. bidirectional type checking

• Template to PCUIC holes remaining, in particuliar wcbvEval translation (Will ask Pierre (Benjamin)).

• Zoe's point about handling primitive objects. Is anyone planning to work on it? Do we expect any difficulty? It would be nice to have at least reification/quotation support for 1.0. Native strings as primitive arrays of primitive integers are coming too.

  Discussion

  Question of how to translate to PCUIC ? Translate away to String or keep them? Same problem for primitive types, do we model them in PCUIC and show some correspondence with the native ones?

  Certainly showing that the primitive type axiomatization and model implement the right reduction will be interesting, as part of the Template <-> PCUIC correctness proofs.

  To investigate: what are the models for primitive types available in Coq to model them in PCUIC?

  Could we have an initial fast path just carrying around Primitive .. hidden as an opaque thing or something else? Best tradeoff is to leave quoting/unquoting as the identity and translate to/from models in/out of PCUIC. We should be able to fuse the back-and-forth translations in the template -> pcuic -> erasure pipeline.

• Subsuming template polymorphism with universe polymorphism -- impact on erasure?

  • Sort-polymorphism should not cause a problem.

• Guardedness checking and quoting of inductives (Lennard, Yannick)

  Discussion

  Following the Coq implementation for now. Extends typing/positivity checking, computing the regular trees. We need to show that guardness checking is terminating, probably enough using the existing PCUICWfReduction relations. We could also remove the axioms showing that guardness checking respects substitution/weakening/etc..