Coercion with type variables
It is currently not possible to add the following coercion
type t 'a = {
t_a : 'a;
}
meta coercion function t_a
Currently only from one type constructor to another is allowed. It seems that allows to compute the transitive closure when inserting new coercion and not during type checking. What would be the complexity to add that? Does it become similar to type-class inference?
EDIT: It could also help if one could define
function t_a_foo: (x:t foo) : foo = x.t_a
meta coercion function t_a_foo
function t_a_bar: (x:t bar) : bar = x.t_a
meta coercion function t_a_bar