diff options
| -rw-r--r-- | pretyping/evarsolve.ml | 49 | ||||
| -rw-r--r-- | test-suite/bugs/closed/5197.v | 44 |
2 files changed, 72 insertions, 21 deletions
diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml index 44bfe4b6cc..6f5cba3e03 100644 --- a/pretyping/evarsolve.ml +++ b/pretyping/evarsolve.ml @@ -42,7 +42,6 @@ let get_polymorphic_positions sigma f = let refresh_universes ?(status=univ_rigid) ?(onlyalg=false) ?(refreshset=false) pbty env evd t = let evdref = ref evd in - let modified = ref false in (* direction: true for fresh universes lower than the existing ones *) let refresh_sort status ~direction s = let s = ESorts.kind !evdref s in @@ -51,18 +50,18 @@ let refresh_universes ?(status=univ_rigid) ?(onlyalg=false) ?(refreshset=false) let evd = if direction then set_leq_sort env !evdref s' s else set_leq_sort env !evdref s s' - in - modified := true; evdref := evd; mkSort s' + in evdref := evd; mkSort s' in let rec refresh ~onlyalg status ~direction t = match EConstr.kind !evdref t with | Sort s -> begin match ESorts.kind !evdref s with | Type u -> - (match Univ.universe_level u with + (* TODO: check if max(l,u) is not ok as well *) + (match Univ.universe_level u with | None -> refresh_sort status ~direction s | Some l -> - (match Evd.universe_rigidity evd l with + (match Evd.universe_rigidity !evdref l with | UnivRigid -> if not onlyalg then refresh_sort status ~direction s else t @@ -76,34 +75,43 @@ let refresh_universes ?(status=univ_rigid) ?(onlyalg=false) ?(refreshset=false) refresh_sort status ~direction s | _ -> t end - | Prod (na,u,v) -> - mkProd (na, u, refresh ~onlyalg status ~direction v) + | Prod (na,u,v) -> + let v' = refresh ~onlyalg status ~direction v in + if v' == v then t else mkProd (na, u, v') | _ -> t + in (** Refresh the types of evars under template polymorphic references *) - and refresh_term_evars onevars top t = + let rec refresh_term_evars ~onevars ~top t = match EConstr.kind !evdref t with | App (f, args) when is_template_polymorphic env !evdref f -> let pos = get_polymorphic_positions !evdref f in - refresh_polymorphic_positions args pos + refresh_polymorphic_positions args pos; t | App (f, args) when top && isEvar !evdref f -> - refresh_term_evars true false f; - Array.iter (refresh_term_evars onevars false) args + let f' = refresh_term_evars ~onevars:true ~top:false f in + let args' = Array.map (refresh_term_evars ~onevars ~top:false) args in + if f' == f && args' == args then t + else mkApp (f', args') | Evar (ev, a) when onevars -> let evi = Evd.find !evdref ev in - let ty' = refresh ~onlyalg univ_flexible ~direction:true evi.evar_concl in - if !modified then - evdref := Evd.add !evdref ev {evi with evar_concl = ty'} - else () - | _ -> EConstr.iter !evdref (refresh_term_evars onevars false) t + let ty = evi.evar_concl in + let ty' = refresh ~onlyalg univ_flexible ~direction:true ty in + if ty == ty' then t + else (evdref := Evd.downcast ev ty' !evdref; t) + | Sort s -> + (match ESorts.kind !evdref s with + | Type u when not (Univ.Universe.is_levels u) -> + refresh_sort Evd.univ_flexible ~direction:false s + | _ -> t) + | _ -> EConstr.map !evdref (refresh_term_evars ~onevars ~top:false) t and refresh_polymorphic_positions args pos = let rec aux i = function | Some l :: ls -> if i < Array.length args then - ignore(refresh_term_evars true false args.(i)); + ignore(refresh_term_evars ~onevars:true ~top:false args.(i)); aux (succ i) ls | None :: ls -> if i < Array.length args then - ignore(refresh_term_evars false false args.(i)); + ignore(refresh_term_evars ~onevars:false ~top:false args.(i)); aux (succ i) ls | [] -> () in aux 0 pos @@ -115,9 +123,8 @@ let refresh_universes ?(status=univ_rigid) ?(onlyalg=false) ?(refreshset=false) (* No cumulativity needed, but we still need to refresh the algebraics *) refresh ~onlyalg:true univ_flexible ~direction:false t | Some direction -> refresh ~onlyalg status ~direction t - else (refresh_term_evars false true t; t) - in - if !modified then !evdref, t' else !evdref, t + else refresh_term_evars ~onevars:false ~top:true t + in !evdref, t' let get_type_of_refresh ?(polyprop=true) ?(lax=false) env sigma c = let ty = Retyping.get_type_of ~polyprop ~lax env sigma c in diff --git a/test-suite/bugs/closed/5197.v b/test-suite/bugs/closed/5197.v new file mode 100644 index 0000000000..b67e93d677 --- /dev/null +++ b/test-suite/bugs/closed/5197.v @@ -0,0 +1,44 @@ +Set Universe Polymorphism. +Set Primitive Projections. +Unset Printing Primitive Projection Compatibility. +Axiom Ω : Type. + +Record Pack (A : Ω -> Type) (Aᴿ : Ω -> (forall ω : Ω, A ω) -> Type) := mkPack { + elt : forall ω, A ω; + prp : forall ω, Aᴿ ω elt; +}. + +Record TYPE := mkTYPE { + wit : Ω -> Type; + rel : Ω -> (forall ω : Ω, wit ω) -> Type; +}. + +Definition El (A : TYPE) : Type := Pack A.(wit) A.(rel). + +Definition Typeᶠ : TYPE := {| + wit := fun _ => Type; + rel := fun _ A => (forall ω : Ω, A ω) -> Type; + |}. +Set Printing Universes. +Fail 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). + +(** Bidirectional typechecking helps here *) +Require Import Program.Tactics. +Program Definition progTypeᵇ : El Typeᶠ := + mkPack _ _ (fun w => Type) (fun w A => (forall ω, A ω) -> Type). + +(** +The command has indeed failed with message: +Error: Conversion test raised an anomaly +**) + +Definition Typeᵇ' : El Typeᶠ. +Proof. +unshelve refine (mkPack _ _ _ _). ++ refine (fun _ => Type). ++ simpl. refine (fun _ A => (forall ω, A ω) -> Type). +Defined. |