Propagating type edits

.> builtins.merge

We introduce a type Foo with a function dependent fooToInt.

use .builtin

unique type Foo = Foo

fooToInt : Foo -> Int
fooToInt _ = +42

And then we add it.

.subpath> add
.subpath> find.verbose
.subpath> view fooToInt

Then if we change the type Foo...

unique type Foo = Foo | Bar

and update the codebase to use the new type Foo...

.subpath> update

... it should automatically propagate the type to fooToInt.

.subpath> view fooToInt

We make a term that has a dependency on another term and also a non-redundant user-provided type signature.

use .builtin

someTerm : Optional foo -> Optional foo
someTerm x = x

otherTerm : Optional baz -> Optional baz
otherTerm y = someTerm y

Add that to the codebase:

.subpath.preserve> add

Let's now edit the dependency:

use .builtin

someTerm : Optional x -> Optional x
someTerm _ = None

Update...

.subpath.preserve> update

Now the type of someTerm should be Optional x -> Optional x and the type of otherTerm should remain the same.

.subpath.preserve> view someTerm
.subpath.preserve> view otherTerm

Cleaning up a bit...

.> delete.namespace subpath

Now, we make two terms, where one depends on the other.

use .builtin

someTerm : Optional foo -> Optional foo
someTerm x = x

otherTerm : Optional baz -> Optional baz
otherTerm y = someTerm y

We'll make two copies of this namespace.

.subpath.one> add
.subpath> fork one two

Now let's edit one of the terms...

use .builtin

someTerm : Optional x -> Optional x
someTerm _ = None

... in one of the namespaces...

.subpath.one> update

The other namespace should be left alone.

.subpath.two> view someTerm