unison/unison-src/transcripts/fix2254.output.md

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:

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 fork of the a namespace:

.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

.> fork a a2

  Done.

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.

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:

.a2> update.old

  ⍟ I've updated these names to your new definition:
  
    type A a b c d

.a2> view A NeedsA f f2 f3 g

  type A a b c d
    = B b
    | D d
    | E a d
    | C c
    | A a
  
  structural type NeedsA a b
    = Zoink Text
    | NeedsA (A a b Nat Nat)
  
  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

.a2> todo

  ✅
  
  No conflicts or edits in progress.

Record updates

Here's a test of updating a record:

structural type Rec = { uno : Nat, dos : Nat }

combine r = uno r + dos r

  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

.a3> 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

structural type Rec = { uno : Nat, dos : Nat, tres : Text }

  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:

.> fork a3 a4

  Done.

.a4> update.old

  ⍟ I've added these definitions:
  
    Rec.tres        : Rec -> Text
    Rec.tres.modify : (Text ->{g} Text) -> Rec ->{g} Rec
    Rec.tres.set    : Text -> Rec -> Rec
  
  ⍟ I've updated these names 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

.a4> todo

  ✅
  
  No conflicts or edits in progress.