Type system information for statically known data size

[mgsloan]

It would be really cool to have compiletime info about datatype size. This has the potential to make both the generics and TH derivations more efficient. Certainly for TH it would cause the compiler to do less overall work. It'd also allow us to use functions that demand ConstSize and have them fail statically. This way the user can't accidentally make their values VarSize (can be much less efficient).

We might need to use some TH hacks to reify runtime Storable info as compiletime type info.

I'm imagining something like the following, using type nats, data kinds, and type families:

-- Can I use Nat here?  You know what I mean.
data StaticSize = KnownSize Nat | UnknownSize

class Store a where
    type StoreSize :: a -> StaticSize
    type StoreSize a = UnknownSize
    -- ...

type instance StoreSize () = 'KnownSize 0
type instance StoreSize Int32 = 'KnownSize 4
-- etc

Probably good to have it as an associated type family, so that it can be given the default of

We'd also likely want the Size a type be a GADT that enforces that ConstSize is yielded when StoreSize a ~ KnownSize n. Marking this "breaking change" as such.

[nfrisby]

I came here to open this same Issue and fortunately found yours first. My motivation is to be able to use the type-checker to ensure that some serialization uses the more efficient ConstSize path.

I suggest the following.

type family StoreConstSize a :: Maybe Nat

data Size :: * -> * where
  ConstSize :: (StoreConstSize a ~ 'Just n,KnownNat n) => Proxy# n -> Size a
  VarSize :: (StoreConstSize a ~ 'Nothing) => !(a -> Int) -> Size a

Though I'm worried that KnownNat essentially being Integer may cost performance. Thus, the following ought to be a better performing middle-ground.

type family StoreConstSize a :: Bool

data Size :: * -> * where
  ConstSize :: (StoreConstSize a ~ 'True) => !Int -> Size a
  VarSize :: (StoreConstSize a ~ 'False) => !(a -> Int) -> Size a

And last, I'm not sure how the pattern exhaustiveness checker will handle the new Size. If it's troublesome, you may want to consider a route using a data family for Size instead of a GADT.