[evincarofautumn]

Nah, that’s fair. However, here’s a neat trick—look at the type of “head”:

    ∀a. [a] → a

Viewed as a logical formula, it’s not a tautology, so I know it must be partial. Proof:

    Given: L(a) = μr. 1 + (a × r)

    ∀a. L(a) → a
    = [definition of L]
    ∀a. (μr. 1 + (a × r)) → a
    = [unroll μ]
    ∀a. (1 + (a × μr. 1 + (a × r))) → a
    = [∀xyz. (x + y) → z ⇔ (x → z) × (y → z)]
    ∀a. (1 → a) × ((a × μr. 1 + (a × r)) → a)
    = [(∀a. 1 → a) = 0]
    ∀a. 0 × ((a × μr. 1 + (a × r)) → a)
    = [∀x. 0 × x = 0]
    ∀a. 0
    =
    0

Unfortunately, this is also false if a is false (void/bottom), and all those “→ a”s are actually “→ ¬¬a” because Haskell isn’t a total language—with that pesky intuitionistic double-negative, any function can be partial. But it’s a good rule of thumb for quickly checking whether a function must not return for some (or all) inputs.