Cases essentially act like named arguments, except the names are inferred from the case of an argument, which is inferred through morphological analysis. And that analysis can be ambiguous, so the ambiguities are solved by the type checker / elaborator. It's different from record types in the sense that you can provide the arguments in any order to a function, and the system will figure it out because of the cases.

Cases essentially act like named arguments

... and there are only eight argument names. Which seems... limiting.

It's different from record types in the sense that you can provide the arguments in any order to a function

You can provide the fields of a record in any order, and call a function with it!

   f { foo=3, bar=5 }
   g { bar=5, foo=3 }