The first example isn't a type annotation, it's a type definition. The curly braces are consistent with the literal syntax for records. I agree that the use of double colons in record types seems inconsistent. I assume it resolves some ambiguity.
You are spot on. Its because we reserve `:` for type and kind ascriptions. For example, `42 : Int` or `true : Bool`. But we also have `Bool : Type`, i.e. `true : Bool : Type`. While kinds are not that common in every day code, we aim for consistency with ascriptions rather than with records. Hence we had to use a different symbol in record types.
