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 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 ⍟ I've added these definitions: type A a b c d structural type NeedsA a b f : A Nat Nat Nat Nat -> Nat f2 : A Nat Nat Nat Nat -> Nat f3 : NeedsA Nat Nat -> Nat g : A Nat Nat Nat Nat -> Nat scratch/a> branch /a2 Done. I've created the a2 branch based off of a. Tip: To merge your work back into the a branch, first `switch /a` then `merge /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 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 Okay, I'm searching the branch for code that needs to be updated... That's done. Now I'm making sure everything typechecks... Everything typechecks, so I'm saving the results... Done. scratch/a2> view A NeedsA f f2 f3 g type A a b c d = A a | D d | E a d | B b | C c 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 Nat Nat Nat Nat -> Nat f2 a = use Nat + n = f a n + 1 f3 : NeedsA Nat Nat -> Nat f3 = cases NeedsA a -> f a Nat.+ 20 _ -> 0 g : A Nat Nat Nat Nat -> Nat g = cases D n -> n _ -> 43 scratch/a2> todo You have no pending todo items. Good work! ✅ ``` ## Record updates Here's a test of updating a record: ``` unison structural type Rec = { uno : Nat, dos : Nat } combine r = uno r + dos r ``` ``` ucm Loading changes detected in scratch.u. I found and typechecked these definitions in scratch.u. If you do an `add` or `update`, here's how your codebase would change: ⍟ These new definitions are ok to `add`: structural type Rec Rec.dos : Rec -> Nat Rec.dos.modify : (Nat ->{g} Nat) -> Rec ->{g} Rec Rec.dos.set : Nat -> Rec -> Rec Rec.uno : Rec -> Nat Rec.uno.modify : (Nat ->{g} Nat) -> Rec ->{g} Rec Rec.uno.set : Nat -> Rec -> Rec combine : Rec -> Nat ``` ``` ucm scratch/r1> add ⍟ I've added these definitions: structural type Rec Rec.dos : Rec -> Nat Rec.dos.modify : (Nat ->{g} Nat) -> Rec ->{g} Rec Rec.dos.set : Nat -> Rec -> Rec Rec.uno : Rec -> Nat Rec.uno.modify : (Nat ->{g} Nat) -> Rec ->{g} Rec Rec.uno.set : Nat -> Rec -> Rec combine : Rec -> Nat scratch/r1> branch r2 Done. I've created the r2 branch based off of r1. Tip: To merge your work back into the r1 branch, first `switch /r1` then `merge /r2`. ``` ``` unison structural type Rec = { uno : Nat, dos : Nat, tres : Text } ``` ``` ucm Loading changes detected in scratch.u. I found and typechecked these definitions in scratch.u. If you do an `add` or `update`, here's how your codebase would change: ⍟ These new definitions are ok to `add`: Rec.tres : Rec -> Text Rec.tres.modify : (Text ->{g} Text) -> Rec ->{g} Rec Rec.tres.set : Text -> Rec -> Rec ⍟ These names already exist. You can `update` them to your new definition: structural type Rec Rec.dos : Rec -> Nat Rec.dos.modify : (Nat ->{g} Nat) -> Rec ->{g} Rec Rec.dos.set : Nat -> Rec -> Rec Rec.uno : Rec -> Nat Rec.uno.modify : (Nat ->{g} Nat) -> Rec ->{g} Rec Rec.uno.set : Nat -> Rec -> Rec ``` And checking that after updating this record, there's nothing `todo`: ``` ucm scratch/r2> update Okay, I'm searching the branch for code that needs to be updated... That's done. Now I'm making sure everything typechecks... Everything typechecks, so I'm saving the results... Done. scratch/r2> todo You have no pending todo items. Good work! ✅ ```