  We prove that the pattern matching problem is undecidable in polymorphic
lambda-calculi (as Girard's system F) and calculi supporting inductive types
(as G{\"o}del's system T) by reducing Hilbert's tenth problem to it. More
generally pattern matching is undecidable in all the calculi in which primitive
recursive functions can be fairly represented in a precised sense.

Logic in Computer Science