The Coq mailing list

[Matthieu Sozeau <mattam AT mattam.org>]

Hi Talia,

  Indeed Typing.type_of infers missing constraints, while the kernel only checks w.r.t the existing ones. You could also add the constraints explicitly if you know them using the interfaces in Evd (add_universe_constraints or add_constraints), but it’s usually simpler to just retype and infer them.

Best,
— Matthieu

Le mar. 10 avr. 2018 à 10:30, Sylvain Boulmé <Sylvain.Boulme AT univ-grenoble-alpes.fr> a écrit :

Hello Talia,

I am not sure to fully understand your problem, but here is an hint: in
a plugin, when you define a term introducing potentially new universe
constraints, you have to refresh universe constraints. A simple way to
do it in Coq 8.7 is to use the function "Typing.type_of" (you will only
need the first component of its result).

See https://github.com/coq/coq/blob/v8.7/pretyping/typing.mli

As I understand it, this should correspond to your first alternative...

Hope this helps,

Sylvain.


Le 10/04/2018 à 03:06, Talia Ringer a écrit :
> Hello,
>
> I am writing a plugin, and as part of this plugin, I occasionally need
> to type-check terms. This is usually fine, but sometimes, I get errors
> like this:
>
>     The 2nd term has type "nat -> Type@{max(Foo, Bar)}"
>     which should be coercible to "nat -> Type@{Baz}".
>
>
> I know what this means, but the thing is, these constraints are actually
> solvable; if I wrote the term outside of my plugin, it would type-check
> and go through. But inside of the plugin, the type-checking routine fails.
>
> I'm looking for one of two things:
>
> 1. A way to tell type-checking from within a plugin about the universe
> constraints so that it knows to solve them correctly, or
> 2. a way to tell type-checking from within a plugin to just assume all
> universe constraints go through, because this will always be true for
> me, and if it isn't, then the plugin will just fail later anyways
>
> I'm assuming #1 is the proper way to call type-checking from within a
> plugin, but I'm not sure how to do it.
>
> Best,
>
> Talia