Hello. Why does this fail? (`U`

is a free variable here)

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

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). *)
```

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?

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 ;-)

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

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: Feb 05 2023 at 13:02 UTC