WIP: Extended Typed-Holes

This is a WIP for the Extended Typed-Holes extension, which extends the parser to allow for richer typed-hole syntax.

It allows the following:

• _(...) -> An extended typed-hole. The contents here are either empty or a haskell expression.
• _$(...) -> Simliar to _(...), but the contents are an untyped template haskell expression that is run before being passed to the hole plugin. This allows for richer interaction with plugins with complex strings or a data structure defined as a TH splice by the plugin.
• _$$(...) -> Same as _$(...), except the contents are interpeted as typed template haskell.

All the holes can be followed by an integer (i.e. _(...)0) for identification.

The expressions and resulting expressions are run during renaming, and wrapped in toDyn during typechecking. A function runExtHExpr :: LHsExpr GhcTc -> TcM Dynamic is provided to plugins to extract the value from the hole, so e.g. _([Hoogle]) will evaluate to _([Hoogle]), and allow the plugin to change behavior based on the value.

This will allow us to do very feature rich editing in co-operation with the compiler. This would ostensibly solve #16875 (closed), as we could disable suggestions for regular holes _ and only the search on extended holes such as _(...)0. This will also enable advanced editing actions a la. Extensible Type-Directed Editing, and makes such type-aware editor features more easily implementable.

The Extended Holes Plugin is an example of a plugin that uses the template haskell holes (rabbit holes?) to receive commands from the user.

As this is a user-facing change to the syntax of Haskell, this is accompanied by GHC Proposal #280, supported by this merge request as an implementation of the feature.

As this is still WIP and not a complete feature, I have not added testcases nor comprehensive comments, but these will be added after more comments have been received and the feature comes closer to its final form.

As an example, compiling the following file:

{-# OPTIONS_GHC -funclutter-valid-hole-fits #-}
{-# LANGUAGE TemplateHaskell #-} 
{-# LANGUAGE ExtendedTypedHoles #-}
module Main where
import Language.Haskell.TH

main :: IO ()
main = _$(return $ LitE $ StringL $ unwords (replicate 10 "Na") ++ " BATMAN!")0

Gives the following output:

[1 of 1] Compiling Main             ( batman.hs, batman.o )

batman.hs:8:8: error:
    • Found hole: _$(...)0 :: IO ()
      Or perhaps ‘_$(...)0’ is mis-spelled, or not in scope
      Hole content: ("Na Na Na Na Na Na Na Na Na Na BATMAN!")
    • In the expression: _$(...)0
      In an equation for ‘main’: main = _$(...)0
    • Relevant bindings include main :: IO () (bound at batman.hs:8:1)
      Valid hole fits include
        main :: IO ()
        readLn :: forall a. Read a => IO a
        mempty :: forall a. Monoid a => a
  |
8 | main = _$(return $ LitE $ StringL $ unwords (replicate 10 "Na") ++ " BATMAN!")0
  | 

We can also use a plugin (here the Extended Holes Plugin) and compile the following:

{-# OPTIONS -fplugin=ExtendedHolesPlugin -funclutter-valid-hole-fits #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE ExtendedTypedHoles #-}
module Main where
import ExtendedHolesPlugin
import Control.Monad

f :: (a,b) -> a
f = _([Hoogle])


g :: (a,b) -> b
g = _$( exec $ do
        invoke Hoogle
        filterBy "Control.Monad"
        invoke Djinn)0

h :: (a,b) -> b
h = _$$( execTyped $ do
         filterBy "Prelude"
         invoke Djinn)1

And get the following output:

Main.hs:9:5: error:
    • Found hole: _(...) :: (a, b) -> a
      Where: ‘b’, ‘a’ are rigid type variables bound by
               the type signature for:
                 f :: forall a b. (a, b) -> a
               at Main.hs:8:1-15
      Or perhaps ‘_(...)’ is mis-spelled, or not in scope
    • In the expression: _(...)
      In an equation for ‘f’: f = _(...)
    • Relevant bindings include f :: (a, b) -> a (bound at Main.hs:9:1)
      Valid hole fits include
        Hoogle: Prelude fst :: (a, b) -> a
        Hoogle: Data.Tuple fst :: (a, b) -> a
        f :: (a, b) -> a
        fst :: forall a b. (a, b) -> a
  |
9 | f = _([Hoogle])
  |     ^^^^^^^^^^^

Main.hs:13:5: error:
    • Found hole: _$(...)0 :: (a, b) -> b
      Where: ‘a’, ‘b’ are rigid type variables bound by
               the type signature for:
                 g :: forall a b. (a, b) -> b
               at Main.hs:12:1-15
      Or perhaps ‘_$(...)0’ is mis-spelled, or not in scope
    • In the expression: _$(...)0
      In an equation for ‘g’: g = _$(...)0
    • Relevant bindings include
        g :: (a, b) -> b (bound at Main.hs:13:1)
      Valid hole fits include
        (\ (_, a) -> a)
        Hoogle: Prelude fst :: (a, b) -> a
        Hoogle: Data.Tuple fst :: (a, b) -> a
        g :: (a, b) -> b
   |
13 | g = _$( exec $ do
   |     ^^^^^^^^^^^^^...

Main.hs:19:5: error:
    • Found hole: _$$(...)1 :: (a, b) -> b
      Where: ‘a’, ‘b’ are rigid type variables bound by
               the type signature for:
                 h :: forall a b. (a, b) -> b
               at Main.hs:18:1-15
      Or perhaps ‘_$$(...)1’ is mis-spelled, or not in scope
    • In the expression: _$$(...)1
      In an equation for ‘h’: h = _$$(...)1
    • Relevant bindings include
        h :: (a, b) -> b (bound at Main.hs:19:1)
      Valid hole fits include
        (\ (_, a) -> a)
        (\ (_, a) -> g (head (cycle (([]) ++ ([]))), a))
        h :: (a, b) -> b
        g :: forall a b. (a, b) -> b
        snd :: forall a b. (a, b) -> b
   |
19 | h = _$$( execTyped $ do
   |     ^^^^^^^^^^^^^^^^^^^...

where invoke, (&) and filterBy are part of a DSL defined by the plugin itself.