我怎样才能让 Idris 取消映射向量以推断类型？

Question

我有以下工作功能：

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

这个函数工作正常：

> unMaybe (Maybe Int)
Int

我还有一个类似的功能：

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

很遗憾，以下操作失败：

> 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]

但以下有效：

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

是否有一种方法可以让 Idris 自动对向量有多少 _ 执行 {xs=[_,_]}？

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

可能通过使用 elaborator 脚本在上面的函数中自动填充 p？

我在下面有一个 elab 脚本的大纲。我只需要弄清楚如何从目标生成 n、ts 和 xs。

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 看似地道，但相当困难。如果您想 auto 搜索非简单证明，请编写显式证明类型。然后证明搜索将 try the constructors 并被引导到正确的方向。

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

还有这个：

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

我怎样才能让 Idris 取消映射向量以推断类型？

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

idris