From 99ff3208206a3e758dab7507119859a2f1131a78 Mon Sep 17 00:00:00 2001
From: Dan Doel <dan.doel@gmail.com>
Date: Mon, 12 Jul 2021 10:45:07 -0400
Subject: [PATCH] Add tests

---
 .../transcripts-using-base/fix2158-1.md       | 25 ++++++++++++
 .../fix2158-1.output.md                       | 39 +++++++++++++++++++
 unison-src/transcripts/fix2167.md             | 28 +++++++++++++
 unison-src/transcripts/fix2167.output.md      | 37 ++++++++++++++++++
 4 files changed, 129 insertions(+)
 create mode 100644 unison-src/transcripts-using-base/fix2158-1.md
 create mode 100644 unison-src/transcripts-using-base/fix2158-1.output.md
 create mode 100644 unison-src/transcripts/fix2167.md
 create mode 100644 unison-src/transcripts/fix2167.output.md

diff --git a/unison-src/transcripts-using-base/fix2158-1.md b/unison-src/transcripts-using-base/fix2158-1.md
new file mode 100644
index 000000000..c80faa3f1
--- /dev/null
+++ b/unison-src/transcripts-using-base/fix2158-1.md
@@ -0,0 +1,25 @@
+This transcript tests an ability check failure regression.
+
+```unison
+ability Async t g where
+  fork : '{Async t g, g} a -> t a
+  await : t a -> a
+
+Async.parMap : (a ->{Async t g, g} b) -> [a] ->{Async t g} [b]
+Async.parMap f as = 
+  tasks = List.map (a -> fork '(f a)) as 
+  List.map await tasks
+```
+
+The issue was that certain ability processing was happing in less
+optimal order. `g` appears both as an ability used and as a parameter
+to `Async`. However, the latter occurrence is more strict. Unifying
+the types `Async t g1` and `Async t g2` requires `g1` and `g2` to
+be equal, while abilities that occur directly in a row are subject to
+some subtyping.
+
+However, the ability handling was just processing rows in whatever
+order they occurred, and during inference it happened that `g`
+occurred in the row before `Async t g`. Processing the stricter parts
+first is better, becauase it can solve things more precisely and avoid
+ambiguities relating to subtyping.
diff --git a/unison-src/transcripts-using-base/fix2158-1.output.md b/unison-src/transcripts-using-base/fix2158-1.output.md
new file mode 100644
index 000000000..f9419e4a4
--- /dev/null
+++ b/unison-src/transcripts-using-base/fix2158-1.output.md
@@ -0,0 +1,39 @@
+This transcript tests an ability check failure regression.
+
+```unison
+ability Async t g where
+  fork : '{Async t g, g} a -> t a
+  await : t a -> a
+
+Async.parMap : (a ->{Async t g, g} b) -> [a] ->{Async t g} [b]
+Async.parMap f as = 
+  tasks = List.map (a -> fork '(f a)) as 
+  List.map await tasks
+```
+
+```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 new definitions are ok to `add`:
+    
+      ability Async t g
+      Async.parMap : (a ->{g, Async t g} b)
+                     -> [a]
+                     ->{Async t g} [b]
+
+```
+The issue was that certain ability processing was happing in less
+optimal order. `g` appears both as an ability used and as a parameter
+to `Async`. However, the latter occurrence is more strict. Unifying
+the types `Async t g1` and `Async t g2` requires `g1` and `g2` to
+be equal, while abilities that occur directly in a row are subject to
+some subtyping.
+
+However, the ability handling was just processing rows in whatever
+order they occurred, and during inference it happened that `g`
+occurred in the row before `Async t g. Processing the stricter parts
+first is better, becauase it can solve things more precisely and avoid
+ambiguities relating to subtyping.
diff --git a/unison-src/transcripts/fix2167.md b/unison-src/transcripts/fix2167.md
new file mode 100644
index 000000000..cb5a64f30
--- /dev/null
+++ b/unison-src/transcripts/fix2167.md
@@ -0,0 +1,28 @@
+```ucm:hide
+.> builtins.merge
+```
+
+This is just a simple transcript to regression check an ability
+inference/checking issue.
+
+```unison
+ability R t where
+  die : () -> x
+  near.impl : Nat -> Either () [Nat]
+
+R.near n = match near.impl n with
+  Left e -> die ()
+  Right a -> a
+
+R.near1 region loc = match R.near 42 with
+  [loc] -> loc
+  ls -> R.die ()
+```
+
+The issue was that abilities with parameters like this were sometimes
+causing failures like this because the variable in the parameter would
+escape to a scope where it no longer made sense. Then solving would
+fail because the type was invalid.
+
+The fix was to avoid dropping certain existential variables out of
+scope.
diff --git a/unison-src/transcripts/fix2167.output.md b/unison-src/transcripts/fix2167.output.md
new file mode 100644
index 000000000..4a6f3de65
--- /dev/null
+++ b/unison-src/transcripts/fix2167.output.md
@@ -0,0 +1,37 @@
+This is just a simple transcript to regression check an ability
+inference/checking issue.
+
+```unison
+ability R t where
+  die : () -> x
+  near.impl : Nat -> Either () [Nat]
+
+R.near n = match near.impl n with
+  Left e -> die ()
+  Right a -> a
+
+R.near1 region loc = match R.near 42 with
+  [loc] -> loc
+  ls -> R.die ()
+```
+
+```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 new definitions are ok to `add`:
+    
+      ability R t
+      R.near  : Nat ->{R t} [Nat]
+      R.near1 : region -> loc ->{R t} Nat
+
+```
+The issue was that abilities with parameters like this were sometimes
+causing failures like this because the variable in the parameter would
+escape to a scope where it no longer made sense. Then solving would
+fail because the type was invalid.
+
+The fix was to avoid dropping certain existential variables out of
+scope.