Extensional conversions in F* (not included in EMF*) break subject reduction

[nikswamy]

This is an example from Andrej Bauer via @leodemoura.

let coerce (a:Type) (b:Type{a == b}) (x:a) : b = x

let test (a:Type)
         (b:Type)
         (c:Type)
         (f: (a -> b))
         (x:a)
         (y:b)
         (z:c)
         (h:squash ((a -> b) == (a -> c)))
    =  (coerce (a -> b) (a -> c) (fun (x:a) -> y)) x == z

The term is well-typed but if you reduce the coerce and the beta redex you're left with y == z which is ill-typed.

I guess we say very little about reduction of open terms (e.g., open terms can diverge). But, this is still interesting and something to consider as we look to beef up EMF* to include more of F*.

In its current form, EMF* lacks the conversion rule needed to typecheck coerce although F* allows it.

Thoughts?

[cpitclaudel]

IIUC, the difference with Coq here is that we internalized treatment of ==. Correct?

The Coq equivalent of your example is this, I think:

Definition coerce (A B: Type) (p: A = B) (a: A) : B :=
  eq_rect A (fun T => T) a B p.

Definition test
           (A B C: Type)
           (x: A) (y: B) (z: C)
           (p: (A -> B) = (A -> C)) :=
  (coerce (A -> B) (A -> C) p (fun x => y)) x = z.

Compute test.
(* fun (A B C : Type) (x : A) (y : B) (z : C) (p : (A -> B) = (A -> C)) =>
       match p in (_ = x0) return x0 with
       | eq_refl => fun _ : A => y
       end x = z *)

Is this really a problem with open terms, though? For example, suppose I have A.fst like this:

module A

abstract type a = int
abstract type b = int
abstract type c = int
abstract let x: a = 0
abstract let y: b = 0
abstract let z: c = 0
abstract let abc: squash ((a -> b) == (a -> c)) = ()

then I can write this in B.fst:

module B

open A
let coerce (a:Type) (b:Type{a == b}) (x:a) : b = x
let closed = (coerce (a -> b) (a -> c) (fun (x:a) -> y)) x == z

Evaluating closed with C-c C-s C-e yields closed ↓βδιζ x:Prims.unit{ Prims.equals A.y A.z }, which is ill-typed.

This is probably pretty obvious, but the problem also happens with other constructors:

type wrap a =
| Wrap : a -> wrap a

let unwrap = function | Wrap aa -> aa

let coerce (a:Type) (b:Type{a == b}) (x:a) : b = x

let test (a:Type)
         (b:Type)
         (c:Type)
         (x:a)
         (y:b)
         (z:c)
         (h:squash (wrap a == wrap b))
    = unwrap (coerce (wrap a) (wrap b) (Wrap x)) == y

[kyoDralliam]

Along the same line, Andrej Bauer and Théo Winterhalter seem to have come up with a simple counter-example to subject reduction in Extensional Type Theory that is quite striking (and puzzling).

The counter-example to SR boils down to the fact that the context with only an hypothesis h : nat -> nat = nat -> bool is consistent (i.e. we cannot derive syntactically false out of it). The proof of this fact comes from the construction of a model where types are interpreted as cardinals (sets up to bijection) in which it is clear that the equality does hold (and so its negation is not derivable in ETT).

From that, the term fun (h:nat -> nat = nat -> bool) -> (fun (x:nat) -> x) 42 <: bool returning a boolean is well typed but not its reduced variant (indeed it is provable inside ETT that nat =!= bool since bool has exactly 2 elements).

In order to recover SR in his work on conservativity of ETT over ITT, Théo Winterhalter used a "typed" beta-reduction where all lambda-abstractions and applications are annotated with both the types of the domain and the codomain, and the beta-reduction can happen only if these syntactically match.