unify_f_g_h.txt

f g h x y = g (g x) (h y)

assign the full rhs expression to type a, because we need a name 
for the result of the whole expression. This will be
the ultimate return type of f :

g (g x) (h y) :: a

So far we only know that:

f :: ? -> ? -> ? -> ? -> a


h y :: b                -- assign the first argument to type b

g (g x) :: b -> a       -- expand

g x :: c                -- expand again

g :: c -> b -> a        

x :: d                  -- expand g x again
g :: d -> c

So we've built constraints from two different applications of g:

g :: c -> (b -> a)
g :: d -> c

Inspecting the left operand, c and d must be the same type: c ~ d .
This is because of referential transparency: g must take inputs of 
the same type, so let's call it c :                        
          
                          g :: c -> c
           
Proving that g :: id    
we can now substitute c with the more specific (b -> a) :

g :: (b -> a) -> b -> a

Let's assign type e to our y; we now know all the types:

y :: e
h :: e -> b
x :: b -> a        -- because originally x :: d
 
So f returns an a , as per the top expression:

f :: ((b -> a) -> b -> a) -> (e -> b) -> (b -> a) -> e -> a

-----------------------------------------------------------------
https://stackoverflow.com/questions/50777884/manual-type-inference-in-haskell