Postpone non-linear solutions

TODO.md

@@ -12,8 +12,11 @@
 - [x] Erasure checking happens at compile time and isn't surfaced to editor..
 - [ ] Erasure issue during AoC from case building replacing a non-erased value with erased.
 - [ ] Add Foldable?
+- [ ] Maybe return constraints instead of solving metas during unification
+  - We already return non-meta constraints for work on the LHS.
+  - We might get into a situation where solving immediately would have gotten us more progress?
 - [ ] "Failed to unify %var0 and %var1" - get names in there
-  - Need fancier `Env` or the index...
+  - Need fancier `Env` or the index on the type of `Tm`
 - Editor support:
   - [ ] add missing cases should skip indented lines
   - [ ] add missing cases should handle `_::_`

src/Lib/Elab.newt

@@ -395,7 +395,14 @@ solve env m sp t = do
       addConstraint env m sp t
   let l = length' env
   debug $ \ _ => "meta \{show meta}"
-  ren <- invert l sp
+
+  -- tests/UnifyPi.newt - Solution is non-linear, but is solved later
+  -- REVIEW We add constraints to be checked later (here and above) and assume the unification succeeds
+  -- Will this get is into trouble?
+  Right ren <- tryError $ invert l sp
+    | Left err => do
+        debug $ \ _ => "postpone constraint \{showError "" err}"
+        addConstraint env m sp t
   -- force unlet
   hack <- quote l t
   t <- eval env hack

tests/UnifyPi.newt

@@ -0,0 +1,17 @@
+module UnifyPi
+
+Graph : U -> U
+Graph obj = obj -> obj -> U
+
+/-
+ERROR at tests/UnifyPi.newt:14:31--14:36: unification failure: non-linear pattern: [%var0, %var1, %var2, %var1]
+  failed to unify ?m:UnifyPi.$m2 k:2 a:1 b:0 a:1
+             with ( :ins : ?m:UnifyPi.$m3 k:2 a:1 b:0) -> ?m:UnifyPi.$m4 k:3 a:2 b:1 :ins:0
+
+Possibly just a case where we can postpone the constraints. I think the BCC k a b might solve k and the
+other bits work themselves out? But do I not do that? I certainly postpone ones with extra args.
+-/
+
+data BCC : Graph U -> Graph U where
+  -- newt can't infer the type of K, but Idris succeeds
+  Prim : {k : _} {a b : U} -> k a b -> BCC k a b