GHC issueshttps://gitlab.haskell.org/ghc/ghc/-/issues2023-12-21T21:18:04Zhttps://gitlab.haskell.org/ghc/ghc/-/issues/24190Allow untyped brackets in typed splices and vice versa.2023-12-21T21:18:04ZOleg GrenrusAllow untyped brackets in typed splices and vice versa.```haskell
Prelude> :set -XTemplateHaskell
Prelude> :m +Language.Haskell.TH
Prelude Language.Haskell.TH> $(unTypeCode [|| 'x' ||])
<interactive>:3:14: error: [GHC-45108]
• Typed brackets may not appear in untyped splices.
• In t...```haskell
Prelude> :set -XTemplateHaskell
Prelude> :m +Language.Haskell.TH
Prelude Language.Haskell.TH> $(unTypeCode [|| 'x' ||])
<interactive>:3:14: error: [GHC-45108]
• Typed brackets may not appear in untyped splices.
• In the Template Haskell typed quotation [|| 'x' ||]
In the untyped splice: $(unTypeCode [|| 'x' ||])
Prelude Language.Haskell.TH> $$(unsafeCodeCoerce [| 'x' |])
<interactive>:4:21: error: [GHC-45108]
• Untyped brackets may not appear in typed splices.
• In the Template Haskell quotation [| 'x' |]
In the typed splice: $$(unsafeCodeCoerce [| 'x' |])
```
but I don't see any reason to disallow these.
In my use case I want to use type brackets (`[t| ... |]`) and there isn't typed variant of that.https://gitlab.haskell.org/ghc/ghc/-/issues/23250Allow generation of TTH syntax with TH2023-06-14T19:21:22ZOleg GrenrusAllow generation of TTH syntax with TH<!--
READ THIS FIRST: If the feature you are proposing changes the language that GHC accepts
or adds any warnings to `-Wall`, it should be written as a [GHC Proposal](https://github.com/ghc-proposals/ghc-proposals/).
Other features, appr...<!--
READ THIS FIRST: If the feature you are proposing changes the language that GHC accepts
or adds any warnings to `-Wall`, it should be written as a [GHC Proposal](https://github.com/ghc-proposals/ghc-proposals/).
Other features, appropriate for a GitLab feature request, include GHC API/plugin
innovations, new low-impact compiler flags, or other similar additions to GHC.
-->
## Motivation
That is useful in cases where a library is build with TTH in mind, but we still want to generate some auxiliary declarations, where TTH cannot help us, but untyped TH can. One such example is `staged-sop` which works with TTH, but we would like to derive `Generic` declarations with TH.
An alternative approach is to use `unsafeCodeCoerce`, but then the derived `Generic` instances would be type-checked only at use sites, i.e. much later. Also `-ddump-splices` output is quite ugly: user-written instances would use TTH brackets, not `unsafeCodeCoerce`.
## Proposal
In other words allow generation of typed splices and brackets with Untyped Template Haskell.Oleg GrenrusOleg Grenrushttps://gitlab.haskell.org/ghc/ghc/-/issues/23148template-haskell: rewrite TExp and Code documentation2023-05-08T16:21:39ZDanila Dankotemplate-haskell: rewrite TExp and Code documentation## Summary
https://hackage.haskell.org/package/template-haskell-2.19.0.0/docs/Language-Haskell-TH.html#t:TExp
mentions that
> typed quotes, written as [|| ... ||] where ... is an expression; if that expression has type a, then the qu...## Summary
https://hackage.haskell.org/package/template-haskell-2.19.0.0/docs/Language-Haskell-TH.html#t:TExp
mentions that
> typed quotes, written as [|| ... ||] where ... is an expression; if that expression has type a, then the quotation has type Q (TExp a)
However, [|| ... ||] produces Code Q a, as expected
https://downloads.haskell.org/ghc/latest/docs/users_guide/exts/template_haskell.html#syntax
## Proposed improvements or changes
Re-write docs for TExp and Code for newer compilers.
## Environment
GHC 925Matthew PickeringMatthew Pickeringhttps://gitlab.haskell.org/ghc/ghc/-/issues/22260panic when building haddock for ghc-check2022-12-13T11:43:44Zmaralornmail@maralorn.depanic when building haddock for ghc-check## Summary
While trying to build ghc-check 0.5.0.0 within nixpkgs I encounter the following error when generating haddocks.
## Steps to reproduce
`nix build .#haskell.packages.ghc942.ghc-check` on a current `haskell-updates` branch of...## Summary
While trying to build ghc-check 0.5.0.0 within nixpkgs I encounter the following error when generating haddocks.
## Steps to reproduce
`nix build .#haskell.packages.ghc942.ghc-check` on a current `haskell-updates` branch of nixpkgs (bbd00e8632c).
build ends with:
```
ghc-check> haddockPhase
ghc-check> Preprocessing library for ghc-check-0.5.0.8..
ghc-check> Running Haddock on library for ghc-check-0.5.0.8..
ghc-check> Warning: --source-* options are ignored when --hyperlinked-source is enabled.
ghc-check> 75% ( 3 / 4) in 'GHC.Check.Executable'
ghc-check> Missing documentation for:
ghc-check> trim (src/GHC/Check/Executable.hs:25)
ghc-check>
ghc-check> <no location info>: error:
ghc-check> panic! (the 'impossible' happened)
ghc-check> GHC version 9.4.2:
ghc-check> hsExprType: Unexpected HsSpliceE
ghc-check> unTypeCode (liftSplice . pure $ TExp verLifted_agFU)
ghc-check> Call stack:
ghc-check> CallStack (from HasCallStack):
ghc-check> callStackDoc, called at compiler/GHC/Utils/Panic.hs:182:37 in ghc:GHC.Utils.Panic
ghc-check> pprPanic, called at compiler/GHC/Hs/Syn/Type.hs:134:30 in ghc:GHC.Hs.Syn.Type
ghc-check>
ghc-check> Please report this as a GHC bug: https://www.haskell.org/ghc/reportabug
ghc-check>
ghc-check> haddock: Cannot typecheck modules
error: builder for '/nix/store/s3ahary8r0bysjpdzdafx9s2sp8vf151-ghc-check-0.5.0.8.drv' failed with exit code 1;
```
I realize, this is not a very nice reproducer, because it uses nix. If desired I can try to contribute to the debugging.
Still the error told me to report this, so I did.9.4.3Matthew PickeringMatthew Pickeringhttps://gitlab.haskell.org/ghc/ghc/-/issues/22056panic! no skolem info when using typed template haskell2022-08-16T15:49:59Zoberblastmeisterpanic! no skolem info when using typed template haskell## Summary
When using typed template haskell with equality constraints GHC panics.
## Steps to reproduce
```haskell
{-# LANGUAGE TemplateHaskell #-}
module A where
import Language.Haskell.TH
bomb :: Code Q Int
bomb = [||1||]
```
```...## Summary
When using typed template haskell with equality constraints GHC panics.
## Steps to reproduce
```haskell
{-# LANGUAGE TemplateHaskell #-}
module A where
import Language.Haskell.TH
bomb :: Code Q Int
bomb = [||1||]
```
```haskell
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE GADTs #-}
module B where
import A
boom :: (a ~ Int) => a
boom = $$(bomb)
```
## Expected behavior
GHC should not panic.
## Environment
* GHC version used: 9.2.3
Optional:
* Operating System: NixOS
* System Architecture: x86_64https://gitlab.haskell.org/ghc/ghc/-/issues/21910Scoped type variables in typed quotes lose scope2022-07-25T09:20:36ZAndrasKovacsScoped type variables in typed quotes lose scopeConsider the following code. I used GHC-9.2.3.
```haskell
{-# language TemplateHaskell, ScopedTypeVariables #-}
import Language.Haskell.TH
f :: forall a. CodeQ a -> CodeQ a
f x = [|| let y :: a; y = $$x in y ||]
```
This typechecks, bu...Consider the following code. I used GHC-9.2.3.
```haskell
{-# language TemplateHaskell, ScopedTypeVariables #-}
import Language.Haskell.TH
f :: forall a. CodeQ a -> CodeQ a
f x = [|| let y :: a; y = $$x in y ||]
```
This typechecks, but the following doesn't:
```haskell
g :: Bool -> Bool
g x = $$(f [||x||])
```
I get
```
• Couldn't match expected type ‘a’ with actual type ‘Bool’
‘a’ is a rigid type variable bound by
the type signature for:
x_a8Yw :: forall a. a
```
It looks like the scoped `a` is transformed into a generalized `a` after splicing.
Looking at `-ddump-simpl -dsuppress-all`, it seems that the connection between the scoped `forall a.` and the `a` in `x :: a` is completely lost in the code for `f`, although GHC does know about it during type checking `f`'s definition. As far as I see, the same thing happens with all scoped variables in quotes.
One solution would be to have quoting for types. In hypothetical syntax:
```haskell
f :: forall (a : CodeQ Type). CodeQ $$a -> CodeQ $$a
f @a x = [|| let y :: $$a; y = $$x in y ||]
```
This one seems a rather big change but I'm not sure about other solutions which are perhaps more realistic to integrate to TH (I don't really know how splice processing works).https://gitlab.haskell.org/ghc/ghc/-/issues/21051Stage restriction differs between untyped and typed TH2022-02-08T12:50:31ZKrzysztof GogolewskiStage restriction differs between untyped and typed THFile:
```haskell
{-# LANGUAGE TemplateHaskell, TypeApplications #-}
module M where
data T
x = $(const @_ @T [| 'a' |] undefined)
y = $$(const @_ @T [|| 'a' ||] undefined)
```
`x` is rejected:
```
• GHC stage restriction:
...File:
```haskell
{-# LANGUAGE TemplateHaskell, TypeApplications #-}
module M where
data T
x = $(const @_ @T [| 'a' |] undefined)
y = $$(const @_ @T [|| 'a' ||] undefined)
```
`x` is rejected:
```
• GHC stage restriction:
‘T’ is used in a top-level splice, quasi-quote, or annotation,
and must be imported, not defined locally
```
But `y` is accepted. Is there any reason why untyped and typed TH behave differently?
I don't have any example where this actually goes wrong. If there's a reason, it might be added to the documentation.https://gitlab.haskell.org/ghc/ghc/-/issues/21050Assertion failure with typed Template Haskell type variable2023-05-09T22:40:48ZKrzysztof GogolewskiAssertion failure with typed Template Haskell type variableFile:
```haskell
{-# LANGUAGE TemplateHaskell, RankNTypes #-}
module M where
import Language.Haskell.TH.Syntax
data T = MkT (forall a. a)
f x = [|| MkT $$(x) ||]
```
In 9.2 and earlier, this compiles, even with `-dcore-lint` enabled. B...File:
```haskell
{-# LANGUAGE TemplateHaskell, RankNTypes #-}
module M where
import Language.Haskell.TH.Syntax
data T = MkT (forall a. a)
f x = [|| MkT $$(x) ||]
```
In 9.2 and earlier, this compiles, even with `-dcore-lint` enabled. But the inferred type, `f :: Q (TExp a) -> Q (TExp T)`, is wrong; that'd be correct if `MkT :: a -> T` while `MkT :: (forall a. a) -> T`.
In master, this gives an assertion failure about levels inside `writeMetaTyVarRef`. If assertions are disabled, it fails Lint.
```
*** Core Lint errors : in result of Desugar (before optimization) ***
M.hs:6:1: warning:
The type variable @a_a1W4[sk:2] is out of scope
In the type of a binder: f
In the type ‘forall {m :: * -> *}.
Quote m =>
Code m a_a1W4[sk:2] -> Code m T’
Substitution: [TCvSubst
In scope: InScope {m_a1Ib}
Type env: [a1Ib :-> m_a1Ib]
Co env: []]
```
This looks related to #19893, but I'm not sure if it's the same bug.https://gitlab.haskell.org/ghc/ghc/-/issues/20969Panic in the Template Haskell2023-08-22T07:58:11ZDavid FeuerPanic in the Template Haskell## Summary
Write a brief description of the issue.
## Steps to reproduce
Write a module like this
```haskell
{-# language TemplateHaskellQuotes #-}
module SequenceCode where
import Data.Sequence.Internal
import qualified Language.Has...## Summary
Write a brief description of the issue.
## Steps to reproduce
Write a module like this
```haskell
{-# language TemplateHaskellQuotes #-}
module SequenceCode where
import Data.Sequence.Internal
import qualified Language.Haskell.TH.Syntax as TH
class Functor t => SequenceCode t where
traverseCode :: TH.Quote m => (a -> TH.Code m b) -> t a -> TH.Code m (t b)
traverseCode f = sequenceCode . fmap f
sequenceCode :: TH.Quote m => t (TH.Code m a) -> TH.Code m (t a)
sequenceCode = traverseCode id
instance SequenceCode Seq where
sequenceCode (Seq t) = [|| Seq $$(traverseCode sequenceCode t) ||]
instance SequenceCode Elem where
sequenceCode (Elem t) = [|| Elem $$t ||]
instance SequenceCode FingerTree where
sequenceCode (Deep s pr m sf) =
[|| Deep s $$(sequenceCode pr) $$(traverseCode sequenceCode m) $$(sequenceCode sf) ||]
sequenceCode (Single a) = [|| Single $$a ||]
sequenceCode EmptyT = [|| EmptyT ||]
instance SequenceCode Digit where
sequenceCode (One a) = [|| One $$a ||]
sequenceCode (Two a b) = [|| Two $$a $$b ||]
sequenceCode (Three a b c) = [|| Three $$a $$b $$c ||]
sequenceCode (Four a b c d) = [|| Four $$a $$b $$c $$d ||]
instance SequenceCode Node where
sequenceCode (Node2 s x y) = [|| Node2 s $$x $$y ||]
sequenceCode (Node3 s x y z) = [|| Node3 s $$x $$y $$z ||]
```
Then write another one importing it and doing thus:
```haskell
{-# LANGUAGE TemplateHaskell, ScopedTypeVariables #-}
glumber :: forall a. Num a => a -> Seq a
glumber x = $$(sequenceCode (fromList [TH.liftTyped _ :: TH.Code TH.Q a, [||x||]]))
```
Result:
```haskell
tests/seq-properties.hs:974:40: error:
• No instance for (TH.Lift a) arising from a use of ‘TH.liftTyped’
• In the expression: TH.liftTyped _ :: TH.Code TH.Q a
In the first argument of ‘fromList’, namely
‘[TH.liftTyped _ :: TH.Code TH.Q a, [|| x ||]]’
In the first argument of ‘sequenceCode’, namely
‘(fromList [TH.liftTyped _ :: TH.Code TH.Q a, [|| x ||]])’
|
974 | glumber x = $$(sequenceCode (fromList [TH.liftTyped _ :: TH.Code TH.Q a, [||x||]]))
| ^^^^^^^^^^^^
tests/seq-properties.hs:974:53: error:ghc: panic! (the 'impossible' happened)
(GHC version 9.2.1:
No skolem info:
[a_aaba[sk:1]]
Call stack:
CallStack (from HasCallStack):
callStackDoc, called at compiler/GHC/Utils/Panic.hs:181:37 in ghc:GHC.Utils.Panic
pprPanic, called at compiler/GHC/Tc/Errors.hs:2888:17 in ghc:GHC.Tc.Errors
```
## Expected behavior
I expect my error messages not to be accompanied by panics.
## Environment
* GHC version used: 9.2.1
Optional:
* Operating System:
* System Architecture:Matthew PickeringMatthew Pickeringhttps://gitlab.haskell.org/ghc/ghc/-/issues/20157Suggest TemplateHaskell when failing to parse a typed splice2021-07-27T16:06:41ZKirill Elaginkirelagin@gmail.comSuggest TemplateHaskell when failing to parse a typed splice## Summary
If you forget to enable `TemplateHaskell` and then write `$(foo)`, you will get:
```
parse error on input ‘$’
Perhaps you intended to use TemplateHaskell
```
However, for `$$(foo)` you will only get:
```
parse erro...## Summary
If you forget to enable `TemplateHaskell` and then write `$(foo)`, you will get:
```
parse error on input ‘$’
Perhaps you intended to use TemplateHaskell
```
However, for `$$(foo)` you will only get:
```
parse error on input ‘$$’
```
and no suggestion to enable the extension. That’s unfair!
## Steps to reproduce
* `echo 'foo = $$()' > test.hs && ghc test.hs`
## Expected behavior
Say “parse error on input ‘$$’” and suggest `TemplateHaskell`.
## Environment
* GHC version used: 8.10.4
Optional:
* Operating System:
* System Architecture:Krzysztof GogolewskiKrzysztof Gogolewskihttps://gitlab.haskell.org/ghc/ghc/-/issues/19893Core Lint error with typed Template Haskell (The type variable ... is out of ...2023-08-11T11:04:21ZRyan ScottCore Lint error with typed Template Haskell (The type variable ... is out of scope)The `parsley-0.1.0.1` Hackage library fails to compile with `-dcore-lint`. Here is a minimized version of the failing code:
```hs
{-# LANGUAGE TemplateHaskell #-}
module Bug where
import Control.Monad.ST
import Language.Haskell.TH
f :...The `parsley-0.1.0.1` Hackage library fails to compile with `-dcore-lint`. Here is a minimized version of the failing code:
```hs
{-# LANGUAGE TemplateHaskell #-}
module Bug where
import Control.Monad.ST
import Language.Haskell.TH
f :: Code Q Char
f = [|| runST $$([|| pure 'a' ||]) ||]
```
```
$ /opt/ghc/9.0.1/bin/ghc Bug.hs -dcore-lint
[1 of 1] Compiling Bug ( Bug.hs, Bug.o, Bug.dyn_o )
*** Core Lint errors : in result of Desugar (before optimization) ***
<no location info>: warning:
The type variable @s_a20Z[sk:1] is out of scope
In the type of a binder: $dApplicative_a218
In the type ‘Applicative (ST s_a20Z[sk:1])’
Substitution: [TCvSubst
In scope: InScope {}
Type env: []
Co env: []]
*** Offending Program ***
Rec {
$dQuote_a211 :: Quote Q
[LclId]
$dQuote_a211 = $dQuote_a20R
$dQuote_a20R :: Quote Q
[LclId]
$dQuote_a20R = $fQuoteQ
$dApplicative_a218 :: Applicative (ST s_a20Z[sk:1])
[LclId]
$dApplicative_a218 = $fApplicativeST @s_a20Z[sk:1]
$trModule :: Module
[LclIdX]
$trModule = Module (TrNameS "main"#) (TrNameS "Bug"#)
f :: Code Q Char
[LclIdX]
f = unsafeCodeCoerce
@'LiftedRep
@Char
@Q
$dQuote_a20R
(appE
@Q
$dQuote_a20R
(varE
@Q
$dQuote_a20R
(mkNameG_v
(unpackCString# "base"#)
(unpackCString# "GHC.ST"#)
(unpackCString# "runST"#)))
(unTypeCode
@'LiftedRep
@(ST s_a20Z[sk:1] Char)
@Q
$dQuote_a20R
(unsafeCodeCoerce
@'LiftedRep
@(ST s_a20Z[sk:1] Char)
@Q
$dQuote_a211
(appE
@Q
$dQuote_a211
(varE
@Q
$dQuote_a211
(mkNameG_v
(unpackCString# "base"#)
(unpackCString# "GHC.Base"#)
(unpackCString# "pure"#)))
(litE @Q $dQuote_a211 (charL (C# 'a'#)))))))
end Rec }
*** End of Offense ***
<no location info>: error:
Compilation had errors
```https://gitlab.haskell.org/ghc/ghc/-/issues/19470GHCi does not error when typed template haskell errors in IO2022-01-22T01:03:07ZolligobberGHCi does not error when typed template haskell errors in IO## Summary
If some expression using typed template haskell would cause an exception when running compile-time code, then putting that expression into IO using pure or print suppresses the error and does not execute the IO action.
## St...## Summary
If some expression using typed template haskell would cause an exception when running compile-time code, then putting that expression into IO using pure or print suppresses the error and does not execute the IO action.
## Steps to reproduce
Enter GHCi with -XTemplateHaskell and run `print ($$undefined :: String)`.
## Expected behavior
Print an error, similar to when running `($$undefined :: String)` or `print ($undefined :: String)` in GHCi.
## Environment
* GHC version used: 8.10.4
Optional:
* Operating System: 5.11.1-arch1-1
* System Architecture: x86_64Matthew PickeringMatthew Pickeringhttps://gitlab.haskell.org/ghc/ghc/-/issues/19368Typed Template Haskell suppresses -Wunused-top-binds warnings2021-02-21T15:24:30ZRyan ScottTyped Template Haskell suppresses -Wunused-top-binds warningsIn this program:
```hs
{-# LANGUAGE TemplateHaskell #-}
{-# OPTIONS_GHC -Wunused-top-binds #-}
module Bug (a) where
a :: Int
a = $([| 42 |])
-- a = $$([|| 42 ||])
z :: Int
z = 42
```
GHC correctly informs me that `z` is defined but n...In this program:
```hs
{-# LANGUAGE TemplateHaskell #-}
{-# OPTIONS_GHC -Wunused-top-binds #-}
module Bug (a) where
a :: Int
a = $([| 42 |])
-- a = $$([|| 42 ||])
z :: Int
z = 42
```
GHC correctly informs me that `z` is defined but not used:
```
$ /opt/ghc/8.10.3/bin/ghc Bug.hs
[1 of 1] Compiling Bug ( Bug.hs, Bug.o, Bug.dyn_o )
Bug.hs:10:1: warning: [-Wunused-top-binds]
Defined but not used: ‘z’
|
10 | z = 42
| ^
```
If I comment out the definition of `a` and replace it with `a = $$([|| 42 ||])`, however, then GHC doesn't report any warnings at all!
```
$ /opt/ghc/8.10.3/bin/ghc Bug.hs
[1 of 1] Compiling Bug ( Bug.hs, Bug.o, Bug.dyn_o )
```
I'm unclear why the use of typed Template Haskell would change things here, as I would expect `-Wunused-top-binds` warnings in both scenarios.https://gitlab.haskell.org/ghc/ghc/-/issues/18736Linear types: type inference in Typed Template Haskell2021-02-06T15:14:03ZKrzysztof GogolewskiLinear types: type inference in Typed Template HaskellThe following module should compile, but it doesn't:
```
{-# LANGUAGE TemplateHaskell, LinearTypes #-}
module Bug where
import Language.Haskell.TH
idenq :: Quote m => Code m (a #-> a)
idenq = [|| \x -> x ||]
```
```
• Couldn't mat...The following module should compile, but it doesn't:
```
{-# LANGUAGE TemplateHaskell, LinearTypes #-}
module Bug where
import Language.Haskell.TH
idenq :: Quote m => Code m (a #-> a)
idenq = [|| \x -> x ||]
```
```
• Couldn't match type ‘'Many’ with ‘'One’
Expected: Code m (a #-> a)
Actual: Code m (a -> a)
```
The workaround is `[|| (\x -> x) :: a #-> a ||]`.
Originally reported at https://gitlab.haskell.org/ghc/ghc/-/merge_requests/852#note_280765.https://gitlab.haskell.org/ghc/ghc/-/issues/18600Typed Template Haskell can observe order of type checking2020-09-30T21:53:45ZRichard Eisenbergrae@richarde.devTyped Template Haskell can observe order of type checkingSuppose I say
```hs
{-# LANGUAGE ScopedTypeVariables, TemplateHaskell, TypeApplications, GADTs #-}
module Meta where
import Type.Reflection
import Language.Haskell.TH
foo :: forall a. Typeable a => Code Q a
foo | Just HRefl <- typeRe...Suppose I say
```hs
{-# LANGUAGE ScopedTypeVariables, TemplateHaskell, TypeApplications, GADTs #-}
module Meta where
import Type.Reflection
import Language.Haskell.TH
foo :: forall a. Typeable a => Code Q a
foo | Just HRefl <- typeRep @a `eqTypeRep` typeRep @String
= [|| "TyDe " ||]
| otherwise
= error "urk"
```
```hs
{-# LANGUAGE TemplateHaskell #-}
module Meta2 where
import Meta
both :: a -> a -> (a,a)
both = (,)
ex1 = both $$foo "hello"
ex2 = both "hello" $$foo
```
Then `ex1` is rejected while `ex2` is accepted. The reason is that `ex2` solves for the choice of type variable `a` *before* we encounter the TTH splice, while `ex1` doesn't have that happy circumstance. Sadly, this means that TTH succeeds or fails depending on the order of type checking, which is distasteful.
One approach is outlined in https://icfp20.sigplan.org/details/tyde-2020-papers/6/Predictable-Macros-for-Hindley-Milner-Extended-Abstract- (which will hopefully be posted publicly somewhere -- I just watched the talk) and it involves *stuck macros*. The idea would be that we delay evaluating TTH splices with `Typeable` constraints until all metavariables are solved.https://gitlab.haskell.org/ghc/ghc/-/issues/18521Code is levity-polymorphic, but CodeQ and TExpQ aren't2020-08-20T23:55:51ZRyan ScottCode is levity-polymorphic, but CodeQ and TExpQ aren'tOn HEAD, the following will typecheck:
```hs
{-# LANGUAGE MagicHash #-}
{-# LANGUAGE TemplateHaskell #-}
module Bug where
import GHC.Exts (Int#)
import Language.Haskell.TH
a :: Code Q Int#
a = [|| 42# ||]
```
But @buggymcbugfix obser...On HEAD, the following will typecheck:
```hs
{-# LANGUAGE MagicHash #-}
{-# LANGUAGE TemplateHaskell #-}
module Bug where
import GHC.Exts (Int#)
import Language.Haskell.TH
a :: Code Q Int#
a = [|| 42# ||]
```
But @buggymcbugfix observed that neither of the following will typecheck:
```hs
b :: CodeQ Int#
b = a
c :: TExpQ Int#
c = examineCode a
```
```
[1 of 1] Compiling Bug ( Bug.hs, interpreted )
Bug.hs:11:12: error:
• Expecting a lifted type, but ‘Int#’ is unlifted
• In the first argument of ‘CodeQ’, namely ‘Int#’
In the type signature: b :: CodeQ Int#
|
11 | b :: CodeQ Int#
| ^^^^
Bug.hs:14:12: error:
• Expecting a lifted type, but ‘Int#’ is unlifted
• In the first argument of ‘TExpQ’, namely ‘Int#’
In the type signature: c :: TExpQ Int#
|
14 | c :: TExpQ Int#
| ^^^^
```
This is because `Code` is levity polymorphic in its last argument, but neither `CodeQ` nor `TExpQ` are. It feels like they should be for the sake of consistency.9.0.1https://gitlab.haskell.org/ghc/ghc/-/issues/18211Types of Typed Spliced are not inferred (looks like only checked)2023-02-16T12:45:37ZOleg GrenrusTypes of Typed Spliced are not inferred (looks like only checked)I think this might be duplicate of #10271, but I'm not sure. This example is simpler.
Consider a small utility type-class (a variant discussed in !3290
```haskell
{-# LANGUAGE GADTs #-}
module CodeFromString where
import La...I think this might be duplicate of #10271, but I'm not sure. This example is simpler.
Consider a small utility type-class (a variant discussed in !3290
```haskell
{-# LANGUAGE GADTs #-}
module CodeFromString where
import Language.Haskell.TH
import Language.Haskell.TH.Syntax
class CodeFromString a where
codeFromString :: String -> TExpQ a
instance a ~ Char => CodeFromString [a] where
codeFromString = liftTyped
```
It seems to work
```haskell
{-# LANGUAGE TemplateHaskell #-}
module Main (main) where
import CodeFromString
main :: IO ()
main = do
putStrLn $$(codeFromString "example string")
```
Yet, if we make the setting just slightly more complicated like:
```haskell
-- doesn't work
print $ $$(codeFromString "example string") == "example string"
-- doesn't work
print $ $$(codeFromString "example string") == ("example string" :: String)
```
The type of splice `TExpQ String` should be easily inferrable, but GHC refuses to infer it. If we make GHC check the type with
```haskell
-- works.
print $ ($$(codeFromString "example string") :: String) == ("example string" :: String)
```
it works again. But the explicit type-annotation / checked positions make this kind of usage quite impractical.
cc @mpickeringhttps://gitlab.haskell.org/ghc/ghc/-/issues/18170More Typed Template Haskell unsoundness due to levity polymorphism2022-05-10T16:26:58ZMatthew PickeringMore Typed Template Haskell unsoundness due to levity polymorphismThe levity polymorphism check does not run on quoted expressions which means you can use quotes to define a levity polymorphic code generator.
This leads to unsoundness as a well-typed code generator leads to an ill-typed program.
```
...The levity polymorphism check does not run on quoted expressions which means you can use quotes to define a levity polymorphic code generator.
This leads to unsoundness as a well-typed code generator leads to an ill-typed program.
```
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE TemplateHaskell #-}
module Bad where
import Language.Haskell.TH.Lib
import GHC.Exts
-- Example from the user guide but with the function wrapped in quotes
bad :: forall (r1 :: RuntimeRep) (r2 :: RuntimeRep)
(a :: TYPE r1) (b :: TYPE r2).
TExpQ ((a -> b) -> a -> b)
bad = [|| \f x -> f x ||]
```
```
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE TemplateHaskell #-}
module Lev where
import Language.Haskell.TH.Lib
import Bad
import GHC.Exts
-- Code generator type checked but splicing fails to produce well-typed
-- program -- unsound
unsound :: forall (r1 :: RuntimeRep) (r2 :: RuntimeRep)
(a :: TYPE r1) (b :: TYPE r2).
((a -> b) -> a -> b)
unsound = $$(bad)
-- Generating a monomorphic program is sound, and hence a workaround for
-- normal levity polymorphic restrictions.
workaround :: Int
workaround = $$bad id 5
```
https://gist.github.com/144e42b4429673d8449f59413cc10ca4
cc @RyanGlScott who was interested in this issue.https://gitlab.haskell.org/ghc/ghc/-/issues/18102TemplateHaskellQuotes and RebindableSyntax don't play nicely2021-02-05T10:11:11ZRichard Eisenbergrae@richarde.devTemplateHaskellQuotes and RebindableSyntax don't play nicelyEDIT: The original problem described here was about untyped TH, and it was fixed in !2960. But we identify a new problem with typed Template Haskell, which has yet to be solved. https://gitlab.haskell.org/ghc/ghc/-/issues/18102#note_2922...EDIT: The original problem described here was about untyped TH, and it was fixed in !2960. But we identify a new problem with typed Template Haskell, which has yet to be solved. https://gitlab.haskell.org/ghc/ghc/-/issues/18102#note_292247 shows two illustrative examples.
-------------------------------------------------------
If I say
```hs
{-# LANGUAGE TemplateHaskell, RebindableSyntax #-}
module Bug where
import Prelude ( Monad(..), Bool(..), print, ($) )
import Language.Haskell.TH.Syntax
$( do stuff <- [| if True then 10 else 15 |]
runIO $ print stuff
return [] )
```
then I get errors about `ifThenElse` and `fromInteger` not being in scope. When I bring them into scope, the code is accepted, but the quoted syntax does not mention them, instead accurately reflecting the original source Haskell I wrote.
There are several problems in this story:
1. Template Haskell quotes are meant to work even in the presence of unbound identifiers.
2. Template Haskell is all about quoting (and splicing) surface syntax. Quoting should not care about `-XRebindableSyntax`.
3. If we were to decide that quoting should respect `-XRebindableSyntax` (I disagree with this design, to be clear), then the output of the quote is incorrect.
I propose: disable `-XRebindableSyntax` within quotes. That should fix all these problems.
Other reasonable possibility: disable `-XRebindableSyntax` within quotes, but use the TH combinators that are in scope (like `conE` and `appE`, etc.). I think this would be nightmarish to implement, and no one is asking for it, but it would be a consistent way forward.https://gitlab.haskell.org/ghc/ghc/-/issues/17863Typed template haskell is very underdocumented2020-02-26T17:01:10ZadamTyped template haskell is very underdocumentedThere is a lack of documentation in both the [users guide][1] and the [template-haskell haddocks][2]. Every time I go looking it takes a while to find the 2 bullet points in the users guide on the syntax.
An own section and a worked exa...There is a lack of documentation in both the [users guide][1] and the [template-haskell haddocks][2]. Every time I go looking it takes a while to find the 2 bullet points in the users guide on the syntax.
An own section and a worked example would be a big improvement.
[1]: https://downloads.haskell.org/~ghc/latest/docs/html/users_guide/glasgow_exts.html?highlight=typed%20expression#th-syntax
[2]: https://hackage.haskell.org/package/template-haskell-2.15.0.0/docs/Language-Haskell-TH.html#g:12