diff options
| -rw-r--r-- | kernel/environ.ml | 5 | ||||
| -rw-r--r-- | kernel/environ.mli | 1 | ||||
| -rw-r--r-- | pretyping/evardefine.ml | 24 | ||||
| -rw-r--r-- | pretyping/evardefine.mli | 8 | ||||
| -rw-r--r-- | pretyping/pretyping.ml | 29 | ||||
| -rw-r--r-- | test-suite/bugs/closed/bug_12623.v | 18 | ||||
| -rw-r--r-- | test-suite/bugs/closed/bug_5197.v | 6 |
7 files changed, 58 insertions, 33 deletions
diff --git a/kernel/environ.ml b/kernel/environ.ml index e497b7904a..dec9e1deb8 100644 --- a/kernel/environ.ml +++ b/kernel/environ.ml @@ -274,6 +274,11 @@ let is_impredicative_sort env = function let is_impredicative_univ env u = is_impredicative_sort env (Sorts.sort_of_univ u) +let is_impredicative_family env = function + | Sorts.InSProp | Sorts.InProp -> true + | Sorts.InSet -> is_impredicative_set env + | Sorts.InType -> false + let type_in_type env = not (typing_flags env).check_universes let deactivated_guard env = not (typing_flags env).check_guarded diff --git a/kernel/environ.mli b/kernel/environ.mli index 47a118aa42..f443ba38e1 100644 --- a/kernel/environ.mli +++ b/kernel/environ.mli @@ -122,6 +122,7 @@ val indices_matter : env -> bool val is_impredicative_sort : env -> Sorts.t -> bool val is_impredicative_univ : env -> Univ.Universe.t -> bool +val is_impredicative_family : env -> Sorts.family -> bool (** is the local context empty *) val empty_context : env -> bool diff --git a/pretyping/evardefine.ml b/pretyping/evardefine.ml index f33030d6a4..eaf8c65811 100644 --- a/pretyping/evardefine.ml +++ b/pretyping/evardefine.ml @@ -175,10 +175,7 @@ let define_evar_as_sort env evd (ev,args) = let evd' = Evd.define ev (mkSort s) evd in Evd.set_leq_sort env evd' (Sorts.super s) (ESorts.kind evd' sort), s -(* Propagation of constraints through application and abstraction: - Given a type constraint on a functional term, returns the type - constraint on its domain and codomain. If the input constraint is - an evar instantiate it with the product of 2 new evars. *) +(* Unify with unknown array *) let rec presplit env sigma c = let c = Reductionops.whd_all env sigma c in @@ -189,25 +186,6 @@ let rec presplit env sigma c = presplit env sigma (mkApp (lam, args)) | _ -> sigma, c -let split_tycon ?loc env evd tycon = - match tycon with - | None -> evd,(make_annot Anonymous Relevant,None,None) - | Some c -> - let evd, c = presplit env evd c in - let evd, na, dom, rng = match EConstr.kind evd c with - | Prod (na,dom,rng) -> evd, na, dom, rng - | Evar ev -> - let (evd,prod) = define_evar_as_product env evd ev in - let (na,dom,rng) = destProd evd prod in - let anon = {na with binder_name = Anonymous} in - evd, anon, dom, rng - | _ -> - (* XXX no error to allow later coercion? Not sure if possible with funclass *) - error_not_product ?loc env evd c - in - evd, (na, mk_tycon dom, mk_tycon rng) - - let define_pure_evar_as_array env sigma evk = let evi = Evd.find_undefined sigma evk in let evenv = evar_env env evi in diff --git a/pretyping/evardefine.mli b/pretyping/evardefine.mli index e5c3f8baa1..5702e169c8 100644 --- a/pretyping/evardefine.mli +++ b/pretyping/evardefine.mli @@ -8,7 +8,6 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) -open Names open EConstr open Evd open Environ @@ -31,10 +30,6 @@ val mk_valcon : constr -> val_constraint val evar_absorb_arguments : env -> evar_map -> existential -> constr list -> evar_map * existential -val split_tycon : - ?loc:Loc.t -> env -> evar_map -> type_constraint -> - evar_map * (Name.t Context.binder_annot * type_constraint * type_constraint) - val split_as_array : env -> evar_map -> type_constraint -> evar_map * type_constraint (** If the constraint can be made to look like [array A] return [A], @@ -51,3 +46,6 @@ val define_evar_as_sort : env -> evar_map -> existential -> evar_map * Sorts.t val pr_tycon : env -> evar_map -> type_constraint -> Pp.t +(** Used for bidi heuristic when typing lambdas. Transforms an applied + evar to an evar with bigger context (ie ?X e to ?X'@{y=e}). *) +val presplit : env -> evar_map -> EConstr.t -> evar_map * EConstr.t diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index b9825b6a92..7597661ca8 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -925,7 +925,32 @@ struct let sigma, ty' = Coercion.inh_coerce_to_prod ?loc ~program_mode !!env sigma ty in sigma, Some ty' in - let sigma, (name',dom,rng) = split_tycon ?loc !!env sigma tycon' in + let sigma,name',dom,rng = + match tycon' with + | None -> sigma,Anonymous, None, None + | Some ty -> + let sigma, ty = Evardefine.presplit !!env sigma ty in + match EConstr.kind sigma ty with + | Prod (na,dom,rng) -> + sigma, na.binder_name, Some dom, Some rng + | Evar ev -> + (* define_evar_as_product works badly when impredicativity + is possible but not known (#12623). OTOH if we know we + are impredicative (typically Prop) we want to keep the + information when typing the body. *) + let s = Retyping.get_sort_of !!env sigma ty in + if Environ.is_impredicative_sort !!env s + || Evd.check_leq sigma (Univ.Universe.type1) (Sorts.univ_of_sort s) + then + let sigma, prod = define_evar_as_product !!env sigma ev in + let na,dom,rng = destProd sigma prod in + sigma, na.binder_name, Some dom, Some rng + else + sigma, Anonymous, None, None + | _ -> + (* XXX no error to allow later coercion? Not sure if possible with funclass *) + error_not_product ?loc !!env sigma ty + in let dom_valcon = valcon_of_tycon dom in let sigma, j = eval_type_pretyper self ~program_mode ~poly resolve_tc dom_valcon env sigma c1 in let name = {binder_name=name; binder_relevance=Sorts.relevance_of_sort j.utj_type} in @@ -934,7 +959,7 @@ struct let var',env' = push_rel ~hypnaming sigma var env in let sigma, j' = eval_pretyper self ~program_mode ~poly resolve_tc rng env' sigma c2 in let name = get_name var' in - let resj = judge_of_abstraction !!env (orelse_name name name'.binder_name) j j' in + let resj = judge_of_abstraction !!env (orelse_name name name') j j' in discard_trace @@ inh_conv_coerce_to_tycon ?loc ~program_mode resolve_tc env sigma resj tycon let pretype_prod self (name, bk, c1, c2) = diff --git a/test-suite/bugs/closed/bug_12623.v b/test-suite/bugs/closed/bug_12623.v new file mode 100644 index 0000000000..9fdcb94e0c --- /dev/null +++ b/test-suite/bugs/closed/bug_12623.v @@ -0,0 +1,18 @@ +Set Universe Polymorphism. + +Axiom M : Type -> Prop. +Axiom raise : forall {T}, M T. + +Inductive goal : Type := +| AHyp : forall {A : Type}, goal. + +Definition gtactic@{u u0} := goal@{u} -> M@{u0} (False). + +Class Seq (C : Type) := + seq : C -> gtactic. +Arguments seq {C _} _. + +Instance seq_one : Seq@{Set _ _} (gtactic) := fun t2 => fun g => raise. + +Definition x1 : gtactic := @seq@{_ _ _} _ _ (fun g : goal => raise). +Definition x2 : gtactic := @seq@{_ _ _} _ seq_one (fun g : goal => raise). diff --git a/test-suite/bugs/closed/bug_5197.v b/test-suite/bugs/closed/bug_5197.v index 0c236e12ad..00b9e9bd9d 100644 --- a/test-suite/bugs/closed/bug_5197.v +++ b/test-suite/bugs/closed/bug_5197.v @@ -20,11 +20,11 @@ Definition Typeᶠ : TYPE := {| rel := fun _ A => (forall ω : Ω, A ω) -> Type; |}. Set Printing Universes. -Fail Definition Typeᵇ : El Typeᶠ := +Definition Typeᵇ : El Typeᶠ := mkPack _ _ (fun w => Type) (fun w A => (forall ω, A ω) -> Type). -Definition Typeᵇ : El Typeᶠ := - mkPack _ (fun _ (A : Ω -> Type) => (forall ω : Ω, A ω) -> _) (fun w => Type) (fun w A => (forall ω, A ω) -> Type). +(* Definition Typeᵇ : El Typeᶠ := *) +(* mkPack _ (fun _ (A : Ω -> Type) => (forall ω : Ω, A ω) -> _) (fun w => Type) (fun w A => (forall ω, A ω) -> Type). *) (** Bidirectional typechecking helps here *) Require Import Program.Tactics. |