How many fields does it take to break defprod?  Hint: you already know the answer.  42!

Why is this?  Suppose you have the following forms:

(include-book "centaur/fty/deftypes" :dir :system)
(fty::defprod slow-it-down
 ((a booleanp) (b booleanp) (c booleanp) (d booleanp) (e booleanp)
 (f booleanp) (g booleanp) (h booleanp) (i booleanp) (j booleanp)
 (k booleanp) (l booleanp) (m booleanp) (n booleanp) (o booleanp)
 (p booleanp) (q booleanp) (r booleanp) (s booleanp) (tt booleanp)
 (u booleanp) (v booleanp) (w booleanp) (xx booleanp) (y booleanp)
 (z booleanp) (aa booleanp) (ab booleanp) (ac booleanp) (ad booleanp)
 (ae booleanp) (af booleanp) (ag booleanp) (ah booleanp) (ai booleanp)
 (aj booleanp) (ak booleanp) (al booleanp) (am booleanp) (an booleanp)
 (ao booleanp) (ap booleanp)
 (aq booleanp) ;; the offending threshold
 ))

As of May 16, 2016, you’ll get a nice error that says the preprocessor’s rewrite stack has reached its limit and quit:

HARD ACL2 ERROR in PREPROCESS: The call depth limit of 1000 has been
exceeded in the ACL2 preprocessor (a sort of rewriter). There is probably
a loop caused by some set of enabled simple rules.

But there are no such looping rules (that I found).  This is evident by the error going away (and an analogous proof completes over a weekend in 130,000 seconds — hah!).

You might think it clever to disable the preprocessor.  That _might_ work, but there are three difficulties with that:

1. There isn’t any published way to disable the preprocessor at the top-level (there may not be any), and we’re deep inside defprod
2. Modifying defprod not to call the preprocessor in just the right place could break  other uses of defprod
3. The subgoal generated when you do disable the preprocessor looks a lot like something a preprocessor could be good at (though, I suspect that in ACL2 we need generalization):

   (IMPLIES
    (AND
     (ALISTP X)
     (CONSP X)
     (CONSP (CDR X))
     (CONSP (CDDR X))
     (CONSP (CDDDR X))
     (CONSP (CDDDDR X))
     (CONSP (CDR (CDDDDR X)))
     (CONSP (CDDR (CDDDDR X)))
     (CONSP (CDDDR (CDDDDR X)))
     (CONSP (CDDDDR (CDDDDR X)))
     ...)
    (EQUAL (LIST (CONS 'B (<booleanp-fix> (CDR (CAR X))))
                 (CONS 'C (<booleanp-fix> (CDR (CADR X)))))
           X))

With what solution did I end up?