Infer Sum.inl or Sum.inr

Stream: lean4

[Ian Riley]

Hey everyone! I was playing around with a few different ways to manipulate lists of numbers in a generic way. The approach I took this morning was to look at using a Sum type since I haven't used the Sum type much. I was very surprised to find out that Lean can't infer that a value whose type is a member of a Sum type is itself an element of that Sum type. For example, this was not allowed:

def List.sum (xs : List (Sum Nat Int)) : (Sum Nat Int) := sorry
def l := [1, 2, 3, 4]
#eval List.sum l

I apologize if some of that is a bit off. I was using the unicode symbols in my editor. I do have a working implementation of List.sum that I can post if need be. Anyway, I had to change it to:

def l := [Sum.inl 1, Sum.inl 2, Sum.inl 3, Sum.inl 4]

I did try other permutations and explicit types. All resulted in the same thing. Is there anyway that I can have lean infer that 1 : Nat is a valid element when the input type is Sum Nat Int?

[Arthur Adjedj]

You can use coercions for that:

instance : Coe A (Sum A B) := ⟨Sum.inl⟩
instance [Coe A B] : Coe (List A) (List B) where
  coe x := x.map Coe.coe

def List.sum (xs : List (Sum Nat Int)) : (Sum Nat Int) := sorry
def l := [1, 2, 3, 4]

#check List.sum l --no type error

[Ian Riley]

Nice! Thank you. It doesn't work for literals, but I was able to follow the same pattern to get literals working.

instance : OfNat (Sum Nat Int) x where
ofNat := Sum.inl x

However, I can't seem to get negative literals to work.

[Ian Riley]

It also seems counter intuitive to have literals work differently in this context than definitions, especially since there’s very little visibility when using check. I think people would naturally expect that if I check [1,2,3,4] and it comes back as List Nat and if I define list := [1,2,3,4], which also checks as a List Nat, that if the latter works under type coercion, then the former would too. But that’s not the case.

[Ian Riley]

Got it! I was trying to use Neg like Nat or like OfNat. Then it dawned on me that it might work more like Coe. Sure enough, this works.

instance : Neg (Sum Nat Int) where
neg x := match x with
| Sum.inl x => Sum.inr (-x)
| Sum.inr x => Sum.inr (-x)

I do appreciate all the help! I also want to say that any criticisms I may add are only because I want Lean to do really well.