: We describe an algorithm approximatingthe following question: Given two types t1 and t2, are there instances (t1) and (t2) denoting a common element? By answering this question we solve a main problem towards a type checking algorithm for non-disjoint types that raises an error just for function calls that cannot be executed successfully. For dynamically typed functional languages such a type checker can extend actual soft typing systems in order to reject provably ill-typed programs.