Resolution of constructor names

[favonia]

Proposal

NameRes should associate each constructor name to a list of {datatype : Name.t; clbl : string} which represents all possible interpretations. This will automatically support renaming, namespaces, shadowing, etc., correctly. A type checker should first consult the name resolver and then use typing information to disambiguate overloaded constructors if needed.

favonia: I think the following example should be forbidden due to self-shadowing:

data tt where tt

---

Spec of shadowing

These should work:

data bool where tt | ff
def tt : bool = ff
def x : [i] bool [i=0 -> tt | i=1 -> ff] = refl

data bool where tt | ff
def mybool : type = bool
def bool : type^1 = type
def x : mybool = tt

These should not work:

data bool where tt | ff
def tt : type^1 = type
data unit where tt
def x : bool = tt

These I do not know:

data bool where tt | ff
data tt where tt
def x : bool = tt

Thoughts? @ecavallo @jonsterling @cangiuli

[clayrat]

This also comes up when defining something like:

def prop/unit (A : type) (A/prop : is-prop A) (x0 : A) : equiv A unit = 
  iso→equiv A unit (λ _ → ★, λ _ → x0, unit/prop ★, A/prop x0)

def foo (A : type) (A/prop : is-prop A) (a : A) (i : 𝕀) : 
  ua A unit (prop/unit A A/prop a) i = 
  let uu : unit = ★ in `(vin i a uu)

Would be nice if the last line could be written directly as

`(vin i a ★)

[favonia]

Would be nice if the last line could be written directly as

`(vin i a ★)

This would be possible if the name resolver can confirm that ★ is a constructor used by only one data type. @jonsterling I wonder if you have anything to say?