Implement a model of computation using a type system Implement any model of computation as powerful as a Turing machine using any existing language's type system.  

Your solution should handle the computation using the language's type system, not the language's regular Turing complete features, nor a macro system.  It is however acceptable to use the language's regular features for IO, typical boilerplate, etc. so long as your program's Turing completeness hangs on the type system.

You are certainly welcome to use optional type system features that require compiler options to activate.

Please specify how to program and run your machine, ala "edit these numbers/constructs in the source, compile it and run it."  

As an example, there is an implementation of brainfuck in C++ template meta-programming.  In fact, brainfuck is more complex than necessary because it offers user IO separate from its tape.  A few simpler models of computation include Brainfuck's ancestor P", λ-calculus, the (2,3) Turing Machine, and Conway's Game of Life.

We'll declare the winner to be whoever minimizes : their code's length plus 10 times the number of commenters who assert they already knew the language had a turing complete type system.
My limited Haskell-fu has come up with this implementation of SK-calculus in Haskell's type system:

data S = S
data K = K
data A l r = A l r

class C i o | i -&gt; o
instance C (A (A K a) b) a
instance C (A (A (A S a) b) c) (A (A a c) (A b c))