Rigid type variable -- why no error appears?

The function

f :: (Int,[a]) -> a -> (Int,[a])
f (k,l) r
  | k==n = (1,l++[r])
  | otherwise = (k+1,l)

is general enough to type check on its own (assuming n::Int). The type a here can indeed be any type -- there's no need to assume that a is the same a as the one in the signature of foo, so no error is generated.

Put in different terms, we could rename a into b without any harm:

foo :: Int -> [a] -> [a]
foo n list = snd $ foldl f (1,[]) list where
  f :: (Int,[b]) -> b -> (Int,[b])
  f (k,l) r
    | k==n = (1,l++[r])
    | otherwise = (k+1,l)

Here's a simpler example to stress the point. This compiles without errors:

foo :: a -> [a]
foo x = [f x]
   where
   f :: a -> a   -- this could also be b->b
   f y = y

By contrast, changing the last line to f y = x would immediately trigger the error since x has type "the a in the signature of foo", not "the a in the signature of f", and the two type variables can't be unified since they are both rigid.

foo :: Int -> [a] -> [a]
foo n list = snd $ foldl f (1,[]) list where
  f :: (Int,[a]) -> a -> (Int,[a])
  f (k,l) r
    | k==n = (1,l++[r])
    | otherwise = (k+1,l)

Notice how your inner function f only uses n from the outer function's scope. n is of type Int; only list (and foo itself) are names whose type has anything to do with the a variable in the type of foo. Since f doesn't use those, it doesn't need to have a type that uses ScopedTypeVariables to refer to the a from the type of foo.

In effet, f is fully polymorphic on its own; it can work with its own a instantiated to any type. Because it's only used in one place (inside foo) it will only ever actually be used with its a instantiated to the a from the outer foo. But that happens by exactly the same process any polymorphic type is instantiated in Haskell; the definition of f has to treat a as a black box and work with any possible type, and the place where f is used can instantiate it at anything (in this case, the a from the type of foo).

Lets show that more explicitly by using explicit foralls and not giving the same name to different type variables:

foo :: forall a. Int -> [a] -> [a]
foo n list = snd $ foldl f (1,[]) list where
  f :: forall b. (Int,[b]) -> b -> (Int,[b])
  f (k,l) r
    | k==n = (1,l++[r])
    | otherwise = (k+1,l)

f works forall b, and its only a coincidence of one particular usage that wants to instantiate b ~ a (even if that "one particular usage" is in fact the only usage).

The typical error in trying to write a type of a local function (that needs ScopedTypeVariables to resolve) is when the inner function uses something from the outer function that has a variable in its type. Say, something like this:

bar :: (a -> Bool) -> [a] -> [a]
bar f xs = filter g xs
  where g :: a -> Bool
        g = not . f

This might look fine at first glance, but the type signature for g is actually a lie, because without ScopedTypeVariables it means this:

bar :: forall a. (a -> Bool) -> [a] -> [a]
bar f xs = filter g xs
  where g :: forall b. b -> Bool
        g = not . f

It's claiming that g can take something of any type at all and turn it into a Bool, when in fact g uses the function f. f doesn't work on any type at all, only the particular type that bar was called with. bar can take a function f of any type (the caller of bar can choose to instantiate a as any type), but g is operating "inside one particular call to bar", when we've already been passed one particular f.

To write this type correctly we need (using ScopedTypeVariables) this:

bar :: forall a. (a -> Bool) -> [a] -> [a]
bar f xs = filter g xs
  where g :: a -> Bool
        g = not . f

There's no error because your inner function does not reference any type variable from the outer one. It uses n but its type is plain Int, not a polymorphic one

The "rigid type variables" error happens when we make n's type polymorphic:

foo :: Num a => a -> [a] -> [a]
foo n list = snd $ foldl f (1,[]) list where
  f :: Num a => (a,[a]) -> a -> (a,[a])
  f (k,l) r
    | k==n = (1,l++[r])
    | otherwise = (k+1,l)

Since all type signatures have an implicit forall added in front of them, so does the one for f. And each forall defines its own scope.