Demonstrating TypeScript 0.8 type system to be unsound. The subtyping relationship is defined in a way that admits the following code that results in TypeError exception being thrown.

subtyping.v

Require Import Utf8.

Inductive subtype (a b : Set) : Set :=
| ST : (a -> b) -> subtype a b.

Infix ":>" := subtype (at level 50).

Definition st {x y} f := ST x y f.

Definition unpack {a b : Set} (st : a :> b) :=
  match st with
    | ST f => f
  end.

Notation " x ~ y " := (unpack x y) (at level 50).

Definition sub_call {s x y} (p : s :> x) (f : x → y) : (s → y) :=
  fun x => f (p ~ x).

Definition sub_ret {s x y} (p : s :> y) (f : x → s) : (x → y) :=
  fun x => p ~ f x.

Definition sub_refl {a : Set} : a :> a :=
  st (fun x => x).

Definition sub_fst {a b : Set} : (a * b) :> a :=
  st (fun xy => fst xy).

Definition sub_snd {a b : Set} : (a * b) :> b :=
  st (fun xy => snd xy).

Definition sub_fun {a b p q : Set} :
  (p :> a) → (b :> q) → (a → b) :> (p → q) :=  
  fun g h => st (fun f x => h ~ f (g ~ x)).

Definition sub_fun_bad {a b p q : Set} :=
  (a :> p) → (b :> q) → (a → b) :> (p → q).

Inductive empty : Set := .

Theorem empty_absurd : empty → False.
Proof. intro H. case H. Qed.

Definition fun_rule_absurd (r : sub_fun_bad) : False :=
  let f (k : unit → empty) : empty := k tt in
    let g (i : unit * empty) : empty := snd i in
      empty_absurd (sub_call (r sub_fst sub_refl) f g).

unsound.ts

class A {}

class B extends A {
  foo(x: string) : string {
    return x + "!";
  };
}

function f1(k: (a: A) => void) : void {
  k(new A());
}

function f2(k: (a: B) => void) : void {
  f1(k);
}

f2(function (x: B) { console.log(x.foo("ABC")); });

@mindplay-dk This is two years late, but PureScript. :)

I find the demonstration a bit easier to follow without the lambda:

class A {}

class B extends A {
  foo(x: string) : string {
    return x + "!";
  };
}

function f1(k: (a: A) => void) : void {
  k(new A());
}

function f2(x: B) {
  console.log(x.foo("ABC"));
}

f1(f2);