Open pi8027 opened 1 year ago
Iirc there is a piece of code cleaning up the type. I guess it is broken if the primitive term constructors shows up
@gares Can you point out the part of the code declaring these constants and synthesizing their types? I have a rough idea of how to fix the issue.
clean-op-ty
in structure.elpi
is what I suspect messes up things.
Thanks. I believe that constructing the types of these constants from the declaration of the record type is much easier than doing so from the types of the projections. While the latter requires some replacements using copy
(as we can see in clean-op-ty
), the former should be just a matter of substitution.
I will take a closer look when I have some time.
Example:
The type of
addrA
should beassociative add
.