Allow inferring constructor for Sum

Stream: general

[nrs]

Is there any practical way to have the following typecheck?

example : List (Sum Int (List Int)) := [7, 9, [10, 1]]

Instead of having to write

example : List (Sum Int (List Int)) := [.inl 7, .inl 9, .inr [10, 1]]

[nrs]

solved: you can achieve this with coercions. See https://lean-lang.org/functional_programming_in_lean/type-classes/coercion.html

[Eric Wieser]

Note that this is arguably a bad idea, because what would 1 : Sum Int Int mean?