DPair indiziert über Fin

Question

Ich folge einem Idris Tutorial und wollte mit abhängigen Paaren und Fin experimentieren.

Der folgende Code gibt keine Eingabe in Idris ein.

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' 

Der Fehler ist der folgende

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) 

ich überprüft haben, dass P FZ ist Char, also bin ich verwirrt über die Typenkonflikt Beschwerde. Der entsprechende Code mit Nat statt Fin 1 kompiliert perfekt. Was mache ich falsch?

Answer 1

P FZ wird nicht normalisiert auf Char, da der Compiler nicht sieht, dass P insgesamt ist (Verwendung %default total eine Warnung zu erhalten). Dies funktioniert:

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'