What's the property (Γ ⊢ x : T) → (Γ ⊢ T type)
called? I presume it's a bug if Coq's kernel fails to validate this property?
Hrm, is it known that Goal foo. Admitted.
can fail on Admitted
with the claim that foo
has a type error, when SProp
s are involved?
Set Allow StrictProp.
Inductive sTrue : SProp := sI.
Goal forall (b : bool) (x y : if b return Type then sTrue else nat) (pf : b = true), x = y.
Admitted.
Jason Gross said:
What's the property
(Γ ⊢ x : T) → (Γ ⊢ T type)
called? I presume it's a bug if Coq's kernel fails to validate this property?
In MetaCoq this property is called validity. Dont' know how standard it is though.
I think in Coq currently it doesn't hold yet, because T
might involve algebraic universes. So the property is that either T
is a type, or it is a well-formed arity (quantification over a well-formed context, ending in a universe, possibly algebraic).
Also, SProp related stuff are only checked at Qed time like in that example I think
SProp handling in the upper layers is fairly buggy currently.
We have a kernel hack to fix relevance annotations post-hoc, but I find this to be horrendous.
It makes the use of SProp possible despite tactics being utterly broken.
Interestingly, it seems that Check
does extra checks when there are no evars:
Set Allow StrictProp.
Inductive sTrue : SProp := sI.
Check fun (b : bool) (x y : if b return Type then sTrue else nat) => _. (* success *)
Check fun (b : bool) (x y : if b return Type then sTrue else nat) => nat. (* failure *)
Last updated: Sep 25 2023 at 12:01 UTC