Definition of extensional and propositional equality in Martin-Lof extensional type theory

Question

Martin Hofmann states in Extensional Concepts in Intensional Type Theory (§1.1 p.[4-5]) that:

A similar situation occurs in extensional Martin-Lof type theory where propositional and definitional equality are forcefully identified by the equality reflection rule

$\frac{\Gamma \vdash P:Id_\sigma(M,N)}{\Gamma \vdash M=N: \sigma}\text{(Id-DefEq)}$

Does the above mean that we purposefully drop the proof that M and N are equal and just consider them to be equal definitionally (like a presumption)?

Then it goes on and says:

This rule makes definitional equality extensional and undecidable.

How does it become extensional and what does it mean by becoming extensional in the first place?

And then it states:

Moreover, type checking becomes undecidable because $Refl(M):Id_\sigma (M,N)$ holds iff $M$ and $N$ are definitionally equal.

Why would $Refl(M)$ hold only if $M$ and $N$ are definitionally equal? And why would it make it undecidable?