Main.hs

import Reverse
import Prelude hiding (reverse)

main :: IO ()
main = print $ reverse [1, 2, 3]

Reverse.hs

module Reverse (reverse) where

import Prelude hiding (foldr, reverse)

foldr :: (a -> acc -> acc) -> acc -> [a] -> acc
foldr _ acc [] = acc
foldr f acc (x:xs) = f x (foldr f acc xs)

reverse :: [a] -> [a]
reverse xs = foldr (flip (.) . (:)) id xs []

Signatures.md

Hypothetical co-call signatures for module Reverse (assuming that foldr isn't inlined):

binder	E0	E1	E2	E3	E4	E5
foldr	{}	{f}2	{f, acc}2	C3 ∪ {(f,f)}	E3·x4	((E3·x4)·x5)
reverse	{}	C1 (still {})	E1·x2	E1·x2·x3	E1·x2·x3·x4	E1·x2·x3·x4·x5

C_n is the complete graph in n nodes without self-edges, V² is the complete graph of all nodes in V with self-edges.

G·x (left-assoc) inserts x into the graph and adds an edge to every node in V(G)∪{x}. x_i are non-formal arguments added via possible eta-expansion (are those even necessary?) in the scenario were the function call is over-saturated, e.g. the call to foldr in the body of reverse. (Not so sure about this part, do we need self-edges or not?)

If I'm not missing something, there should be no loss in precision compared to doing the analysis without signatures.