unison icon indicating copy to clipboard operation
unison copied to clipboard

Changing constructors of a type leads to error about constructors being nested between the type

Open ceedubs opened this issue 3 months ago • 0 comments

Describe and demonstrate the bug

> builtins.merge

  Done.

Create a type

type Foo = Foo Nat

foo: Foo -> Nat
foo = cases Foo n -> n
  Loading changes detected in scratch.u.

  + type Foo

  + foo : Foo -> Nat

  Run `update` to apply these changes to your codebase.
> update

  Done.

Change the constructors of the type such that none of them match the previous name

It's expected that this doesn't update cleanly since we haven't fixed foo yet.

It's unexpected that I have to repeat this stanza twice for it to get picked up by the transcript runner...

type Foo = Bar Int | Baz Text
  Loading changes detected in scratch.u.

  ~ type Foo

  ~ (modified)

  Run `update` to apply these changes to your codebase.
> update

  Some definitions don't typecheck with your changes. I've
  update the file scratch.u with the definitions that need
  fixing. Once the file is compiling, try `update` again.

  I've also switched you to a new branch update-main for this
  work. On `update`, it will be merged back into main.
type Foo = Bar Int | Baz Text

-- The definitions below no longer typecheck with the changes above.
-- Please fix the errors and try `update` again.

foo : Foo -> Nat
foo = cases Foo n -> n

type Foo = Bar Int | Baz Text

foo: Foo -> Nat
foo = cases
  Bar i -> 0
  Baz t -> 1

The previous stanza got ignored, so try it again?

type Foo = Bar Int | Baz Text

foo: Foo -> Nat
foo = cases
  Bar i -> 0
  Baz t -> 1
  Loading changes detected in scratch.u.

  ~ type Foo

  ~ foo : Foo -> Nat

  (and 103 unchanged types and 512 unchanged terms)

  ~ (modified)

  Run `update` to apply these changes to your codebase.

Get error about constructors being nested below the type

I'm eliminating the Foo.Foo constructor, which I think that ucm should be able to tell by the new type Foo definition in my scratch file.

> update

🛑

The transcript failed due to an error in the stanza above. The error is:

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

The constructor Foo.Foo is not nested beneath the corresponding
type name. Please either use `move` to move it, or if it's an
extra copy, you can simply `delete` it. Then try updating again.

Screenshots If applicable, add screenshots to help explain your problem.

Environment (please complete the following information):

  • ucm --version 0b5d33643

ceedubs avatar Oct 06 '25 19:10 ceedubs