Why doesn't cong typecheck in Idris 2

Question

I'm writing a function to test propositional equality of Nat, and it typechecks in Idris 1.

sameNat : (n : Nat) -> (m : Nat) -> Maybe (n = m)
sameNat Z Z = Just Refl
sameNat (S n) (S m) = case sameNat n m of
                        Just e => Just (cong e)
                        Nothing => Nothing
sameNat _ _ = Nothing

But it doesn't typecheck in Idris 2 (0.4.0) and I got this error.

Error: While processing right hand side of sameNat. When
unifying n = m and Nat m e -> :: ?x ?xs n m e.
Mismatch between: n = m and Nat m e -> :: ?x ?xs n m e.

It typechecks when I write a specific version of cong and use it.

cong' : n = m -> S n = S m
cong' Refl = Refl

Why doesn't this typecheck and how can I make it typecheck?

Answer 1

The type signature of cong changed:

Idris 1:

cong : (a = b) -> f a = f b

Idris 2:

Prelude.cong : (0 f : (t -> u)) -> a = b -> f a = f b