how type checking fails?

I was doing a type checking example in system f sub on paper to understand how it works.

according to Pierce's book Types and Programming Languages, numbers and their types are following in system f sub. (see chapter 26.3, page 399)

1)top is universal type, 
   2)capital letters are type variables, small letters are term variables  

    church number 1
    sone = λAB).λy:C.x y
    stwo = λAB).λy:C.x (x y)

    type for church number 0
    SZero = ∀AB)-->C-->C

    type for numbers except 0
    SPos = ∀AB)-->C-->B
    SNat = ∀AB)-->C-->A

for the type checking

Γ |-  stwo :  SZero

should fail.

book said "SPos is inhabited by all the elements of SNat except SZero".

Also I saw there is a input test test files, it shows above example should fail.

Therefore, I assume

Γ |-  sone :  SZero

should fail too.

I want to see how it is going to fail and did pen-paper type checking as following (see type checking rules in the same book, previous page)

```
1)for convenience, I wrote from top to down fashion
2)variables are given distinct

Γ |- (λAB).λy:C.x y)
: (∀A1B1)-->C1-->C1)
---------------------------------------------(T-TABS) =>assume A=A1,top=top
,and renamed A1 to A
AB).λy:C.x y)
:(∀B1B1)-->C1-->C1)
----------------------------------------------(T-TABS) =>assume B=B1, rename B1 to B

AB).λy:C.x y)
:(∀C1B)-->C1-->C1)
---------------------------------------------------(T-TABS) =>assume C=C1, rename C1 to C
AB).λy:C.x y)
: (A-->B)-->C-->C
-----------------------------------------------------T_ABS =>have A-->B=A-->B, get A=A,B=B,remove them

AB |- (λy:C.x y) : C-->C
------------------------------------------------T-ABS ==>have C=C
AB,y:C | ( x y ) : C
----------------------------------------------- T-APP introduce type variable T1
AB,y:C | x : T1-->C A:top,BB,y:C | y:T1
-------------

I finally figured it out. The key is using sub-typing rules.

ctx[]|- t:S     ctx[]|S<:T
         ---------------------------t-sub
               ctx[]|-t:T

By applying this rule after T-APP rules, you can eliminate all "A==B" equations by using

eq(A,A) -> .
       eq(A-->B,A-->B) -> eq(A,A),eq(B,B).
         ........

One can easily observe how to write these rules to eliminate "eq"s. If there is one or some "eq"s left, such as "eq(A,B)", means a contradiction, so type checking fails.

If you can eliminate all "eq"s, means type checking successful.

One important point about "t-sub" rule is that it is not suitable for implementation, because it is not syntax directed. That rule is applicable for any statement with the form of

ctx[]|t:T

therefore, algorithmic version is proved to has the same power in the book "Types and Programming Languages".

:)

StackExchange Computer Science Q#64075, answer score: 2