Do modern GHC versions have any kind of proof erasure?

Question

Suppose I have a parameter that exists only for the benefit of the type system, for example as in this small program:

{-# LANGUAGE GADTs #-}
module Main where
import Data.Proxy
import Data.List

data MyPoly where
  MyConstr :: Proxy a -> a -> (Proxy a -> a -> Int -> Int) -> MyPoly

listOfPolys :: [MyPoly]
listOfPolys = [MyConstr Proxy 5 (const (+))
              , MyConstr Proxy 10 (const (+))
              , MyConstr Proxy 15 (const (+))]

main = print $ foldl' (\v (MyConstr p n a) -> a p n v) 0 listOfPolys

The Proxy arguments and members in the structure only really need to exist at compile time to help with type checking while maintaining the polymorphic MyPoly (in this case, the program will compile without it, but this contrived example is a more general problem where there are proofs or proxies that are only needed at compile time) - there is only one constructor for Proxy, and the type argument is a phantom type.

Compiling with ghc with -ddump-stg shows that at least at the STG stage, there is no erasure of the Proxy argument to the constructor or the third argument to the constructor.

Is there any way to mark these as being compile-time only, or otherwise help ghc to do proof erasure and exclude them?

Answer 1

Indeed, your code does lead to Proxys being stored in the constructor:

ProxyOpt.listOfPolys8 :: ProxyOpt.MyPoly
[GblId, Caf=NoCafRefs, Unf=OtherCon []] =
    CCS_DONT_CARE ProxyOpt.MyConstr! [Data.Proxy.Proxy
                                      ProxyOpt.listOfPolys9
                                      ProxyOpt.listOfPolys4];

However, with a small change, we get the wanted optimization. No more Proxy!

ProxyOpt.listOfPolys8 :: ProxyOpt.MyPoly
[GblId, Caf=NoCafRefs, Unf=OtherCon []] =
    CCS_DONT_CARE ProxyOpt.MyConstr! [ProxyOpt.listOfPolys9
                                      ProxyOpt.listOfPolys4];

What did I do? I made the Proxy field strict:

data MyPoly where
  MyConstr :: !(Proxy a) -> a -> (Proxy a -> a -> Int -> Int) -> MyPoly
           -- ^ --

In general, we can't erase non-strict proxies because of bottoms. Proxy and undefined are both of type Proxy a but they are not observationally equivalent, so we have to distinguish them at runtime.

Instead, a strict Proxy only has one value, so GHC can optimize that away.

There's no similar feature to optimize away a (non-constructor) function parameter, though. Your field (Proxy a -> a -> Int -> Int) will require a Proxy at runtime.

Answer 2

There are two ways to accomplish what you want.

The slightly older way is to use Proxy# from GHC.Prim, which is guaranteed to be erased at compile-time.

{-# LANGUAGE GADTs, MagicHash #-}
module Main where

import Data.List
import GHC.Prim

data MyPoly where
  MyConstr :: Proxy# a -> a -> (Proxy# a -> a -> Int -> Int) -> MyPoly

listOfPolys :: [MyPoly]
listOfPolys = [MyConstr proxy# 5 (\_ -> (+))
              , MyConstr proxy# 10 (\_ -> (+))
              , MyConstr proxy# 15 (\_ -> (+))]

Although this is a little cumbersome.

The other way is to forgo the Proxy altogether:

{-# LANGUAGE GADTs #-}

module Main where

import Data.List

data MyPoly where
  MyConstr :: a -> (a -> Int -> Int) -> MyPoly

listOfPolys :: [MyPoly]
listOfPolys = [ MyConstr 5  (+)
              , MyConstr 10 (+)
              , MyConstr 15 (+)
              ]

main = print $ foldl' (\v (MyConstr n a) -> a n v) 0 listOfPolys

Nowadays, we have some tools which make it easier to work without Proxy: extensions like AllowAmbiguousTypes and TypeApplications, for instance, mean that you can apply the type you mean directly. I don't know what your use-case is, but take this (contrived) example:

import Data.Proxy

asTypeP :: a -> Proxy a -> a
asTypeP x _ = x

readShow :: (Read a, Show a) => Proxy a -> String -> String
readShow p x = show (read x `asTypeP` p)

>>> readShow (Proxy :: Proxy Int) "01"
"1"

We want to read and then show a value of some type, so we need a way to indicate what the actual type is. Here's how you'd do it with extensions:

{-# LANGUAGE AllowAmbiguousTypes, TypeApplications, ScopedTypeVariables #-}

readShow :: forall a. (Read a, Show a) => String -> String
readShow x = show (read x :: a)

>>> readShow @Int "01"
"1"