CPR for constructors with existentials
Motivation
Consider the following two functions:
{-# LANGUAGE GADTs #-}
{-# LANGUAGE UnboxedSums #-}
module Lib where
data Ex where
Ex :: a -> Ex
data Box a where
Box :: a -> Box a
f :: Int -> Ex
f n = case sum [1..n] of m -> Ex m
{-# NOINLINE f #-}
g :: Int -> Box Int
g n = case sum [1..n] of m -> Box m
{-# NOINLINE g #-}
If you look at the optimised Core, you'll see that g
was worker/wrappered to expose the Box
constructor, while f
was not. consequently, call sites can't cancel away the Ex
constructor.
I don't see why we can't do this transformation, with a little help from unboxed sums in the general case (although we probably want CPR for sums first, which in turn depends on Nested CPR...).
Proposal
Make CPR recognise non-vanilla constructed products (let's focus on existentials in this ticket): Group construction sites by how they instantiate existential type parameters. Each of these groups becomes an alternative in the unboxed sum constructed by WW. Example
{-# LANGUAGE GADTs #-}
{-# LANGUAGE UnboxedSums #-}
{-# LANGUAGE TypeApplications #-}
module Lib where
data Ex where
Ex :: a -> Ex
f :: Int -> Ex
f n = case sum [1..n] of
0 -> Ex @Bool True
1 -> Ex @Char 'a'
2 -> Ex @Char 'b'
m -> Ex @Int m
{-# NOINLINE f #-}
fwork :: Int -> (# Bool | Char | Int #)
fwork n = case sum [1..n] of
0 -> (# True | | #)
1 -> (# | 'a' | #)
2 -> (# | 'b' | #)
m -> (# | | m #)
fwrap :: Int -> Ex
fwrap n = fwork n of
(# b | | #) -> Ex b
(# | c | #) -> Ex c
(# | | m #) -> Ex m
Where fwrap
is the wrapper of f
after optimisations. Note how there are only 3 alternatives in the sum because Ex
was instantiated at Char
twice.