∘ can't compose dependent functions.

In first example, the argument p in f is infered as fun _ => a, so f become independent function so ∘ works coincidentally.

If you want to compose dependent functions, write fun a => g (f a), or use g ∘' f in Mathlib.