Proof of Void using type constructor injectivity

[david-christiansen]

I hadn't realized that type constructor injectivity caused inconsistency without excluded middle in the past. But @leodemoura pointed me at an example on the Lean issue tracker that proves Void without any postulates, relying on type constructor injectivity alone. I ported it to Idris.

The following code type checks in master for me:

module ProveVoid

%default total

data In : (f : Type -> Type) -> Type where
  MkIn : In f

-- This step requires definitional type constructor injectivity and is
-- the source of the problem.
injIn : In x = In y -> x = y
injIn Refl = Refl

P : Type -> Type
P x = (a : (Type -> Type) ** (In a = x, a x -> Void))

inP : Type
inP = In P

oops : P ProveVoid.inP -> Void
oops (a ** (Ha0, Ha1)) =
  let ohNo : (P (In P) -> Void) = replace {P=\ x => x (In P) -> Void} (injIn Ha0) Ha1
  in ohNo (P ** (Refl, ohNo))

total -- for extra oumph!
ohNo : Void
ohNo =
  let foo : P ProveVoid.inP = (P ** (Refl, oops))
  in oops foo

[edwinb]

Yikes! On the one hand, we can fix this by turning off type constructor injectivity. On the other hand, this would break a lot of other things (mostly involving interfaces). Any ideas?

[edwinb]

So this is leading me down a rabbit hole, which is very interesting. But I suppose there is one question which could lead to at least a temporary fix: even if type constructors aren't injective in general, are there any circumstances under which we can know they are injective?

[leodemoura]

Here is the original source for this example: https://lists.chalmers.se/pipermail/agda/2010/001526.html

are there any circumstances under which we can know they are injective?

@edwinb I'm also curious about this question, but I didn't manage to find an answer in the literature. I came across this example when trying to implement OTT in Lean. AFAICT, type constructor injectivity in used in the OTT coercion reduction rules. I'm not claiming OTT is unsound, they consider only a finite set of type constructors (e.g., Sigma, W, Pi, ...), and type constructor injectivity is harmless for them. They point out that in OTT other inductive datatypes can be compiled into this finite set. This observation provides a partial answer (i.e., a sufficient condition) to the question above. For example, a Triple a b c would be compiled using two Sigmas, then using injectivity for Sigma we can deduce that Triple is also injective. In contrast, In would be compiled into the Unit type, and the parameter f would vanish.

[ahmadsalim]

@edwinb An option would be to not treat big forced arguments (functions that involve Type) as injective I think.

[ahmadsalim]

Per https://lists.chalmers.se/pipermail/agda/2015/007391.html.

[david-christiansen]

@edwinb I'm sorry I threw this up on your day off!

I don't know what the fix is, exactly because of the interface issue. I suppose the place to start is to look at how Agda's instance arguments work around the lack of definitional type constructor injectivity.

[yanok]

Regardless of type constructor injectivity (which is still good to get rid of), I think this exact example is just another instance of #3194: if I change built-in pair type to MPair defined in the same file, it doesn't longer type check and universe inconsistence is reported:

module ProveVoid

data MPair : (a : Type) -> (P : a -> Type) -> Type where
     MkMPair : .{P : a -> Type} -> (x : a) -> (pf : P x) -> MPair a P

%default total

data In : (f : Type -> Type) -> Type where
  MkIn : In f

-- This step requires definitional type constructor injectivity and is
-- the source of the problem.
injIn : In x = In y -> x = y
injIn Refl = Refl

P : Type -> Type
P x = MPair (Type -> Type) (\a => (In a = x, a x -> Void))

inP : Type
inP = In P

oops : P ProveVoid.inP -> Void
oops (MkMPair a (ha0, ha1)) =
  let ohNo : (P (In P) -> Void) = replace {P=\ x => x (In P) -> Void} (injIn ha0) ha1
  in ohNo (MkMPair P (Refl, ohNo))

total -- for extra oumph!
ohNo : Void
ohNo =
  let foo : P ProveVoid.inP = (MkMPair P (Refl, oops))
  in oops foo

and of course if I move MPair definition to a separate module it type checks again.

[milessabin]

On Sun, Mar 12, 2017 at 6:29 PM, David Christiansen notifications@github.com wrote:

I don't know what the fix is, exactly because of the interface issue.

What complications do interfaces add to the problem?

Cheers,

Miles

-- Miles Sabin tel: +44 7813 944 528 skype: milessabin gtalk: miles@milessabin.com http://milessabin.com/blog http://twitter.com/milessabin

[ahmadsalim]

@milessabin Implementation (type class instace) resolution relies on type constructor injectivity to resolve that e.g. a = String when Show a = Show String I believe.

I am not sure how essential it is, i.e., whether there is an acceptable workaround. I believe someone (@yanok ? ) tried to turn it off and it broke a few things, so it is definitely used currently.

[ahmadsalim]

Well, maybe https://lirias.kuleuven.be/bitstream/123456789/582749/1/CW705.pdf could work better, but I don't know how much effort it requires and whether it does avoid issues with type constructor injectivity.