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 <ietf-d...@dukhovni.org> wrote: > > 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 _______________________________________________ ghc-devs mailing list ghc-devs@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
