# Are all terms of type forall a. a operationally bottom?

Is there a proof that all terms of type $\forall{a}. a$ are operationally $\bot$, in a non-weakly-normalising version of System F?

If you ask a free theorem calculator such as this one for the free theorem of $\forall{a}. a$ (written just $a$, as the tool adds implicit $\forall$s for each free type variable), you get the rather unhelpful

forall t1,t2 in TYPES, R in REL(t1,t2). (f_{t1}, f_{t2}) in R


Which seems to me only to imply that instantiations of $f$ at any two types are related by any relation.

Does this imply that $f$ must be a looping term?

Sure, just take R to be $\{(\bot,\bot)\}$, the relation which only relates bottoms.