(\f.(f 1,f true)) (\x.succ x) 는 거부하고 (\f.(f 1,f true)) (\x. x) 는 통과시켜야 한다.

더불어 PolymorphicRecursion 에 나오는 것들도 당연히 통과시켜야 한다.

system F 의 강력함까지는 아니라도 마치 system F 를 자동으로 생성하는

듯한 그런 타입시스템이 있었으면 한다.

요한1서 5:16 표준새번역

누구든지, 자기의 형제나 자매가 죄를 짓는 것을 볼 때에, 그것이 죽음에 이르게 하는 죄가 아니면, 하나님께 간구하십시오. 그러면 하나님께서는, 죽을 죄를 짓지 않은 그 사람들에게 생명을 주실 것입니다. 죽을 죄가 있습니다. 이 죄를 두고 간구하라고 하는 말은 아닙니다.