Allow same type assignment for left- and right-hand side of assignment
Currently, it is not possible to define a self-referential structure the following way:
struct s
{
struct s *self;
};
[[rc::args("&own<uninit<struct_s>>")]]
void self_write(struct s *x)
{
x->self = x;
}
Where type system gets stuck in the context
Goal:
arg_x : loc
x : loc
Q : (gmap label stmt)
R : (val → type → iProp Σ)
v : val
---------------------------------------
--------------------------------------∗
find_in_context (FindVal v)
(* ... *)
According to Michael the problem here is that both sides of the assignment cannot use the same type assignment. One quickfix is to use an alias to circumvent the limitation :
void self_write(struct s *x)
{
struct s *y = x;
x->self = y;
}
However, I have no clue what in the type system should change to fix the issue.