xoltar (3) [Avatar] Offline
Around p. 248 in v9, we're talking about equality, and cong. After this section, I have two questions:

checkEqNat : (num1 : Nat) -> (num2: Nat) -> Maybe (num1 = num2)
checkEqNat Z Z = Just (Refl)
checkEqNat Z (S k) = Nothing
checkEqNat (S k) Z = Nothing
checkEqNat (S k) (S j) = do
           prf <- checkEqNat k j
           pure (cong prf)

exactLength : (len : Nat) -> (input : Vect m a) -> Maybe (Vect len a)
exactLength {m} len input = do
            Refl <- checkEqNat m len
            pure input

1. Why do we have to pattern match in exactLength? Why isn't
prf <- checkEqNat m len
2. It seems like the function that cong is using as its implicit argument in checkEqNat is S. So why doesn't the following work?

??> the (S 3 = S 3) (cong (the (3=3) Refl))
(input):1:5:When checking argument value to function Prelude.Basics.the:
        Type mismatch between
                f 3 = f 3 (Type of cong (the (3 = 3) Refl))
                S 3 = S 3 (Expected type)
                Type mismatch between
                        f 3

Edwin Brady (65) [Avatar] Offline
1. Even though Refl is the only constructor for =, the type checker needs to know that when you run checkEqNat it really does return Refl. If checkEqNat isn't total, for example, it might not return anything at all.

2. Idris is more careful about inferring values of implicit arguments of function types, because in general there could be any number of functions which match. Here, for example, another function which could match might be something like:

other : Nat -> Nat
other x = if x < 10 then S x else S (S x)

So here, you need to be explicit since Idris won't work it out on its own