Hi
Why are native arrays universe polymorphic?
To allow for arrays of arrays?
Do you face a bug?
@Guillaume Melquiond you don't need polymorphic arrays to nest them
this is because 1. you might want to store stuff that lives in various levels, and 2. monomorphic constraints in the kernel are a real plague
Thanks for your answers.
So for instance, I want to define a constr
which is a native array, at the OCaml level. What is the first argument I should give to mkArray
?
@Enrico Tassi indeed, I face "universe inconsistency" when switching a development based on non universe polymorphic arrays to native arrays, but it is very difficult to make a small example...
I think we are very firmly in the Coq plugin dev and Coq dev territory here
This topic was moved here from #Coq users > Why are native arrays universe polymorphic? by Karl Palmskog
are you working with econstr or constr?
what's the type of the elements of the array?
Hi Gaëtan
I guess you could pass it the result of Evd.fresh_array_instance
, if you are working at the econstr level.
the type of the type of the elements is some universe
if it's a level use that
if it's algebraic you need to generate a fresh level and constrain it to be higher
if using fresh_array_instance you will need to use Typing.type_of
on the generated array term (or on the type array@{u} (some inductive type)
) so that the right constraints get generated
Ok, thanks a lot for these explanations. I will get back to you if I run into a problem.
Last updated: Oct 13 2024 at 01:02 UTC