Yep, but for any notational shortcut the compiler infers a single thing for it. It's still unambiguous as far as computers are concerned (but it may be confusing reading it without context)
It’s not only a notational shortcut as in syntactic sugar though.
It can apply a set of rewrite rules given you were able to construct the right type at some point.
It’s type inference on steroids because you can brute force the solution by applying the rewrite rules and other tactics on propositions until something (propositional equality) is found, or nothing.
