Stefan pushed to branch master at Stefan / Typer

Commits: 2bd6aa15 by Stefan Monnier at 2020-08-10T23:52:31-04:00 * btl/builtins.typer (Eq_comm): Update FIXME

- - - - -

3 changed files:

- btl/builtins.typer - src/elab.ml - src/lexp.ml

Changes:

===================================== btl/builtins.typer ===================================== @@ -47,7 +47,7 @@ Void = typecons Void;

%% Eq : (l : TypeLevel) ≡> (t : Type_ l) ≡> t -> t -> Type_ l %% Eq' : (l : TypeLevel) ≡> Type_ l -> Type_ l -> Type_ l -Eq_refl : ((x : ?t) ≡> Eq x x); % FIXME: `Eq ?x ?x` causes an error! +Eq_refl : ((x : ?t) ≡> Eq x x); Eq_refl = Built-in "Eq.refl";

Eq_cast : (x : ?) ≡> (y : ?) @@ -63,8 +63,11 @@ Eq_cast = Built-in "Eq.cast"; %% Eq_comm : Eq ?x ?y -> Eq ?y ?x`; Eq_comm : (x : ?t) ≡> (y : ?t) ≡> Eq x y -> Eq y x; Eq_comm p = Eq_cast (f := lambda xy -> Eq xy x) - %% FIXME: I can't figure out how `(p := p)` - %% gets inferred here, yet it seems to work!?! + %% FIXME: The code is incorrectly accepted even without + %% this `(p := p)` because we just get a metavar which + %% remains uninstantiated and undetected (and then gets + %% throw away by erasure)! + (p := p) Eq_refl;

%% General recursion!! @@ -77,7 +80,7 @@ Eq_comm p = Eq_cast (f := lambda xy -> Eq xy x) %% %% But this is not sufficient, because you could use `Y` to create %% new recursive *types* which then let you construct new arbitrary -%% recursive values of previously uninhabited types. +%% recursive values of previously non-existent types. %% E.g. you could create `Y <something> = ((... → t) -> t) -> t` %% and then give the term `λx. x x` inhabiting that type, and from that %% get a proof of False.

===================================== src/elab.ml ===================================== @@ -238,9 +238,9 @@ let ctx_define_rec (ctx: elab_context) decls = * infer the types and perform macro-expansion. * * More specifically, we do it with 2 mutually recursive functions: - * - `check` takes a Pexp along with its expected type and returns an Lexp + * - `check` takes an Sexp along with its expected type and returns an Lexp * of that type (hopefully) - * - `infer` takes a Pexp and infers its type (which it returns along with + * - `infer` takes an Sexp and infers its type (which it returns along with * the Lexp). * This is the idea of "bidirectional type checking", which minimizes * the amount of "guessing" and/or annotations. Since we infer types anyway

===================================== src/lexp.ml ===================================== @@ -150,7 +150,7 @@ type metavar_info = | MVal of lexp (* Exp to which the var is instantiated. *) | MVar of scope_level (* Outermost scope in which the var appears. *) * ltype (* Expected type. *) - (* We'd like to keep the lexp_content in which the type is to be + (* We'd like to keep the lexp_context in which the type is to be * understood, but lexp_context is not yet defined here, * so we just keep the length of the lexp_context. *) * ctx_length @@ -274,7 +274,7 @@ let hcs_table : ((lexp * subst), lexp) Hashtbl.t = Hashtbl.create 1000 let rec mkSusp e s = if S.identity_p s then e else (* We apply the substitution eagerly to some terms. - * There's no deep technical rason for that: + * There's no deep technical reason for that: * it just seemed like a good idea to do it eagerly when it's easy. *) match e with | Imm _ -> e @@ -313,7 +313,7 @@ let rec sunshift n = let _ = assert (S.identity_p (scompose (S.shift 5) (sunshift 5)))

(* The quick test below seemed to indicate that about 50% of the "sink"s - * are applied on top of another "sink" and hence cound be combined into + * are applied on top of another "sink" and hence could be combined into * a single "Lift^n" constructor. Doesn't seem high enough to justify * the complexity of adding a `Lift` to `subst`. *)

View it on GitLab: https://gitlab.com/monnier/typer/-/commit/2bd6aa15e783ef5ce69df7339a9dcfe2f2...