Higher library allows derivation of 'false'

[stedolan]

It's debatable whether this is a bug - there's no segfaulting, just nontermination. But the nontermination arises without any use of recursion or loops at the type or value level, using one call to Newtype1:

type 'a i = T

type (_, _) eq = Refl : ('a, 'a) eq

let inj (type a) (type b) (Refl : (a i, b i) eq) : (a, b) eq = Refl

type empty = |

type 'x r = { r : 'p . ('x, 'p i) eq -> ('x, 'p) app -> empty }
module R = Newtype1 (struct type 'a t = 'a r end)

let eqv_1 (type p) : p i r -> (p i, p) app -> empty =
  fun { r } p -> r Refl p

let eqv_2 (type p) : ((p i, p) app -> empty) -> p i r =
  fun np -> { r = fun (type a) (eq : (p i, a i) eq) (xp : (p i, a) app) ->
    match inj eq with Refl -> np xp }

type bad = R.t i r

let bad_1 : bad -> empty =
  fun b -> eqv_1 b (R.inj b)

let bad_2 : (bad -> empty) -> bad =
  fun nb -> eqv_2 (fun b -> nb (R.prj b))

let absurd : empty =
  let b : bad = bad_2 bad_1 in
  bad_1 b

This is an OCaml port of Alexandre Miquel's Coq program, showing that the mixture of injectivity, impredicativity and large type parameters is unsound. (The first two are present in OCaml, the third is added by higher).

[lpw25]

Interesting. As you say, I don't think it really constitutes a bug. For a start, if you strip all the type annotations away and replace Higher with just a polymorphic variant you get:

type empty = |
let inj x = `Box x
let prj = function `Box x -> x

let eqv_1 = fun r p -> r () p
let eqv_2 = fun np -> fun eq xp -> np xp
let bad_1 = fun b -> eqv_1 b (inj b)
let bad_2 = fun nb -> eqv_2 (fun b -> nb (prj b))

let absurd : empty =
  let b = bad_2 bad_1 in
  bad_1 b;;

which also type checks fine, so it doesn't seem like Higher is really changing anything here.

I'm curious if the same thing happens in Haskell, since I tend to think of Higher as providing Haskell-style type constructors in OCaml, and they don't have any eqi-recursive types so maybe the simpler version doesn't already work there.

[yallop]

Thanks for the interesting example, @stedolan.

@lpw25:

I'm curious if the same thing happens in Haskell,

Oleg describes a somewhat similar example in Impredicativity + injectivity + type case analysis = inconsistency (Russell paradox). Here's a port to OCaml with higher:

type empty = |
type ('a,'b) iapp = App of ('a, 'b) app

type 'c r = MkR : (((unit, 'c) iapp, 'c) iapp -> empty) -> (unit, 'c) iapp r
module R = Newtype1(struct type 'a t = 'a r end)

let cond_false : (unit, R.t) iapp r -> empty =
  fun (MkR f as x) -> f (App (R.inj x))

let absurd : empty =
   cond_false (MkR (fun (App x) -> cond_false (R.prj x)))

if you strip all the type annotations away and replace Higher with just a polymorphic variant

Indeed, with polymorphic variants, type inference can be made to introduce recursive types, and it's straightforward to write non-terminating programs without explicitly introducing recursion. Here's one such (complete) example:

(fun (`x x) -> x (`x x)) (`x (fun (`x x) -> x (`x x)))