"not an accessible pattern variable" in Idris

Question

I'm having a problem where pattern-matches in Idris give "not an accessible pattern variable" errors, even when I'm just using the compiler to guide the pattern matching.

Here's an example of what I'm trying to do. The specifics aren't terribly important, the main thing is that I've got something that's like a vector, except it's parameterized over a relation between vector indices, instead of using equality. I've then got another type that defines a relation, where one variant is a relation PC between vectors. (My actual code has other cases, I've just chopped them out).

I'm then trying to define a function "trans" by pattern matching on a PC proof. If I do "trans pf1 pf2 = ?foo", then it works. But if I case split (using the editor command to case-split), I get "nwhole is not an accessible pattern variable". This seems odd to me, that doing the compiler-given case-split on a program that typechecks produces one that doesn't. And, I have no clue how to make the code typecheck.

Does anyone have an idea what's going on here? Is this a bug, or am I doing something wrong with my implicit arguments/type indices?

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

Jason Carr Jason Carr · Accepted Answer · 2019-10-31T22:19:54

First of all, the case-splitter is rather dumb, and is independent from the typechecker at the moment. Primarily what it does is create every case and ask the typechecker if that branch is valid.

I've found a minimal example that shows similar issues.

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})

Using these in a similar way will give errors on the Bad constructors, but be find on the good ones.

I can't say I fully understand the issue, but it seems to mostly have to do with the resolution order for implicits like types, it likely is a compiler bug. Basically, the implicit tipe1 depends on the variable n which is packaged within the constructor itself. My guess is that the implicits in the type get filled in before the constructor is opened, so that n is not in scope for the type of the pattern.

There seem to be multiple patches to fix it. If the variable tipe1 (or tipe2) is made explicit rather than implicit, it happens that using _ everywhere synthesizes the type correctly for your example. Alternatively, changing the return type to:

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

Also succeeds. One thing that does not succeed is changing every other implicit to explicit, it only has to do with these tipe1 and tipe2. Every instance of them in the constructors is constrained, so there is no problem with the type itself. It is only when performing the pattern match that this situation arises.

"not an accessible pattern variable" in Idris

1 Answers