Elide empty dictionaries

Suppose you define a type class C with no methods, and use it as a constraint on a function f :: C => Foo. GHC's generated Core for f currently passes an empty dictionary for C. With optimizations, it seems to be true that at use sites, calls to f will be replaced with calls to an inner function that skips the typeclass dictionary. But can I count on this optimization always working?

Would it possible to get a guarantee that the C => constraint will have no run-time overhead, by dropping it entirely from the generated Core? Or is there a subtlety that prevents this from being sound?

For context, I would like to implicitly pass compile-time evidence that various properties hold (e.g. such-and-such a list is non-empty), while retaining a guarantee that the evidence will have no run-time cost. Like this:

newtype Named a name = Named a

class Fact p

-- Ideally, we'd have a guarantee that the following function
--   compiles to exactly the same code as `Prelude.head`
head :: Fact (IsCons xs) => ([a] `Named` xs) -> a
head xs = Prelude.head (coerce xs)

changed milestone to %8.6.1

changed weight to 5

added Tfeature request Trac import labels

changed the description

See discussion in goldfire's "Constrained Type Families", subsection **7.3 Runtime Efficiency**

Constrained type families may also seem to have a non-trivial efficiency impact. For a simple example, suppose we have a type family F, and consider an existentially-packaged type family application:

data FPack a where
FPack :: F a -> FPack a

We might expect an FPack a value to contain exactly a value of type F a. With constrained type families, however, the declaration above would be incorrect; we would need to add a predicate for its constraining class, say C:

data FPack1 a where
FPack1 :: C a => F a -> FPack1 a

Now, a value of type FPack1 a does not just contain an F a value, but must also carry a C a dictionary, and uses of FPack1 will be responsible for constructing, packing, and unpacking these dictionaries. Over sufficiently many uses of FPack1, this additional cost could be noticeable.

This efficiency impact can be mitigated, however. This issue can crop up only when we have a value of type F a (or other type family application) without an instance of the associated class C a. But in order for the value of type F a to be useful, parametricity tells us that C a, or some other class with a similar structure to the equations for F a must be in scope. Barring this, it must be that F a is used as a phantom type. In this case, we would want a “phantom dictionary” for C a, closely paralleling existing work on proof irrelevance in the dependently-typed programming community (..): the C a dictionary essentially represents a proof that will never be examined. While we do not propose here a new solution to this problem, we believe that existing work will be applicable in our case as well.

In Core, an empty dictionary turns into a dead variable, which is optimised away (with -O anyway).

But it'll still take up a field in FPack1. Reason: it might be bottom.

I'd be surprised if you found any appreciable performance impact.

added Pnormal label

mentioned in issue #19275

marked this issue as related to #20418