Typechecking inside quasi-quotes in Template Haskell

Question

I'm trying to become familiar with Template Haskell, and to my surprise the code below compiles under ghc (version 6.10.4).

    main = do
       let
           y = [| "hello" + 1 |]
       putStr ""

This suggest to me that there's no typechecking inside quasi-quotes. This is not what I'd have expected after reading the original paper on Template Haskell. Moreover the following program does not compile.

    main = do
       let
          y = [| "hello" && True |]
       putStr ""

What's going on here?

Answer 1

It looks like GHC does type check all quotations but assumes that all generated instance constraints can be satisfied.

In this code:

main = do
   let
       y = [| "hello" + 1 |]
   putStr ""

The y bracket is typeable under the assumption that we have a Num String instance. Since GHC can't say for sure that you won't introduce such an instance before y is spliced in, it doesn't give a type error.

In this code:

 main = do
   let
      y = [| "hello" && True |]
   putStr ""

There is no way that y can ever be spliced in successfully, no matter what instance environment you set up.

This is just one example of how Template Haskell's typechecking mechanism is too lenient -- further examples are discussed in Simon PJ's blog post at http://hackage.haskell.org/trac/ghc/blog/Template%20Haskell%20Proposal, where he proposes a change to not type check any quotations at all.

Answer 2

Template Haskell has two main operations:

• lifting: [| |]
• splicing $( )

When you wrap something in the Oxford brackets, you delay its type checking (and evaluation), and instead build an AST fragment that will be type checked when it is spliced back in.

The AST that is built can be observed:

{-# LANGUAGE TemplateHaskell #-}
import Language.Haskell.TH
main = print =<< runQ  [| "hello" + 1 |]

Running this program (or typing the bracket expression into GHCi), and we get a well-formed AST, but one that is not type correct if treated as a Haskell fragment:

InfixE (Just (LitE (StringL "hello"))) (VarE GHC.Num.+) (Just (LitE (IntegerL 1)))

Now when we try to actually splice it, type checking happens:

*Main> :t [| "hello" + 1 |]
[| "hello" + 1 |] :: Q Exp

*Main> $( [| "hello" + 1 |] )
<interactive>:1:4:
  No instance for (Num [Char])
    arising from the literal `1'

As we expect. So, yes, TH expressions are type checked, but at a late point, when spliced back into a program.