Concrete value <-> interface conversions
julian-klode opened this issue · 3 comments
We can move a: ol * ol into b: ol interface {}. We can however, cast an interface to a struct (type assertion or type switch). If we can b to a pointer type, the resulting pointer would be ol * om, as derived from convert(om * om, ol) = ol * om, because linear pointer targets only lose mutability if the pointer loses linearity.
This is unsound, as we can now accept an pointer to a read-only linear value and unsoundly convert it to a pointer to a mutable value. The only possible solution is to prevent the conversion to the interface in such a case.
Proposed solution
- Define: A strictly consistent permission is a permission that is equivalent to the permission gained by converting the permission the type yields to the outer permission. Specifically, in a pointer type, the target of the pointer must have the same base permission as the pointer.
- Specify: If a value is converted from a non-interface type to an interface type, the permission of the value must be strictly consistent.
I don't think we actually allow moving, copying, or referencing concrete types as interfaces yet. That needs to be fixed too.
Note that currently the default convert(om * om, ol) would be ol * om, so the definition might need some tweaking, or we need to introduce other convert rules.
Another problem that appears with value to interface conversions is that we must ensure that the methods from the value match the methods in the interface. This is difficult: Methods are not associated with other permissions, as methods are independent of values. Essentially, what we'd have to do when assigning a value to an interface is creating a new interface permission with the values outer permission and add all the matching methods to it.