#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:
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.
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. ---- Minimal example (without TH): {{{ module AnnTest (thing) where {-# ANN thing False #-} thing :: Int thing = 7 }}} {{{ ➜ ghc -O0 -ddump-simpl AnnTest.hs [1 of 1] Compiling AnnTest ( AnnTest.hs, AnnTest.o ) ==================== Simplified expression ==================== GHC.Desugar.toAnnotationWrapper @ GHC.Types.Bool Data.Data.$fDataBool GHC.Types.False ==================== Tidy Core ==================== Result size of Tidy Core = {terms: 3, types: 1, coercions: 0} thing :: Int [GblId, Caf=NoCafRefs, Str=DmdType] thing = GHC.Types.I# 7 }}} {{{ module AnnTest () where {-# ANN thing False #-} thing :: Int thing = 7 }}} {{{ ➜ ghc -O0 -ddump-simpl AnnTest.hs [1 of 1] Compiling AnnTest ( AnnTest.hs, AnnTest.o ) ==================== Simplified expression ==================== GHC.Desugar.toAnnotationWrapper @ GHC.Types.Bool Data.Data.$fDataBool GHC.Types.False ==================== Tidy Core ==================== Result size of Tidy Core = {terms: 0, types: 0, coercions: 0} }}} -- Comment (by spinda): Yes, it can be reproduced without TH. Minimal example attached to the ticket description. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10823#comment:10 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler