Stefan pushed to branch master at Stefan / Typer

Commits: 60431a62 by Stefan Monnier at 2022-04-15T19:30:26-04:00 Improve support for typelevels in inductive types

* src/opslexp.ml (check''): Allow (erasable) typelevel fields. (get_type): Adjust accordingly.

* src/log.ml (handle_error): Don't catch internal errors.

* src/lexp.ml (mkSLsucc): Add some info in the error.

- - - - -

3 changed files:

- src/lexp.ml - src/log.ml - src/opslexp.ml

Changes:

===================================== src/lexp.ml ===================================== @@ -371,7 +371,8 @@ let mkSLsucc e = match lexp_lexp' e with | SortLevel _ | Var _ | Metavar _ | Susp _ -> SLsucc e - | _ -> Log.log_fatal ~section:"internal" "SLsucc of non-level " + | _ -> Log.log_fatal ~section:"internal" "SLsucc of non-level: %s" + (lexp_head e)

(********************** Lexp tests ************************)

===================================== src/log.ml ===================================== @@ -217,9 +217,11 @@ let handle_error ~(on_error : unit -> 'a) (action : unit -> 'a) : 'a = | User_error message -> show_error ("fatal user error: " ^ message); on_error () - | Internal_error message - -> show_error ("internal error: " ^ message); - on_error () + (* Don't catch these internal errors, so `OCAMLRUNPARAM=b` can + * give us a usable backtrace. + * | Internal_error message + * -> show_error ("internal error: " ^ message); + * on_error () *)

let log_fatal ?section ?print_action ?loc fmt = typer_log_config.print_at_log <- true;

===================================== src/opslexp.ml ===================================== @@ -710,19 +710,25 @@ and check'' erased ctx e = (fun _ case level -> let (level, _, _, _) = List.fold_left - (fun (level, ictx, erased, n) (ak, v, t) -> - ((let lwhnf = lexp_whnf (check_type erased ictx t) ictx in - match lexp_lexp' lwhnf with + (fun (level, ictx, erased, subst) (ak, v, t) -> + let lwhnf = lexp_whnf + (check_type erased ictx t) ictx in + ((match lexp_lexp' lwhnf with | Sort (_, Stype _) when ak == P.Aerasable && impredicative_erase -> level | Sort (_, Stype level') -> mkSLlub ctx level - (* We need to unshift because the final type - * cannot refer to the fields! *) - (* FIXME: If it does refer, - * we get an ugly error! *) - (mkSusp level' (L.sunshift n)) + (mkSusp level' subst) + | Sort (_, StypeLevel) + -> (if not(ak == P.Aerasable + && impredicative_universe_poly) + then log_tc_error + ~loc:(lexp_location t) + ~print_action:(fun _ -> ()) + "Field of type %s not-allowed!" + (lexp_string t)); + level | _tt -> log_tc_error ~loc:(lexp_location t) @@ -733,8 +739,15 @@ and check'' erased ctx e = level), DB.lctx_extend ictx v Variable t, DB.set_sink 1 erased, - n + 1)) - (level, ctx, erased, 0) + (* The final type(level) cannot refer + * to the fields! *) + S.cons + (match lexp_lexp' lwhnf with + (* The non-erasable case is tested above! *) + | Sort (_, StypeLevel) -> DB.level0 + | _ -> impossible) + subst)) + (level, ctx, erased, S.identity) case in level) cases (mkSortLevel SLz) in @@ -1143,20 +1156,25 @@ and get_type ctx e = (fun _ case level -> let (level, _, _) = List.fold_left - (fun (level, ictx, n) (ak, v, t) -> - ((match lexp'_whnf (get_type ictx t) ictx with + (fun (level, ictx, subst) (ak, v, t) -> + let s = lexp'_whnf (get_type ictx t) ictx in + ((match s with | Sort (_, Stype _) when ak == P.Aerasable && impredicative_erase -> level | Sort (_, Stype level') -> mkSLlub ctx level - (* We need to unshift because the final type - * cannot refer to the fields! *) - (mkSusp level' (L.sunshift n)) + (mkSusp level' subst) | _tt -> level), DB.lctx_extend ictx v Variable t, - n + 1)) - (level, ctx, 0) + (* The final type(level) cannot refer + * to the fields! *) + S.cons + (match s with + | Sort (_, StypeLevel) -> DB.level0 + | _ -> impossible) + subst)) + (level, ctx, S.identity) case in level) cases (mkSortLevel SLz) in

View it on GitLab: https://gitlab.com/monnier/typer/-/commit/60431a62a804edb74e98d08978deafc863...