unison/unison-src/transcripts/fix2254.md
2024-07-11 12:45:44 -07:00

95 lines
1.6 KiB
Markdown

```ucm:hide
scratch/a> builtins.merge lib.builtins
```
This transcript checks that updates to data types propagate successfully to dependent types and dependent terms that do pattern matching. First let's create some types and terms:
```unison:hide
unique type A a b c d
= A a
| B b
| C c
| D d
structural type NeedsA a b = NeedsA (A a b Nat Nat)
| Zoink Text
f : A Nat Nat Nat Nat -> Nat
f = cases
A n -> n
_ -> 42
f2 a =
n = f a
n + 1
f3 : NeedsA Nat Nat -> Nat
f3 = cases
NeedsA a -> f a + 20
_ -> 0
g : A Nat Nat Nat Nat -> Nat
g = cases
D n -> n
_ -> 43
```
We'll make our edits in a new branch.
```ucm
scratch/a> add
scratch/a> branch /a2
scratch/a2>
```
First let's edit the `A` type, adding another constructor `E`. Note that the functions written against the old type have a wildcard in their pattern match, so they should work fine after the update.
```unison:hide
unique type A a b c d
= A a
| B b
| C c
| D d
| E a d
```
Let's do the update now, and verify that the definitions all look good and there's nothing `todo`:
```ucm
scratch/a2> update
scratch/a2> view A NeedsA f f2 f3 g
scratch/a2> todo
```
## Record updates
Here's a test of updating a record:
```ucm:hide
scratch/r1> builtins.merge lib.builtins
```
```unison
structural type Rec = { uno : Nat, dos : Nat }
combine r = uno r + dos r
```
```ucm
scratch/r1> add
scratch/r1> branch r2
```
```unison
structural type Rec = { uno : Nat, dos : Nat, tres : Text }
```
And checking that after updating this record, there's nothing `todo`:
```ucm
scratch/r2> update
scratch/r2> todo
```