Skip to content

GitLab

Closed
Created by Simon Peyton Jones@simonpjDeveloper

Template Haskell: less type checking in quotations?

This ticket introduces two related Template Haskell design questions. It's inspired by several other tickets, for which these issues are the underlying cause

= 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 (closed), #4135 (closed)

  • 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.

Edited by Simon Peyton Jones