You can actually encode his example in just regular Haskell98 using type classes, without having to use GADTs: http://www.cs.rutgers.edu/~ccshan/tagless/jfp.pdf

Though, it comes with some loss of clarity. And might hurt your brain.

Note that his definition for `eq` using phantom types does not compile. It has two different notions of `a`: Int and Bool, but the type constructor for Eq only has one: Expr a -> Expr a -> Expr a.

Other than that, a great overview!

Does anyone have idea how was this video created? What application was used?