idris-0.11.1: test/error008/error008a.idr

import Data.Vect

s1 : Num a => {x : a} -> x + sum {a} Nil = x -- * fromInteger 0
s1 = Refl