class Error extends Object { Error () { super (); } }

class Nat extends Object {
    Nat () { super (); }
    Object nth (List l) { return new Error (); }
}
class Zero extends Nat {
    Zero () { super (); }
    Object nth (List l) { return l.head (); }
}
class Succ extends Nat {
    Nat n;
    Succ (Nat n) { super (); this.n = n; }
    Object nth (List l) { return this.n.nth (l.tail ()); }
}

class List extends Object {
    List () { super (); }
    Object head () { return new Error (); }
    List   tail () { return (List)(Object)new Error (); }
    List append (List l) { return l; }
}
class Nil extends List {
    Nil () { super (); }
}
class Cons extends List {
    Object hd;
    List tl;
    Cons (Object hd, List tl) { super(); this.hd = hd; this.tl = tl; }
    Object head () { return this.hd; }
    List   tail () { return this.tl; }
    List append (List l) { return new Cons (this.hd, this.tl.append (l)); }
    // The following method should non type-check
    // List illTyped () { return this.append (new Zero()); }
}

Nat zero = new Zero();
Nat one  = new Succ(zero);
Nat two  = new Succ(one);

List l21  = new Cons (two, new Cons (one, new Nil ()));
List l0   = new Cons (zero, new Nil ());
List l210 = l21.append (l0);

Nat a = (Nat) two.nth (l210);

List empty = new Nil();
List empt1 = l0.tail();

// The following expressions should not type-check
// List ill  = l210.append (zero);
// List ill2 = new Cons (new Zero(), new Zero ());

// These are legal casts:
List l0v0 = (List) l0;
Object l0v1 = (Object) l0;
List l0v2 = (List) l0v1;

// The following expressions should raise class cast exceptions
// List err1  = l0.tail().tail();
// List error = empty.tail ();