merge precondition message: Stray constructor alias

[aryairani]

Stray constructor alias

Constructors may only exist within the corresponding decl's namespace.

Alice's branch:

project/alice> add

  ⍟ I've added these definitions:
  
    type Foo

project/alice> alias.term Foo.Bar AliasOutsideFooNamespace

  Done.

Bob's branch:

project/bob> add

  ⍟ I've added these definitions:
  
    bob : Nat

project/alice> merge bob

  On project/alice, the constructor AliasOutsideFooNamespace is
  not in a subnamespace of a name of its type. Please either
  delete it or rename it before merging.

---

Assuming it's hard to know at this stage whether there is already another name for AliasOutsideFooNamespace under Foo:

Sorry, I wasn't able to perform the merge, because I need all constructor names to be nested somewhere beneath the corresponding type name.

On project/alice, the constructor AliasOutsideFooNamespace is not nested beneath the corresponding type name.
Please either use rename to move it; or if it's an extra copy, you can simply delete it. Then try the merge again.

---

or if the type name is also available:

Sorry, I wasn't able to perform the merge, because I need all constructor names to be nested somewhere beneath the corresponding type name.

On project/alice, the constructor AliasOutsideFooNamespace is not nested beneath Foo.
Please either use rename to move it; or if it's an extra copy, you can simply delete it. Then try the merge again.