Skip to content

Commit

Permalink
add transcript demonstrating 4424
Browse files Browse the repository at this point in the history
  • Loading branch information
tstat committed Nov 28, 2023
1 parent 79eeee7 commit 1956322
Show file tree
Hide file tree
Showing 2 changed files with 166 additions and 0 deletions.
55 changes: 55 additions & 0 deletions unison-src/transcripts/fix4424.md
Original file line number Diff line number Diff line change
@@ -0,0 +1,55 @@
```ucm:hide
.> builtins.merge
```

Some basics:

```unison:hide
unique type Cat.Dog = Mouse Nat
unique type Rat.Dog = Bird
countCat = cases
Cat.Dog.Mouse x -> Bird
```

```ucm
.> add
```

Now I want to add a constructor.

```unison:hide
unique type Rat.Dog = Bird | Mouse
```

```ucm:error
.> update
```

Here's the code that `update` produced:

```unison:error
countCat : Cat.Dog -> Rat.Dog
countCat = cases Mouse x -> Bird
unique type Rat.Dog = Bird | Mouse
```

Okay, hmm. TBH I think this code should have type-checked without user intervention, but the way it printed (`cases Mouse x`) is ambiguous, and UCM assumed `Mouse` meant `Rat.Dog.Mouse` instead of `Cat.Dog.Mouse`, which caused parsing to fail.

I'll fix it by making it explicit:

```unison
countCat : Cat.Dog -> Rat.Dog
countCat = cases Cat.Dog.Mouse x -> Bird
unique type Rat.Dog = Bird | Mouse
```

Ok, all set! Now let's update.

```ucm:error
.> update
```

Why is it still printing just `Mouse` and failing?
111 changes: 111 additions & 0 deletions unison-src/transcripts/fix4424.output.md
Original file line number Diff line number Diff line change
@@ -0,0 +1,111 @@
Some basics:

```unison
unique type Cat.Dog = Mouse Nat
unique type Rat.Dog = Bird
countCat = cases
Cat.Dog.Mouse x -> Bird
```

```ucm
.> add
⍟ I've added these definitions:
unique type Cat.Dog
unique type Rat.Dog
countCat : Cat.Dog -> Rat.Dog
```
Now I want to add a constructor.

```unison
unique type Rat.Dog = Bird | Mouse
```

```ucm
.> update
Okay, I'm searching the branch for code that needs to be
updated...
That's done. Now I'm making sure everything typechecks...
countCat : Cat.Dog -> Rat.Dog
countCat = cases Mouse x -> Bird
unique type Rat.Dog = Bird | Mouse
Typechecking failed. I've updated your scratch file with the
definitions that need fixing. Once the file is compiling, try
`update` again.
```
Here's the code that `update` produced:

```unison
countCat : Cat.Dog -> Rat.Dog
countCat = cases Mouse x -> Bird
unique type Rat.Dog = Bird | Mouse
```

```ucm
This pattern has the wrong number of arguments
2 | countCat = cases Mouse x -> Bird
The constructor has type
Rat.Dog
but you supplied 1 arguments.
```
Okay, hmm. TBH I think this code should have type-checked without user intervention, but the way it printed (`cases Mouse x`) is ambiguous, and UCM assumed `Mouse` meant `Rat.Dog.Mouse` instead of `Cat.Dog.Mouse`, which caused parsing to fail.

I'll fix it by making it explicit:

```unison
countCat : Cat.Dog -> Rat.Dog
countCat = cases Cat.Dog.Mouse x -> Bird
unique type Rat.Dog = Bird | Mouse
```

```ucm
I found and typechecked these definitions in scratch.u. If you
do an `add` or `update`, here's how your codebase would
change:
⍟ These names already exist. You can `update` them to your
new definition:
unique type Rat.Dog
countCat : Cat.Dog -> Rat.Dog
```
Ok, all set! Now let's update.

```ucm
.> update
Okay, I'm searching the branch for code that needs to be
updated...
That's done. Now I'm making sure everything typechecks...
countCat : Cat.Dog -> Rat.Dog
countCat = cases Mouse x -> Rat.Dog.Bird
unique type Rat.Dog = Bird | Mouse
Typechecking failed. I've updated your scratch file with the
definitions that need fixing. Once the file is compiling, try
`update` again.
```
Why is it still printing just `Mouse and failing?

0 comments on commit 1956322

Please sign in to comment.