Check length of a tuple by pattern matching

Question

I want to learn idris by writing a length function that checks the length of a tuple. I leanred a tuple is made by the MkPair constructor so I try to do pattern matching.

length : {t2:_} -> Pair t1 t2 -> Nat

length (MkPair a b) = case b of
                           MkPair c d => 1 + (length b)
                           _ => 2

Error: While processing right hand side of length. When unifying:
    t2
and:
    (?_, ?_)
Mismatch between: t2 and (?_, ?_).

coroutine:25:28--25:29
 21 |                            Pair c d => 1 + (length b)
 22 |                            _ => 2
 23 |
 24 |
 25 | length (MkPair a b) = case b of
                                 ^

What does the error mean? How do I fix it? In deed I'm not sure if I used the case syntax correctly.

Answer 1

The type of b is t2 i.e. unknown, so you can't pattern match on it. You'd need to pattern match on t2. Once you've done that there's no need to pattern match on b.

BTW you're right about MkPair and Pair but they both have the shorthand (·, ·)

length : {t2 : _} -> (t1, t2) -> Nat
length (_, b) = case t2 of
                     (_, _) => 1 + (length b)
                     _ => 2