stefan-hoeck / idris2-pq Goto Github PK

I have to admit, I was not able to figure out how to write a function that
can get the columns from the Table data structure at compile time.

I.e. a function with the following definition:

getT :  HasIO io
    => MonadError SQLError io
    => Connection
    -> (t        : Table)
    -> {auto 0 _ : Elems cs (columns t)}
    -> (query : Op)
    -> io (List $ GetRow cs)

where the list of columns would be calculated from the Table object, so for example

rows <- get c User (columns User) (Name /= "Eleni" && Age >= 33)

would be just

rows <- getT c User (Name /= "Eleni" && Age >= 33)

What I could not figure out is how to pass the proof that (columns t) is a subset of (columns t)