Counterexamples in Type Systems

collated by Stephen Dolan, with thanks to Andrej Bauer, Leo White and Jeremy Yallop

let singleton x = [x]

static <A> List<A> singleton(A x) {
    return Arrays.asList(x);
}

let r = ref [] in           (* r : ∀ α . α list ref *)
r := [0];                   (* using r as an int list ref *)
print_string (List.hd !r)   (* using r as a string list ref *)
(* Crash! (Well, it would, if the OCaml compiler allowed this) *)

let f =
  let r = ref None in
  fun x ->
    match !r with
    | None -> r := Some x; x
    | Some x -> x
(* The value restriction means f is not polymorphic,
   but if it were then this would crash: *)
let _ =
  let _ = f 42 in
  print_string (f "hello")

(* Counterexample by Bob Harper and Mark Lillibridge *)
fun left (x,y) = x;
fun right (x,y) = y;

let val later = (callcc (fn k =>
	(fn x => x,
         fn f => throw k (f, fn f => ()))))
in
	print (left(later)"hello world!\n");
	right(later)(fn x => x+2)
end

(* Counterexample by Thierry Martinez *)
let f x =
  let ref : type a . a option ref = ref None in
  ref := Some x;
  Option.get !ref

let () = print_string (f 0)

-- Counterexample by Izaak Meckler
import Signal
import Html
import Html.Attributes(style)
import Html.Events(..)
import Maybe

c = Signal.channel Nothing

s : Signal Int
s = Signal.map (Maybe.withDefault 0) (Signal.subscribe c)

draw x =
  Html.div
  [ onClick (Signal.send c (Just "I am not an Int"))
  , style [("width", "100px"), ("height", "100px")]
  ]
  [ Html.text (toString (x + 1)) ]
  |> Html.toElement 100 100

main = Signal.map draw s

good :: forall a . IO (IORef (Maybe a))
bad  :: IO (forall a . IORef (Maybe a))

import Data.IORef
import System.IO.Unsafe
badref :: IORef (Maybe a)
badref = unsafePerformIO (newIORef Nothing)
main = do
  writeIORef badref (Just 42)
  Just x <- readIORef badref
  putStrLn (x 1)

class Vehicle {}
class Car extends Vehicle {}
class Bus extends Vehicle {}
public class App {
  public static void main(String[] args) {
    Car[] c = { new Car() };
    Vehicle[] v = c;
    v[0] = new Bus(); // crashes with ArrayStoreException
  }
}

// Counterexample by Martin Odersky
class C[+A] {
  private[this] var y: A = _
  def getY: A = y
  class Inner(x: A) {
    y = x
  }
}

object Test {
  def main(args: Array[String]) = {
    val x = new C[String]
    val y: C[Any] = x
    val i = new y.Inner(1)
    val s: String = x.getY
    println(s)
    // Exception in thread "main" java.lang.ClassCastException:
    // java.lang.Integer cannot be cast to java.lang.String
  }
}

// Counterexample by Derek Lam (edited)
class Base {}
class Derived extends Base {
    public function __construct(public int $foo) {}
}
<<__ConsistentConstruct>>
abstract class A<+T> {
    abstract public function __construct(T $v);
}
class B extends A<Derived> {
    public function __construct(Derived $v){echo $v->foo;}
}
class C {
    public static function foo(): void {
        self::bar(B::class);
    }
    public static function bar(classname<A<Base>> $v): void {
        new $v(new Base()); // crashes
    }
}

(* Counterexample by Jeremy Yallop *)
let magic : 'a 'b. 'a -> 'b =
  fun (type a) (type b) (x : a) ->
    let bad_proof (type a) =
      (Refl : (< m : a>, <m : a>) eq :> (<m : a>, < >) eq) in
    let downcast : type a. (a, < >) eq -> < > -> a =
      fun (type a) (Refl : (a, < >) eq) (s : <>) -> (s :> a) in
    (downcast bad_proof ((object method m = x end) :> < >)) # m

// Counterexample by Owen Healy
object Test extends App {
  sealed trait Node[+A]
  case class L[C,D](f: C => D) extends Node[C => D]

  def test[A,B](n: Node[A => B]): A => B = n match {
    case l: L[c,d] => l.f
  }

  println {
    test(new L[Int,Int](identity) with
      Node[Nothing]: Node[Int => String])(3): String
  }
}

// Counterexample by Derek Lam
class Base {}
class Derived extends Base {
    public function __construct(public int $derived_prop) {}
}
final class ImplCov<+T> {
    public function __construct(private T $v) {}
    public function put(this $v): void {
        $this->v = $v->v;
    }
    public function pull(): T {
        return $this->v;
    }
}
class Violate {
    public static function foo(ImplCov<Derived> $v): void {
        self::bar($v);
        echo $v->pull()->derived_prop;
        // Wait... Base doesn't have $derived_prop!
    }
    public static function bar(ImplCov<Base> $v): void {
        $v->put(new ImplCov(new Base()));
    }
}
// Violate::foo(new ImplCov(new Derived(42))); crashes

// Counterexample by Paul Phillips
class A[+T] {
  val foo0 = {
    class AsVariantAsIWantToBe { def contains(x: T) = () }
    new AsVariantAsIWantToBe
  }
}

object Test {
  def main(args: Array[String]): Unit = {
    val xs: A[String] = new A[String]
    println(xs.foo0 contains "abc")
    println((xs: A[Any]).foo0 contains 5) // crashes
  }
}

// Counterexample by Ilya Gorbunov
// List is covariant, MutableList is an invariant subclass
private fun <E> List<E>.addAnything(element: E) {
    if (this is MutableList<E>) {
        this.add(element)
    }
}

arrayListOf(1, 2).addAnything("string")

// Counterexample by Chung-Kil Hur
sealed abstract class MyADT[+A]
case object MyNone extends MyADT[Nothing]
case class MyFun[A](fun: A=>A) extends MyADT[A]

def data : MyADT[Any] = MyFun((x:Int)=>x+1)

val foo : Any =
  data match {
    case MyFun(f) => f("a")
    case _ => 0
  }

type t = { foo : int; bar : string }
let make () = { foo = 42; bar = "hello" }

struct t { int foo; const char* bar; };
struct t* x = malloc(sizeof(struct t));
x->foo = 42;
x->bar = "hello";

class T {
  int foo;
  String bar;
  T () { this.foo = 42; this.bar = "hello"; }
}

class A {
  private final int x;
  public void printX() { System.out.println(x); }
  public A () { printX(); this.x = 42; printX(); }
}

// Counterexample by Joshua Rosen
class Foo {
    val nonNull: String

    init {
        this.crash()
        nonNull = "Initialized"
    }

    fun crash() {
        nonNull.startsWith("foo") // crashes
    }
}

fun main(args: Array<String>) {
    Foo()
}

class Ex extends RuntimeException {
    public Object o;
    public Ex(Object a) { this.o = a; }
    static int leak(Object x) { throw new Ex(x); }
}

class A {
    public final int leak = Ex.leak(this);
    public final int thing = Integer.parseInt("42");
}

public class Test {
    static A make() {
        try {
            return new A();
        } catch (Ex x) {
            return (A)x.o;
        }
    }
    public static void main(String []args){
       A a = make();
       // a is uninitialised: its 'thing' field is zero
       System.out.println(a.thing);
    }
}

newtype Curry = Curry { r :: Curry -> Int }

f c = r c c
loop = f (Curry f)

type curry = { r : curry -> int }

let f c = c.r c
let loop = f { r = f }

interface Curry {
  public int r(Curry x);
}
static int loop() {
  Curry c = new Curry() {
    public int r(Curry x) { return x.r(x); }
  };
  return c.r(c);
}

enum Empty {}

type empty = |

data Empty

fn elim<T>(v : Empty) -> T { match v {} }

let elim (x : empty) = match x with _ -> .

{-# LANGUAGE EmptyCase #-}
elim :: Empty -> a
elim x = case x of {}

fn bottom() -> Empty { loop {} }

let bottom : empty =
  let rec loop () = loop () in loop ()

bottom :: Empty
bottom = bottom

let s : &str = elim(bottom());
println!("string: {}", s);

(* The OCaml compiler does not delete empty loops, so
   computing bottom correctly hangs rather than crashing *)
print_endline (elim bottom)

-- GHC does not delete empty loops, so
-- this correctly hangs rather than crashing
putStrLn (elim bottom)

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

data Eq a b where
  Refl :: Eq a a

Inductive eq {S : Set} : S -> S -> Prop :=
  Refl a : eq a a.

data Eq {S : Set} : S -> S -> Set where
  refl : (a : S) -> Eq a a

// Counterexample by Nada Amin and Ross Tate
class Unsound {
  static class Constrain<A, B extends A> {}
  static class Bind<A> {
    <B extends A>
    A upcast(Constrain<A,B> constrain, B b) {
      return b;
    }
  }
  static <T,U> U coerce(T t) {
    Constrain<U,? super T> constrain = null;
    Bind<U> bind = new Bind<U>();
    return bind.upcast(constrain, t);
  }
  public static void main(String[] args) {
    String zero = Unsound.<Integer,String>coerce(0);
  }
}

// Counterexample by Nada Amin and Ross Tate
object unsoundMini {
  trait A { type L >: Any}
  def upcast(a: A, x: Any): a.L = x
  val p: A { type L <: Nothing } = null
  def coerce(x: Any): Nothing = upcast(p, x)
  coerce("Uh oh!")
}

(* Counterexample by Stephen Dolan *)
type (_,_) eq = Refl : ('a, 'a) eq
let cast (type a) (type b) (Refl : (a, b) eq) (x : a) = (x : b)

let is_int (type a) =
  let rec (p : (int, a) eq) = match p with Refl -> Refl in
  p

let bang =
  (* segfaults *)
  print_string (cast (is_int : (int, string) eq) 42)

// Counterexample by Paolo G. Giarrusso
new {
  val a: String = (((1: Any): b.A): Nothing): String
  def loop(): Nothing = loop()
  val b: { type A >: Any <: Nothing } = loop()
}

// Counterexample by Lionel Parreaux
import scala.quoted.staging._

given Toolbox = Toolbox.make(getClass.getClassLoader)
trait T { type A >: Any <: Nothing }

withQuoteContext { '{ (x: T) => ${ 42: x.A } } }
// crashes with java.lang.ClassCastException

(* Counterexample by Jeremy Yallop *)
type _ t = T : string t

let f : type a. a t option code -> a -> unit code =
  fun c x -> .< match .~c with
  | None -> ()
  | Some T -> .~(print_endline x; .<()>.) >.

let _ = f .< None >. 0

// Counterexample by Paul Chiusano
/* The 'coinductive' view of streams, represented as their unfold. */
trait Stream[+A]
case class Unfold[S,+A](s: S, f: S => Option[(A,S)]) extends Stream[A]

object Stream {
  def fromList[A](a: List[A]): Stream[A] = 
    Unfold(a, (l:List[A]) => l.headOption.map((_,l.tail)))
}

/* If I have a Stream[Int], and I match and obtain an Unfold(s, f),
   the type of (s,f) should be (S, S => Option[(A,S)]) forSome { type S }.
   But Scala just promotes everything to Any: */
val res0 = Stream.fromList(List(1,2,3,4))
val res1 = res0 match { case Unfold(s, f) => s }
// res1: Any = List(1, 2, 3, 4)

/* Notice that the type of s is Any.
   Likewise, the type of f is also wrong, it accepts an Any: */

val res2 = res0 match { case Unfold(s, f) => f }
// res2: Any => Option[(Int, Any)] = <function1>

/* Since f expects Any, we can give it a String and get a runtime error: */

res0 match { case Unfold(s, f) => f("a string!") } // crashes

// Counterexample by Alan Jeffrey
public class Problem {
    // This code compiles, but produces a ClassCastException when executed
    // even though there are no explicit casts in the program.

    public static void main (String [] args) {
        Integer x = new Integer (5);
        String y = castit (x);
        System.out.println (y);
    }

    static <A,B> A castit (B x) {
        // This method casts any type to any other type.
        // Oh dear.  This shouldn't type check, but does
        // because build () returns a type Ref<*>
        // which is a subtype of RWRef<A,B>.
        final RWRef<A,B> r = build ();
        r.set (x);
        return r.get ();
    }

    static <A> Ref<A> build () {
        return new Ref<A> ();
    }
}

interface RWRef<A,B> {
    public A get ();
    public void set (B x);
}

class Ref<A> implements RWRef <A,A> {
    A contents;
    public void set (A x) { contents = x; }
    public A get () { return contents; }
}

// Counterexample by Stephen Compall
trait Magic {
  type S
  def init: S
  def step(s: S): String
}

case class Pair[A](left: A, right: A)

object Main extends App {
  type Aux[A] = Magic {type S = A}

  // I can't call this one from outerd,
  def outertp[A](p: Pair[Aux[A]]) =
    p.right.step(p.left.init)

  // but I can call this one.
  def outere(p: Pair[Aux[E]] forSome {type E}) =
    outertp(p)

  // This one means the left and the right may have *different* S.  I
  // shouldn't be able to call outere with p.
  def outerd(p: Pair[Magic]) =
    outere(p)

  def boom =
    outerd(Pair(new Magic {
                  type S = String
                  def init = "hi"
                  def step(s: S) = s.reverse
                },
                new Magic {
                  type S = Int
                  def init = 42
                  def step(s: S) = (s - 3).toString
                }))
  boom
}

// Counterexample by Victor Petukhov
class A<R1, K1>(val r1: R1, var k1: K1)
class B<R2, K2>(val r2: R2, val k2: K2)
interface I
class Q1 : I
class Q2 : I {
    fun x() = ""
}
fun <L, M> foo(x: A<L, M>, y: B<L, M>) {
    x.k1 = y.k2
}
inline fun <reified T : I> bar(): B<T, T> {
    val w = T::class.constructors.first().call()
    return B(w, w)
}
fun main() {
    val a1 = A(Q1(), Q2())
    val a = a1 as A<Q1, out Any?>
    foo(a, bar()) // type mismatch in NI
    println(a1.k1.x())
}

match x, y with
| 42, 0 -> "foo"
| 42, n -> "bar"
| n, _ -> "baz"

(* Counterexample by Stephen Dolan *)
type app = App : ('x -> unit) option * 'x -> app

let app1 = App (Some print_string, "hello")
let app2 = App (None, 42)

type t = { 
  a : bool; 
  mutable b : app
}

let f = function
| { a = false } -> assert false
| { a = true; b = App (None, _) } -> assert false 
| { a = true; b = App (Some _, _) } as r 
    when (r.b <- app2; false) -> assert false
| { b = App (Some f, x) } ->
   f x

let _ = f { a = true; b = app1 }

// Counterexample by Iulian Dragos
abstract class Bomb {
    type T
    val x: T

    def size(that: T): Int
}

class StringBomb extends Bomb {
    type T = String
    val x = "abc"
    def size(that: String): Int = that.length
}

class IntBomb extends Bomb { 
    type T = Int
    val x = 10

    def size(that: Int) = x + that
}

case class Mean(var bomb: Bomb)

object Main extends App {
    def foo(x: Mean) = x match {
        case Mean(b) => 
            // b is assumed to be a stable identifier, 
            // but it can actually be mutated
			println(b.size({ mutate(); b.x }))
	}

	def mutate() {
	   	m.bomb = new IntBomb
	}

	val m = Mean(new StringBomb)
	foo(m)
}

// Counterexample by Ariel Ben-Yehuda
fn main() {
    match Some(&4) {
        None => {},
        ref mut foo
            if {
                (|| { let bar = foo; bar.take() })();
                false
            } => {},
        Some(s) => println!("{}", *s)
    }
}

newtype EscapedString = EscapedString String

// Counterexample by David R. MacIver
object Test extends Application {
    case class L();
    object N extends L();

    def empty(xs : L) : Unit = xs match {
        case x@N => println(x); println(x);
    }

    empty(L())
}
/*
The compiler inserts a cast of xs to N.type, which is unsound:
The pattern match will succeed for any L, because N == L().
*/

// Counterexample by Andrew Kennedy
function mycast<T>(mixed $x, classname<T> $t) : T {
  if ($x instanceof $t) { return $x; }
  else throw new Exception("Type didn't match");
}
function expectListOfString(List<string> $x) { ... }

// If I write expectListOfString(mycast($y, List::class))
// but with $y having type List<int> then no exception will
// get thrown at runtime (because of generics erasure).

// Counterexample by William Chargin
// @flow
class Box<T> {
  +field: T;
  constructor(x) {
    this.field = x;
  }
}

function asBox<T>(x: T | Box<T>): Box<T> {
  if (x instanceof Box) {
    // Here, `x` is refined to be `Box<T>`. This is unsound: `T` could
    // well be `Box<U>` for some other `U`. Example below.
    return x;
  } else {
    // whatever
    return new Box(x);
  }
}

const stringStringBox: Box<Box<string>> = asBox(new Box("wat"));  // unsound!
stringStringBox.field.field.substr(0);  // runtime error

// Counterexample by Vladimir Reshetnikov
class A<T>(var value: T) {
    fun replaceValue(x: Any) : Any {
        class C(var v: T)
        if(x is C) {
            value = x.v
            return x
        }

        return C(value)
    }
}

fun main(args: Array<String>) {
    val a = A("string")
    a.replaceValue(A(0).replaceValue("something not of type C"))

    // a.value has type String, but now contains integer 0
    val s = a.value // crashes
}

// This function would do an unsound conversion from Integer to String
// because the cls.cast always passes: it's only checking List
static String bad(Class<List<String>> cls) {
    List<Integer> i = Arrays.asList(42);
    List<String> badList = cls.cast(i);
    String badString = badList.get(0);
    return badString;
}

// But Java provides no way to get a Class<List<String>>.
// (Arrays.asList("a").getClass() is a Class<? extends List>)

// Counterexample by Hiromasa Kido
class A{
       public int compareTo(Object o){ return 0; }
}
class B extends A implements Comparable<B>{
       public int compareTo(B b){ return 0; }
       public static void main(String[] argv){
               System.out.println(new B().compareTo(new Object()));
       }
}

// Counterexample by Kota Mizushima
// (translation of Java counterexample, with the same effect)
class A {
  def compareTo(o: Any): Int = 0
}
class B extends A with Comparable[B] {
  def compareTo(b: B): Int = 0
}
object C {
  def main(args: Array[String]): Unit = {
    println(new B().compareTo(new Object()))
  }
}

// Counterexample by Paul Phillips
object Test {
  class MyGraph[V <: Any] {
    def addVertex(v: V): Boolean = true
  }

  type DuckGraph = {
    def addVertex(vertex: Int): Boolean
  }

  def fail(graph: DuckGraph) = graph addVertex 1

  def main(args: Array[String]): Unit = {
    fail(new MyGraph[Int])
  }
}

type (_,_) eq = Refl : ('a, 'a) eq
type ('a, 'b) either = Left of 'a | Right of 'b

let f (x : (string, (int,string) eq) either) =
  match x with
  | Left s -> s
  (* no case for Right, and yet the match is exhaustive *)

-- Agda can reason about distinctness of more than just types
open import Agda.Builtin.String
data Eq (a : String) : String -> Set where
  Refl : Eq a a

data Sum (A B : Set) : Set where
  Left : A -> Sum A B
  Right : B -> Sum A B

f : Sum String (Eq "foo" "bar") -> String
f (Left s) = s
f (Right ()) -- "()" is the absurd pattern

// Counterexample by Aleksander Boruch-Gruszecki
object Test {
  sealed trait EQ[A, B]
  final case class Refl[T]() extends EQ[T, T]

  def absurd[F[_], X, Y](eq: EQ[F[X], F[Y]], x: X): Y = eq match {
    case Refl() => x
  }

  var ex: Exception = _
  try {
    type Unsoundness[X] = Int
    val s: String = absurd[Unsoundness, Int, String](Refl(), 0)
  } catch {
    case e: ClassCastException => ex = e
  }

  def main(args: Array[String]) =
    assert(ex != null)
}

-- Counterexample by Andreas Abel
{-# OPTIONS --injective-type-constructors #-}

open import Common.Prelude
open import Common.Equality

abstract
  f : Bool → Bool
  f x = true

  same : f true ≡ f false
  same = refl

not-same : f true ≡ f false → ⊥
not-same ()

absurd : ⊥
absurd = not-same same

data Equ a b where
  Refl : Equ a a

-- not in fact unsound! see below
everythingIsInjective :: Equ (f a) (f b) -> Equ a b
everythingIsInjective Refl = Refl

type family Foo :: * -> *
type family Bar a :: *

type instance Bar a = Int

eqFoo :: Equ (Foo a) (Foo b) -> Equ a b
eqFoo = everythingIsInjective -- works

eqBar :: Equ (Bar a) (Bar b) -> Equ a b
eqBar = everythingIsInjective -- error

-- Counterexample by Akio Takano
-- Base.hs
{-# LANGUAGE TypeFamilies #-}
module Base where

-- This program demonstrates how Int can be cast to (IO String)
-- using GHC 7.6.3.
type family F a
type instance F (a -> a) = Int
type instance F (a -> a -> a) = IO String

-- Given this type family F, it is sufficient to prove
-- (LA -> LA) ~ (LA -> LA -> LA)
-- for some LA. This needs to be done in such a way that
-- GHC does not notice LA is an infinite type, otherwise
-- it will complain.
--
-- This can be done by using 2 auxiliary modules, each of which
-- provides a fragment of the proof using different partial knowledge
-- about the definition of LA.
--
-- LA -> LA
-- = {LA~LB->LB} -- only Int_T.hs knows this
-- LA -> LB -> LB
-- = {LA~LB}     -- only T_IOString.hs knows this
-- LA -> LA -> LA
type family LA
type family LB
data T = T (F (LA -> LB -> LB))

-- Int_T.hs
{-# LANGUAGE TypeFamilies, UndecidableInstances #-}
module Int_T where
import Base
type instance LA = LB -> LB

int_t0 :: Int -> T
int_t0 = T

-- T_IOString.hs
{-# LANGUAGE TypeFamilies, UndecidableInstances #-}
module T_IOString where
import Base
type instance LB = LA

t_ioString :: T -> IO String
t_ioString (T x) = x

-- Main.hs
import Int_T
import T_IOString

main :: IO ()
main = t_ioString (int_t0 100) >>= print

(* Counterexample by Stephen Dolan *)
type (_, _) eqp = Y : ('a, 'a) eqp | N : string -> ('a, 'b) eqp
let f : ('a list, 'a) eqp -> unit = function N s -> print_string s

(* Using recursive modules, we can construct a type t = t list,
   even without -rectypes: *)

module rec A : sig
  type t = B.t list
end = struct
  type t = B.t list
end and B : sig
  type t
  val eq : (B.t list, t) eqp
end = struct
  type t = A.t
  let eq = Y
end

(* The expression f B.eq segfaults *)

(* Counterexample by Gabriel Scherer and Benoît Vaugon *)
(* blah.ml, compiled without -rectypes *)
type ('a, 'b, 'c) eqtest =
  | Refl : ('a, 'a, float) eqtest
  | Diff : ('a, 'b, int) eqtest

let test : type a b . (unit -> a, a, b) eqtest -> b = function
  | Diff -> 42

(* bluh.ml, compiled with -rectypes *)
let () =
  print_float Blah.(test (Refl : (unit -> 'a as 'a, 'a, _) eqtest))

interface Base {
    name: string;
}
interface Sub {
    name: string;
    doStuff: () => number;
}

class A {
    go(_ : Base) {}
}
class B extends A {
    go(x : Sub) { x.doStuff(); }
}

let x : Base = { name: "x" };
let b = new B();
let a : A = b;
a.go(x); // crashes

-- Counterexample by W. R. Cook
class Base feature
  base (n : Integer) : Integer
    do Result := n * 2 end;
end
---
class Extra inherit Base feature
  extra (n : Integer) : Integer
    do Result := n * n end;
end
---
class P2 feature
  get (arg : Base) : Integer
    do Result := arg.base(1) end
end
---
class C2 inherit P2 redefine get end feature
  get (arg : Extra) : Integer
    do Result := arg.extra(2) end
end
---
  local
    a : Base
    v : P2
    b : C2
    i : Integer
  do
    create a;
    create b;
    v := b;
    i := v.get(a) -- crashes!
  end

class type base = object
  method name : string 
end
class type sub = object
  method name : string
  method do_stuff : int
end

class a = object
  method go (_ : base) = ()
end

class b = object (self : < go : sub -> int; .. >)
  (* does not compile *)
  inherit a
  method! go (x : sub) = x#doStuff
end

class A {
  public void go(Object arg) {}
}
class B : A {
  // does not compile
  public override void go(String arg) {}
}

// Counterexample by Ben Pious
class C<T> {

    let t: T

    init(t: T) {
        self.t = t
        type(of: self).f()(self)
    }

    class func f<U>() -> (U) -> () where U: C  {
        return { (u: U) in
            print(u.t)
        }
    }
}

class E {
    let g = "Expected to Print"
}

class D: C<E> {
    override class func f<U>() -> (U) -> () where U: E {
        return { (u: E) in
            print(u.g)
        }
    }
}

let d = D(t: E()) // prints random garbage

class c (name : string) =
  object (self : 'self)
    method name = name
    method equals (x : 'self) =
      (name = x#name)
  end

class d (name : string) (size : int) =
  object
    inherit c name as super
    method size = size
    method equals (x : 'self) =
      (super#equals x && size = x#size)
  end

let sub (x : d) = (x :> c)
(* OCaml correctly rejects this coercion:
   despite inheriting from it, d is not a subtype of c *)

// Counterexample by Hamish Knight
protocol P {
  associatedtype X where X == Self
  func foo() -> X
}

class C : P {
  typealias X = C
  func foo() -> X {
    return C()
  }
}
class D : C {
    var name = "D"
}

func foo<T : P>(_ x: inout T) {
  x = x.foo()
}

var d = D()
foo(&d)
print(d.name) // crashes

// Counterexample by Niko Matsakis
trait Make {
    fn make() -> Self;
}

impl Make for *const uint {
    fn make() -> *const uint {
        ptr::null()
    }
}

fn maker<M:Make>() -> M {
    Make::make()
}

fn main() {
    let a: *uint = maker::<*uint>();
    // we have "produced" a *uint even though there is no
    // function in this program that returns one.
}

class Box<+X> {
  // allowed, X is an output (covariant)
  public X get() { ... }

  // disallowed, X is an input (contravariant)
  public void set(X x) { ... }
}

// Counterexample by Emir et al.
class Bad<+X> {
  private X item;
  public void BadAccess(Bad<string> bs) {
    Bad<object> bo = bs;
    bo.item = new Button(); // we just wrote a button as a string
  }
}

// Counterexample by Andrew Kennedy
class Box<+T> {
  // OK, we've got a private field whose type involves the covariant T
  public function __construct(private T $elem) {
  }

  // As usual, a (safe) getter method
  public function get(): T { return $this->elem; }

  // Private gives us access to arbitrary instances of Box, even in static
  // methods. Note the use of covariant subtyping to put a string in
  // a Box<mixed>
  public static function updateAsString(Box<mixed> $x, string $s) : void {
    $x->elem = $s;
  }

  // We can now use this method to overwrite an integer with a string
  // but return it as an integer
  public static function morphIntToString(int $i) : int {
    $x = new Box($i);
    Box::updateAsString($x, 'hey you turned me into a string');
    return $x->get();
  }

  // Actually do it
  public static function useBox(): void {
    $i = Box::morphIntToString(23);
    echo('this should be an integer: ' . $i);
  }
}

// Counterexample by Jason Zaugg
trait A[+X] {
  protected[this] def f(x: X): X = x
}

trait B extends A[B] {
  def kaboom = f(new B {})
}

// protected[this] disables variance checking
// of the signature of `f`.
//
// C's parent list unifies A[B] with A[C]
//
// The protected[this] loophole is widely used
// in the collections, every newBuilder method
// would fail variance checking otherwise.
class C extends B with A[C] {
  override protected[this] def f(c: C) = c
}

// java.lang.ClassCastException: B$$anon$1 cannot be cast to C
//  at C.f(<console>:15)
new C().kaboom

// Counterexample by Derek Lam
abstract class Base[+T] {
  protected[this] type TSeq <: MutableList[T]
  val v: TSeq
}

class Sub extends Base[Int] {
  type TSeq = MutableList[Int]
  val v = MutableList(42)
}

val x = new Sub()
(x: Base[Any]).v += "string!"
x.v.last + 42
// java.lang.ClassCastException: java.lang.String cannot be cast to java.lang.Integer

(* Counterexample by Claudio Russo *)
module F = functor (X:sig val b:bool end)
  unpack
    if X.b then
      pack struct
        type t = int
        val x = 1
        fun y n = -n
      end
      as sig 
        type t
        val x : t
        val y : t -> t
      end
    else
      pack struct
        type t = bool
        val x = true
        fun y b = if b then false else true
      end
      as sig
        type t
        val x : t
        val y : t -> t
      end
end
as sig
  type t
  val x : t
  val y : t → t
end
module A = F (struct val b = true end)
module B = F (struct val b = false end)
val z = A.y B.x

// Counterexample by Vladimir Reshetnikov
trait A {
  type T
  var v : T
}

object B {
  def f(x : { val y : A }) { x.y.v = x.y.v } 

  var a : A = _
  var b : Boolean = false
  def y : A = {
    if(b) {
      a = new A { type T = Int; var v = 1 }
      a
    } else {
      a = new A { type T = String; var v = "" }
      b = true
      a
    }
  }
}

// B.f(B) causes a ClassCastException

module X = struct type t = int end
module FX = F (X)                           (* ok *)
type t1 = (F (X)).t                         (* ok *)
module FX = F (struct type t = int end)     (* ok *)
type t2 = (F (struct type t = int end)).t   (* error *)

module type S = sig type t end
module F (X : S) = struct type u = X.t type v = X.t end
module AppF = F((struct type t = int end : S))

module AppF : sig type u type v end

module G (X : S) = struct type u = X.t type v = u end

module AppG : sig type u type v = u end

// Counterexample by Guillaume Martres
class Contra[-T >: Null]

object Test {
  def foo = {
    class A
    new Contra[A]
  }
}
// The inferred type of foo is Contra[Nothing],
// but this isn't a legal type

module F : sig
 (* Deleting '= float' on the line below
    makes this program compile *)
 type t = float
end = struct
 type t = float
end

module M : sig
 type t
 type r = { foo : t }
end = struct
 type t = F.t
 type r = { foo : t }
end

(* Counterexample by Stephen Dolan *)
type (_, _) eq = Eq : ('a, 'a) eq
let cast : type a b . (a, b) eq -> a -> b =
  fun Eq x -> x

module Fix (F : sig type 'a f end) = struct
  type 'a fix = ('a, 'a F.f) eq
  let uniq (type a) (type b)
    (Eq : a fix) (Eq : b fix) : (a, b) eq =
    Eq
end

module FixId = Fix (struct type 'a f = 'a end)
let bad : (int, string) eq = FixId.uniq Eq Eq
let _ = Printf.printf "Oh dear: %s" (cast bad 42)

type A >: String <: Int
// Error: lower bound String does not conform to upper bound Int

// Counterexample by Nada Amin
trait O { type A >: Any <: B; type B >: A <: Nothing }
val o = new O {}
def id(a: Any): Nothing = (a: o.B)
id("Boom")

{-# LANGUAGE RankNTypes #-}

idful :: (forall a. a -> a) -> (Int,String)
idful id = (id 5, id "hello")

g f = idful (\x -> let _ = f x in x)
-- GHC error:
--     Couldn't match expected type ‘a -> p0’ with actual type ‘p’
--     because type variable ‘a’ would escape its scope

type idful = { id : 'a . 'a -> 'a }
let idful i = i.id 5, i.id "hello"

let g f = idful { id = fun x -> f x; x }
(* Error: This field value has type 'b -> 'b which is less general than
         'a. 'a -> 'a *)

-- Counterexample by Simon Peyton Jones
{-# LANGUAGE MultiParamTypeClasses, TypeFamilies, FlexibleContexts #-} 

module Foo where

type family F a

class C b where {}

foo :: a -> F a
foo x = error "urk"

h :: (b -> ()) -> Int
h = error "urk"

f = h (\x -> let g :: C (F a) => a -> Int
                 g y = length [x, foo y]
             in ())
-- Causes an internal compiler error in Core Lint

(* Counterexample by Leo White *)
let (n : 'b -> < m : 'a . ([< `Foo of int] as 'b) -> 'a >) = 
  fun x -> object
    method m : 'x. [< `Foo of 'x] -> 'x = fun x -> assert false
  end;;
(* Type inference gave:
   Error: Values do not match:
          val n : ([< `Foo of int & 'a ] as 'b) -> < m : 'a0. 'b -> 'a0 >
        is not included in
          val n : ([< `Foo of int & 'a ] as 'b) -> < m : 'a0. 'b -> 'a0 >
   Note the & 'a in the argument type.
   That is the univar from 'a . ([< `Foo of int] as 'b) -> 'a.
   (Unknown whether this is a soundness issue) *)

// Counterexample by @WildCryptoFox
fn f<I>(i: I)
where
    I: IntoIterator,
    I::Item: for<'a> Into<&'a ()>,
{}

fn main() {
    // triggers internal compiler error
    f(&[f()]);
}

// Counterexample by Nada Amin
object Test {
  trait A { a =>
    type X
    val x: a.X
  }
  val a = new A {
    type X = Int
    val x = 1
  }
  def f(arg: A): arg.X = arg.x
  val x = f(a: A)
  // Inferred type of x references out-of-scope 'arg'
  // (Still unknown whether this is a soundness issue)
}

type empty = |
type (_,_) eq =
  Refl : ('a, 'a) eq
let f (x : empty) =
  let eq : (int, string) eq = match x with _ -> . in
  ...

{-# LANGUAGE EmptyCase #-}
data Empty
data Eq a b where
  Refl :: Eq a a

f :: Empty -> ...
f x = ...
  where
    eq : Eq Int String
    eq = case x of {}

(* Counterexample by Maxime Dénès *)
Require Import ClassicalFacts.

Section func_unit_discr.
Hypothesis Heq : (False -> False) = True.
Fixpoint contradiction (u : True) : False :=
  contradiction (
    match Heq in (_ = T) return T with
    | eq_refl => fun f:False => match f with end
    end
  ).
End func_unit_discr.

Lemma foo : provable_prop_extensionality -> False.
Proof.
  intro; apply contradiction.
  apply H.
  trivial.
  trivial.
Qed.

-- Andreas Abel, 2014-01-10
-- Code by Jesper Cockx and Conor McBride and folks from the Coq-club

{-# OPTIONS --without-K #-}

-- An empty type.

data Zero : Set where

-- A unit type as W-type.

mutual
  data WOne : Set where wrap : FOne -> WOne
  FOne = Zero -> WOne

-- Type equality.

data _<->_ (X : Set) : Set -> Set where
  Refl : X <-> X

-- This postulate is compatible with univalence:

postulate
  iso : WOne <-> FOne

-- But accepting that is incompatible with univalence:

noo : (X : Set) -> (WOne <-> X) -> X -> Zero
noo .WOne Refl (wrap f) = noo FOne iso f

-- Matching against Refl silently applies the conversion
-- FOne -> WOne to f.  But this conversion corresponds
-- to an application of wrap.  Thus, f, which is really
-- (wrap f), should not be considered a subterm of (wrap f)
-- by the termination checker.
-- At least, if we want to be compatible with univalence.

absurd : Zero
absurd = noo FOne iso (\ ())

(* Counterexample by Maxime Dénès *)
CoInductive CoFalse : Prop := CF : CoFalse -> False -> CoFalse.

CoInductive Pandora : Prop := C : CoFalse -> Pandora.

Axiom prop_ext : forall P Q : Prop, (P<->Q) -> P = Q.

Lemma foo : Pandora = CoFalse.
  apply prop_ext.
  constructor.
  intro x; destruct x; assumption.
  exact C.
Qed.

CoFixpoint loop : CoFalse :=
  match foo in (_ = T) return T with eq_refl => C loop end.

Definition ff : False := match loop with CF _ t => t end.

-- Counterexample by Andreas Abel
open import Common.Coinduction
open import Common.Equality

prop = Set

data False : prop where

data CoFalse : prop where
  CF : False → CoFalse

data Pandora : prop where
  C : ∞ CoFalse → Pandora

postulate
  ext : (CoFalse → Pandora) → (Pandora → CoFalse) → CoFalse ≡ Pandora

out : CoFalse → False
out (CF f) = f

foo : CoFalse ≡ Pandora
foo = ext (λ{ (CF ()) }) (λ{ (C c) → CF (out (♭ c))})

loop : CoFalse
loop rewrite foo = C (♯ loop)

false : False
false = out loop

-- Counterexample by Stefan O'Rear
{-# OPTIONS_GHC -ftype-families #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
data family Z :: * -> *

newtype Moo = Moo Int

newtype instance Z Int = ZI Double
newtype instance Z Moo = ZM (Int,Int)

newtype Moo = Moo Int deriving(IsInt)
class IsInt t where
    isInt :: c Int -> c t
instance IsInt Int where isInt = id
main = case isInt (ZI 4.0) of
         ZM tu -> print tu -- segfaults

(* Counterexample by Rowan Davies and Frank Pfenning *)
(* Suppose we have types nat and pos,
   where nat is nonnegative integers
   and pos is its subtype of positive integers *)
let x : nat ref ∧ pos ref = ref 1 in
let () = (x := 0) in   (* typechecks: x is a nat ref *)
let z : pos = !x in    (* typechecks: x is a pos ref *)
z : pos                (* now we have the positive number zero *)

(* Counterexample by Rowan Davies and Frank Pfenning *)
let f : (unit → nat ref) ∧ (unit → pos ref) =
  fun () → ref 1 in        (* passes the value restriction *)
let f' : unit → (nat ref ∧ pos ref) =
  f in                     (* uses the above rule *)
let x : nat ref ∧ pos ref = f ()
let () = (x := 0) in
let z : pos = !x in
z : pos                    (* same problem as before *)

function numberwang(x: number | string): string {
  if (typeof x === "number") {
    // in this block, `x: number`
    return `half of ${x * 2}`;
  } else {
    // in this block, `x: string`
    return `a string with ${x.length} characters`;
  }
}

class Dog {
  name: string;
  constructor(name: string) { this.name = name; }
}
class Car {
  wheels: number;
  constructor(wheels: number) { this.wheels = wheels; }
}

function description(x: Dog | Car): string {
  if (x instanceof Dog) {
    // in this block, `x: Dog`
    return `the dog ${x.name}`;
  } else {
    // in this block, `x: Car`
    return `a car with ${x.wheels} wheels`;
  }
}

function orSingleton<T>(x: T | Array<T>): Array<T> {
  if (x instanceof Array) {
    return x;
  }
  return [x];
}

// Purports to be the identity function, but fails when `x` happens to
// be an array.
function id<T>(x: T): T {
  const singletonArray: T[] = orSingleton(x);
  return singletonArray[0];
}

const digits: number[] = id([3, 1, 4]);
// unsound: `digits` is actually `3`
digits.includes(4);  // TypeError: digits.includes is not a function

// Counterexample by Lionel Parreaux
def test[A]: List[Int] | A => Int =
  { case ls: List[Int] => ls.head  case _ => 0 }
test(List("oops")) // crashes

#lang typed/racket

(: valid-refinement (All (T) (U Number (Boxof T)) (-> Number T) -> T))
(define (valid-refinement x from-number)
  (if (box? x)
      (unbox x)  ;; works: must be a `Boxof T` (good)
      (from-number x)))

(: invalid-refinement (All (T) (U T (Boxof T)) -> T))
(define (invalid-refinement x)
  (if (box? x)
      (unbox x)  ;; type error here: could be a box of something else (good!)
      x))

type ElementOrArray<T> =
  {type: "ELEMENT", value: T} | {type: "ARRAY", array: T[]};

function orSingleton<T>(x: ElementOrArray<T>): T[] {
  if (x.type === "ARRAY") {
    return x.array;
  }
  return [x.value];
}

// Actually the identity function.
function id<T>(x: T): T {
  const singletonArray: T[] = orSingleton({type: "ELEMENT", value: x});
  return singletonArray[0];
}

-- rejected by Coq
Inductive bad := r (c : bad -> nat).

-- rejected by Agda
data Bad : Set where
  r : (Bad → ℕ) → Curry

-- also rejected by Coq
Inductive bad2 := r (c : (bad2 -> nat) -> nat).

-- also rejected by Agda
data Bad2 : Set where
  r : ((Bad2 → ℕ) → ℕ) → Bad2

(* Counterexample by Thierry Coquand and Christine Paulin
   Translated into Coq by Vilhelm Sjöberg *)

(* Phi is a positive, but not strictly positive, operator. *)
Definition Phi (a : Type) := (a -> Prop) -> Prop.

(* If we were allowed to form the inductive type
     Inductive A: Type :=
       introA : Phi A -> A.
   then among other things, we would get the following. *)
Axiom A : Type.
Axiom introA : Phi A -> A.
Axiom matchA : A -> Phi A.
Axiom beta : forall x, matchA (introA x) = x.

(* In particular, introA is an injection. *)
Lemma introA_injective : forall p p', introA p = introA p' -> p = p'.
Proof.
  intros.
  assert (matchA (introA p) = (matchA (introA p'))) as H1 by congruence.
  now repeat rewrite beta in H1.
Qed.

(* However, ... *) 

(* Proposition: For any type A, there cannot be an injection
   from Phi(A) to A. *)

(* For any type X, there is an injection from X to (X->Prop),
   which is λx.(λy.x=y) . *)
Definition i {X:Type} : X -> (X -> Prop) := 
  fun x y => x=y.

Lemma i_injective : forall X (x x' :X), i x = i x' -> x = x'.
Proof.
  intros.
  assert (i x x = i x' x) as H1 by congruence.
  compute in H1.
  symmetry.
  rewrite <- H1.
  reflexivity.
Qed.  

(* Hence, by composition, we get an injection f from A->Prop to A. *)
Definition f : (A->Prop) -> A 
  := fun p => introA (i p).

Lemma f_injective : forall p p', f p = f p' -> p = p'.
Proof.
  unfold f. intros.
  apply introA_injective in H. apply i_injective in H. assumption.
Qed.

(* We are now back to the usual Cantor-Russel paradox. *)
(* We can define *)
Definition P0 : A -> Prop
  := fun x => 
       exists (P:A->Prop), f P = x /\ ~ P x.
  (* i.e., P0 x := x codes a set P such that x∉P. *)

Definition x0 := f P0.

(* We have (P0 x0) iff ~(P0 x0) *)
Lemma bad : (P0 x0) <-> ~(P0 x0).
Proof.
split.
  * intros [P [H1 H2]] H.
    change x0 with (f P0) in H1.
    apply f_injective in H1. rewrite H1 in H2.
    auto.
  * intros.
    exists P0. auto.
Qed.

(* Hence a contradiction. *)
Theorem worse : False.
  pose bad. tauto.
Qed.

type 'a g = G_int : { name : string } -> int g

type 'a c = { name: string } constraint 'a = int

sealed trait G[T]
case class G_int(i: Int) extends G[Int]

class C[A >: Int <: Int](name : String)

type ok = string g

type bad = string c
(* Error: This type string should be an instance of type int *)

type Ok = G[String]

type Bad = C[String]
// Error: type arguments [A] do not conform to
// class C's type parameter bounds [A >: Int <: Int]

let poly : 'a . 'a c -> string =
  fun _ -> "hello"
(* Error: The universal type variable 'a cannot be generalized:
          it is bound to int. *)

def poly[A](x: C[A]): String = "hello"
// Error: type arguments [A] do not conform to
// class C's type parameter bounds [A >: Int <: Int]

// Counterexample by Aaron Turon
static UNIT: &'static &'static () = &&();

fn foo<'a, 'b, T>(_: &'a &'b (), v: &'b T) -> &'a T { v }

fn bad<'c, T>(x: &'c T) -> &'static T {
    let f: fn(&'static &'c (), &'c T) -> &'static T = foo;
    f(UNIT, x)
}

fn foo<'a, 'b, T> (_: &'a &'b (), v: &'b T) -> &'a T

fn foo<'a, 'b, T> (_: &'a &'static (), v: &'b T) -> &'a T

fn foo<T> (_: &'static &'static (), v: &'c T) -> &'static T