371392 (9) [Avatar] Offline
#1
(MEAP v12, Idris 0.12.3)

In exercise 8.2.6.2, if I type in the skeleton definition in the book:

my_reverse : Vect n a -> Vect n a
my_reverse xs = reverse' [] xs
  where
    reverse' : Vect n a -> Vect m a -> Vect (n+m) a
    reverse' acc []        = ?revPrfNil acc
    reverse' acc (x :: xs) = ?revPrfXs (reverse' (x :: acc) xs)


… I don't get the nice listing of holes, but instead the following error:


     When checking left hand side of Main.my_reverse, reverse':
     Type mismatch between
             Vect {a = Type} (S k) a (Type of x :: xs)
     and
             Vect {a = ty} (S k) a (Expected type)
     
     Specifically:
             Type mismatch between
                     Type
             and
                     ty


After some fumbling around, I found a way to make the error go away, but I don't really know why this works, nor what the original error meant.

my_reverse : {a : Type} -> Vect n a -> Vect n a
my_reverse xs = reverse' [] xs
  where
    reverse' : {a : Type} -> Vect n a -> Vect m a -> Vect (n+m) a
    reverse' acc []        = ?revPrfNil acc
    reverse' acc (x :: xs) = ?revPrfXs (reverse' (x :: acc) xs)


Is this expected behaviour here? Did I do something wrong?
371392 (9) [Avatar] Offline
#2
Turns out that my own Vect definition was wrong… Sorry for the noise. smilie