Typed Template Haskell can observe order of type checking

Suppose I say

{-# 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"

{-# 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.