Search code examples
haskellsyntaxtemplate-haskellquasiquotes

Quasiquoter concrete syntax for visible type application


In the following snippet, the first argument to foo, SNat @n, is assembled manually:

[e|foo $(appTypeE (conE 'SNat) n')|]
  where
    n' = litT . numTyLit . fromIntegral $ n

Is there concrete TH quasiquoter syntax for this? I.e. I'd like to write something like

[e|foo (SNat @$n')|]

but that is seemingly parsed as if I was applying an infix operator ($@):

> runQ [e|foo (SNat @$n')|]
AppE (VarE foo) (InfixE (Just (ConE SNat)) (UnboundVarE @$) (Just (VarE n')))

Interestingly, the [e| |] quasi-quoter does seem to support the concrete syntax for non-quasi visible type application:

> runQ [e|foo (SNat @5)|]
AppE (VarE foo) (AppTypeE (ConE SNat) (LitT (NumTyLit 5)))

Solution

  • Parentheses.

    let n  = 5
        n' = litT $ numTyLit $ fromIntegral n
    in  runQ [e| foo (SNat @($n')) |]
    -- ==>
    AppE (UnboundVarE foo) (AppTypeE (UnboundVarE SNat) (LitT (NumTyLit 5)))
    

    A space also works, but I wouldn't use one:

    [e| foo (SNat @ $n') |]