Linear types: GADTs and role inference
If I say
data T m a where
MkT :: a %m -> T m a
then role inference gives type role T phantom representational
. This is wrong, coercion from T 'One a
to T 'Many a
is unsound. (coerce
is currently not linear, so this doesn't lead immediately to unsoundness, but there's probably a way.)