The :type command at the GHCi prompt is your friend. Let's take your second example first
λ> :type let g = \x -> (\y -> y) x in g
let g = \x -> (\y -> y) x in g :: p -> p
So g is well-typed and is a convoluted way to write an identity function :: p -> p. Specifically, g takes some x and applies an identity function (\y -> y) to x, resulting in x. GHCi in giving the type uses a fresh type name p, to avoid confusion. No your g x y = ... is not equivalent. (Check it with :type.)
You can abbreviate :type to just :t. Then let's take your first example.
λ> :t let f = \x -> x (\y -> x y) in f
* Occurs check: cannot construct the infinite type: t2 ~ t2 -> t3
* In the first argument of `x', namely `(\ y -> x y)'
In the expression: x (\ y -> x y)
In the expression: \ x -> x (\ y -> x y)
* Relevant bindings include
x :: t2 -> t3 (bound at <interactive>:1:10)
f :: (t2 -> t3) -> t3 (bound at <interactive>:1:5)
Errk. Is your suggested f the same as that?
λ> :t let f x y = x x y in f
* Occurs check: cannot construct the infinite type:
t3 ~ t3 -> t4 -> t5
* In the first argument of `x', namely `x'
It at least looks like a similar error message. What are these t2, t3, t4, t5? Again it's GHCi using fresh names for the types, to avoid confusion.
Looking at the let f = ..., GHCi sees x is applied to something, so it gives x :: t2 -> t3 where t2 is the type of its argument, t3 is the return type. It also sees f = \x -> x (blah). So the return type of f must be whatever x returns, i.e. t3, and the argument to f is x. So f :: (t2 -> t3) -> t3.
Inside the (blah), there's x applied to something. So the something (i.e. y) must be the type of x's argument, and the return type must be x's return type. I.e. (\y -> x y) :: t2 -> t3. Errk: then we must have x's argument type same as that, because x is applied to it. And the way we write 'same as' is with ~.
Then the error message tells you GHCi is trying to make sense of t2 ~ (t2 -> t3). (-> binds tighter than ~.) And if you try to subsitute that equivalence for t2 into the RHS you'll get t2 ~ (((... -> t3) -> t3)-> t3) ad infinitum.
Your suggested equivalent for f x y = is not equivalent (the message/typing is a little different). But they're both infinite types, so not allowed.
f x = x (x $) = x x. It has no type, lambda or no lambda. By eta-expansionf x y = x x ywhich still has no type.g x = id x = x. I can't follow your reasoning.(forall a. a -> b) -> b.f . (. f)though. :)