The Coq mailing list

[Sylvain Boulmé <Sylvain.Boulme AT univ-grenoble-alpes.fr>]

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