Welcome to SWI-Prolog (threaded, 64 bits, version 7.6.4)
SWI-Prolog comes with ABSOLUTELY NO WARRANTY. This is free software.
Please run ?- license. for legal details.

For online help and background, visit http://www.swi-prolog.org
For built-in help, use ?- help(Topic). or ?- apropos(Word).

?- isIType(IType), types(isa(I, IType)).
IType = arr(α, α),
I = λ(_3970, _3970)

?- isKType(KType), types(isa(K, KType)).
false.

?- isKType(KType), types(isa(K, KType)).
KType = arr(α, arr(β, α)),
K = λ(_5242, λ(_5266, _5242))

?- isKsType(KsType), types(isa(K, KsType)).
KsType = arr(β, arr(α, α)),
K = λ(_5648, λ(_5672, _5672))

?- isSType(SType), types(isa(S, SType)).
false.

?- trace.
true.

[trace]  ?- isSType(SType), types(isa(S, SType)).
   Call: (9) isSType(_9680) ? 
   Exit: (9) isSType(arr(arr(α, arr(β, γ)), arr(arr(α, β), arr(α, γ)))) ? 
   Call: (9) types(isa(_9684, arr(arr(α, arr(β, γ)), arr(arr(α, β), arr(α, γ))))) ? 
   Call: (10) types([], isa(_9684, arr(arr(α, arr(β, γ)), arr(arr(α, β), arr(α, γ))))) ? 
   Call: (11) lists:member(isa(_9684, arr(arr(α, arr(β, γ)), arr(arr(α, β), arr(α, γ)))), []) ? 
   Fail: (11) lists:member(isa(_9684, arr(arr(α, arr(β, γ)), arr(arr(α, β), arr(α, γ)))), []) ? 
   Redo: (10) types([], isa(_9684, arr(arr(α, arr(β, γ)), arr(arr(α, β), arr(α, γ))))) ? 
   Call: (11) types([isa(_10054, arr(α, arr(β, γ)))], isa(_10056, arr(arr(α, β), arr(α, γ)))) ? 
   Call: (12) lists:member(isa(_10056, arr(arr(α, β), arr(α, γ))), [isa(_10054, arr(α, arr(β, γ)))]) ? 
   Fail: (12) lists:member(isa(_10056, arr(arr(α, β), arr(α, γ))), [isa(_10054, arr(α, arr(β, γ)))]) ? 
   Redo: (11) types([isa(_10054, arr(α, arr(β, γ)))], isa(_10056, arr(arr(α, β), arr(α, γ)))) ? 
   Call: (12) types([isa(_10078, arr(α, β)), isa(_10054, arr(α, arr(β, γ)))], isa(_10080, arr(α, γ))) ? 
   Call: (13) lists:member(isa(_10080, arr(α, γ)), [isa(_10078, arr(α, β)), isa(_10054, arr(α, arr(β, γ)))]) ? 
   Fail: (13) lists:member(isa(_10080, arr(α, γ)), [isa(_10078, arr(α, β)), isa(_10054, arr(α, arr(β, γ)))]) ? 
   Redo: (12) types([isa(_10078, arr(α, β)), isa(_10054, arr(α, arr(β, γ)))], isa(_10080, arr(α, γ))) ? 
   Call: (13) types([isa(_10102, α), isa(_10078, arr(α, β)), isa(_10054, arr(α, arr(β, γ)))], isa(_10104, γ)) ? 
   Call: (14) lists:member(isa(_10104, γ), [isa(_10102, α), isa(_10078, arr(α, β)), isa(_10054, arr(α, arr(β, γ)))]) ? 
   Fail: (14) lists:member(isa(_10104, γ), [isa(_10102, α), isa(_10078, arr(α, β)), isa(_10054, arr(α, arr(β, γ)))]) ? 
   Redo: (13) types([isa(_10102, α), isa(_10078, arr(α, β)), isa(_10054, arr(α, arr(β, γ)))], isa(_10104, γ)) ? 
   Fail: (13) types([isa(_10102, α), isa(_10078, arr(α, β)), isa(_10054, arr(α, arr(β, γ)))], isa(_10104, γ)) ? 
   Fail: (12) types([isa(_10078, arr(α, β)), isa(_10054, arr(α, arr(β, γ)))], isa(_10080, arr(α, γ))) ? 
   Fail: (11) types([isa(_10054, arr(α, arr(β, γ)))], isa(_10056, arr(arr(α, β), arr(α, γ)))) ? 
   Fail: (10) types([], isa(_9684, arr(arr(α, arr(β, γ)), arr(arr(α, β), arr(α, γ))))) ? 
   Fail: (9) types(isa(_9684, arr(arr(α, arr(β, γ)), arr(arr(α, β), arr(α, γ))))) ? 
false.

?- isCType(CType), types(isa(C, CType)).
CType = arr(α, arr(arr(α, α), α)),
C = λ(_3150, λ(_3174, _3150)) ;
CType = arr(α, arr(arr(α, α), α)),
C = λ(_3150, λ(_3174, app(_3174, _3150))) ;
CType = arr(α, arr(arr(α, α), α)),
C = λ(_3150, λ(_3174, app(_3174, app(_3174, _3150)))) ;
CType = arr(α, arr(arr(α, α), α)),
C = λ(_3150, λ(_3174, app(_3174, app(_3174, app(_3174, _3150))))) ;
CType = arr(α, arr(arr(α, α), α)),
C = λ(_3150, λ(_3174, app(_3174, app(_3174, app(_3174, app(_3174, _3150))))))

?- isSType(SType), types(isa(S, SType)).
SType = arr(arr(α, arr(β, γ)), arr(arr(α, β), arr(α, γ))),
S = λ(_3568, λ(_3592, λ(_3616, app(app(_3568, _3616), app(_3592, _3616))))) 

?- types(isa(M, α)).
false.

?- types(isa(M, arr(α, β))).
false.

?- isBadType1(BT), types(isa(M, BT)).
false.

?- isBadType2(BT), types(isa(M, BT)).
false.

?- isCType(T), types(isa(M, T)).
T = arr(α, arr(arr(α, α), α)),
M = λ(_5216, λ(_5240, _5216)) ;
T = arr(α, arr(arr(α, α), α)),
M = λ(_5216, λ(_5240, app(_5240, _5216))) ;
T = arr(α, arr(arr(α, α), α)),
M = λ(_5216, λ(_5240, _5216)) ;
false.

?- isSType(T), types(isa(M, T)).
T = arr(arr(α, arr(β, γ)), arr(arr(α, β), arr(α, γ))),
M = λ(_6064, λ(_6088, λ(_6112, app(app(_6064, _6112), app(_6088, _6112))))) ;
T = arr(arr(α, arr(β, γ)), arr(arr(α, β), arr(α, γ))),
M = λ(_6064, λ(_6088, λ(_6112, app(app(_6064, _6112), app(_6088, _6112))))) ;
T = arr(arr(α, arr(β, γ)), arr(arr(α, β), arr(α, γ))),
M = λ(_6064, λ(_6088, λ(_6112, app(app(_6064, _6112), app(_6088, _6112))))) ;
T = arr(arr(α, arr(β, γ)), arr(arr(α, β), arr(α, γ))),
M = λ(_6064, λ(_6088, λ(_6112, app(app(_6064, _6112), app(_6088, _6112))))) ;
false.

?- isKType(T), types(isa(M, T)).
T = arr(α, arr(β, α)),
M = λ(_54, λ(_78, _54)) ;
T = arr(α, arr(β, α)),
M = λ(_54, λ(_78, _54)) ;
false.

?- isIType(T), types(isa(M, T)).
T = arr(α, α),
M = λ(_48, _48) ;
T = arr(α, α),
M = λ(_48, _48) ;
false.

?- isGoodType(T), types(isa(M, T)).
false.

?- isGoodType(T), types(isa(M, T)).
T = arr(arr(α, β), arr(arr(arr(β, β), α), β)),
M = λ(_4852, λ(_4876, app(_4852, app(_4876, λ(_4984, _4984))))) 
?- isBadType1(T), types(isa(M, T)).
false.

?- isBadType2(T), types(isa(M, T)).
false.