I think that "second-order lambda-calculus" usually refers to system F, which doesn't even have dependent types. What I'm getting at is that there are plenty o

I think that "second-order lambda-calculus" usually refers to system F, which doesn't even have dependent types. What I'm getting at is that there are plenty of parts of GHC's flavor of Haskell that you can't depend on type inference for. You have to give type signatures for polymorphic recursion, for instance.