Idris中的“不可访问的模式变量”

Question

我有一个问题，即使我只是使用编译器来指导模式匹配，Idris中的模式匹配也会给出“不可访问的模式变量”错误。

这是我要做的事的一个例子。细节并不是很重要，主要是我有一个像矢量的东西，除了它是通过矢量索引之间的关系进行参数化的，而不是使用相等性。然后，我得到了另一种定义关系的类型，其中一个变体是向量之间的关系PC。 （我的实际代码还有其他情况，我已经将它们砍掉了。）

然后，我试图通过PC证明上的模式匹配来定义函数“ trans”。如果我执行“ trans pf1 pf2 =？foo”，则它可以工作。但是，如果我进行大小写拆分（使用编辑器命令进行大小写拆分），则会得到“ nwhole不是可访问的模式变量”。对于我来说，这似乎很奇怪，在对类型进行检查的程序上进行编译器给定的大小写分割不会产生这种情况。而且，我不知道如何进行代码类型检查。

有人知道这里发生了什么吗？这是一个错误，还是我的隐式参数/类型索引做错了什么？

module MinimalExample

data NNat = NNone | NZ | NSucc NNat

parameters (rel : NNat -> NNat -> Type )
  data PreVec : Type -> NNat -> Type where
    VNil : {elem : Type} -> {nindex : NNat} -> rel nindex NZ -> PreVec elem nindex
    VCons : {elem : Type} -> {nindex : NNat} -> {ntail : NNat} -> elem -> PreVec elem ntail -> rel (NSucc ntail) nindex -> PreVec elem nindex


data PC :  {tipe1 : Type} -> {tipe2 : Type} -> tipe1 -> tipe2 -> Type where
    PCNone : {a : tipe1} -> {b : tipe2} -> PC a b 
    PCCons : {elemType : Type} -> {n1 : NNat} -> {n2 : NNat} -> {nwhole : NNat} ->
            {t1 : PreVec (PC {tipe1 = NNat} {tipe2 = NNat} ) elemType n1} -> 
            {t2 : PreVec (PC {tipe1 = NNat} {tipe2 = NNat} ) elemType n2} ->  
            PC h1 h2 ->
            PC t1 t2 -> 
            (pf1 : PC (NSucc n1) (NSucc nwhole)) -> 
            (pf2: PC (NSucc n2) (NSucc nwhole)) ->
            PC (VCons PC {ntail=n1} {elem=elemType} h1 t1 pf1) (VCons PC {ntail=n2} {elem=elemType} h2 t2 pf2) 


trans : {tx : Type} -> {ty : Type} -> {tz : Type} -> {x : tx} -> {y : ty} -> {z : tz} ->  
     PC x y -> PC y z -> PC x z
trans PCNone pf2 = ?trans_1
trans (PCCons y z pf1 x) pf2 = ?trans_2 

Answer 1

首先，大小写分隔符相当笨拙，目前与类型检查器无关。主要是创建每种情况，然后询问类型检查器该分支是否有效。

我找到了一个显示类似问题的最小示例。

data PreVec : Nat -> Type where
  VCons : PreVec n

data Bad :  {tipe1 : Type} -> tipe1 -> Type where
  MkBad : Bad VCons

data Good1 : PreVec n -> Type where
  MkGood1 : Good1 VCons

data Bad2 : {tipe1: Type} -> tipe1 -> Type where
  MkBad2 : {n: Nat} -> Bad2 (VCons {n})

以类似的方式使用它们会在Bad构造函数上产生错误，但在好的构造函数上会发现错误。

我不能说我完全理解这个问题，但是它似乎主要与类型等隐式的解析顺序有关，这很可能是编译器错误。基本上，隐式tipe1依赖于包装在构造函数本身中的变量n。我的猜测是类型的隐式函数在打开构造函数之前就已被填充，因此n不在模式类型的范围内。

似乎有多个补丁可以修复它。如果将变量tipe1（或tipe2）设置为显式而不是隐式，则会发生在您的示例中到处使用_正确合成类型的情况。或者，将返回类型更改为：

PC (the (PreVec elemType (NSucc nwhole)) (VCons PC elemType (NSucc nwhole) n1 h1 pf1))
          (VCons PC elemType (NSucc nwhole) n2 h2 pf2) 

也成功。不成功的一件事是将所有其他隐式更改为显式，仅与这些tipe1和tipe2有关。构造函数中它们的每个实例都受约束，因此类型本身没有问题。仅在执行模式匹配时才会出现这种情况。