How can I get Idris to unmap a vector in order to infer a type?

Question

I have the following working function:

unMaybe : (t : Type) -> {auto p : t = Maybe x} -> Type
unMaybe {x} _ = x

This function works fine:

> unMaybe (Maybe Int)
Int

I also have another similar function:

unMaybesA : (ts : Vect n Type) -> {xs : Vect n Type} -> {auto p : map Maybe xs = ts} -> Vect n Type
unMaybesA {xs} _ = xs

Unfortunately the following fails:

> unMaybesA [Maybe Int, Maybe String]

(input):1:1-35:When checking argument p to function Main.unMaybesA:
        Can't find a value of type
                Data.Vect.Vect n implementation of Prelude.Functor.Functor, method map Maybe
                                                                                       xs =
                [Maybe Int, Maybe String]

But the following works:

> unMaybesA {xs=[_,_]} [Maybe Int, Maybe String]
[Int, String]

Is the a way to get Idris to automatically do {xs=[_,_]} with however many _ the vector has?

unMaybesB : (ts : Vect n Type) -> {auto p : (xs : Vect n Type ** map Maybe xs = ts)} -> Vect n Type
unMaybesB {p} _ = fst p

Possibly by using an elaborator script to automatically fill p in the function above?

I have the outline of an elab script below. I just need to figure out how to generate n, ts, and xs from the goal.

helper1 : Vect n Type -> Vect n Type -> Type
helper1 ts xs = (map Maybe xs) = ts

unMaybesC : (ts : Vect n Type) -> {auto p : DPair (Vect n Type) (helper1 ts)} -> Vect n Type
unMaybesC {p} _ = fst p

helper2 : (n : Nat) -> (ts : Vect n Type) -> (xs : Vect n Type) -> helper1 ts xs -> DPair (Vect n Type) (helper1 ts)
helper2 _ _ xs p = MkDPair xs p

q : Elab ()
q = do
    let n = the Raw `(2 : Nat)
    let ts = the Raw `(with Vect [Maybe String, Maybe Int])
    let xs = the Raw `(with Vect [String, Int])
    fill `(helper2 ~n ~ts ~xs Refl)
    solve

qC : Vect 2 Type
qC = unMaybesC {p=%runElab q} [Maybe String, Maybe Int]

Answer 1

map Maybe xs = ts seems idiomatic, but is quite difficult. If you want to auto search for a non-simple proof, write an explicit proof type. Then the proof search will try the constructors and is guided in the right direction.

data IsMaybes : Vect n Type -> Vect n Type -> Type where
  None : IsMaybes [] []
  Then : IsMaybes xs ms -> IsMaybes (t :: xs) (Maybe t :: ms)

unMaybes : (ts : Vect n Type) -> {xs : Vect n Type} -> {auto p : IsMaybes xs ts} -> Vect n Type
unMaybes ts {xs} = xs

And with this:

> unMaybes [Maybe Nat, Maybe Int, Maybe (Maybe String)]
[Nat, Int, Maybe String] : Vect 3 Type