DPairがFinでインデックスされています

Question

Idrisのチュートリアルに従っており、従属ペアとFinで を実験したかったのです。

次のコードはIdrisにチェックを入れません。

data Fin : Nat -> Type where 
    FZ : Fin (S k) 
    FS : Fin k -> Fin (S k) 

P : (Fin 1) -> Type 
P FZ = Char 

vec : DPair (Fin 1) P 
vec = MkDPair FZ 'c' 

エラーは、次の

prims.idr:9:15: 
When checking right hand side of vec with expected type 
     DPair (Fin 1) P 

When checking argument pf to constructor Builtins.MkDPair: 
    Type mismatch between 
      Char (Type of 'c') 
    and 
      P FZ (Expected type) 

である私は、P FZがCHARであることを確認しているので、私は型の不一致苦情について混乱しています。 Fin 1の代わりにNatを使用する対応するコードは、 を完全にコンパイルします。私は間違って何をしていますか？コンパイラはPは（警告を取得するために%default totalを使用）の合計であることを確認していないため

Answer 1

P FZは、Charに正規化されません。これは動作します：

data Fin : Nat -> Type where 
    FZ : Fin (S k) 
    FS : Fin k -> Fin (S k) 

P : (Fin 1) -> Type 
P FZ = Char 
P (FS FZ) impossible 
P (FS (FS _)) impossible 

vec : DPair (Fin 1) P 
vec = MkDPair FZ 'c'