This allows terms of type STRecord r a to be coerced to type STRecord r b when Coercible a b holds, hence allowing the zero cost coerce instead of map wrap and map unwrap to introduce and eliminate newtypes under ST records for instance.
I couldn’t think of a case where a phantom roled region is an issue but in doubt I preferred to keep it nominal.
JordanMartinez
commented
3 years ago
This allows terms of type
STRecord r ato be coerced to typeSTRecord r bwhenCoercible a bholds, hence allowing the zero costcoerceinstead ofmap wrapandmap unwrapto introduce and eliminate newtypes under ST records for instance.I couldn’t think of a case where a phantom roled region is an issue but in doubt I preferred to keep it nominal.