GHC issueshttps://gitlab.haskell.org/ghc/ghc/-/issues2022-08-16T15:49:59Zhttps://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/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/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/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/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:12https://gitlab.haskell.org/ghc/ghc/-/issues/17804Ideas about testing and verifying code generated by typed template haskell2021-03-05T04:14:05ZMatthew PickeringIdeas about testing and verifying code generated by typed template haskellIn the recent practical experience of myself, Jamie and Andes we have felt the need for some more support for *verifing* that the programs that we generate using typed template haskell adhere to certain properties we had in mind.
This ...In the recent practical experience of myself, Jamie and Andes we have felt the need for some more support for *verifing* that the programs that we generate using typed template haskell adhere to certain properties we had in mind.
This ticket is a public place to write down some of these ideas so they are not lost forever.
## Size of subtrees
We want to be able to assert, at compile time, that the size of the generated code bares some known relationship to a statically known input. For example, the generated code is linear in the size of the input list.
In order to implement this we need the compiler to be able to report the size of a quotation. If the size of a quotation can be
inspected then the assertion functionality can be built into a library.
## Certain constructors are not present
We want to assert that in generated code certain constructors are not present. In particular, asserting that generic constructors never appear is an important property. In our own closed programs you can know this with reasonable confidence but in a hypothetical open world where people provide more staged interfaces, a rogue library may inefficiently implement an operation.
This would be a limited analysis at first because you can easily call already compiled functions in your generated code but can't inspect their definition.
## Thresholds for generating programs
A common mistake that people make when writing a staged program is to create an infinite compile time loop which generates an infinitely sized program rather than generating a loop which executes at runtime. This is much easier to do than when writing normal programs. It would be good if there was a limit as to how much recursion you were allowed to do at compile time so that beginners can get a good warning rather than puzzle, like we all did, about why the program is looping forever.
Other compile time evaluation features in GHC such as type class resolution and the inliner already have these warnings built in.
## Warning for CSP by lifting
In general, cross-stage persistence is bad. It makes it easy to accidentally create bloated programs if you accidentally use a variable at the wrong stage. For advanced users it should be possible to at least issue a warning if your program contains a cross-stage reference as you probably didn't mean it. If you did mean it, write it using an explicit splice and lift.
## Use overloaded quotes in order to perform analysis at runtime?
In order to perform some other verification it could be possible to instead perform runtime code generation by using overloaded quotations and inspecting the generating `Exp` value.https://gitlab.haskell.org/ghc/ghc/-/issues/17221Constraint scoping is wrong when using top-level splices2021-11-15T22:49:53ZMatthew PickeringConstraint scoping is wrong when using top-level splicesI claim this program should work:
```
top :: Ord a => a -> a -> Ordering
top = $$([|| compare ||])
```
because the following program works
```
top :: (a -> a -> Ordering) -> a -> a -> O...I claim this program should work:
```
top :: Ord a => a -> a -> Ordering
top = $$([|| compare ||])
```
because the following program works
```
top :: (a -> a -> Ordering) -> a -> a -> Ordering
top c = $$([|| c ||])
```
Related to #17220https://gitlab.haskell.org/ghc/ghc/-/issues/17220Interaction of constraints and top-level splices is poorly specified and hard...2020-01-08T13:13:13ZMatthew PickeringInteraction of constraints and top-level splices is poorly specified and hard to controlOn a fresh Thursday morning I set out to achieve the seemingly simple task of defining an instance for a type using typed template haskell. However, as I am sure the reader can already guess, I ran into some unexpected difficulties conce...On a fresh Thursday morning I set out to achieve the seemingly simple task of defining an instance for a type using typed template haskell. However, as I am sure the reader can already guess, I ran into some unexpected difficulties concerning type class constraints.
Code: https://github.com/mpickering/tth-define-instances
## Take 1
I want to implement an `Ord` instance using the generically defined `gcompare`. `gcompare` requires each field of the datatype to
be an instance of `Ord`, as it is recursive, including the instance we are currently defining.
```
instance Ord (BinTree Int) where
compare = $$(gcompare)
gcompare_1 :: (GenericSyntax a, All (All Ord) (Description a)) => Q (TExp (a -> a -> Ordering)))
```
However, this leads to an error because we can't use the instance for `Ord (BinTree Int)` in the top-level splice, because
it's being define in the current module, it would be possible to use it to influence the code we are currently generating.
```
Use.hs:14:16: error:
• GHC stage restriction:
instance for ‘Ord
(BinTree
Int)’ is used in a top-level splice, quasi-quote, or annotation,
and must be imported, not defined locally
• In the expression: gcompare
In the Template Haskell splice $$(gcompare)
In the expression: $$(gcompare)
|
14 | compare = $$(gcompare)
|
```
The problem is, the use of the `Ord` dictionary is in fact safe, because it's only used in generated code.
In order to reflect the static information about the dictionaries, I modified the definition of `gcompare` in order to
explicitly take the necessary evidence.
## Take 2
```
gcompare_2 :: GenericSyntax a => POP Compa (Description a) -> Syntax (a -> a -> Ordering)
data Compa a where
Compa :: Q (TExp (a -> a -> Ordering)) -> Compa a
```
`gcompare_2` takes an explicit argument which plays the role of the `All (All Ord) xs` constraint from `gcompare_1` but with the
difference that we only have access to the comparison functions in the next stage.
This means we can use `gcompare_2` as follows:
### Attempt 1
Firstly just trying to use it directly in the instance with quoted `compare` functions. I expected this to work.
```
instance Ord (BinTree Int) where
compare = $$(gcompare_2 (POP (Nil :* ((Compa [|| compare ||] :* Compa [|| compare ||] :* Compa [|| compare ||] :* Nil) :* Nil))))
```
```
Use.hs:21:48-62: error:
• GHC stage restriction:
instance for ‘Ord
(BinTree
Int)’ is used in a top-level splice, quasi-quote, or annotation,
and must be imported, not defined locally
• In the Template Haskell quotation [|| compare ||]
In the first argument of ‘Compa’, namely ‘[|| compare ||]’
In the first argument of ‘(:*)’, namely ‘Compa [|| compare ||]’
|
21 | compare = $$(gcompare_2 (POP (Nil :* ((Compa [|| compare ||] :* Compa [|| compare ||] :* Compa
[|| compare ||] :* Nil) :* Nil))))
| ^^^^^^^^^^^^^^^
```
Analysis: GHC isn't smart enough to know that `compare` is the function we are currently defining.
### Attempt 2
Try defining the function just at the top-level without the complications of the instance.
```
compareBinTree :: (Ord a) => BinTree a -> BinTree a -> Ordering
compareBinTree = $$(gcompare_2 (POP (Nil :* ((Compa [|| compareBinTree ||] :* Compa [|| compare ||] :* Compa [|| compareBinTree ||] :* Nil) :* Nil))))
```
Still doesn't work.
```
Use.hs:25:53-74: error:
• No instance for (Ord a) arising from a use of ‘compareBinTree’
• In the Template Haskell quotation [|| compareBinTree ||]
In the first argument of ‘Compa’, namely ‘[|| compareBinTree ||]’
In the first argument of ‘(:*)’, namely
‘Compa [|| compareBinTree ||]’
|
25 | compareBinTree = $$(gcompare_2 (POP (Nil :* ((Compa [|| compareBinTree ||] :* Compa [|| compare ||]
:* Compa [|| compareBinTree ||] :* Nil) :* Nil))))
| ^^^^^^^^^^^^^^^^^^^^^^
```
Analysis: This looks like a simple bug of the constraint environment not being restored inside a quotation.
### Attempt 3
Explicitly pass the comparison argument, this one works.
```
compareBinTree :: (a -> a -> Ordering) -> BinTree a -> BinTree a -> Ordering
compareBinTree c = $$(gcompare_2 (POP (Nil :* ((Compa [|| compareBinTree c ||] :* Compa [|| c ||] :* Compa [|| compareBinTree c ||] :* Nil) :* Nil))))
instance Ord (BinTree Int) where
compare = compareBinTree compare
```
----
It's not clear what to do about this ticket. It's clear that generating code which relies on constraints is currently quite inconvenient.
cc @kosmikushttps://gitlab.haskell.org/ghc/ghc/-/issues/17212Allow default methods to be implemented using template haskell2023-06-12T14:48:02ZMatthew PickeringAllow default methods to be implemented using template haskellIn conversations with @kosmikus he suggested that it would be nice to integrate default implementations with typed template haskell.
For example,
```
class Eq a where
eq :: a -> a -> Bool
default splice eq :: Generic a => Cod...In conversations with @kosmikus he suggested that it would be nice to integrate default implementations with typed template haskell.
For example,
```
class Eq a where
eq :: a -> a -> Bool
default splice eq :: Generic a => Code (a -> a -> Bool)
eq = _impl_
```
This has the massive advantage that the default implementation can be efficient than the usual `Data` or `Generics` based implementations.
There would need to be a GHC proposal related to this ticket but I write it down here in case anyone else finds it interesting.
Related to #12457Matthew PickeringMatthew Pickeringhttps://gitlab.haskell.org/ghc/ghc/-/issues/16524unused-top-binds Warning is Disabled in the Presence of TemplateHaskell2022-03-28T05:18:02Zrprijeunused-top-binds Warning is Disabled in the Presence of TemplateHaskell# Summary
If `TemplateHaskell` is enabled and a template haskell splice is used in code used by exported toplevel binds, then `unused-top-binds` fails to warn on any unused toplevel binds.
# Steps to reproduce
Given this code:
```
{-...# Summary
If `TemplateHaskell` is enabled and a template haskell splice is used in code used by exported toplevel binds, then `unused-top-binds` fails to warn on any unused toplevel binds.
# Steps to reproduce
Given this code:
```
{-# LANGUAGE TemplateHaskell #-}
module Main (main) where
import Foo
breakTopBindCheck :: IO ()
breakTopBindCheck = let _ = $$(foo 'f') in pure ()
normalOperation :: IO ()
normalOperation = pure ()
main :: IO ()
main = run
where
-- run = normalOperation
run = breakTopBindCheck
```
And any template haskell implementation of foo. For example:
```
{-# LANGUAGE TemplateHaskell #-}
module Foo (foo) where
import Language.Haskell.TH (Q)
import Language.Haskell.TH.Syntax (Exp (..), Lit (..), TExp (..))
foo :: Char -> Q (TExp Char)
foo c = pure $ TExp $ LitE $ CharL c
```
The Main module, when compiled, will fail to complain about the unused top binding for the `normalOperation` function. If the `run` definition binding to `breakTopBindCheck` is commented out, and the `run` definition binding to `normalOperation` is uncommented, then compiling successfully warns about the unused `breakTopBindCheck` binding.
# Expected behavior
I expect unused top binds to result in warnings when unused top binds warnings are enabled, regardless of whether TemplateHaskell is in use.
# Environment
* GHC version used: 8.4.4
Optional:
* Operating System: Linux, NixOS, Kernel 4.14.107
* System Architecture: x86-64https://gitlab.haskell.org/ghc/ghc/-/issues/16178Brackets and splices should be overloaded like the static keyword2019-07-07T18:01:06ZMatthew PickeringBrackets and splices should be overloaded like the static keywordIt's quite convenient that the `static` keyword is rebindable. To recap, if `e :: T` then `static e :: (IsStatic p) => p t`.
It should also be possible rebind brackets and splices in the same manner.
So we introduce two type classes `Is...It's quite convenient that the `static` keyword is rebindable. To recap, if `e :: T` then `static e :: (IsStatic p) => p t`.
It should also be possible rebind brackets and splices in the same manner.
So we introduce two type classes `IsBracket` and `IsSplice`. Now quoting a term `e :: T` has type `e :: IsBracket p => p T` and the argument to a splice
must have type `e :: IsSplice p => p T` which results in a value of type `T`.
```
class IsBracket p where
fromBracket :: Code t -> p t
class IsSplice p where
toBracket :: p t -> Code t
foo :: IsBracket p => p Int
foo = [|| 5 ||]
qux :: (IsSplice p, IsBracket p) => Int
qux = $$(foo)
```
As an aside, arguably the `static` form should only be rebindable when `RebindableSyntax` is enabled but that boat seems to have sailed.
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ---------------- |
| Version | 8.6.3 |
| Type | FeatureRequest |
| TypeOfFailure | OtherFailure |
| Priority | normal |
| Resolution | Unresolved |
| Component | Template Haskell |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"Brackets and splices should be overloaded like the static keyword","status":"New","operating_system":"","component":"Template Haskell","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.6.3","keywords":["TypedTemplateHaskell"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"FeatureRequest","description":"It's quite convenient that the `static` keyword is rebindable. To recap, if `e :: T` then `static e :: (IsStatic p) => p t`. \r\n\r\nIt should also be possible rebind brackets and splices in the same manner. \r\nSo we introduce two type classes `IsBracket` and `IsSplice`. Now quoting a term `e :: T` has type `e :: IsBracket p => p T` and the argument to a splice\r\nmust have type `e :: IsSplice p => p T` which results in a value of type `T`. \r\n\r\n{{{\r\nclass IsBracket p where\r\n fromBracket :: Code t -> p t\r\n\r\nclass IsSplice p where\r\n toBracket :: p t -> Code t\r\n\r\nfoo :: IsBracket p => p Int\r\nfoo = [|| 5 ||]\r\n\r\nqux :: (IsSplice p, IsBracket p) => Int\r\nqux = $$(foo)\r\n}}}\r\n\r\n\r\nAs an aside, arguably the `static` form should only be rebindable when `RebindableSyntax` is enabled but that boat seems to have sailed. ","type_of_failure":"OtherFailure","blocking":[]} -->https://gitlab.haskell.org/ghc/ghc/-/issues/16176Let-insertion for template haskell2019-07-07T18:01:07ZMatthew PickeringLet-insertion for template haskellWhen using Template Haskell to generate programs it's very easy to end up with a lot of duplication as splices are naively spliced in place.
For example
```
foo x = [|| $$x + $$x ||]
```
Will generate a program which completely duplic...When using Template Haskell to generate programs it's very easy to end up with a lot of duplication as splices are naively spliced in place.
For example
```
foo x = [|| $$x + $$x ||]
```
Will generate a program which completely duplicates its argument. In this case I can manually remove the duplicate by inserting a let.
```
foo x = [|| let x' = $$x in x' + x' ||]
```
Not too bad but a bit annoying to have to do manually.
When constructing bigger programs however this process becomes tedious or impossible to do correctly by hand.
```
foo :: (Q (TExp (Bool)) -> Q (TExp Int)) -> Q (TExp Int)
foo xf = [|| (let x = True in $$(xf [|| x ||])) + (let x = False in $$(xf [|| x ||]) ||]
```
Now if I pass a constant function to `foo`, the resulting code won't mention `x` so it could be floated out. However, there's not way I can tell that without running `xf` so I can't perform the same transformation as I did for the earlier program and manually insert a let. In the case of splicing in fully static data you really want it to float to the top-level and turn into a CAF.
The proposal of this ticket is to implement something like the mechanism for let-insertion in
metaocaml.
http://okmij.org/ftp/meta-programming/\#let-insert
We add two new primitives:
```
genlet :: Q (TExp a) -> Q (TExp a)
let_locus :: Q (TExp a) -> Q (TExp a)
```
`genlet` marks a code value that we want to float. `let_locus` marks places where we want to insert a let. When we evaluate the code fragment and encounter a `genlet` call, whatever the argument evaluates to is floated as far upwards as possible and inserted at the position of one of the loci.
For example,
```
sqr :: Code Int -> Code Int
sqr c = [|| $$c + $$c ||]
sqr_let :: Code Int -> Code Int
sqr_let c = let_locus (sqr (genlet c))
```
Splicing `sqr [|| 1 ||]` will result in `1 + 1` but `sqr_let [|| c ||]` will equal `let x = 1 in x + x ||]`.
It's important to do this earlier rather than later as a lot of duplication can take place which the simplifier does not like.
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ---------------- |
| Version | 8.6.3 |
| Type | FeatureRequest |
| TypeOfFailure | OtherFailure |
| Priority | normal |
| Resolution | Unresolved |
| Component | Template Haskell |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"Let-insertion for template haskell","status":"New","operating_system":"","component":"Template Haskell","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.6.3","keywords":["TypedTemplateHaskell"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"FeatureRequest","description":"When using Template Haskell to generate programs it's very easy to end up with a lot of duplication as splices are naively spliced in place. \r\n\r\nFor example\r\n\r\n{{{\r\nfoo x = [|| $$x + $$x ||]\r\n}}}\r\n\r\nWill generate a program which completely duplicates its argument. In this case I can manually remove the duplicate by inserting a let.\r\n\r\n{{{\r\nfoo x = [|| let x' = $$x in x' + x' ||]\r\n}}}\r\n\r\nNot too bad but a bit annoying to have to do manually. \r\n\r\nWhen constructing bigger programs however this process becomes tedious or impossible to do correctly by hand.\r\n\r\n{{{\r\nfoo :: (Q (TExp (Bool)) -> Q (TExp Int)) -> Q (TExp Int) \r\nfoo xf = [|| (let x = True in $$(xf [|| x ||])) + (let x = False in $$(xf [|| x ||]) ||]\r\n}}}\r\n\r\nNow if I pass a constant function to `foo`, the resulting code won't mention `x` so it could be floated out. However, there's not way I can tell that without running `xf` so I can't perform the same transformation as I did for the earlier program and manually insert a let. In the case of splicing in fully static data you really want it to float to the top-level and turn into a CAF.\r\n\r\nThe proposal of this ticket is to implement something like the mechanism for let-insertion in\r\nmetaocaml.\r\n\r\nhttp://okmij.org/ftp/meta-programming/#let-insert\r\n\r\nWe add two new primitives:\r\n\r\n{{{\r\ngenlet :: Q (TExp a) -> Q (TExp a)\r\nlet_locus :: Q (TExp a) -> Q (TExp a)\r\n}}}\r\n\r\n`genlet` marks a code value that we want to float. `let_locus` marks places where we want to insert a let. When we evaluate the code fragment and encounter a `genlet` call, whatever the argument evaluates to is floated as far upwards as possible and inserted at the position of one of the loci. \r\n\r\nFor example,\r\n\r\n{{{\r\nsqr :: Code Int -> Code Int\r\nsqr c = [|| $$c + $$c ||]\r\n\r\nsqr_let :: Code Int -> Code Int\r\nsqr_let c = let_locus (sqr (genlet c))\r\n}}}\r\n\r\nSplicing `sqr [|| 1 ||]` will result in `1 + 1` but `sqr_let [|| c ||]` will equal `let x = 1 in x + x ||]`. \r\n\r\nIt's important to do this earlier rather than later as a lot of duplication can take place which the simplifier does not like. ","type_of_failure":"OtherFailure","blocking":[]} -->https://gitlab.haskell.org/ghc/ghc/-/issues/16169Unused variable warning affects compositionality when generating code2019-10-03T08:46:45ZMatthew PickeringUnused variable warning affects compositionality when generating codeIf I'm generating a program using template haskell, I might define
a combinator to help me generate lambdas.
```
type Code a = Q (TExp a)
_lam :: (Code a -> Code b) -> Code (a -> b)
_lam f = [|| \a -> $$(f [|| a ||]) ||]
```
However, ...If I'm generating a program using template haskell, I might define
a combinator to help me generate lambdas.
```
type Code a = Q (TExp a)
_lam :: (Code a -> Code b) -> Code (a -> b)
_lam f = [|| \a -> $$(f [|| a ||]) ||]
```
However, if I now pass a constant function into `_lam`, the generated code contains an unused variable `a` that I can do nothing about and desire not to do anything about.
```
c5 :: Code (a -> Int)
c5 = _lam (const [|| 5 ||])
```
However, GHC decides that it's wise to warn me about this when I splice it in.
```
> $$c5
F2.hs:6:5: warning: [-Wunused-matches] Defined but not used: ‘a’
|
6 | q = $$c5
| ^^^
```
As Ryan will tell you, I'm against emitting warnings from generated code as it breaks the abstraction. The code that is generated is guaranteed to be type and scope correct but any aesthetic warning is irrelevant to the consumer.
I see it in precisely the same way as warning if we use a function that contains an unused variable in a library. Once the definition is exported from the library, its definition is opaque. The same principle should be applied to code generated by template haskell.
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ------------ |
| Version | 8.6.3 |
| Type | Bug |
| TypeOfFailure | OtherFailure |
| Priority | normal |
| Resolution | Unresolved |
| Component | Compiler |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"Unused variable warning affects compositionality when generating code","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.6.3","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"If I'm generating a program using template haskell, I might define\r\na combinator to help me generate lambdas. \r\n\r\n{{{\r\ntype Code a = Q (TExp a)\r\n\r\n_lam :: (Code a -> Code b) -> Code (a -> b)\r\n_lam f = [|| \\a -> $$(f [|| a ||]) ||]\r\n}}}\r\n\r\nHowever, if I now pass a constant function into `_lam`, the generated code contains an unused variable `a` that I can do nothing about and desire not to do anything about.\r\n\r\n{{{\r\nc5 :: Code (a -> Int)\r\nc5 = _lam (const [|| 5 ||])\r\n}}}\r\n\r\nHowever, GHC decides that it's wise to warn me about this when I splice it in.\r\n\r\n{{{\r\n> $$c5\r\nF2.hs:6:5: warning: [-Wunused-matches] Defined but not used: ‘a’\r\n |\r\n6 | q = $$c5\r\n | ^^^\r\n}}}\r\n\r\nAs Ryan will tell you, I'm against emitting warnings from generated code as it breaks the abstraction. The code that is generated is guaranteed to be type and scope correct but any aesthetic warning is irrelevant to the consumer. \r\n\r\nI see it in precisely the same way as warning if we use a function that contains an unused variable in a library. Once the definition is exported from the library, its definition is opaque. The same principle should be applied to code generated by template haskell. \r\n\r\n","type_of_failure":"OtherFailure","blocking":[]} -->https://gitlab.haskell.org/ghc/ghc/-/issues/15865Typed template haskell and implicit parameters lead to incorrect results2020-10-30T19:29:43ZMatthew PickeringTyped template haskell and implicit parameters lead to incorrect resultsIn a similar vein to #15863 but this time with implicit parameters.
https://gist.github.com/b6919b13abe0954fdad844e16e0edb48
```
{-# LANGUAGE ImplicitParams #-}
{-# LANGUAGE TemplateHaskell #-}
module A where
import Language.Haskell.T...In a similar vein to #15863 but this time with implicit parameters.
https://gist.github.com/b6919b13abe0954fdad844e16e0edb48
```
{-# LANGUAGE ImplicitParams #-}
{-# LANGUAGE TemplateHaskell #-}
module A where
import Language.Haskell.TH
import Data.List (sortBy)
sort :: (?cmp :: a -> a -> Ordering) => [a] -> [a]
sort = sortBy ?cmp
me :: Q (TExp ([Int] -> [Int]))
me = let ?cmp = compare in [|| sort ||]
```
In module `A` we quote a value which has an implicit argument but in its context we bind the implicit so the type of the quote is the monomorphic type.
```
{-# LANGUAGE ImplicitParams #-}
{-# LANGUAGE TemplateHaskell #-}
module B where
import A
foo :: [Int] -> [Int]
foo =
--let ?cmp = compare in
$$(me)
```
When we splice in `me`, we get an error about an unbound implicit parameter which is totally bogus as we already bound it in `A`. There is also dynamic binding if another implicit parameter with the same name is in scope but the type of `me` mentions nothing about implicit parameters so this shouldn't be allowed.
```
B.hs:8:10: error:
• Unbound implicit parameter (?cmp::Int -> Int -> Ordering)
arising from a use of ‘sort’
• In the expression: sort
In the result of the splice:
$me
To see what the splice expanded to, use -ddump-splices
In the Template Haskell splice $$(me)
|
8 | foo = $$(me)
| ^^
Failed, one module loaded.
```
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ------------ |
| Version | 8.6.1 |
| Type | Bug |
| TypeOfFailure | OtherFailure |
| Priority | normal |
| Resolution | Unresolved |
| Component | Compiler |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"Typed template haskell and implicit parameters lead to incorrect results","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.6.1","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"In a similar vein to #15863 but this time with implicit parameters.\r\n\r\nhttps://gist.github.com/b6919b13abe0954fdad844e16e0edb48\r\n\r\n{{{\r\n{-# LANGUAGE ImplicitParams #-}\r\n{-# LANGUAGE TemplateHaskell #-}\r\nmodule A where\r\n\r\nimport Language.Haskell.TH\r\nimport Data.List (sortBy)\r\n\r\n\r\nsort :: (?cmp :: a -> a -> Ordering) => [a] -> [a]\r\nsort = sortBy ?cmp\r\n\r\nme :: Q (TExp ([Int] -> [Int]))\r\nme = let ?cmp = compare in [|| sort ||]\r\n}}}\r\n\r\nIn module `A` we quote a value which has an implicit argument but in its context we bind the implicit so the type of the quote is the monomorphic type.\r\n\r\n{{{\r\n{-# LANGUAGE ImplicitParams #-}\r\n{-# LANGUAGE TemplateHaskell #-}\r\nmodule B where\r\n\r\nimport A\r\n\r\nfoo :: [Int] -> [Int]\r\nfoo =\r\n --let ?cmp = compare in\r\n $$(me)\r\n}}}\r\n\r\nWhen we splice in `me`, we get an error about an unbound implicit parameter which is totally bogus as we already bound it in `A`. There is also dynamic binding if another implicit parameter with the same name is in scope but the type of `me` mentions nothing about implicit parameters so this shouldn't be allowed.\r\n\r\n{{{\r\nB.hs:8:10: error:\r\n • Unbound implicit parameter (?cmp::Int -> Int -> Ordering)\r\n arising from a use of ‘sort’\r\n • In the expression: sort\r\n In the result of the splice:\r\n $me\r\n To see what the splice expanded to, use -ddump-splices\r\n In the Template Haskell splice $$(me)\r\n |\r\n8 | foo = $$(me)\r\n | ^^\r\nFailed, one module loaded.\r\n}}}","type_of_failure":"OtherFailure","blocking":[]} -->