[catnaroek]

> Now, by parametricity that should have only one inhabitant (upto iso).

I can count at least three: `undefined`, `const undefined` and `id`.

> Use your claimed break in parametricity from type families and provide me two distinct inhabitants.

Does this count? Here Oleg constructs an inhabitant of False using just some means to case-analyze types (GADTs or type families): http://okmij.org/ftp/Haskell/impredicativity-bites.html

[sclv]

i should have specified "modulo bottom" because i somehow didn't cotton i was talking to someone more interested in pedantry than actual discussion.

that said, constructing an inhabitant of false a _different_ way (when we can already write "someFalse = someFalse") is not particularly interesting, and again doesn't speak to parametricity in any direct way.

[wyager]

Sounds like the problem there is that the Haskell typechecker assumes injectivity, not that it supports case-analysis.

[catnaroek]

The injectivity assumption isn't unjustified - type constructors are injective.

[wyager]

> The injectivity assumption isn't unjustified

Strongly disagree.

(+2) 3 == (+1) 4 implies neither (+2) == (+1) nor 3 == 4. So Fst goes out the window.

(even 5) == (even 7) does not imply 5 == 7.

>type constructors are injective.

But type functions aren't, and that's what we want.

I agree that it's misleading to have type functions look like type constructors syntactically.

[catnaroek]

The type constructor that's being assumed injective in the section “Deriving `absurd` with type families” is `R`.