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.

[athas]

I think I will solve this by banning specs having a size-lifted type. If it turns out people really want to write code like this, it can certainly be supported, but the plumbing is a little tricky, so I'd rather not do it without a good reason.