To make this a bit more concrete, imagine you were passing the identity function into another function or context, but then using it both with an Int term, and

To make this a bit more concrete, imagine you were passing the identity function into another function or context, but then using it both with an Int term, and a Bool term. Thus by inference that identity function has the type Int->Int, and Bool->Bool. Under Curry, this is ok, but under Church, it is not. I don't think it has much to do with static vs dynamic, or indeed type labels.