Stefan pushed to branch master at Stefan / Typer

Commits: b4bacaf0 by Stefan Monnier at 2020-03-17T14:26:41-04:00 * src/opslexp.ml (impredicative_erase): Disable it

(impredicative_universe_poly): Rename from deep_universe_poly.

- - - - -

1 changed file:

- src/opslexp.ml

Changes:

===================================== src/opslexp.ml ===================================== @@ -1,6 +1,6 @@ (* opslexp.ml --- Operations on Lexps

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

Author: Stefan Monnier monnier@iro.umontreal.ca Keywords: languages, lisp, dependent types. @@ -46,11 +46,13 @@ let conv_erase = true (* Makes conv ignore erased terms. *)

(* `impredicative_erase` is inconsistent: as shown in samples/hurkens.typer * it allows the definition of an inf-looping expression of type ⊥. *) -let impredicative_erase = true (* Allows erasable args to be impredicative. *) +let impredicative_erase = false (* Allows erasable args to be impredicative. *)

-(* The safety of `deep_universe_poly` is unknown. - * But I also like the idea. *) -let deep_universe_poly = true (* Assume arg is TypeLevel.z when erasable. *) +(* The safety of `impredicative_universe_poly` is unknown. + * But I also like the idea. + * Furthermore it is sufficient to be able to encode System-F (tho + * I haven't been able to generalize this result to Fω). *) +let impredicative_universe_poly = true (* Assume arg is TypeLevel.z when erasable. *)

(* Lexp context *)

@@ -360,7 +362,7 @@ let sort_compose ctx1 ctx2 l ak k1 k2 = else let l2' = (mkSusp l2 (S.substitute impossible)) in SortResult (mkSort (l, Stype (mkSLlub ctx1 l1 l2'))) | (StypeLevel, Stype l2) - when ak == P.Aerasable && deep_universe_poly + when ak == P.Aerasable && impredicative_universe_poly (* The safety/soundness of this rule is completely unknown. * It's pretty powerful, e.g. allows tuples containing * level-polymorphic functions, and makes impredicative-encoding

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