I think there's no fundamental reason to prevent this kind of match.
Certainly it wouldn't do to allow you to write
f (MkPoint x1) = x1
and have that match a partially-applied constructor, i.e. a function. So, one reason to specify it as it was specified here is for simplicity: the RHS of an @ has to be a pattern. Simple, easy to parse, easy to understand. (Remember, the very first origins of the language were to serve as a testbed for PL researchers to tinker. Simple and uniform is the word of the day for that purpose.) MkPoint x1 isn't a pattern, therefore mkPx@(MkPoint x1) isn't allowed.
I suspect that if you did the work needed to carefully specify what is and isn't allowed, wrote up a proposal, and volunteered to hack on the parser and desugarer as needed, the GHC folks would be amenable to adding a language extension. Seems like a lot of work for not much benefit, though.
Perhaps record update syntax will scratch your itch with much less effort.
data Point = MkPoint {x, y :: Float}
m@(MkPoint { x = x5 }) = m { x = x5 + 1 }
You also indicate that, aside from the motivation, you wonder what part of the Report says that the pattern you want can't happen. The relevant grammar productions from the Report are here:
pat → lpat
lpat → apat
| gcon apat1 … apatk (arity gcon = k, k ≥ 1)
apat → var [ @ apat] (as pattern)
| gcon (arity gcon = 0)
| ( pat ) (parenthesized pattern)
(I have elided some productions that don't really change any of the following discussion.)
Notice that as-patterns must have an apat on their right-hand side. apats are 0-arity constructors (in which case it's not possible to partially apply it) or parenthesized lpats. The lpat production shown above indicates that for constructors of arity k, there must be exactly k apat fields. Since MkPoint has arity 2, MkPoint x is therefore not an lpat, and so (MkPoint x) is not an apat, and so m@(MkPoint x) is not an apat (and so not produced by pat → lpat → apat).