The Coq mailing list

[Talia Ringer <tringer AT cs.washington.edu>]

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