Multiple `RowLacks`?

[garyb]

Is there some trick that I'm missing that would allow me to say that a row lacks more than one label?

I encountered this when trying to do some stuff with purescript-record:

import Data.Record as Rec
import Data.Symbol (SProxy(..))
import Type.Prelude (class RowLacks)

insertA ∷ ∀ r. RowLacks "a" r ⇒ { | r } → { a ∷ Int | r }
insertA = Rec.insert (SProxy ∷ SProxy "a") 1

insertB ∷ ∀ r. RowLacks "b" r ⇒ { | r } → { b ∷ Int | r }
insertB = Rec.insert (SProxy ∷ SProxy "b") 1

insertAB ∷ ∀ r. RowLacks "a" r ⇒ RowLacks "b" r ⇒ { | r } → { a ∷ Int, b ∷ Int | r }
insertAB = insertA <<< insertB -- seems to be unimplementable, this and any combination of annotations etc. I could come up with for intermediate steps fails

As far as I can see there's no way that multiple RowLacks constraints can be satisfied, given the Union-based implementation. Maybe this is something that would be better off solved by the compiler after all?

[LiamGoodacre]

@garyb in this case, you'll want proof of RowLacks "a" (b :: Int | r), i.e:

insertAB ∷ ∀ r. RowLacks "a" (b :: Int | r) ⇒ RowLacks "b" r ⇒ { | r } → { a ∷ Int, b ∷ Int | r }
insertAB = insertA <<< insertB

[LiamGoodacre]

Alternatively you'd need some a way of conjuring up an instance of RowLacks "a" (b :: Int | r) from RowLacks "a" r and "a" /= "b". Which sounds more difficult.

[garyb]

RowLacks "a" (b :: Int | r)

That's probably the only thing I didn't try when attempting to work around it, thanks!