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.)