As versões modernas do GHC têm algum tipo de apagamento de prova?

Suponha que eu tenha um parâmetro que exista apenas para o benefício do sistema de tipos, por exemplo, como neste pequeno programa:

{-# 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

Os argumentos e membros do Proxy na estrutura realmente precisam existir no momento da compilação para ajudar na verificação de tipo enquanto mantêm o MyPoly polimórfico (nesse caso, o programa será compilado sem ele, mas este exemplo artificial é um problema mais geral em que existem provas ou proxies necessários apenas em tempo de compilação) - existe apenas um construtor para Proxy, e o argumento type é um tipo fantasma.

Compilar com ghc with -ddump-stgmostra que, pelo menos no estágio STG, não há apagamento do argumento Proxy para o construtor ou o terceiro argumento para o construtor.

Existe alguma maneira de marcá-las como sendo apenas em tempo de compilação ou de outra forma ajudar o ghc a apagar provas e excluí-las?

De fato, seu código leva a que Proxys sejam armazenados no construtor:

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

No entanto, com uma pequena alteração, obtemos a otimização desejada. Não mais Proxy!

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

O que eu fiz? Eu fiz o Proxycampo estrito :

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

Em geral, não podemos apagar proxies não estritos por causa dos fundos. Proxye undefinedsão do tipo Proxy amas não são observacionalmente equivalentes; portanto, precisamos distingui-los em tempo de execução.

Em vez disso, um rigoroso Proxytem apenas um valor, portanto o GHC pode otimizar isso.

Não há recurso semelhante para otimizar um parâmetro de função (não construtor). Seu campo (Proxy a -> a -> Int -> Int)exigirá um Proxyem tempo de execução.

Existem duas maneiras de realizar o que você deseja.

A maneira um pouco mais antiga é usar o Proxy # do GHC.Prim, que é garantido que será apagado em tempo de compilação.

{-# 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 (\_ -> (+))]

Embora isso seja um pouco complicado.

A outra maneira é renunciar Proxycompletamente:

{-# 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

Atualmente, temos algumas ferramentas que facilitam o trabalho sem Proxy: extensões como AllowAmbiguousTypese TypeApplications, por exemplo, significam que você pode aplicar o tipo que você quer dizer diretamente. Não sei qual é o seu caso de uso, mas tome este exemplo (artificial):

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"

Queremos ler e mostrar um valor de algum tipo, portanto, precisamos de uma maneira de indicar qual é o tipo real. Veja como você faria isso com extensões:

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

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

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