Incorrect type role for `n` in `Vector n a`

[Cajunvoodoo]

Currently, Vector has the inferred role type role Vector representational phantom nominal, which allows the following:

newtype Foo = Foo (Vector 10 Int)

exVec :: Vector 15 Int
exVec = fromJust $ fromListN @15 [1..15]

exFoo :: Foo
exFoo = coerce exVec -- no error

There is no error because n is phantom, so the coercion always works.
Instead, Vector should have type role Vector representational nominal nominal to disallow this coercion.

[kozross]

I'm amazed this leaked through! Thanks, will fix.

[kozross]

Actually, are you sure this works? To coerce through the Vector newtype, the constructor needs to be in scope, and I'm fairly sure there's no way to achieve this without importing an internal module.

[Cajunvoodoo]

It's not coercing the internal representation of vector, merely Vector n a -> Foo see:

>>> import Data.Vector.Sized qualified as Sized
>>> import Data.Maybe (fromJust)
>>> newtype Foo = Foo (Sized.Vector 1 Int) deriving Show
>>> exVec = fromJust $ Sized.fromListN @5 [1..5]
>>> exVec
>>> coerce @(Sized.Vector 5 Int) @Foo exVec
Vector [1,2,3,4,5]
Foo (Vector [1,2,3,4,5])

while Foo exVec results in the expected type error.

[maxigit]

I'm trying to coerce Vector n (Identity a) to Vector n a and it doesn't work (even though doing so on unsized vector works)
I believe the role should be type role Vector representational nominal representational.

At the moment I can do withUnsafeVector coerce but this doesn't work (I believe) on nested structures as coerce will.