Skip to content

Don't mark functions with annotations as dead

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}
Edited by spinda
To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information