Module ascription does not type check

[athas]

module type dict = {
  type~ dict
  val empty : dict
}

module naive_dict : dict = {
  type~ dict = []bool
  def empty = []
}

The problem is related to how we handle size-lifted types in module ascriptions. We end up requiring that empty can produce an array of any size, because after substitution its type scheme becomes val empty [d₀] : [d₀]bool. Probably we should lift these anonymous sizes to the top level instead of attaching them as size parameters.