Stream: MetaCoq

Topic: tmUnquote and printing a term in SProp


view this post on Zulip Thomas Lamiaux (May 28 2024 at 20:03):

Hi, I am generating recursion principles and I am printing them using the function

  | TestTerm =>  x <- (tmUnquote tm_rec) ;;
                 ker_tm_rec <- (tmEval all x.(my_projT2)) ;;
                 tmPrint ker_tm_rec

For a reason I have trouble to locate, when trying to unquote and print with the functions above a generated term that should of type SProp, I get the error message

Illegal application:
The term "existT_typed_term" of type "forall my_projT1 : Type, my_projT1 -> typed_term"
cannot be applied to the terms
[my term : its type]
The 1st term has type "SProp" which should be a subtype of "Type". (universe inconsistency: Cannot enforce SProp <=
GenRecursor.recursors_named.unit_tests.1034)

I can see it is an issue with sort as if the term generated is in Prop there is no issue, but I am a bit confused about what it is supposed to be

view this post on Zulip Yannick Forster (May 28 2024 at 20:04):

I don't think there's anything deep here, isn't it just that SProp is not a subtype of Type while Prop is?

view this post on Zulip Yannick Forster (May 28 2024 at 20:07):

The buzzword to look for seems to be SProp not being cumulative

view this post on Zulip Thomas Lamiaux (May 28 2024 at 20:12):

I agree on that, I am just confused about what I should change to make it work

view this post on Zulip Yannick Forster (May 28 2024 at 20:15):

Mh, maybe use something likeInductive Box : Type := box (A : SProp). and unquote box A instead of A?

view this post on Zulip Gaëtan Gilbert (May 28 2024 at 20:21):

maybe existT_typed_term should be sort polymorphic?

view this post on Zulip Thomas Lamiaux (May 28 2024 at 20:26):

I do not see how I could use box ?

view this post on Zulip Yannick Forster (May 28 2024 at 20:27):

Quote it and unquote the application of box to the thing you actually want to unquote

view this post on Zulip Yannick Forster (May 28 2024 at 20:27):

Technically it could be possible to make existT_typed_term polymorphic, yes! I'd be worried that some template programs somewhere break then though


Last updated: Jul 23 2024 at 20:01 UTC