[Haskell-cafe] resources on static analysis

Dear list, I am interested in learning more about static analysis of Haskell code. Specifically of the relation between arguments of recursive and non-recursive calls. For example if we look at the ++ function from Prelude: (++) [] ys = ys (++) (x:xs) ys = x : xs ++ ys amongst others, we could infer the relations: ys_i+1 = ys_i (x:xs)_i+1 = xs_i Searching the web I found several tools (HLint, Haskabelle, Sourcegraph), but I am interested in the theory behind this. If you could recommend a paper or a book on this topic I would be grateful. Thanks, Maarten Faddegon