Problem

In a dependently typed language, type checking requires evaluating arbitrary program segments at compile time.

Doesn’t play well with:

• Programs that might loop infinitely
• Programs that might panic
• Programs with side effects

That is… general-purpose programs!