Stefan pushed to branch master at Stefan / Typer

Commits: 31ee7094 by Stefan Monnier at 2017-07-12T00:07:13-04:00 * src/elab.ml (lexp_decls_1): Accept multiple decls for the same var

- - - - -

3 changed files:

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

Changes:

===================================== btl/builtins.typer ===================================== --- a/btl/builtins.typer +++ b/btl/builtins.typer @@ -115,6 +115,10 @@ Sexp_eq = Built-in "Sexp.=" (Sexp -> Sexp -> Bool); %% List %% -----------------------------------------------------

+%% FIXME: "List : ?" should be sufficient but triggers +%% [!] Error ELAB `(List[2] a[1]) : ?ta · Id[18]` is not a proper type +%% > Call: (List[2] a[1]) +%% "Subst-inversion-bug: <anon> · (↑2 () · () · () · Id) ∘ <anon0> · () · (↑4 Id) == <anon> · () · (↑2 Id) !!" List : Type -> Type; %% List a = typecons List (nil) (cons a (List a)); %% nil = lambda a ≡> datacons (List a) nil;

===================================== btl/pervasive.typer ===================================== --- a/btl/pervasive.typer +++ b/btl/pervasive.typer @@ -327,9 +327,10 @@ Decidable = typecons (Decidable (prop : Type)) test1 : Option Int; test2 : Option Int; test3 : Option Int; -test4 : Option Int; test1 = test2; +test4 : Option ?; test2 = none; +test4 : Option Int; test4 = test1; test3 = test4;

===================================== src/elab.ml ===================================== --- a/src/elab.ml +++ b/src/elab.ml @@ -385,6 +385,9 @@ and infer_type pexp ectx var = (let meta_ctx, _ = !global_substitution in match OL.lexp_whnf s (ectx_to_lctx ectx) meta_ctx with | Sort (_, _) -> () (* All clear! *) + (* FIXME: We could automatically coerce Type levels to Sorts, so we + * could write `(a : TypeLevel) -> a -> a` instead of + * `(a : TypeLevel) -> Type_ a -> Type_ a` *) | _ -> (* FIXME: Here we rule out TypeLevel/TypeOmega. *) match Unif.unify (mkSort (lexp_location s, Stype (newMetalevel ()))) s @@ -885,8 +888,21 @@ and lexp_decls_1 -> let ltp = infer_type stp (ectx_new_scope nctx) (Some v) in if SMap.mem vname pending_decls then (* Don't burp: take'em all and unify! *) - (error l ("Variable `" ^ vname ^ "` declared twice!"); - lexp_decls_1 sdecls ectx nctx pending_decls pending_defs) + let pt_idx = senv_lookup vname nctx in + (* Take the previous type annotation. *) + let pt = match Myers.nth pt_idx (ectx_to_lctx nctx) with + | (_, _, ForwardRef, t) -> push_susp t (S.shift (pt_idx + 1)) + | _ -> U.internal_error "Var not found at its index!" in + (* Unify it with the new one. *) + let meta_ctx, _ = !global_substitution in + let _ = match Unif.unify ltp pt (ectx_to_lctx nctx) meta_ctx with + | (None | Some (_, _::_)) + -> lexp_error l ltp + ("New type annotation `" + ^ lexp_string ltp ^ "` incompatible with previous `" + ^ lexp_string pt ^ "`") + | Some subst -> global_substitution := subst in + lexp_decls_1 sdecls ectx nctx pending_decls pending_defs else if List.exists (fun ((_, vname'), _) -> vname = vname') pending_defs then (error l ("Variable `" ^ vname ^ "` already defined!");

View it on GitLab: https://gitlab.com/monnier/typer/commit/31ee70949f6176f17872d8b1ce2cb044b139...

--- View it on GitLab: https://gitlab.com/monnier/typer/commit/31ee70949f6176f17872d8b1ce2cb044b139... You're receiving this email because of your account on gitlab.com.