Jean-Alexandre Barszcz pushed to branch ja-barszcz at Stefan / Typer

Commits: f2b81386 by Stefan Monnier at 2020-04-02T19:31:41-04:00 * src/elab.ml (meta_to_var): Fix debruijn error.

* btl/pervasive.typer (Decidable): Make it universe-polymorphic. * src/builtin.ml (register_builtin_csts): Fix Type0 typo.

- - - - - 85d12bf5 by Stefan Monnier at 2020-04-07T22:21:39-04:00 * src/elab.ml (infer_and_generalize_type): Add more exceptions

Don't generalize over the level of the final return type if it doesn't appear elsewhere.

* btl/builtins.typer (Eq_cast): Give a name to the proof arg.

- - - - - 4993afa5 by Stefan Monnier at 2020-04-07T23:15:21-04:00 * src/lexp.ml (srename): New function

* src/unification.ml (unify): * src/opslexp.ml (conv_p'): * src/elab.ml (sform_lambda): Use it.

- - - - - 63f7644b by Stefan Monnier at 2020-04-07T23:21:05-04:00 * src/elab.ml (meta_to_var): Rework to be able to infer universe levels

(generalize): Adjust for new calling convention of `meta_to_var` and also for the fact that `meta_to_var` now takes care of the S.shift for us.

- - - - - 886a3589 by Stefan Monnier at 2020-04-08T18:07:18-04:00 Remove most uses of L.clean

* src/elab.ml (elab_check_sort, elab_check_def, infer_type): Skip `L.clean` since `lexp_string` already cleans up on the fly. (track_fv): Skip `L.clean` since `fv` already cleans up on the fly. (lexp_eval): Skip `L.clean` since `fv` and `erase_type` already clean up on the fly. (sform_new_attribute, sform_add_attribute, sform_built_in): Explicitly call `clean` now that `lexp_close` doesn't do it any more.

* src/eval.ml (from_lctx): Skip `L.clean` since `fv` and `erase_type` already clean up on the fly.

* src/lexp.ml (print_context_value): Remove `Expr` constructor. (pretty_ppctx): Remove unused `parent` and now unused `metavar`. (smap_lexp, pp_parent, pp_meta, set_parent, set_parent): Remove functions.. (lexp_str): Don't call `set_parent` any more. Rewrite metavar case to use `metavar_lookup` rather than `clean`.

* src/opslexp.ml (lexp_close): Don't call `clean` any more. (conv_p', mkSLlub): Skip `L.clean` since `level_canon` already cleans up on the fly. (check''.assert_type): Skip `L.clean` since `lexp_string` already cleans up on the fly. (erase_type): Clean up metavars on the fly.

* src/unification.ml (unify_metavar): Skip `L.clean` since `lexp_string` already cleans up on the fly.

- - - - - bf3c818e by Jean-Alexandre Barszcz at 2020-04-12T02:05:40-04:00 Add a nix shell

* shell.nix : When using nixpkgs/nixos, run `nix-shell` to get a shell with Typer's dependencies available.

- - - - - c39ff3d5 by Jean-Alexandre Barszcz at 2020-04-12T02:05:40-04:00 Improve the implementation of Sexp.dispatch

* src/elab.ml (sexp_dispatch) : Sexp.dispatch assumed that its arguments were closures. Instead, we use eval_call and also accept constructors, builtins, etc.

- - - - - 7b623a26 by Jean-Alexandre Barszcz at 2020-04-12T02:05:40-04:00 Add the inductive type `Sexp_wrapper` to match on sexps

* btl/pervasive.typer : Add the inductive type `Sexp_wrapper` to wrap the Sexp values in typer code, and the function `Sexp_wrap` to do the wrapping. This makes possible the use of pattern matching to destructure Sexps instead of the more verbose calls to `Sexp_dispatch`.

- - - - - 8419c419 by Jean-Alexandre Barszcz at 2020-04-12T02:05:40-04:00 Fix lexp_whnf when the case scrutinee is a call

* src/opslexp.ml (lexp_whnf) : Make sure that we take the WHNF of the function when the scrutinee of a case expression is a call, before checking that the function is a constructor. Otherwise, expressions like `case (let ... in (constructor ...))` fail to reduce, for example.

- - - - - cc20d841 by Jean-Alexandre Barszcz at 2020-04-12T02:05:40-04:00 Fix some lexp constructor calls where hash-consing has been forgotten

- - - - - 742049a9 by Jean-Alexandre Barszcz at 2020-04-12T02:05:40-04:00 [WIP] Make unification symmetric

- - - - - 7bc1f309 by Jean-Alexandre Barszcz at 2020-04-12T02:05:40-04:00 [WIP] Handle variables earlier during unification

- - - - - ef1aeb13 by Jean-Alexandre Barszcz at 2020-04-13T21:48:54-04:00 [WIP] experiments with Decidable and proofs

- - - - - 3b72b8d2 by Jean-Alexandre Barszcz at 2020-04-13T21:48:54-04:00 [WIP] unify instead of conv_p in sform_lambda

- - - - -

11 changed files:

- btl/builtins.typer - btl/pervasive.typer - + samples/decidable.typer - + shell.nix - src/builtin.ml - src/elab.ml - src/eval.ml - src/inverse_subst.ml - src/lexp.ml - src/opslexp.ml - src/unification.ml

Changes:

===================================== btl/builtins.typer ===================================== @@ -31,6 +31,9 @@

%%%% Base Types used in builtin functions

+%% Box : Type_ ?ℓ₁ -> Type_ ?ℓ₂; +%% Box = lambda (ℓ₃ : TypeLevel) ≡> typecons (Box (t : Type_ ℓ₃)) (box t); + %% TypeLevel_succ = Built-in "TypeLevel.succ" : TypeLevel -> TypeLevel; %% TypeLevel_⊔ = Built-in "TypeLevel.⊔" : TypeLevel -> TypeLevel -> TypeLevel;

@@ -48,7 +51,7 @@ Eq_refl : ((x : ?t) ≡> Eq x x); % FIXME: `Eq ?x ?x` causes an error! Eq_refl = Built-in "Eq.refl";

Eq_cast : (x : ?) ≡> (y : ?) - ≡> Eq x y + ≡> (p : Eq x y) ≡> (f : ? -> ?) ≡> f x -> f y; %% FIXME: I'd like to just say:

===================================== btl/pervasive.typer ===================================== @@ -358,6 +358,18 @@ type-impl = lambda (x : List Sexp) ->

type_ = macro type-impl;

+%%%% An inductive type to wrap Sexp + +type Sexp_wrapper + | node Sexp (List Sexp) + | symbol String + | string String + | integer Integer + | float Float + | block Sexp; + +Sexp_wrap s = Sexp_dispatch s node symbol string integer float block; + %%%% Tuples

%% Sample tuple: a module holding Bool and its constructors. @@ -446,7 +458,8 @@ Not prop = prop -> False; %% We don't use the `type` macro here because it would make these `true` %% and `false` constructors override `Bool`'s, and we currently don't %% want that. -Decidable = typecons (Decidable (prop : Type)) +%% FIXME generalize typecons formal arguments +Decidable = typecons (Decidable (ℓ ::: TypeLevel) (prop : Type_ ℓ)) (true (p ::: prop)) (false (p ::: Not prop));

%% Testing generalization in inductive type constructors.

===================================== samples/decidable.typer ===================================== @@ -0,0 +1,116 @@ +False = Void; +True = Unit; + +% FIXME improved "case" fails with no branches +exfalso : False -> ?a; +exfalso f = ##case_ f; + +%type Decidable (prop : Type) +% | yes (p ::: prop) +% | no (p ::: Not prop); +yes = datacons Decidable true; +no = datacons Decidable false; + +Eq_trans : + (x : ?t) => (y : ?t) => (a : ?t) -> + (ax : Eq a x) => (ay : Eq a y) => Eq x y; +Eq_trans a = + lambda (ax : Eq a x) (ay : Eq a y) => + Eq_cast (f := lambda ax -> Eq ax y) ay; + +Eq_cong : % not sure about levels here + (t : (Type_ ?ℓ)) ≡> (r : (Type_ ?ℓ)) ≡> + (x : t) ≡> (y : t) ≡> (p : (Eq x y)) ≡> + (f : (t -> r)) -> (Eq (f x) (f y)); +Eq_cong f = + Eq_cast (p := p) (f := lambda xy -> Eq (f x) (f xy)) Eq_refl; + +discriminate_nocheck = + macro (lambda args -> + case args + | cons x (cons y nil) => + do { + sd <- gensym (); + sp <- gensym (); + IO_return + (quote ((lambda (uquote sp) -> + (Eq_cast (p := (uquote sp)) + (f := (lambda (uquote sd) -> + (case uquote sd + | (uquote x) => True + | _ => False))) + ())) : Not (Eq (uquote x) (uquote y)))) + } + | _ => IO_return Sexp_error); + +discriminate = + macro (lambda args -> + case args + | cons x (cons y nil) => + (case (Sexp_wrap x, Sexp_wrap y) + | (symbol sx, symbol sy) => % FIXME get the constructor even when its a call + do { + env <- Elab_getenv (); + if (and (Elab_isconstructor sx env) + (and (Elab_isconstructor sy env) + (not (Sexp_eq x y)))) + then + Macro_expand discriminate_nocheck args + else (IO_return Sexp_error) + } + | _ => IO_return Sexp_error) + | _ => IO_return Sexp_error); + +test : (Not (Eq true false)); +test = discriminate true false; + +absurd = + lambda (p : ?prop) -> + lambda (contra : (Not ?prop)) -> + contra p; + +% We can't (usefully) have a `Decidable Bool` because it's +% impossible to have a `Not Bool`. Instead, we can decide boolean +% equality: + +decideBoolEq : (a : Bool) => (b : Bool) => Decidable (Eq a b); +decideBoolEq = + lambda (a : Bool) (b : Bool) => + case (a, b) + | (false, false) => yes (p := Eq_trans false) + | (false, true) => no (p := lambda (p : Eq a b) -> + absurd (Eq_trans (ax := Eq_trans a) b) (discriminate false true)) + | (true, false) => no (p := lambda (p : Eq a b) -> + absurd (Eq_trans (ax := Eq_trans a) b) (discriminate true false)) + | (true, true) => yes (p := Eq_trans true); + +type Nat + | zero + | succ Nat; + +type even (a : Nat) + | eZ (p ::: Eq a zero) + | eSS (p :: even ?a) (pss ::: Eq a (succ (succ ?a))); + +decideEven : (a : Nat) => Decidable (even a); +decideEven = + lambda (a : Nat) => + case a + | zero => yes (p := eZ) + | succ zero => no (p := + lambda (p : even a) -> + case p + | eZ => absurd (Eq_trans a) (discriminate_nocheck zero (succ zero)) + | eSS => absurd (Eq_trans a) (discriminate_nocheck (succ (succ ?)) (succ zero))) + | succ (succ a') => + case (decideEven : Decidable (even a')) + | yes => yes (p := eSS) + | no => no (p := + lambda (p : even a) -> + case p + | eZ => absurd (Eq_trans a) (discriminate_nocheck zero (succ (succ ?))) + | eSS => absurd (? : even a') (? : Not (even a'))); + +type _<_ (a : Nat) (b : Nat) + | ltZ (pa ::: Eq a zero) (pb ::: Eq b (succ ?b)) + | ltS (p : (?a < ?b)) (pa ::: Eq a (succ ?a)) (pb ::: Eq b (succ ?b));

===================================== shell.nix ===================================== @@ -0,0 +1,10 @@ +{ pkgs ? import <nixpkgs> {} }: +pkgs.mkShell { + name = "typer"; + buildInputs = + with pkgs.ocamlPackages; [ + pkgs.gnumake ocaml ocamlbuild findlib utop # tooling + zarith # ocaml libraries + merlin # for emacs + ]; +}

===================================== src/builtin.ml ===================================== @@ -155,7 +155,7 @@ let register_builtin_csts () = add_builtin_cst "TypeLevel" DB.type_level; add_builtin_cst "TypeLevel_z" DB.level0; add_builtin_cst "Type" DB.type0; - add_builtin_cst "Type0" DB.type1; + add_builtin_cst "Type0" DB.type0; add_builtin_cst "Type1" DB.type1; add_builtin_cst "Int" DB.type_int; add_builtin_cst "Integer" DB.type_integer;

===================================== src/elab.ml ===================================== @@ -128,8 +128,7 @@ let elab_check_sort (ctx : elab_context) lsort var ltp = "Exception during whnf of sort:"; raise e) with | Sort (_, _) -> () (* All clear! *) - | _ -> let lexp_string e = lexp_string (L.clean e) in - let typestr = lexp_string ltp ^ " : " ^ lexp_string lsort in + | _ -> let typestr = lexp_string ltp ^ " : " ^ lexp_string lsort in match var with | (l, None) -> lexp_error l ltp ("`" ^ typestr ^ "` is not a proper type") @@ -159,7 +158,6 @@ let elab_check_def (ctx : elab_context) var lxp ltype = let lctx = ectx_to_lctx ctx in let loc = lexp_location lxp in

- let lexp_string e = lexp_string (L.clean e) in let ltype' = try OL.check lctx lxp with e -> match e with | Log.Stop_Compilation _ -> raise e @@ -311,39 +309,142 @@ let elab_varref ctx (loc, name) "` was not declared" ^ relateds); sform_dummy_ret ctx loc)

-(* Turn metavar into plain vars after generalization. *) -let rec meta_to_var ids o (e : lexp) = - let rec loop e = match e with +(* Turn metavar into plain vars after generalization. + * ids: an IMap that maps metavars to their position as argument + * (first arg gets position 0). *) +let rec meta_to_var ids (e : lexp) = + + let count = IMap.cardinal ids in + + (* Yuck! Yuck! Yuck! + * This is very messy. What we need to do starts as follows: + * We have a `Γ ⊢ e : τ` and this `e` contains some metavars `m₁…mₙ : τ₁…τₙ` + * that we want to change into formal arguments, i.e. we want to turn `e` + * into something like + * + * Γ ⊢ λ x₁…xₙ ≡> e[x₁…xₙ/m₁…mₙ] : τ₁…τₙ ≡> τ + * + * The above substitution is not the usual capture-avoiding substitution + * since it replaces metavars with vars rather than vars with terms. + * It's more like *instanciation* of those metavars. + * And indeed, ideally it should be a simple matter of instanciating + * those metavars with temrs that are variable references. + * + * An important aspect here is that the rest of `e` also needs to be + * changed because it will now live in a new context: + * + * Γ,x₁:τ₁,…,xₙ:τₙ ⊢ e[x₁…xₙ/m₁…mₙ] : τ + * + * So we need to adjust all the variable references in `e` to account for + * that, which we normally do with a simple `S.shift n`. + * + * The first problem comes here: `S.shift n` takes a term from + * `Γ` to `Γ,x₁:τ₁,…,xₙ:τₙ`, making sure it still references the same + * bindings as before, i.e. it makes sure the result *cannot* refer to + * any `x₁…xₙ`! + * I first thought "it's OK, I'll first do the `S.shift n` and I only + * instanciate the metavars afterwards", but that does not help, + * because every reference to a metavar is properly wrapped in a + * pending application of the relevant substitution, so the `S.shift n` + * still applies to it. + * + * For this reason, we have a `loop` below which does the substitution + * of variable references for the metavars (since just instanciating + * the metavars doesn't work). + * + * The second problem comes with the other metavars in `e`. + * There are 3 kinds of metavars in `e`: + * + * A. Those that we want to replace with variable references. + * B. Those that live in some higher enclosing scope. + * C. The "others". + * + * Presumably, we have (A) under control. + * For (B) the situation is easy enough: since they live in a higher + * enlosing scope they can only refer to those variables that exist in + * some prefix of `Γ`, so we just need to apply `S.shift n` to them. + * + * For (C), we'd like those metavars (which originally could refer to + * any var in `Γ`) to now be a able to also refer to any of the + * new vars `x₁…xₙ`. So `S.shift n` is definitely not right for them. + * Instead, I ended up writing `adjust_subst` which hacks up + * the substitution attached to each metavar reference so it can + * now refer to its original context *and* to `x₁…xₙ`. + * + * Arguably, now that we handle (C), we could handle (A) by + * first treating them as (C) and then using instantiation. + * But the code for (A) was already written, and it doesn't seem like + * it would make things any simpler currently. + * + * Note: in the original HM algorithm (and in Twelf), (C) cannot occur + * because every metavariable that's not in (B) is generalized + * (i.e. will be in A). But here we need (C) for cases like: + * + * List : Type ? -> Type ?; + * + * Since the second `?` should not be generalized but should + * be inferred from the definition. I.e. the above should be + * generalized to: + * + * List : (ℓ : TypeLevel) ≡> Type ℓ -> Type ?; + * + * where the remaining `?` will be inferred by unification + * when type-checking the definition of `Box` where ti be unified with `ℓ`, + * the newly introduced variable! + *) + + (* `o` is the binding offset until the root. *) + let rec adjust_subst o s = match s with + | S.Identity n + -> let o' = o - n in + if o' < 0 then + (* This metavar's original context is outside of our scope + * (case (B) above), so don't let it refer to the new vars. *) + S.Identity (n + count) + else + Identity n + | S.Cons (e, s', n) + -> let o' = o - n in + if o' < 0 then + (* This metavar's original context is outside of our scope + * (case (B) above), so don't let it refer to the new vars. *) + S.Cons (e, s', n + count) + else + S.Cons (loop o' e, adjust_subst o' s', n) + + (* `o` is the binding depth at which we are relative to the "root" + * of the expression (i.e. where the new vars will be inserted). *) + and loop o e = match e with | Imm _ -> e | SortLevel SLz -> e - | SortLevel (SLsucc e) -> mkSortLevel (mkSLsucc (loop e)) - | SortLevel (SLlub (e1, e2)) -> mkSortLevel (mkSLlub' (loop e1, loop e2)) - | Sort (l, Stype e) -> mkSort (l, Stype (loop e)) + | SortLevel (SLsucc e) -> mkSortLevel (mkSLsucc (loop o e)) + | SortLevel (SLlub (e1, e2)) -> mkSortLevel (mkSLlub' (loop o e1, loop o e2)) + | Sort (l, Stype e) -> mkSort (l, Stype (loop o e)) | Sort (_, (StypeOmega | StypeLevel)) -> e | Builtin _ -> e - | Var _ -> e - | Susp (e, s) -> loop (push_susp e s) + | Var (n,i) -> if i < o then e else mkVar (n, i + count) + | Susp (e, s) -> loop o (push_susp e s) | Let (l, defs, e) -> let len = List.length defs in let (_, ndefs) = List.fold_right (fun (l,e,t) (o', defs) -> let o' = o' - 1 in - (o', (l, meta_to_var ids (len + o) e, - meta_to_var ids (o' + o) t) :: defs)) + (o', (l, loop (len + o) e, + loop (o' + o) t) :: defs)) defs (len, []) in - mkLet (l, ndefs, meta_to_var ids (len + o) e) + mkLet (l, ndefs, loop (len + o) e) | Arrow (ak, v, t1, l, t2) - -> mkArrow (ak, v, loop t1, l, meta_to_var ids (1 + o) t2) + -> mkArrow (ak, v, loop o t1, l, loop (1 + o) t2) | Lambda (ak, v, t, e) - -> mkLambda (ak, v, loop t, meta_to_var ids (1 + o) e) + -> mkLambda (ak, v, loop o t, loop (1 + o) e) | Call (f, args) - -> mkCall (loop f, List.map (fun (ak, e) -> (ak, loop e)) args) + -> mkCall (loop o f, List.map (fun (ak, e) -> (ak, loop o e)) args) | Inductive (l, label, args, cases) -> let alen = List.length args in let (_, nargs) = List.fold_right (fun (ak, v, t) (o', args) -> let o' = o' - 1 in - (o', (ak, v, meta_to_var ids (o' + o) t) + (o', (ak, v, loop (o' + o) t) :: args)) args (alen, []) in let ncases @@ -354,28 +455,29 @@ let rec meta_to_var ids o (e : lexp) = = List.fold_right (fun (ak, v, t) (o', fields) -> let o' = o' - 1 in - (o', (ak, v, meta_to_var ids (o' + o) t) + (o', (ak, v, loop (o' + o) t) :: fields)) - fields (flen, []) in + fields (flen + alen, []) in nfields) cases in mkInductive (l, label, nargs, ncases) - | Cons (t, l) -> mkCons (loop t, l) + | Cons (t, l) -> mkCons (loop o t, l) | Case (l, e, t, cases, default) -> let ncases = SMap.map (fun (l, fields, e) - -> (l, fields, meta_to_var ids (o + List.length fields) e)) + -> (l, fields, loop (o + List.length fields) e)) cases in - mkCase (l, loop e, loop t, ncases, - match default with None -> None | Some (v, e) -> Some (v, loop e)) + mkCase (l, loop o e, loop o t, ncases, + match default with None -> None + | Some (v, e) -> Some (v, loop (1 + o) e)) | Metavar (id, s, name) -> if IMap.mem id ids then - mkVar (name, o + IMap.find id ids) + mkVar (name, o + count - IMap.find id ids) else match metavar_lookup id with - | MVal e -> loop (push_susp e s) - | _ -> e - in loop e + | MVal e -> loop o (push_susp e s) + | _ -> mkMetavar (id, adjust_subst o s, name) + in loop 0 e

let move_typelevel_to_front ctx mfvs = (* TypeLevel arguments have to come first, so move them accordingly. *) @@ -418,17 +520,17 @@ let generalize (nctx : elab_context) e = let len = List.length mfvs in let mfvs = move_typelevel_to_front (ectx_to_lctx nctx) mfvs in fun wrap e -> - let rec loop ids n mfvs = match mfvs with - | [] -> assert (n = 0); - let e = mkSusp e (S.shift len) in - meta_to_var ids 0 e + let rec loop ids n mfvs = + assert (n = IMap.cardinal ids); + match mfvs with + | [] -> assert (n = len); + meta_to_var ids e | ((id, vname, mt) :: mfvs) - -> let mt' = mkSusp mt (S.shift (len - n)) in - let mt'' = meta_to_var ids (- n) mt' in - let n = n - 1 in + -> let mt' = meta_to_var ids mt in + let n = n + 1 in let e' = loop (IMap.add id n ids) n mfvs in - wrap (IMap.mem id nes) vname mt'' l e' in - loop (IMap.empty) len mfvs + wrap (IMap.mem id nes) vname mt' l e' in + loop (IMap.empty) 0 mfvs

let elab_p_id ((l,name) : symbol) : vname = (l, match name with "_" -> None | _ -> Some name) @@ -551,8 +653,7 @@ and infer_type pexp ectx var = s (ectx_to_lctx ectx) with | (_::_) - -> (let lexp_string e = lexp_string (L.clean e) in - let typestr = lexp_string t ^ " : " ^ lexp_string s in + -> (let typestr = lexp_string t ^ " : " ^ lexp_string s in match var with | (l, None) -> lexp_error l t ("`" ^ typestr ^ "` is not a proper type") @@ -938,13 +1039,12 @@ and track_fv rctx lctx e = name ^ " (" ^ track_fv (Myers.nthcdr drop rctx) (Myers.nthcdr drop lctx) - (L.clean e) + e ^ ")" | _ -> name in String.concat " " (List.map tfv nc)

and lexp_eval ectx e = - let e = L.clean e in let ee = OL.erase_type e in let rctx = EV.from_ectx ectx in

@@ -1034,10 +1134,10 @@ and lexp_check_decls (ectx : elab_context) (* External context. *) and infer_and_generalize_type (ctx : elab_context) se name = let nctx = ectx_new_scope ctx in let t = infer_type se nctx name in - (* FIXME: We should not generalize over metavars which only occur on the rightmost + (* We should not generalize over metavars which only occur on the rightmost * side of arrows in type annotations (aka declarations), since there's no * way for the callee to return something of the proper type if those - * metavar's don't also occur somewhere in the arguments. + * metavars don't also occur somewhere in the arguments. * E.g. for annotations like * * x : ?; @@ -1050,16 +1150,21 @@ and infer_and_generalize_type (ctx : elab_context) se name = * * since there can't be corresponding definitions. So replace the final * return type with some arbitrary closed constant before computing the - * set of free metavars. *) - match OL.lexp_whnf t (ectx_to_lctx ctx) with - (* There's no point generalizing a single metavar, and it's useful - * to keep it ungeneralized so we can use `x : ?` to declare that - * `x` will be defined later without specifying its type yet. *) - | Metavar _ -> t - | _ -> let g = generalize nctx t in - g (fun _ne name t l e - -> mkArrow (Aerasable, name, t, l, e)) - t + * set of free metavars. + * The same argument holds for other *positive* positions, e.g. + * + * f : (? -> Int) -> Int; + * + * But we don't bother trying to catch all cases currently. + *) + let rec strip_rettype t = match t with + | Arrow (ak, v, t1, l, t2) -> Arrow (ak, v, t1, l, strip_rettype t2) + | Sort _ | Metavar _ -> type0 (* Abritrary closed constant. *) + | _ -> t in + let g = generalize nctx (strip_rettype t) in + g (fun _ne name t l e + -> mkArrow (Aerasable, name, t, l, e)) + t

and infer_and_generalize_def (ctx : elab_context) se = let nctx = ectx_new_scope ctx in @@ -1225,7 +1330,7 @@ and sform_new_attribute ctx loc sargs ot = * is False, for example): Should be a type like `AttributeMap t` * instead. *) (mkBuiltin ((loc, "new-attribute"), - OL.lexp_close (ectx_to_lctx ctx) ltp, + L.clean (OL.lexp_close (ectx_to_lctx ctx) ltp), Some AttributeMap.empty), Lazy) | _ -> fatal ~loc "new-attribute expects a single Type argument" @@ -1241,7 +1346,7 @@ and sform_add_attribute ctx loc (sargs : sexp list) ot = | _ -> fatal ~loc "add-attribute expects a table as first argument" in

(* FIXME: Type check (attr: type == attr_type) *) - let attr' = OL.lexp_close (ectx_to_lctx ctx) attr in + let attr' = L.clean (OL.lexp_close (ectx_to_lctx ctx) attr) in let table = AttributeMap.add var attr' map in (mkBuiltin ((loc, "add-attribute"), attr_type, Some table), Lazy) @@ -1302,7 +1407,11 @@ let sform_built_in ctx loc sargs ot = | true, [String (_, name)] -> (match ot with | Some ltp - -> let ltp' = OL.lexp_close (ectx_to_lctx ctx) ltp in + (* FIXME: This `L.clean` is basically the last remaining use of the + * function. It's not indispensible, tho it might still be useful for + * performance of type-inference (at least until we have proper + * memoization of push_susp and/or whnf). *) + -> let ltp' = L.clean (OL.lexp_close (ectx_to_lctx ctx) ltp) in let bi = mkBuiltin ((loc, name), ltp', None) in if not (SMap.mem name (!EV.builtin_functions)) then sexp_error loc ("Unknown built-in `" ^ name ^ "`"); @@ -1512,8 +1621,7 @@ let rec sform_lambda kind ctx loc sargs ot = * in order to account for the fact that `arg` and `v` * might not be the same name! *) | Some lt2 - -> let s = S.cons (mkVar (arg, 0)) (S.shift 1) in - Some (mkSusp lt2 s) in + -> Some (srename arg lt2) in let (lbody, alt) = elaborate nctx sbody olt2 in (mkLambda (kind, arg, lt1, lbody), match alt with @@ -1533,10 +1641,20 @@ let rec sform_lambda kind ctx loc sargs ot = -> (match olt1 with | None -> () | Some lt1' - -> if not (OL.conv_p (ectx_to_lctx ctx) lt1 lt1') - then lexp_error (lexp_location lt1') lt1' - ("Type mismatch! Context expected `" - ^ lexp_string lt1 ^ "`")); + -> (match Unif.unify lt1' lt1 (ectx_to_lctx ctx) with + | ((ck, _ctx, t1, t2)::_) + -> lexp_error (lexp_location lt1') lt1' + ("Type mismatch(" + ^ (match ck with | Unif.CKimpossible -> "impossible" + | Unif.CKresidual -> "residue") + ^ ")! Context expected:\n " + ^ lexp_string lt1 ^ "\nbut parameter has type:\n " + ^ lexp_string lt1' ^ "\ncan't unify:\n " + ^ lexp_string t1 + ^ "\nwith:\n " + ^ lexp_string t2); + assert (not (OL.conv_p (ectx_to_lctx ctx) lt1' lt1)) + | [] -> ())); mklam lt1 (Some lt2)

| Arrow (ak2, v, lt1, _, lt2) when kind = Anormal

===================================== src/eval.ml ===================================== @@ -552,20 +552,11 @@ and eval_decls (decls: (vname * elexp) list) (String -> Sexp) -> (Int -> Sexp) -> (Float -> Sexp) -> (List Sexp -> Sexp) -> Sexp *) and sexp_dispatch loc depth args = - let eval a b = eval a b depth in - let sxp, nd, ctx_nd, - sym, ctx_sym, - str, ctx_str, - it, ctx_it, - flt, ctx_flt, - blk, ctx_blk = match args with - (* FIXME: Don't match against `Closure` to later use `eval`, instead - * pass the value to "funcall". *) - | [sxp; Closure(_, nd, ctx_nd); Closure(_, sym, ctx_sym); - Closure(_, str, ctx_str); Closure(_, it, ctx_it); - Closure(_, flt, ctx_flt); Closure(_, blk, ctx_blk)] -> - sxp, nd, ctx_nd, sym, ctx_sym, str, ctx_str, it, ctx_it, - flt, ctx_flt, blk, ctx_blk + let trace_dum = (Var ((loc, None), -1)) in + let eval_call a b = eval_call loc trace_dum depth a b in + let sxp, nd, sym, str, it, flt, blk = match args with + | [sxp; nd; sym; str; it; flt; blk] -> + sxp, nd, sym, str, it, flt, blk | _ -> error loc "sexp_dispatch expects 7 arguments" in

let sxp = match sxp with @@ -573,34 +564,17 @@ and sexp_dispatch loc depth args = | _ -> value_fatal loc sxp "sexp_dispatch expects a Sexp as 1st arg" in

match sxp with - | Node (op, s) ->( - let rctx = ctx_nd in - let rctx = add_rte_variable vdummy (Vsexp(op)) rctx in - let rctx = add_rte_variable vdummy (o2v_list s) rctx in - match eval nd rctx with - | Closure(_, nd, _) -> eval nd rctx - | _ -> error loc "Node has 2 arguments") - - | Symbol (_ , s) -> - let rctx = ctx_sym in - eval sym (add_rte_variable vdummy (Vstring s) rctx) - | String (_ , s) -> - let rctx = ctx_str in - eval str (add_rte_variable vdummy (Vstring s) rctx) - | Integer (_ , i) -> - let rctx = ctx_it in - eval it (add_rte_variable vdummy (Vinteger (BI.of_int i)) - rctx) - | Float (_ , f) -> - let rctx = ctx_flt in - eval flt (add_rte_variable vdummy (Vfloat f) rctx) + | Node (op, s) -> eval_call nd [Vsexp op; o2v_list s] + | Symbol (_ , s) -> eval_call sym [Vstring s] + | String (_ , s) -> eval_call str [Vstring s] + | Integer (_ , i) -> eval_call it [Vint i] + | Float (_ , f) -> eval_call flt [Vfloat f] | Block (_ , _, _) as b -> (* I think this code breaks what Blocks are. *) (* We delay parsing but parse with default_stt and default_grammar... *) (*let toks = Lexer.lex default_stt s in let s = sexp_parse_all_to_list default_grammar toks (Some ";") in*) - let rctx = ctx_blk in - eval blk (add_rte_variable vdummy (Vsexp b) rctx) + eval_call blk [Vsexp b]

(* -------------------------------------------------------------------------- *) and print_eval_result i lxp = @@ -1113,16 +1087,15 @@ let from_lctx (lctx: lexp_context): runtime_env = Myers.cons (loname, ref (match def with | LetDef (_, e) - -> let e = L.clean e in - if closed_p rctx (OL.fv e) then - eval (OL.erase_type e) rctx - else Vundefined + -> if closed_p rctx (OL.fv e) then + eval (OL.erase_type e) rctx + else Vundefined | _ -> Vundefined)) rctx | CVfix (defs, lctx) -> let fvs = List.fold_left (fun fvs (_, e, _) - -> OL.fv_union fvs (OL.fv (L.clean e))) + -> OL.fv_union fvs (OL.fv e)) OL.fv_empty defs in let rctx = from_lctx lctx in

===================================== src/inverse_subst.ml ===================================== @@ -1,6 +1,6 @@ (* inverse_subst.ml --- Computing the inverse of a substitution

-Copyright (C) 2016-2019 Free Software Foundation, Inc. +Copyright (C) 2016-2020 Free Software Foundation, Inc.

Author: Vincent Bonnevalle tiv.crb@gmail.com

@@ -253,7 +253,7 @@ and apply_inv_subst (e : lexp) (s : subst) : lexp = match e with | SortLevel (SLz) -> e | SortLevel (SLsucc e) -> mkSortLevel (mkSLsucc (apply_inv_subst e s)) | SortLevel (SLlub (e1, e2)) - (* Should we use mkSLlub? *) + (* FIXME: use mkSLlub? *) -> mkSortLevel (mkSLlub' (apply_inv_subst e1 s, apply_inv_subst e2 s)) | Sort (l, Stype e) -> mkSort (l, Stype (apply_inv_subst e s)) | Sort (l, (StypeOmega | StypeLevel)) -> e @@ -293,7 +293,7 @@ and apply_inv_subst (e : lexp) (s : subst) : lexp = match e with L.rev ncase) cases in mkInductive (l, label, nargs, ncases) - | Cons (it, name) -> Cons (apply_inv_subst it s, name) + | Cons (it, name) -> mkCons (apply_inv_subst it s, name) | Case (l, e, ret, cases, default) -> mkCase (l, apply_inv_subst e s, apply_inv_subst ret s, SMap.map (fun (l, cargs, e)

===================================== src/lexp.ml ===================================== @@ -295,6 +295,15 @@ and slookup s l v = S.lookup (fun l i -> mkVar (l, i)) s l v let ssink = S.sink (fun l i -> mkVar (l, i))

+(* Apply a "dummy" substitution which replace #0 with #0 + * in order to account for changes to a variable's name. + * This should probably be made into a no-op, but only after we get rid + * of the check in DB.lookup that a `Var` has the same name as the + * one stored in the lctx! + * Using DeBruijn *should* make α-renaming unnecessary + * so this is a real PITA! :-( *) +let srename name le = mkSusp le (S.cons (mkVar (name, 0)) (S.shift 1)) + (* Shift by a negative amount! *) let rec sunshift n = if n = 0 then S.identity @@ -393,7 +402,7 @@ let rec push_susp e s = (* Push a suspension one level down. *) L.rev ncase) cases in mkInductive (l, label, nargs, ncases) - | Cons (it, name) -> Cons (mkSusp it s, name) + | Cons (it, name) -> mkCons (mkSusp it s, name) | Case (l, e, ret, cases, default) -> mkCase (l, mkSusp e s, mkSusp ret s, SMap.map (fun (l, cargs, e) @@ -631,7 +640,6 @@ and lexp_name e = type print_context_value = | Bool of bool | Int of int - | Expr of lexp option | Predtl of grammar (* precedence table *)

type print_context = print_context_value SMap.t @@ -646,8 +654,6 @@ let pretty_ppctx = ("color" , Bool (true) ); (* use console color to display hints *) ("separate_decl" , Bool (true) ); (* print newline between declarations *) ("indent_level" , Int (0) ); (* current indent level *) - ("parent" , Expr (None) ); (* parent expression *) - ("metavar" , Expr (None) ); (* metavar being printed *) ("col_max" , Int (80) ); (* col_size + col_ofsset <= col_max *) ("col_size" , Int (0) ); (* current column size *) ("col_ofsset" , Int (0) ); (* if col does not start at 0 *) @@ -669,8 +675,6 @@ let smap_bool s ctx = match SMap.find s ctx with Bool b -> b | _ -> failwith "Unreachable" and smap_int s ctx = match SMap.find s ctx with Int i -> i | _ -> failwith "Unreachable" -and smap_lexp s ctx = - match SMap.find s ctx with Expr e -> e | _ -> failwith "Unreachable" and smap_predtl s ctx = match SMap.find s ctx with Predtl tl -> tl | _ -> failwith "Unreachable"

@@ -681,8 +685,6 @@ let pp_size = smap_int "indent_size" let pp_color = smap_bool "color" let pp_decl = smap_bool "separate_decl" let pp_indent = smap_int "indent_level" -let pp_parent = smap_lexp "parent" -let pp_meta = smap_lexp "metavar" let pp_grammar = smap_predtl "grammar" let pp_colsize = smap_int "col_size" let pp_colmax = smap_int "col_max" @@ -692,8 +694,6 @@ let pp_implicit = smap_bool "print_implicit" let set_col_size p ctx = SMap.add "col_size" (Int p) ctx let add_col_size p ctx = set_col_size ((pp_colsize ctx) + p) ctx let reset_col_size ctx = set_col_size 0 ctx -let set_parent p ctx = SMap.add "parent" (Expr (Some p)) ctx -let set_meta p ctx = SMap.add "metavar" (Expr (Some p)) ctx let add_indent ctx i = SMap.add "indent_level" (Int ((pp_indent ctx) + i)) ctx

let pp_append_string buffer ctx str = @@ -743,7 +743,6 @@ and lexp_cstring ctx e = lexp_str ctx e (* Implementation *) and lexp_str ctx (exp : lexp) : string =

- let ctx = set_parent exp ctx in let inter_ctx = add_indent ctx 1 in let lexp_str' = lexp_str ctx in let lexp_stri idt e = lexp_str (add_indent ctx idt) e in @@ -805,15 +804,9 @@ and lexp_str ctx (exp : lexp) : string =

| Metavar (idx, subst, (loc, name)) (* print metavar result if any *) - -> (let print_meta exp = - let ctx = set_meta exp ctx in - lexp_str ctx (clean exp) in - - match pp_meta ctx with - | None -> print_meta exp - | Some e when e != exp -> print_meta exp - | _ -> - "?" ^ maybename name ^ (subst_string subst) ^ (index idx)) + -> (match metavar_lookup idx with + | MVal e -> lexp_str ctx e + | _ -> "?" ^ maybename name ^ (subst_string subst) ^ (index idx))

| Let (_, decls, body) -> (* Print first decls without indent *)

===================================== src/opslexp.ml ===================================== @@ -113,7 +113,7 @@ let lexp_close lctx e = * - It turns the lctx (of O(log N) access time) into a subst * (of O(N) access time) * Oh well! *) - L.clean (mkSusp e (lctx_to_subst lctx)) + mkSusp e (lctx_to_subst lctx)

(** Reduce to weak head normal form. @@ -177,7 +177,10 @@ let lexp_whnf e (ctx : DB.lexp_context) : lexp = mkCase (l, e, rt, branches, default) in (match e' with | Cons (_, (_, name)) -> reduce name [] - | Call (Cons (_, (_, name)), aargs) -> reduce name aargs + | Call (f, aargs) -> + (match lexp_whnf f ctx with + | Cons (_, (_, name)) -> reduce name aargs + | _ -> mkCase (l, e, rt, branches, default)) | _ -> mkCase (l, e, rt, branches, default)) | Metavar (idx, s, _) -> (match metavar_lookup idx with @@ -231,6 +234,7 @@ let level_canon e = | SortLevel SLz -> if c < d then (d, m) else acc | SortLevel (SLsucc e) -> canon e (d + 1) acc | SortLevel (SLlub (e1, e2)) -> canon e1 d (canon e2 d acc) + (* FIXME: Apply substitutions from surrounding `Let` bindings. *) | Var (_, i) -> add_var_depth i d acc | Metavar (i, s, _) -> (match metavar_lookup i with @@ -263,8 +267,8 @@ let rec conv_p' (ctx : DB.lexp_context) (vs : set_plexp) e1 e2 : bool = -> (match (sl1, sl2) with | (SLz, SLz) -> true | (SLsucc sl1, SLsucc sl2) -> conv_p sl1 sl2 - | _ -> let ce1 = level_canon (L.clean e1') in - let ce2 = level_canon (L.clean e2') in + | _ -> let ce1 = level_canon e1' in + let ce2 = level_canon e2' in level_leq ce1 ce2 && level_leq ce2 ce1) | (Sort (_, s1), Sort (_, s2)) -> s1 == s2 @@ -277,7 +281,7 @@ let rec conv_p' (ctx : DB.lexp_context) (vs : set_plexp) e1 e2 : bool = -> ak1 == ak2 && conv_p t11 t21 && conv_p' (DB.lexp_ctx_cons ctx vd1 Variable t11) (set_shift vs') - t12 t22 + t12 (srename vd1 t22) | (Lambda (ak1, l1, t1, e1), Lambda (ak2, l2, t2, e2)) -> ak1 == ak2 && (conv_erase || conv_p t1 t2) && conv_p' (DB.lexp_ctx_cons ctx l1 Variable t1) @@ -334,8 +338,8 @@ let rec mkSLlub ctx e1 e2 = | (SortLevel (SLsucc e1), SortLevel (SLsucc e2)) -> mkSortLevel (SLsucc (mkSLlub ctx e1 e2)) | (e1', e2') - -> let ce1 = level_canon (L.clean e1') in - let ce2 = level_canon (L.clean e2') in + -> let ce1 = level_canon e1' in + let ce2 = level_canon e2' in if level_leq ce1 ce2 then e2 else if level_leq ce2 ce1 then e1 else mkSortLevel (mkSLlub' (e1, e2)) (* FIXME: Could be more canonical *) @@ -420,9 +424,9 @@ let rec check'' erased ctx e = if conv_p ctx t t' then () else (error_tc ~loc:(lexp_location e) ("Type mismatch for " - ^ lexp_string (L.clean e) ^ " : " - ^ lexp_string (L.clean t) ^ " != " - ^ lexp_string (L.clean t')); + ^ lexp_string e ^ " : " + ^ lexp_string t ^ " != " + ^ lexp_string t'); (* Log.internal_error "Type mismatch" *)) in let check_type erased ctx t = let s = check erased ctx t in @@ -939,7 +943,11 @@ let rec erase_type (lxp: L.lexp): E.elexp = | L.Sort _ -> E.Type lxp (* Still useful to some extent. *) | L.Inductive(l, label, _, _) -> E.Type lxp - | L.Metavar _ -> Log.internal_error "Metavar in erase_type" + | Metavar (idx, s, _) + -> (match metavar_lookup idx with + | MVal e -> erase_type (push_susp e s) + | MVar (_, t, _) + -> Log.internal_error "Metavar in erase_type")

and filter_arg_list lst = let rec filter_arg_list lst acc =

===================================== src/unification.ml ===================================== @@ -190,20 +190,26 @@ and unify' (e1: lexp) (e2: lexp) if changed && OL.set_member_p vs e1' e2' then [] else let vs' = if changed then OL.set_add vs e1' e2' else vs in match (e1', e2') with - | ((Imm _, Imm _) | (Cons _, Cons _) | (Builtin _, Builtin _) - | (Var _, Var _)) + | ((Imm _, Imm _) | (Cons _, Cons _) | (Builtin _, Builtin _)) -> if OL.conv_p ctx e1' e2' then [] else [(CKimpossible, ctx, e1, e2)] | (l, (Metavar (idx, s, _) as r)) -> unify_metavar ctx idx s r l | ((Metavar (idx, s, _) as l), r) -> unify_metavar ctx idx s l r - | (l, (Call _ as r)) -> unify_call r l ctx vs' - (* | (l, (Case _ as r)) -> unify_case r l subst *) - | (Arrow _ as l, r) -> unify_arrow l r ctx vs' - | (Lambda _ as l, r) -> unify_lambda l r ctx vs' - | (Call _ as l, r) -> unify_call l r ctx vs' - (* | (Case _ as l, r) -> unify_case l r subst *) - (* | (Inductive _ as l, r) -> unify_induct l r subst *) - | (Sort _ as l, r) -> unify_sort l r ctx vs' - | (SortLevel _ as l, r) -> unify_sortlvl l r ctx vs' + | (l, (Call _ as r)) -> unify_call r l ctx vs' + | ((Call _ as l), r) -> unify_call l r ctx vs' + | (l, (Var _ as r)) -> unify_var r l ctx vs' + | ((Var _ as l), r) -> unify_var l r ctx vs' + | (l, (Arrow _ as r)) -> unify_arrow r l ctx vs' + | ((Arrow _ as l), r) -> unify_arrow l r ctx vs' + | (l, (Lambda _ as r)) -> unify_lambda r l ctx vs' + | ((Lambda _ as l), r) -> unify_lambda l r ctx vs' + (* | (l, (Case _ as r)) -> unify_case r l subst *) + (* | ((Case _ as l), r) -> unify_case l r subst *) + (* | (l, (Inductive _ as r)) -> unify_induct r l subst *) + (* | ((Inductive _ as l), r) -> unify_induct l r subst *) + | (l, (Sort _ as r)) -> unify_sort r l ctx vs' + | ((Sort _ as l), r) -> unify_sort l r ctx vs' + | (l, (SortLevel _ as r)) -> unify_sortlvl r l ctx vs' + | ((SortLevel _ as l), r) -> unify_sortlvl l r ctx vs' | (Inductive (_loc1, label1, args1, consts1), Inductive (_loc2, label2, args2, consts2)) -> (* print_string ("Unifying inductives " @@ -222,7 +228,6 @@ and unify' (e1: lexp) (e2: lexp) - (Arrow, Arrow) -> if var_kind = var_kind then unify ltype & lexp (Arrow (var_kind, _, ltype, lexp)) else None - - (Arrow, Var) -> Constraint - (_, _) -> None *) and unify_arrow (arrow: lexp) (lxp: lexp) ctx vs @@ -232,22 +237,16 @@ and unify_arrow (arrow: lexp) (lxp: lexp) ctx vs Arrow (var_kind2, _, ltype2, _, lexp2)) -> if var_kind1 = var_kind2 then (unify' ltype1 ltype2 ctx vs) - @(unify' lexp1 lexp2 + @(unify' lexp1 (srename v1 lexp2) (DB.lexp_ctx_cons ctx v1 Variable ltype1) (OL.set_shift vs)) - else [(CKimpossible, ctx, arrow, lxp)] - | (Arrow _, Imm _) -> [(CKimpossible, ctx, arrow, lxp)] - | (Arrow _, Var _) -> ([(CKresidual, ctx, arrow, lxp)]) - | (Arrow _, _) -> unify' lxp arrow ctx vs + else [(CKimpossible, ctx, arrow, lxp)] | (_, _) -> [(CKimpossible, ctx, arrow, lxp)]

(** Unify a Lambda and a lexp if possible - - Lamda , Lambda -> if var_kind = var_kind + - Lambda , Lambda -> if var_kind = var_kind then UNIFY ltype & lxp else ERROR - - Lambda , Var -> CONSTRAINT - - Lambda , Call -> Constraint - - Lambda , Let -> Constraint - - Lambda , lexp -> unify lexp lambda subst + - Lambda , _ -> Impossible *) and unify_lambda (lambda: lexp) (lxp: lexp) ctx vs : return_type = match (lambda, lxp) with @@ -259,19 +258,12 @@ and unify_lambda (lambda: lexp) (lxp: lexp) ctx vs : return_type = (DB.lexp_ctx_cons ctx v1 Variable ltype1) (OL.set_shift vs)) else [(CKimpossible, ctx, lambda, lxp)] - | ((Lambda _, Var _) - | (Lambda _, Let _) - | (Lambda _, Call _)) -> [(CKresidual, ctx, lambda, lxp)] - | (Lambda _, Arrow _) - | (Lambda _, Imm _) -> [(CKimpossible, ctx, lambda, lxp)] - | (Lambda _, _) -> unify' lxp lambda ctx vs - | (_, _) -> [(CKimpossible, ctx, lambda, lxp)] + | (_, _) -> [(CKimpossible, ctx, lambda, lxp)]

(** Unify a Metavar and a lexp if possible - - lexp , {metavar <-> none} -> UNIFY - - lexp , {metavar <-> lexp} -> UNFIFY lexp subst[metavar] - - metavar , metavar -> if Metavar = Metavar then OK else ERROR - - metavar , lexp -> OK + - metavar , metavar -> if Metavar = Metavar then intersect + - metavar , metavar -> inverse subst (both sides) + - metavar , lexp -> inverse subst *) and unify_metavar ctx idx s1 (lxp1: lexp) (lxp2: lexp) : return_type = @@ -296,8 +288,8 @@ and unify_metavar ctx idx s1 (lxp1: lexp) (lxp2: lexp) | _ -> log_info ?loc:None ("Unification of metavar type failed:\n " - ^ lexp_string (Lexp.clean t) ^ " != " - ^ lexp_string (Lexp.clean (OL.get_type ctx lxp)) + ^ lexp_string t ^ " != " + ^ lexp_string (OL.get_type ctx lxp) ^ "\n" ^ "for " ^ lexp_string lxp ^ "\n"); [(CKresidual, ctx, lxp1, lxp2)] in match lxp2 with @@ -364,6 +356,16 @@ and unify_metavar ctx idx s1 (lxp1: lexp) (lxp2: lexp) | _ -> unif idx2 s2 lxp1) | _ -> unif idx s1 lxp2

+(** Unify a Var (var) and a lexp (lxp) + - Var , Var -> IF same var THEN ok ELSE constraint + - Var , lexp -> Constraint +*) +and unify_var (var: lexp) (lxp: lexp) ctx vs + : return_type = + match (var, lxp) with + | (Var _, Var _) when OL.conv_p ctx var lxp -> [] + | (_, _) -> [(CKresidual, ctx, var, lxp)] + (** Unify a Call (call) and a lexp (lxp) - Call , Call -> UNIFY - Call , lexp -> CONSTRAINT @@ -452,7 +454,6 @@ and unify_sortlvl (sortlvl: lexp) (lxp: lexp) ctx vs : return_type =

(** Unify a Sort and a lexp - Sort, Sort -> if Sort ~= Sort then OK else ERROR - - Sort, Var -> Constraint - Sort, lexp -> ERROR *) and unify_sort (sort_: lexp) (lxp: lexp) ctx vs : return_type = @@ -462,7 +463,6 @@ and unify_sort (sort_: lexp) (lxp: lexp) ctx vs : return_type = | StypeOmega, StypeOmega -> [] | StypeLevel, StypeLevel -> [] | _, _ -> [(CKimpossible, ctx, sort_, lxp)]) - | Sort _, Var _ -> [(CKresidual, ctx, sort_, lxp)] | _, _ -> [(CKimpossible, ctx, sort_, lxp)]

(************************ Helper function ************************************)

View it on GitLab: https://gitlab.com/monnier/typer/-/compare/386de0963b1b57e1ee89e36077294f1ff...