Hi Viktor,
The issue happens since Typed TH quotations use an untyped
representation. These are all bugs in typed TH.
For more info you can refer to my PhD thesis and related papers which
is about this topic. https://mpickering.github.io//papers/thesis.pdf
You can also see this ghc-proposal which aimed to fix the issue for
explicit type applications:
https://github.com/ghc-proposals/ghc-proposals/pull/207
You may also be interested in my recent talk about a potential basis
for an intensionally typed representation:
https://www.youtube.com/watch?v=RbBoLq8AmAA
It turns out to be a tricky implementation problem to use a typed
internal representation, but I hope we can make progress on the issue
one day.
Cheers,
Matt
On Thu, Aug 7, 2025 at 6:55 PM Viktor Dukhovni
With the code below my signature as "Splice.hs", three nearly identical splices are defined: `good1`, `good2` and `bad`. They differ in how conversion of Int to/from Word is orchestrated around a call to the typed splice `go` whose underlying type is:
Code m (Unsigned a -> Unsigned a)
In the "good" variants, either the input conversion (a -> Unsigned a) or the output conversion (Unsigned a -> a) is done via a class method of `IntLike a`, the converse conversion just uses `fromIntegral`.
In the "bad" variant, both use `fromIntegral`. The module compiles, but there are type inference isssues when attempting to use `bad` as a splice, that don't occur with either of the "bad" variants. Is this to be expected?
$ ghci -v0 -XTemplateHaskell Splice.hs λ> :t good1 good1 :: (IntLike a, Lift a, Lift (Unsigned a), Quote m) => a -> Code m (a -> a) λ> :t good2 good2 :: (IntLike a, Lift a, Lift (Unsigned a), Quote m) => a -> Code m (a -> a) λ> :t bad bad :: (IntLike a, IntLike (Unsigned a), Lift a, Lift (Unsigned a), Quote m) => a -> Code m (a -> a) λ> f :: Word -> Word; f = $$(good1 42) λ> g :: Word -> Word; g = $$(good2 42) λ> h :: Word -> Word; h = $$(bad 42)
<interactive>:6:26: error: [GHC-39999] • Ambiguous type variable ‘a0’ arising from a use of ‘meth’ prevents the constraint ‘(WordLike a0)’ from being solved. Relevant bindings include w_a2MX :: a0 (bound at <interactive>:6:26) Probable fix: use a type annotation to specify what ‘a0’ should be. Potentially matching instances: instance WordLike Int -- Defined at Splice.hs:7:10 instance WordLike Word -- Defined at Splice.hs:6:10 • In the expression: meth (fromIntegral 42) w_a2MX In the first argument of ‘($)’, namely ‘(\ w_a2MX -> meth (fromIntegral 42) w_a2MX)’ In the second argument of ‘($)’, namely ‘((\ w_a2MX -> meth (fromIntegral 42) w_a2MX) $ fromIntegral i_a2MW)’
Why does the `bad` splice fail to capture the full context of the `go` method, which one might expect to restrict the `fromIntegral` instance to be either `a -> Unsigned a` or `Unsigned a -> a` just like the `a2w` and `w2a` methods?
It seems that despite "ScopedTypeVariables" and the explicit type signature
go :: Code m (Unsigned a -> Unsigned a)
the $$(go) splice is not tied to the same `a` as one might naïvely expect. I can write:
bad i = [|| \(i :: a) -> fromIntegral $ $$(go) $ fromIntegral @a @(Unsigned a) i ||]
and though that compiles, runs and produces correct results, it elicits warnings:
Splice.hs:30:20: warning: [GHC-86357] [-Wbadly-staged-types] Badly staged type: a is bound at stage 1 but used at stage 2 | 30 | bad i = [|| \(i :: a) -> fromIntegral $ $$(go) $ fromIntegral @a @(Unsigned a) i ||] | ^
Splice.hs:30:64: warning: [GHC-86357] [-Wbadly-staged-types] Badly staged type: a is bound at stage 1 but used at stage 2 | 30 | bad i = [|| \(i :: a) -> fromIntegral $ $$(go) $ fromIntegral @a @(Unsigned a) i ||] | ^
Splice.hs:30:77: warning: [GHC-86357] [-Wbadly-staged-types] Badly staged type: a is bound at stage 1 but used at stage 2 | 30 | bad i = [|| \(i :: a) -> fromIntegral $ $$(go) $ fromIntegral @a @(Unsigned a) i ||] | ^
In a benchmark module with a somewhat fancier splice of the "bad" sort, the use-site only compiles if both the "ScopedTypeVariables" and "TypeApplications" extensions are enabled at that the use-site, and the warnings are still produced when compiling the module that defines the splice.
-- Viktor. 🇺🇦 Слава Україні!
{-# LANGUAGE ScopedTypeVariables , TemplateHaskellQuotes, TypeFamilies #-} module Splice(good1, good2, bad) where import Language.Haskell.TH.Syntax
class (Integral a) => WordLike a where meth :: a -> a -> a instance WordLike Word where meth = (+) instance WordLike Int where meth = (+)
class (WordLike (Unsigned a), WordLike a) => IntLike a where type Unsigned a w2a :: Unsigned a -> a a2w :: a -> Unsigned a instance IntLike Word where { type Unsigned _ = Word; w2a = id; a2w = id } instance IntLike Int where { type Unsigned _ = Word; w2a = fromIntegral; a2w = fromIntegral }
good1 :: forall a m. (IntLike a, Lift a, Lift (Unsigned a), Quote m) => a -> Code m (a -> a) good1 i = [|| \i -> w2a $ $$(go) $ fromIntegral i ||] where go :: Code m (Unsigned a -> Unsigned a) go = [|| \w -> meth (fromIntegral i) w ||]
good2 :: forall a m. (IntLike a, Lift a, Lift (Unsigned a), Quote m) => a -> Code m (a -> a) good2 i = [|| \i -> fromIntegral $ $$(go) $ a2w i ||] where go :: Code m (Unsigned a -> Unsigned a) go = [|| \w -> meth (fromIntegral i) w ||]
bad :: forall a m. (IntLike a, IntLike (Unsigned a), Lift a, Lift (Unsigned a), Quote m) => a -> Code m (a -> a) bad i = [|| \i -> fromIntegral $ $$(go) $ fromIntegral i ||] where go :: Code m (Unsigned a -> Unsigned a) go = [|| \w -> meth (fromIntegral i) w ||] _______________________________________________ ghc-devs mailing list ghc-devs@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs