为什么这个函数/构造函数参数成为一个自由的隐式变量？

Question

我正在尝试在Idris中实现Agda's inspect idiom，作为inspect的可能解决方法，但是，当我在this problem构造函数上进行模式匹配时，似乎丢失了MkReveal的选择，而是变成了自由参数。

首先，是f的Idris端口：

inspect

然后我尝试如何使用它：

%default total

data Reveal : {a : Type} -> {b : a -> Type} -> (f : (x : a) -> b x) -> (x : a) -> (y : b x) -> Type where
  MkReveal : {a : Type} -> {b : a -> Type} -> {f : (x : a) -> b x} -> {x : a} -> {y : b x} -> (f x = y) -> Reveal {b = b} f x y

inspect : {b : a -> Type} -> (f : (x : a) -> b x) -> (x : a) -> Reveal f x (f x)
inspect {b = b} f x = MkReveal {b = b} {f = f} {y = f x} Refl

applyInspect : {b : a -> Type} -> (f : (x : a) -> b x) -> (x : a) -> (y ** Reveal f x y)
applyInspect f x = (f x ** inspect f x)

[这里，在孔

foo : (Monad m) => m ()
foo = do
    let selected = the (Vect 2 Nat) $ pure 0
    let elems = the (Vect 9 Nat) $ pure 0

    let (((n ** xs), (k ** ys)) ** MkReveal eq) = 
            applyInspect (partition (`elem` selected)) elems
    ?wtf

中，我希望?wtf的类型为eq。但是，相反，将一个新的隐式绑定变量partition (`elem` selected) elems = ((n ** xs), (k ** ys))引入了范围：

f

编辑添加：我发现，如果手动将

f : (x : Vect (fromInteger 9) Nat) ->
    (\__pi_arg4 => ((p : Nat ** Vect p Nat), (q : Nat ** Vect q Nat))) x
eq : f elems = ((n ** xs), (k ** ys))

参数指定为b，则可以获得applyInspect的所需类型：

eq

这导致

    let (((n ** xs), (k ** ys)) ** MkReveal eq) = 
            applyInspect {b = \_ => (DPair Nat (\p => Vect p Nat), DPair Nat (\q => Vect q Nat))}
                (partition (`elem` selected)) elems

这就是我想要的。

所以，也许有一个相关的问题，我应该如何解决（没有黄色亮点像您在Agda中得到的未解决的元数据...），并且是否有一种调整

eq : partition (\ARG =>
                  elemBy (\meth, meth =>
                            Prelude.Nat.Nat implementation of Prelude.Interfaces.Eq, method == meth
                                                                                               meth)
                         ARG
                         selected)
               elems =
     ((n ** xs), (k ** ys))

或Reveal的定义以便正确推断applyInspect参数的方法？

Answer 1

导致此问题的根源是重载：在不知道其特定类型的情况下，b的出现在partition和Prelude.List.partition之间是模棱两可的。