define TypeTree {
  // Since TypeKey and LockedType each have a covariant param, setting the param
  // to any in Tree means that any param can be used in an assignment.
  //
  // The catch is that any cannot be converted to anything else, which means
  // that type information is no longer directly accessible. LockedType allows
  // the original type to be recovered via check, given the correct TypeKey.
  @value Tree<TypeKey<any>,LockedType<any>> tree

  new () {
    return TypeTree{ Tree<TypeKey<any>,LockedType<any>>.new() }
  }

  set (k,v) {
    \ tree.set(k,LockedType:create<?>(k,v))
    return self
  }

  remove (k) {
    \ tree.remove(k)
    return self
  }

  get (k) {
    scoped {
      optional LockedType<any> value <- tree.get(k)
    } in if (present(value)) {
      return require(value).check<?>(k)
    } else {
      return empty
    }
  }
}

define TypeKey {
  @category Int counter <- 0
  @value Int index

  new () {
    return TypeKey<#x>{ (counter <- counter+1) }
  }

  lessThan (l,r) {
    return l.get() < r.get()
  }

  equals (l,r) {
    return l.get() == r.get()
  }

  @value get () -> (Int)
  get () {
    return index
  }
}

/* An internal type used for storing a single value.
 *
 * The contained value is only accessible via the check function, which ensures
 * both that the key and the type match.
 */
concrete LockedType<|#x> {
  // Creates a new LockedType, e.g., LockedType:create<#x>(k,v).
  @category create<#x> (TypeKey<#x>,#x) -> (LockedType<#x>)

  // Returns the contained value if the key and type match, or empty otherwise.
  @value check<#y> (TypeKey<#y>) -> (optional #y)
}

define LockedType {
  @value TypeKey<#x> key
  @value #x value

  create (k,v) {
    return LockedType<#x>{ k, v }
  }

  check (k) {
    if (key `TypeKey<any>.equals` k) {
      // reduce is a builtin that returns value (as optional #y) iff #x -> #y.
      // The runtime type of value does not matter here; it just needs to be of
      // type optional #x at compile time.
      //
      // This is more like template meta-programming in C++ than it is like a
      // runtime type cast in Java. The reduce call could in theory be replaced
      // at compile time with either value or empty if parameter substitution
      // happened at compile time. (Like C++ does with templates.)
      return reduce<#x,#y>(value)
    } else {
      return empty
    }
  }
}