module Box[T: Library.Type] {
  rep type S = data {
    case box(unwrap: T)
    case tag(flag: Bool)
  }

  func mkTag() returns (res: S) { tag(true) }
  func getTag(b: S) returns (res: Bool) { b.flag }
}

module BoxTag = Box[Int]

lemma expected_instances() {
  val inferred: Box[Int] := Box.mkTag();
  assert Box.getTag(inferred);
  val annotated := (Box.mkTag() : Box[Int]);
  assert inferred == annotated;

  val named: BoxTag.S := Box.mkTag();
  assert BoxTag.getTag(named);
  assert Box.getTag(named);
  val explicit := BoxTag.mkTag();
  assert named == explicit;
}

module G[E: Library.Type] {
  func flag(b: Box[E]) returns (res: Bool) { Box.getTag(b) }
}

module GI = G[Int]

lemma shared_instance() {
  val b: Box[Int] := Box.mkTag();
  assert GI.flag(b);
  assert G.flag(b);
}