I mentioned this when you were asking about this in IRC, but you may have missed it.

All type variables are implicitly qualified at top level in standard Haskell (and in ghc if they are not explicitly qualified at some level). Thus the actual type signature is

    foo3 :: forall a. a -> Int

and (forall a. a) does *not* unify with Int. This does not work in both directions, though; in your second example, the *inferred* type (t -> t) is permitted to unify with an explicitly specified type (Int -> Int). It is only explicitly specified types that do this (this is what "rigid" means: explicitly specified, therefore not permitted to unify with a more specific type).

The reason for this is that the type signature specifies the contract with callers. (a -> a) which means (forall a. a -> a) promises the caller you will accept any (a) the *caller* chooses. This is why such explicit signatures are rigid: you promised the caller you will accept any (a), so you may not renege on that contract and always produce (Int).
--