[GHC] #12561: Scope extrusion in Template Haskell

2 Sep 2016

      #12561: Scope extrusion in Template Haskell
-------------------------------------+-------------------------------------
           Reporter:  simonpj        |             Owner:
               Type:  bug            |            Status:  new
           Priority:  normal         |         Milestone:
          Component:  Template       |           Version:  8.0.1
  Haskell                            |
           Keywords:                 |  Operating System:  Unknown/Multiple
  TemplateHaskell                    |
       Architecture:                 |   Type of failure:  None/Unknown
  Unknown/Multiple                   |
          Test Case:                 |        Blocked By:
           Blocking:                 |   Related Tickets:
Differential Rev(s):                 |         Wiki Page:
-------------------------------------+-------------------------------------
 With typed quotes `[|| e ||]` and splices `$$(e)`, Template Haskell is
 supposed guarantee to generate type-correct code.  But a conversation with
 Oleg following my talk at the Cambridge Metaprogramming Summer School (Aug
 16) made me realise that it isn't.

 The problem is that
 {{{
 [|| e ||] :: Q (TExp ty)
 }}}
 So a typed quote is still monadic.  That is useful because it means that a
 function returning code can fail gracefully:
 {{{
 f :: Int -> Q (TExp Bool)
 f n | n < 0     = fail "Argument less than zero"
     | otherwise = ....
 }}}
 yielding a civilised error in the type checker's monad.

 But giving ALL the power of Q is too much.  Below is a program cooked up
 by Oleg that demonstrates the problem concretely.
 {{{
 {-# Language TemplateHaskell #-}

 module T where

 import Language.Haskell.TH
 import Language.Haskell.TH.Syntax
 import Language.Haskell.TH.Ppr

 import Data.IORef

 show_code cde = (runQ . unTypeQ $ cde) >>= putStrLn . pprint

 t1 = do
   c1 <- [|| (1::Int) + 2 ||]
   c2 <- [|| 3 + $$(return c1) ||]
   return c2

 t2 :: Q (TExp Int)
 t2 = do
   r <- runIO $ newIORef undefined
   c1 <- [|| \x -> (1::Int) +
                   $$(do
                      xv <- [||x||]
                      runIO $ writeIORef r xv
                      return xv) ||]
   runIO $ readIORef r

 t1s = show_code t1

 ts2 = show_code t2
 }}}

 -----------------------
 Possible solutions.

 * Give typed quotes access to only an emasculated Q monad, thus
 {{{
 [[| e ||] :: QQ (TExp ty)
 }}}
   where `QQ` has more limited effects.  This would work, and has the merit
 of simplicity.  We can read stuff (reification), report errors, and even
 catch those exceptions -- provided that we don't include `TExp` values in
 exceptions (not sure how we prevent that!).

 * Do what Meta OCaml does. Oleg writes "But you can go all the way and
 allow any effects. Q becomes no special (and possibly redundant). The
 stress is not on precluding scope extrusion statically but catch it
 immediately when it occurs (and report it with detailed error information:
 which variable has escaped, on which line of the source code was its
 intended binder, etc). This is what MetaOCaml does. I should stress it
 reports the scope extrusion even for open code, if one (of many) free
 variables in that code cannot eventually be bound. So the problem is not a
 scope extrusion per se: it is waiting until the whole code is generated to
 report it, at which time lots of information is already lost and it
 becomes very difficult to find the error. But reporting the error requires
 quite a bit of internal changes, to track free variables in any TH code
 fragment. Anyway, if you want to write the Wiki page, you can refer to my
 BER MetaOCaml paper, which describes the process."

--
Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12561
GHC http://www.haskell.org/ghc/
The Glasgow Haskell Compiler