constraints icon indicating copy to clipboard operation
constraints copied to clipboard

instance Lift (Dict cls)

Open Icelandjack opened this issue 5 years ago • 2 comments

Hope it's going well, do we want lift instances for Dict here?

instance Lift (Dict cls) where
 lift :: Dict cls -> Q Exp
 lift Dict = [| Dict |]

 liftTyped :: Dict cls -> Q (TExp (Dict cls))
 liftTyped Dict = [|| Dict ||]

Can it be given for a :- b?

instance Lift (a :- b) where
 lift (a :- b) -> Q Exp
 lift ..

 liftTyped :: (a :- b) -> Q (TExp (a :- b))
 liftTyped (Sub dict) = [|| Sub _ ||]

Icelandjack avatar Dec 13 '19 16:12 Icelandjack

Sounds reasonable to me. Care to make a pull request?

Can it be given for a :- b?

Sure, you could do this:

instance Lift (a :- b) where
  lift :: a :- b -> Q Exp
  lift d = [| Sub (Dict \\ d) |]

  liftTyped :: a :- b -> Q (TExp (a :- b))
  liftTyped d = [|| Sub (Dict \\ d) ||]

RyanGlScott avatar Dec 16 '19 20:12 RyanGlScott

On the other hand, @mpickering reminds me that if these instances were to be defined, they would have to be used with care, as today's typed Template Haskell is unsound. For instance, here is an example of unsoundness that can result from splicing in Dict:

f :: a => Q (TExp (Dict a))
f = liftTyped Dict
g :: a => Dict a
g = $$f
error:
    • Could not deduce: a arising from a use of ‘f’
    • In the expression: f
      In the Template Haskell splice $$f
      In the expression: $$f
    • Relevant bindings include g :: Dict a
   |
   | g = $$f
   |       ^

RyanGlScott avatar May 31 '20 11:05 RyanGlScott