Avoid retaining datatypes in PIR which are used only at the type level

[michaelpj]

We currently retain datatypes which are used only at the type level, including their constructors, matchers, and datatypes which they depend on.

This is true even if the datatype is mentioned only as the type of an ignored argument, for example. It would be nice not to do that: as a crude measure, we could replace them with any made up type with the same kind.

---

Example (in pseudo-PIR):

let datatype (Maybe :: Type -> Type) [a :: Type] match_Maybe [Just :: a -> Maybe a, Nothing :: Maybe a]
in \(x :: Maybe Integer) -> \(y :: Integer) -> y

Here Maybe appears only at the type level. We would like to get rid of as much of Maybe as we can (in particular, that will then lead to cascading opportunities to get rid of other stuff), but we do want to keep the program typechecking.

My idea is to replace Maybe with a simple made-up type of kind Type -> Type. In this case we can use a trivial type-lambda:

let Maybe :: Type -> Type = \(t :: Type) -> t
in \(x :: Maybe Integer) -> \(y :: Integer) -> y

More generally, datatypes are going to tend to have types that look like a tree of (->)s with leaves of kind Type. It should be pretty easy to generate a "simple" type of the same kind just using type lambdas.

Then we just replace the datatype binding for Maybe with a simple type binding with the new made-up type, and dead-code elimination should do the rest.

---

Working out which types are only retained in this way may be a bit annoying: the dead code analysis has no notion of "provenance". And we don't want to treat these as "dead", rather we need to identify them separately. Possibly the thing to do would be to run the dead code analysis again in a separate mode that ignores dependencies from terms to types, and then just look at what datatypes look "dead" in that analysis. Or maybe we could do something cleverer.

[michaelpj]

Working out which types are only retained in this way may be a bit annoying

I was overthinking this. If we fixup the dependency analysis for datatypes as discussed in #4148, then we get a fairly simple algorithm:

• If the datatype type itself, its matcher, and all its constructors are dead, then remove the whole thing.
• If the matcher and constructors are dead, but the datatype is not dead, then replace it with a fake type.

The second option is effectively a more dramatic version of #4148 that lets us get rid of the matcher too.

[michaelpj]

Note that this does not have the problem mentioned in #4148 (comment). Since we are only changing the type level, and we erase programs, this really is safe.