Some basics:
unique type Cat.Dog = Mouse Nat
unique type Rat.Dog = Bird
countCat = cases
Cat.Dog.Mouse x -> Bird
.> 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.
unique type Rat.Dog = Bird | Mouse
.> 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:
countCat : Cat.Dog -> Rat.Dog
countCat = cases Mouse x -> Bird
unique type Rat.Dog = Bird | Mouse
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:
countCat : Cat.Dog -> Rat.Dog
countCat = cases Cat.Dog.Mouse x -> Bird
unique type Rat.Dog = Bird | Mouse
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.
.> 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 ambiguous?
