[ghc-steering-committee] Proposal #209: Levity polymorphic lift. Recommendation: accept

[Eric Seidel]

On Tue, Mar 5, 2019, at 16:15, Richard Eisenberg wrote:
> 
> Is it possible to write liftTyped in a generic way, like the way the 
> old lift had a generic default? That might solve all the problems at 
> once.

The old lift's default is

  default lift :: Data t => t -> Q Exp
  lift = liftData

I imagine we could get away with

  default liftTyped :: (r ~ 'LiftedRep, Data t) => t -> Q (TExp t)
  liftTyped = unsafeTExpCoerce . liftData

which would be no less unsafe than what is currently proposed as the default implementation. In which case, we could give both lift and liftTyped generic defaults, which would provide a seamless migration for code with and empty Lift instance.

Ah, but unfortunately this fails to typecheck with the following error.

    • Expected a type, but ‘t’ has kind ‘TYPE r’
    • In the first argument of ‘Data’, namely ‘t’
      In the type signature:
        liftTyped :: forall r (t :: TYPE r).
                     (r ~  'LiftedRep, Data t) => t -> Q (TExp t)

I'm a bit perplexed by this error actually. GHC rightly wants `t` to be a proper type, ie `TYPE LiftedRep`. Instead we have that `t` is a `TYPE r` where `r ~ LiftedRep`. Is there a technical reason GHC can't deduce that `t :: Type` here?