CODEWITHSUNDEEP
functional-programmingidris
mna
mna

Reputation: 263

DPair indexed over Fin

I am following an Idris tutorial and wanted to experiment with dependent pairs and Fin.

The following code does not type check in 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'

The error is the following

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)

I have checked that P FZ is Char, so I am confused about the type mismatch complaint. The corresponding code using Nat instead of Fin 1 compiles perfectly. What am I doing wrong?

Upvotes: 3

Views: 77

Answers (1)

xash
xash

Reputation: 3722

P FZ does not get normalized to Char, because the compiler does not see that P is total (use %default total to get a warning). This works:

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'

Upvotes: 4

Related Questions