Type checker confused by overloaded `fst` (or just a strange error message)

[jendrikw]

Steps to Reproduce

Try to compile this code (Try it online):

module Main
import Data.Vect

myVectSum : Vect _ Nat -> Nat
myVectSum [] = 0
myVectSum (x :: xs) = plus x (myVectSum xs)

myVectMap : (a -> b) -> Vect n a -> Vect n b
myVectMap f [] = []
myVectMap f (x :: xs) = f x :: myVectMap f xs

decodeRle2 : (v : Vect n (Nat, a)) -> Vect (myVectSum $ myVectMap fst v) a
decodeRle2 [] = []
decodeRle2 (tuple :: xs) =
    let
        elemReplicated = Vect.replicate (fst tuple) (snd tuple)
        rest : Vect (myVectSum $ myVectMap fst xs) a = decodeRle2 xs
    in elemReplicated ++ rest

main : IO ()
main = putStrLn $ show $ decodeRle2 [(1,'a'),(3,'b'),(1,'c')]

Expected Behavior

The code should compile, as fst is unambiguous.

Observed Behavior

I get an error message, which I find quite strange because the types look exactly the same.

.code.tio.idr:22:5-25:39:
   |
22 |     let
   |     ~~~ ...
When checking right hand side of decodeRle2 with expected type
        Vect (myVectSum (myVectMap fst (tuple :: xs))) a

Type mismatch between
        Vect (plus (fst tuple) (myVectSum (myVectMap fst xs)))
             a (Type of myVectAppend elemReplicated rest)
and
        Vect (plus (fst tuple) (myVectSum (myVectMap fst xs))) a (Expected type)

Specifically:
        Type mismatch between
                plus (fst tuple) (myVectSum (myVectMap fst xs))
        and
                plus (fst tuple) (myVectSum (myVectMap fst xs))

They are coloured differently when compiling from the repl, but I don't know what the colours mean.

The code compiles fine when you change the signature to decodeRle2 : (v : Vect n (Nat, a)) -> Vect (myVectSum $ myVectMap Basics.fst v) a