id,summary,reporter,owner,description,type,status,priority,milestone,component,version,resolution,keywords,cc,os,architecture,failure,difficulty,testcase,blockedby,blocking,related
4230,Template Haskell: less type checking in quotations?,simonpj,,"This ticket introduces two related Template Haskell design questions.  It's inspired by several other tickets, for which these issues are the underlying cause
 * #4135
 * #4128
 * #4170
 * #4125
 * #4124

-----------------------
= ISSUE 1 =

Consider this module
{{{
  module M where
   import ...
   f x = x
   $(th1 4)
   h y = k y y
   $(th2 10)
}}}
In our present setup we typecheck down to the first splice, run the splice, then typecheck to the second splice, run that, and so on.

But GHC's main structure is: 
 * parse
 * rename (resolve lexical scopes)
 * typecheck

The above setup makes this impossible. We can't even rename the definition of h until we've run the splice $(th1 4) because that might be what brings k into scope.  All this is a bit hard to explain to users.

Now suppose that instead we did the following.  

  * Typecheck and run '''top-level''' splices in the renamer

That is, when the renamer finds a top-level splice:
  * rename it
  * typecheck it
  * run it
  * replace the splice by the result of running it
  * and then rename *that* as if that's what the user had written in the first place
But what about nested quotes?  eg
{{{
     $(th1 [| f x |])
}}}
Well we can't typecheck that quote, because we don't have a type for f and x, because we are in the renamer.  But we don't '''need''' to typecheck the quote to be able to typecheck and run the splice!  Remember, we already have a staging restriction that only imported functions can be '''run''' in a top-level splice.

So the proposal would mean that we don't attempt to typecheck those nested quotes.  Instead they'll be checked after the top-level splice is run, the result spliced in, and the whole shebang typechecked in the context of the program as a whole.
This defers the error message, but not too muce, since typechecking the output of the splice is what will happen next.

This approach would have a number of rather compelling advantages:

 * It would allow us to show the program after renaming and splice
 expansion, but before typechecking.  That's quite helpful.  It
 makes it easier to say that we
   * rename the program, and then
   * typecheck the program
  Remember, GHC is also a Haskell library, and the current
  story (a bit of renaming, a bit of typechecking, then a bit more
  renaming and a bit more typechecking) complicates the API.

 * Geoff Mainland's quasi-quotation mechanism is run in the
   renamer (because it can expand to patterns) so it would make
   all the TH stuff more consistent.

 * Even more exciting, we could support pattern splices, thus
{{{
     f $(g 4) = x+y
}}}
  because the splice $(g 4) would be typechecked and run, perhaps
  expanding to (x,y), say, by the renamer *before* it goes on to
  do scope-analysis on x+y.  This is exactly why quasiquoting
  *can* do pattern splicing at the moment, and TH cannot.
  [[BR]][[BR]]
  This would fix a long-standing infelicity in TH, namely the
  absence of pattern splices.

 * In the same way we could support local declaration
   splices (which are currently ruled out)
{{{
       f x = let $(g [| x |]) in ....
}}}  
 * At the top level we could get rid of the top-to-bottom bias.
   We could allow, say
{{{
     f x = x+x
     $(th [| g |] [| f |])
     g y = y+1
}}}
One disadvantage is that it'd ""bake in"" the staging restriction that a splice can only (typecheck and) run functions imported from another module.  Currently this is only an implementation restriction, which in principle might be lifted.  On the other hand, I have no plans to lift it, and in practice people don't complain about it.

------------------
= ISSUE 2 =

Consider this:
{{{
  f :: Q Type -> Q [Dec]
  f t = [d| data T = MkT $t; 
            g (MkT x) = g+1 |]
}}}
This function f returns a declaration splice, declaring T and g.
You'll see that the constructor MkT takes an argument whose type is passed (as a quotation) to f -- a type splice.

The difficulty is that we can't typecheck the declaration of 'g'
until we know what $t is; and we won't know that until f is called.
So 
 * we can't really typecheck the declaration quote at all

In the case of '''term''' splices in a quotation we can simply give them type (forall a. a), which never gets in the way. But there is no equivalent for *type* splices.  An analogous problem occurs in other declaration splices, for example
{{{
  f t = [d| instance C $t where ... |]
}}}
Here GHC's check that an instance decl is always of form
{{{
   instance C (T a b c)
}}}
falls over, again because we don't know what $t will be.


It's hard to see what to do about this.  

 * We could get rid of type splices (but people like them)

 * We could refrain from typechecking quotations *at all*
   I have users asking me for exactly this: #4125, #4135

 * We could refrain from typechecking *declaration* quotes.
   But the problem still happens for terms
{{{
      [| let { f :: $t; f = e } in .. |]
}}}
 * We could refrain from typechecking any quotation that
   included a type splice.  This is probably the most benign:
   it switches off the type checker just when it's problematic,
   and it's very predictable when that is.  Awkward to implement
   though.
   
Do you have any other ideas?

----------------------
= DISCUSSION =

The two issues are related of course, because both involve doing
less typechecking of quotations.

That seems a pity, because it'd lose one of TH's advantages --
that of typechecking meta programs rather than just typechecking
the output of the meta programs.  And in the case of ISSUE 2,
error messages might get delayed, perhpas to another module
altogether.

However, we deliberately designed TH so that it ''is'' possible to
get a type error when typechecking the result of a type-correct
top-level splice.  Reason: we use type Exp rather than (Exp t) as
in MetaML. That gave us (a lot) more flexibility.  Apart from
anything else, declaration splices would be problematic in the
MetaML approach.

Seen in that light, the proposals here just move a bit further in
the direction of flexibility, at the cost of somewhat-increased
danger of errors being reported later than is ideal.  
",feature request,new,low,7.6.2,Compiler,7.6.3,,,illissius@… jwlato@… gmainlan@…,Unknown/Multiple,Unknown/Multiple,None/Unknown,Unknown,,,"4124, 4125, 4128, 4135, 4170",