Our current approach (using integers) was simple, but it was erasing lots of information. For example 0 could mean that we're taking a first element of a product type, but it could also mean that we're unwrapping a newtype. This change adds an ADT to start distinguishing between a few different kinds of projections, namely: product projections and two flavors of newtype projections: base and compound newtype unwraps. The difference between them is pretty arbitrary and corresponds to what the newtype erasure pass will eliminate (only compound newtypes). The set of base newtype is small and currently is only Nat and Fin.
Our current approach (using integers) was simple, but it was erasing lots of information. For example 0 could mean that we're taking a first element of a product type, but it could also mean that we're unwrapping a newtype. This change adds an ADT to start distinguishing between a few different kinds of projections, namely: product projections and two flavors of newtype projections: base and compound newtype unwraps. The difference between them is pretty arbitrary and corresponds to what the newtype erasure pass will eliminate (only compound newtypes). The set of base newtype is small and currently is only
NatandFin.