ARec: Type of aput, alens unsound

[Philonous]

aput has the following type:

aput :: forall t t' f ts ts'. (NatToInt (RIndex t ts))
      => f t' -> ARec f ts -> ARec f ts'

In that type, the ts', that is, the type of returned fields is entirely unconstrained, so it seems that we can generate an Rec of any type by using aput!

And indeed:

foo :: ARec ElField '[ '("foo", Int) ]
foo = toARec ( Field 3 :& RNil )

bar :: ARec ElField '[ '("bar", Bool), '("oops!", String) ]
bar = aput @'("foo", Int)
        (Field 3 :: ElField '("quux", Double))
        foo

is accepted with fatal consequences:

λ> bar
{*** Exception: Ix{Int}.index: Index (1) out of range ((0,0))

alens has the same problem

[Philonous]

It seems that the mistake is just that they shouldn't have been exported from Data.Vinyl.ARec, they are used as helper definitions for the RecElem instance for ARec which has a correct type (or at least not an obviously incorrect one)

[Philonous]

I opened https://github.com/VinylRecords/Vinyl/pull/152

[Philonous]

152 solved this