Opened 2 years ago

Closed 2 years ago

Last modified 2 years ago

#14296 closed feature request (duplicate)

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

Reported by: heisenbug Owned by:
Priority: normal Milestone:
Component: Template Haskell Version: 8.2.1
Keywords: Cc:
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: Poor/confusing error message Test Case:
Blocked By: Blocking:
Related Tickets: #14030 Differential Rev(s):
Wiki Page:

Description

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).

Change History (8)

comment:1 Changed 2 years ago by RyanGlScott

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

comment:2 Changed 2 years ago by 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.)

comment:3 in reply to:  2 ; Changed 2 years ago by heisenbug

Replying to 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!

comment:4 in reply to:  3 ; Changed 2 years ago by RyanGlScott

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

comment:5 in reply to:  4 ; Changed 2 years ago by heisenbug

Replying to 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 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!

comment:6 in reply to:  5 Changed 2 years ago by RyanGlScott

Replying to 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.

comment:7 Changed 2 years ago by RyanGlScott

Resolution: duplicate
Status: newclosed

I've added a Diff for documenting this Lift law in Phab: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.

comment:8 Changed 2 years ago by Ben Gamari <ben@…>

In 626f045/ghc:

Document a law for TH's Lift class

Inspired by the discussion in #14296, I've decided to
document a law which is usually in the back of my mind when I'm using
Template Haskell's `Lift` class, but isn't formally stated anywhere.
That is, every `Lift` instance should satisfy (for all `x`):

```lang=haskell
$(lift x) == x
```

Test Plan: Read it

Reviewers: austin, goldfire, bgamari

Subscribers: rwbarton, thomie

Differential Revision: https://phabricator.haskell.org/D4050
Note: See TracTickets for help on using tickets.