I think you need to run dataflow analysis. There is a paper I read which explains the approach, but I lost the link. It describes how to propagate types to optimize code, but the exact same method can be used to type check code too.<p>Basically the compiler annotates each value it deals with with what it knows about it. So in your example:<p><pre><code>    (sqrt (car &#x27;(1 2 &quot;hello&quot;))
</code></pre>
First &#x27;(1 2 &quot;hello&quot;) what do we know about it? The value is of type list, the elements types are: integer, integer and string. Since it is a literal, we even know the values: 1, 2, &quot;hello&quot;.<p>We record it somehow. Next we apply car to that value. What do we know about the resulting value? If car was a random function, we wouldn&#x27;t know anything about the result. But car is not random. It is one of the most common Lisp functions so we have custom code for this &quot;known&quot; function that says that its value is the first item of its first parameter.<p>Therefore the type of (car &#x27;(1 2 &quot;hello&quot;) is integer and the value is 1. Since the type of sqrt is an integer N &gt;= 0 (let&#x27;s ignore negative roots), the expression (sqrt (car &#x27;(1 2 &quot;hello&quot;)) type checks! And if we have annotated car and sqrt as side-effect free we can fold the whole expression to 1.<p>Note that if the expression was (sqrt (car &#x27;(x y z)) where x, y, z are unknown variables then it would be a &quot;maybe&quot;. We can&#x27;t know if the code type checks or not. Note also that if the expression was (sqrt (car &#x27;(-1234 y z)), then the code would <i>not</i> type check as (sqrt -1234) has no type (ignoring complex numbers here). That is strictly more powerful than ordinary type systems which can&#x27;t determine that (sqrt -1234) is a programming error.