Is the church-style affine calculus of constructions with unrestricted recursion consistent?
Let me first state that I'm not sure what are you getting at, I'm not sure how linearity/affinity is relevant. I'll answer the question in 'standard' setting. 

How would you define how to compare two infinite types lazily?

It seems to me that it can't be done automatically since they can eventually diverge. 

[Checking for  nominal equality ("pointer quality", exactly same identifier) seems shortsighted since you could define two identical infinite structures Nat and Nat2 and they would not be equal nominally while they should.]

But in some cases it can be done, its just that the programmer needs to lead the checker on how the equality should be verified.

In your case, think about Nat as a type-level fix point:

natF = 
  ∀ nat : * 
  ∀ P : *
  ∀ S : nat -&gt; P
  ∀ Z : P
  P

Nat = fix nat . natF nat


That gives Nat and the two functions:

fix : Nat -&gt; natF Nat
unfix : natF Nat -&gt; Nat


You can use these functions as annotations that control the infinity and allow the checker to work with finite structures all the time. 

This article has a nice intro (there are plenty of similar tutorials):
Gentle introduction to the general technique of F-algebras

For Nat, you would use this functor:

data Nat nat = Z | S nat