Add `Lift Exp` instance to `Language.Haskell.TH.Syntax`

Being open-minded, I played around with TH quotations and encountered a strange error message:

TyFamWitnesses.hs:106:40-71: error:

• No instance for (Lift Exp) arising from a use of ‘lift’

• In the expression: lift eqTypeRep

In the expression:

        [| eqTypeRep (typeRep @Maybe) |]
        pending(rn) [<eqTypeRep, lift eqTypeRep>]
      In an equation for ‘fun'’:
          fun'
            = [| eqTypeRep (typeRep @Maybe) |]
              pending(rn) [<eqTypeRep, lift eqTypeRep>]
    |
106 |                                 fun' = [e|eqTypeRep (typeRep @ Maybe)|]
    |                                        ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

Failed, 0 modules loaded.

Adding an orphan instance locally helped (of course).

instance Lift Exp where lift = pure

It appears to be the right thing to do... Why isn't this in Language.Haskell.TH.Syntax? Just forgotten? If so, and somebody gives me a thumbs up, I'll add it tomorrow to HEAD (with a corresponding @since annotation).

Trac metadata

Trac field	Value
Version	8.2.1
Type	FeatureRequest
TypeOfFailure	OtherFailure
Priority	normal
Resolution	Unresolved
Component	Template Haskell
Test case
Differential revisions
BlockedBy
Related
Blocking
CC
Operating system
Architecture

changed weight to 5

added Tfeature request TemplateHaskell Trac import labels

This is planned as part of a larger proposal to derive Lift instances for all data types in template-haskell. See #14030 (closed).

Trac metadata

Trac field	Value
Related	- → #14030 (closed)

However, it should be noted that a derived Lift instance for Exp would not produce the code above. The problem with that instance is that if x :: Exp, then $(lift x) would not necessarily equal x (or even be of type Exp!), which is a rule you'd generally expect to hold. (I realize this law isn't started anywhere in the Haddocks at the moment, but it probably should be.)

Replying to [ticket:14296#comment:143171 RyanGlScott]:

However, it should be noted that a derived Lift instance for Exp would not produce the code above. The problem with that instance is that if x :: Exp, then $(lift x) would not necessarily equal x (or even be of type Exp!), which is a rule you'd generally expect to hold. (I realize this law isn't started anywhere in the Haddocks at the moment, but it probably should be.)

Interesting. I did not think about that too deeply. Maybe worth documenting this. But in my case (the specific usage in [e|eqTypeRep (typeRep @ Maybe)|]) the invariant is satisfied: lift eqTypeRep should encode an Exp. After all, I use it in this context [p|($here -> Just HRefl)|] as the view function. So I should be safe, right? Should I err, the type checker will remind me after quotation expansion, won't it?

What about the derivation mechanism for Lift instances? Will it do the right thing in this case too?

Anyway, thanks for the insight!

Let me try and articulate more precisely what this invariant is capturing. Here are some examples of the invariant at work:

{-# LANGUAGE TemplateHaskell #-}

import Language.Haskell.TH.Syntax

test :: IO ()
test = mapM_ print
  [ $(lift True)     == True
  , $(lift "hello")  == "hello"
  ]

These should all print True, and more generally, you should be able to stick in any other Bool or String and also have it print all Trues. But it's easy to subvert this with your proposed Lift Exp instance, since you can have, e.g.:

uhOh :: Exp
uhOh = lift "uhOh"

Now $(lift uhOh) won't be an Exp, but rather a String. This is not at all what we want.

Replying to [ticket:14296#comment:143178 heisenbug]:

What about the derivation mechanism for Lift instances? Will it do the right thing in this case too?

Right. Here is an except of the -ddump-deriv output from deriving a Lift instance for Exp:

deriving instance Lift Exp

===>

instance Lift Exp where
  lift (VarE a) = conE 'VarE `appE` lift a
  lift (ConE a) = conE 'ConE `appE` lift a
  lift (AppE f x) = conE 'AppE `appE` lift f `appE` lift x
  ...

Now calling lift on an Exp will produce an ExpQ that represents an Exp value. It's quite meta, granted, but that's how it should be :)

In any case, I've been meaning to resolve #14030 (closed) for a while now, but haven't had much time to look into it recently. One obstacle is that deriving Lift instances for data types in template-haskell during stage-1 compilation is harder than it sounds because GHC HEAD moved around the locations of functions that are used when deriving Lift instances themselves. Therefore, I think I'll have to disable generating Lift instances on stage-1 compilers for now to make it work, but I've yet to figure out how to accomplish that.

Replying to [ticket:14296#comment:143193 RyanGlScott]:

<SNIP>

But it's easy to subvert this with your proposed Lift Exp instance, since you can have, e.g.:

uhOh :: Exp
uhOh = lift "uhOh"

You mean

uhOh :: ExpQ
uhOh = lift "uhOh"

Now $(lift uhOh) won't be an Exp, but rather a String. This is not at all what we want.

Totally agree. My question is when this happens in a [p|($uhOh -> binding)|] and this ends up in a splice, ultimately being compiled by GHC, then I'll get a type error "Expected Exp, got: String", correct?

Replying to [ticket:14296#comment:143178 heisenbug]:

What about the derivation mechanism for Lift instances? Will it do the right thing in this case too?

Right. Here is an except of the -ddump-deriv output from deriving a Lift instance for Exp:

deriving instance Lift Exp

===>

instance Lift Exp where
lift (VarE a) = conE 'VarE `appE` lift a
lift (ConE a) = conE 'ConE `appE` lift a
lift (AppE f x) = conE 'AppE `appE` lift f `appE` lift x
...

Now calling lift on an Exp will produce an ExpQ that represents an Exp value. It's quite meta, granted, but that's how it should be :)

That's good. Thanks!

Replying to [ticket:14296#comment:143195 heisenbug]:

You mean

uhOh :: ExpQ
uhOh = lift "uhOh"

Oops. That's right.

My question is when this happens in a [p|($uhOh -> binding)|] and this ends up in a splice, ultimately being compiled by GHC, then I'll get a type error "Expected Exp, got: String", correct?

Sure, GHC will definitely catch the mistake in the form of a (sometimes hard-to-scrutinize) type error. But I would still be frustrated that that happened in the first place, since it would violate my intuition of how lift interacts with splicing.

closed

I've added a Diff for documenting this Lift law in D4050.

Since we seem to both be in agreement that deriving Lift for Exp is the better way to go, I'll close this in favor of #14030 (closed).

Trac metadata

Trac field	Value
Resolution	Unresolved → ResolvedDuplicate

mentioned in commit 626f0454

added error messages label

added Pnormal label

mentioned in commit 82e2a9e8

mentioned in merge request !12858 (closed)

mentioned in commit 5c975702

mentioned in commit 3c4307bd

mentioned in commit 4ee6eb87

mentioned in commit 0487e457

mentioned in commit 79b15a43

mentioned in commit cf983566

mentioned in commit 90eb495b

mentioned in commit 42fdf7f0

mentioned in commit 223aedd6

mentioned in commit 1da14215

mentioned in commit 4e1b3ea5

mentioned in commit a82770d7

mentioned in commit 7eeae9e0

mentioned in commit bff20301

mentioned in commit e9d6b306

mentioned in commit b426344a

mentioned in commit d0e3f1d9

mentioned in commit 59ea726a

mentioned in commit 88ec3c24

mentioned in commit adb6b199

mentioned in commit 33fee6a2