Here are my thoughts on our attribute business.
*Currently:* How attributes are working is: they are virtually macros that disappear once elaboration is done. attributes are saved inside the elaboration environment in an associative table that associate a variable and an attribute to a lexp (attribute's value).
As I understand it, the current issue is when an attribute is added:
attribute Int default default-int;
It modifies the environment without creating new declarations. Which is not allowed because it would endanger type checking soundness.
(Side note, if a dummy declaration is returned by `attribute`, the assert is still triggered. if the assert is removed, a DB index problem arise when attributes are used. The triggered assert is not in the Pmcall (where `attribute` is processed) but in the Pexpr branch).
*The proposed solution:*
make `attribute w greater-than (lambda (y : Int) -> True);`expand to
attribute_greater-than_table : lexp-table (Int -> Bool); attribute_greater-than_table = lexp-table-empty; attribute_greater-than_table = lexp-table-add attribute_greater-than_table w (lambda (y : Int) ->
True)
We have a lexp-table for each kind of attribute we want to create (Attribute: Int -> Bool, Attribute: Int, etc...). `attribute_greater-than_table` is a regular variable which will only be used under the hood.
`get-attribute w attr` => lexp-table-lookup w attribute_attr_table
Everything has to be done during the elaboration phase because we need to be able to inspect the lexp-table to retrieve the default attribute when processing implicit arguments.
I don't think lexp-table is needed at runtime since all the lookup should have been done already.