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.