[Haskell-cafe] TypeApplications and Proxy

Dear Cafe, since GHC has TypeApplication, we don't need Proxy that much? `natVal (Proxy :: Proxy w)` can be written as `natVal @w Proxy` but then, the argument `Proxy` looks unnecessary. I can define nat :: forall (n::Nat) . KnownNat n => Int nat = fromIntegral $ natVal @n Proxy and then use `nat @w`. (with -XAllowAmbiguousTypes.) I just wonder if that's already in some library. But then, what about the other direction (from value to type)? Is there a shorter way to write, e.g., reifyNat (read e) $ \ (_ :: Proxy w) -> run @w ... I see that Data.Reflection suggests `reifyNat (read 3) run` but then `run` needs the Proxy argument. Thanks, J.W.