[GHC] #10823: Expose keepAlive to Template Haskell

newer
[GHC] #13225: Fannkuch-redux time...

GHC

1 Sep 2015 1 Sep '15

6:21 p.m.

#10823: Expose keepAlive to Template Haskell -------------------------------------+------------------------------------- Reporter: spinda | Owner: Type: feature | Status: new request | Priority: normal | Milestone: Component: Compiler | Version: 7.10.2 Keywords: | Operating System: Unknown/Multiple Architecture: | Type of failure: None/Unknown Unknown/Multiple | Test Case: | Blocked By: Blocking: | Related Tickets: Differential Revisions: | -------------------------------------+------------------------------------- {{{keepAlive}}} is a [https://github.com/ghc/ghc/blob/efa7b3a474bc373201ab145c129262a73c86f959/com... 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}}}. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10823 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

Show replies by date

GHC

1 Sep 1 Sep

6:22 p.m.

GHC

2 Sep 2 Sep

9:25 p.m.

#10823: Expose keepAlive to Template Haskell -------------------------------------+------------------------------------- Reporter: spinda | Owner: Type: feature request | Status: new Priority: normal | Milestone: 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: -------------------------------------+------------------------------------- Comment (by goldfire): It's a bit of a hack, but there's a workaround here. Define this in some available module: {{{ data Anything = forall a. Mk a class KeepAlive (what :: Symbol) where whatToKeep :: proxy what -> Anything }}} And then generate this using existing TH: {{{ instance KeepAlive "gt" where whatToKeep _ = Mk gt }}} Then GHC will mark `gt` as used. This is ugly, but it should work well in practice. In the effort to keep TH from bloating too much, I would lean against adding new features to support operations that can be simulated well today. Feel free to try to convince me otherwise -- I'm not dead set in this position. But I'm worried about feature creep here. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10823#comment:2 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

GHC

9:26 p.m.

GHC

9:57 p.m.

#10823: Expose keepAlive to Template Haskell -------------------------------------+------------------------------------- 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: -------------------------------------+------------------------------------- Comment (by spinda): Is the use of type-level literals essential here? That requires the user to have {{{DataKinds}}} enabled. Otherwise, the hack can fill our use case, I think. On the other hand, I worry about Template Haskell code having to depend too much on tricks that happen to work but aren't a guaranteed, stable, documented part of the interface. See, for example, the issue with quasiquoter behavior that appeared in #10047: suddenly, the "trick" that quasiquoters didn't split declaration groups went away, because it wasn't part of the actual spec. By contrast, functionality exposed through an explicit piece of the Template Haskell API will not suddenly disappear as a consequence of a tangential patch. //That said//, as I write this, I've realized that there may be another way to approach our particular issue. {{{[lq| inline gt |]}}} attaches an annotation to {{{gt}}}, so perhaps the solution should be to tell the desugarer not to consider any function with an annotation attached as dead code. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10823#comment:4 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

GHC

3 Sep 3 Sep

7:05 a.m.

...

Is the use of type-level literals essential here? That requires the user to have {{{DataKinds}}} enabled. Otherwise, the hack can fill our use case, I think.

No. It's just a convenient way to make sure that the instance head is unique. Any such mechanism should work.

...

On the other hand, I worry about Template Haskell code having to depend

too much on tricks that happen to work but aren't a guaranteed, stable, documented part of the interface. 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.

...

//That said//, as I write this, I've realized that there may be another way to approach our particular issue. {{{[lq| inline gt |]}}} attaches an annotation to {{{gt}}}, so perhaps the solution should be to tell the desugarer not to consider any function with an annotation attached as dead code.

This is ''much'' better. Care to repurpose the ticket? -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10823#comment:5 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

GHC

7:17 a.m.

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

...

{{{keepAlive}}} is a [https://github.com/ghc/ghc/blob/efa7b3a474bc373201ab145c129262a73c86f959/com... 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