title: Can I compute a type's cardinality generically?
body: <p>I'd like to have a type class that tells me how big various types are.</p>
  <pre><code>data Cardinality = Finite Natural | Infinite
  class Sized a where cardinality :: Cardinality
  </code></pre>
  <p>It's pretty straightforward to write instances; for example:</p>
  <pre><code>instance Sized Void where cardinality = Finite 0
  instance Sized ()   where cardinality = Finite 1
  instance Sized Bool where cardinality = Finite 2
  
  instance Sized a =&gt; Sized [a] where
      cardinality = case cardinality @a of
          Finite 0 -&gt; Finite 1
          _ -&gt; Infinite
  
  data X = X Y
  data Y = Y X X
  instance Sized X where cardinality = Finite 1
  instance Sized Y where cardinality = Finite 1
  </code></pre>
  <p>In fact, it's so straightforward, it feels like it ought to be automatable. Perhaps generic programming will help?</p>
  <pre><code>class GSized f where gcardinality :: Cardinality
  class Sized a where
      cardinality :: Cardinality
      default cardinality :: (Generic a, GSized (Rep a)) =&gt; Cardinality
      cardinality = gcardinality @(Rep a)
  </code></pre>
  <p>Most of the instances are pretty straightforward:</p>
  <pre><code>instance GSized V1 where gcardinality = Finite 0
  instance GSized U1 where gcardinality = Finite 1
  instance GSized f =&gt; GSized (M1 i c f) where gcardinality = gcardinality @f
  instance (GSized f, GSized g) =&gt; GSized (f :+: g) where
      gcardinality = case (gcardinality @f, gcardinality @g) of
           (Finite n, Finite n') -&gt; Finite (n+n')
           _ -&gt; Infinite
  instance (GSized f, GSized g) =&gt; GSized (f :*: g) where
      gcardinality = case (gcardinality @f, gcardinality @g) of
          (Finite 0, _) -&gt; Finite 0
          (_, Finite 0) -&gt; Finite 0
          (Finite n, Finite n') -&gt; Finite (n*n')
          _ -&gt; Infinite
  </code></pre>
  <p>But then I get stuck. The straightforward thing for individual fields certainly doesn't work:</p>
  <pre><code>instance Sized c =&gt; GSized (K1 i c) where
      gcardinality = cardinality @c
  </code></pre>
  <p>For recursive types, this is a very straightforward infinite loop. I've tried a variety of means of enriching the two classes involved here.</p>
  <ul>
  <li>I generalized <code>cardinality</code> and <code>gcardinality</code> to be functions, so that I could assume I already knew the size of recursive occurrences. Then in the <code>K1</code> instance I could ask: if all your recursive instances were uninhabited, how big would you be? What if all your recursive instances had one inhabitant? And so on.</li>
  <li>I generalized from a single cardinality to a &quot;recurrence relation&quot; like <code>x = a + bx</code>. The intended meaning of <code>x = a + bx</code> is that the type <code>x</code> has <code>a</code> inhabitants that don't involve recursion at all, and <code>b</code> values that can be paired up with a recursive call. (We can define <code>x*x = x</code> without losing anything of interest.) Then equations like <code>x = n + 0x</code> correspond to enumerations, <code>x = 0 + x</code> correspond to trivial 1-element recursive types, and <code>x = a + bx</code> are infinite.</li>
  <li>I used lazy naturals instead of efficient ones.</li>
  <li>I tracked sets of possible cardinalities, ruling them out one by one as new information was learned.</li>
  <li>I took a stab at using <code>Generic1</code> instead of <code>Generic</code>.</li>
  </ul>
  <p>None of these ended up working well. There seem to be three core, hard problems/failure modes:</p>
  <ul>
  <li>A loop in the <code>K1</code> definition for recursive types, or it works okay for recursive types but falls over for mutually recursive types.</li>
  <li><code>K1</code> is used both for recursive occurrences and plain fields, and there doesn't seem to be an easy way to distinguish between these.</li>
  <li>Choosing <code>Finite 0</code> instead of <code>Finite 1</code> for trivially recursive types.</li>
  </ul>
  <p>Is there an approach that solves these problems? Where the generic instances for <code>[Void]</code>, <code>[()]</code>, <code>X</code>, and <code>Y</code> from above are all defined and correct?</p>