Stream: Elpi users & devs

Topic: Unifying a sort with Set

Enzo Crance (Jul 06 2022 at 16:01):

Hello. Why does this fail? (U is a free variable here)

coq.unify-eq (sort (typ U)) {{ Set }} ok.

Kenji Maillard (Jul 06 2022 at 16:32):

Isn't Set necessarily distinct from Type@{u} in Coq (because of Set-impredicative) ?
See for instance this snippet:

Universe u.
Fail Check eq_refl : Set = Type@{u}.
(* The command has indeed failed with message:
The term "eq_refl" has type "Set = Set" while it is expected to have type
 "Set = Type" (universe inconsistency: Cannot enforce Set = u). *)

Enrico Tassi (Jul 06 2022 at 16:43):

I believe set is Type_0 while typ U is morally U > 0.
But I may have messed things up. Are you in the univ-poly-light branch?

Enrico Tassi (Jul 06 2022 at 16:46):

No, now I'm confused. In the master branch I think I do enforce U > set, but not on that new branch, so {{ Set }} should mean typ 0 and be unifiable with typ U. If it is not the case, please scream ;-)

Enrico Tassi (Jul 06 2022 at 16:53):

Maybe what is misleading is that in elpi I tried to not give a syntax to Set, (eg. no set) ditching the impredicative-set option, and this is backfiring.

    K("typ","predicative sort of data (carries a universe level)",A(univ,N),
      B (fun x -> Sorts.sort_of_univ x),
      M (fun ~ok ~ko -> function
        | Sorts.Type x -> ok x
        | Sorts.Set -> ok Univ.Universe.type0
        | _ -> ko ()));

I hope this encoding makes sense... CC @Pierre-Marie Pédrot

Enrico Tassi (Jul 06 2022 at 17:08):

Apparently not, things are off. {{ Set }} = sort (typ U) works, but the two things are not unifiable according to Coq, so the encoding is wrong.
Thanks for reporting.

Last updated: Apr 20 2024 at 00:02 UTC