idris-0.11.1: test/error008/error008.idr

import Data.Vect

s2 : x + sum Nil = x * fromInteger 0
s2 = Refl