Type variable scope in typed Template Haskell splices?

[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 ||]