Well-typed narrowing with extra variables in functional-logic programming