Extensional normalisation and type-directed partial evaluation for typed lambda calculus with sums