[GHC] #10823: Don't mark functions with annotations as dead (was: Expose keepAlive to Template Haskell)

[GHC]

#10823: Don't mark functions with annotations as dead
-------------------------------------+-------------------------------------
        Reporter:  spinda            |                   Owner:
            Type:  feature request   |                  Status:  new
        Priority:  normal            |               Milestone:  7.12.1
       Component:  Template Haskell  |                 Version:  7.10.2
      Resolution:                    |                Keywords:
Operating System:  Unknown/Multiple  |            Architecture:
                                     |  Unknown/Multiple
 Type of failure:  None/Unknown      |               Test Case:
      Blocked By:                    |                Blocking:
 Related Tickets:                    |  Differential Revisions:
-------------------------------------+-------------------------------------

Old description:

> {{{keepAlive}}} is a
> [https://github.com/ghc/ghc/blob/efa7b3a474bc373201ab145c129262a73c86f959/compiler/typecheck/TcRnMonad.hs#L1276
> function in TcRnMonad] that adds a {{{Name}}} to the set of {{{Name}}}s
> to keep when pruning out dead code.
>
> A concrete use case for exposing this to Template Haskell is in
> LiquidHaskell, which will soon function as a Core plugin. In
> LiquidHaskell, a subset of Haskell functions can be "lifted" to the logic
> level and used in types. For example:
>
> {{{
> module Test (ok) where
>
> [lq| inline gt |]
> gt x y = x > y
>
> [lq| ok :: x:Int -> { v:Int | gt x v } |]
> ok x = x + 1
> }}}
>
> LiquidHaskell runs a transformation from the {{{CoreBind}}} for {{{gt}}}
> to its internal representation of decidable logic. Since Core plugins are
> run after "dead" code is removed at the end of desugaring, and since
> {{{gt}}} is not exported, the {{{CoreBind}}} for {{{gt}}} would not reach
> the {{{CoreBinds}}} LH receives as a Core plugin.
>
> The solution for this is to be able to mark names with {{{keepAlive}}}
> from Template Haskell.
>
> Proposed specification:
>
> {{{
> keepAlive :: Name -> Q ()
> }}}
>
> where {{{Name}}} is a Template Haskell {{{Name}}}.

New description:

 A concrete example is in LiquidHaskell, which will soon function as a Core
 plugin. In LiquidHaskell, a subset of Haskell functions can be "lifted" to
 the logic level and used in types. For example:

 {{{
 module Test (ok) where

 [lq| inline gt |]
 gt x y = x > y

 [lq| ok :: x:Int -> { v:Int | gt x v } |]
 ok x = x + 1
 }}}

 {{{[lq| inline gt |]}}} generates an annotation on {{{gt}}}, which
 LiquidHaskell picks up at the plugin stage. It then tries to run a
 transformation from the {{{CoreBind}}} for {{{gt}}} to its internal
 representation of decidable logic. But since Core plugins are run after
 "dead" code is removed at the end of desugaring, and since {{{gt}}} is not
 exported, the {{{CoreBind}}} for {{{gt}}} does not reach the
 {{{CoreBinds}}} LH receives as a Core plugin.

 The solution for this is to prevent the desugarer from discarding
 {{{CoreBinds}}} for things with attached annotations.

--

Comment (by spinda):

 Agreed. Except that this is depending on a guaranteed, stable, documented
 feature: that all instance are always exported from a module. Thus if a
 definition is mentioned in an instance, GHC will never drop it. So this
 isn't a TH hack so much, but a GHC language hack.

 Good point. Although, I think "instance are always exported from a module"
 may not be 100% true in the presence of Backpack, but it should be true
 enough for this to continue to work.

      This is much better. Care to repurpose the ticket?

 Done. The fix for the new issue should be much easier to implement anyway.

--
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/10823#comment:6>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler