[jerf]

It isn't exactly the same. I believe I said that up front.

But it provides a bridge. Both things have "You can assert Property X about all things of type Y" built into them. Trying to jump people straight to C-H without giving any hint whatsoever of why this may be useful in any real code... well, that's a non-trivial percentage of why this approach has completely failed to capture any significant mindspace, though I leave it as an exercise to the reader to determine the exact percentage in their minds.

[immibis]

C-H has nothing to do with "property X is true about all things of type Y". It says "if you can find an object of type Y, you can prove global property Z."

For example, the property corresponding to the type "(Either a a) -> a" is "(A or A) implies A" which doesn't tell you any properties of actual objects of the type "(Either a a) -> a"

The property corresponding to the type "(Either a b) -> a" is "(A or B) implies A" which is not provable, so you can't find any object of this type.