Apply suggestions from code review

Co-authored-by: Alan Lawrence <[email protected]>

brat/Brat/Checker/SolveHoles.hs

@@ -55,20 +55,22 @@ typeEqEta tm (lvy :* kz :* sems) hopeSet (TypeFor m ((_, k):ks)) exp act = do
   typeEqEta tm (Sy lvy :* (kz :<< k) :* (sems :<< nextSem)) hopeSet (TypeFor m ks) exp act
 -- Not higher kinded - check for flex terms
 -- (We don't solve under binders for now, so we only consider Zy here)
--- "easy" flex cases
+-- 1. "easy" flex cases
 typeEqEta _tm (Zy :* _ks :* _sems) hopeSet k (SApp (SPar e) B0) act
   | M.member e hopeSet = solveHope k e act
 typeEqEta _tm (Zy :* _ks :* _sems) hopeSet k exp (SApp (SPar e) B0)
   | M.member e hopeSet = solveHope k e exp
 typeEqEta _ (Zy :* _ :* _) hopeSet Nat exp act
   | Just (SPar e) <- isNumVar exp, M.member e hopeSet = solveHope Nat e act
   | Just (SPar e) <- isNumVar act, M.member e hopeSet = solveHope Nat e exp
+-- 2. harder cases, neither is in the hope set, so we can't define it ourselves
 typeEqEta tm stuff@(ny :* _ks :* _sems) hopeSet k exp act = do
   exp <- quote ny exp
   act <- quote ny act
   case [e | (VApp (VPar e) _) <- [exp,act], M.member e hopeSet] of
     [] -> typeEqRigid tm stuff k exp act
-    _es -> error "TODO"
+    [e1, e2] | e1 == e2 -> pure () -- trivially same, even if both still yet-to-be-defined
+    _es -> error "TODO: must wait for one or the other to become more defined"
 -- uhhh
 -- Yield(AwaitingAny $ S.fromList es) (\_ -> typeEq tm stuff k exp act)
 

brat/Brat/Checker/SolvePatterns.hs

@@ -222,7 +222,7 @@ solveNumMeta e nv = case (e, vars nv) of
    defineSrc idSrc (VNum (nVar (VPar (toEnd idTgt))))
    instantiateMeta (InEnd weeTgt) (VNum (nVar (VPar (toEnd idSrc))))
    wire (idSrc, TNat, NamedPort weeTgt "")
-   let nv' = fmap (const (VPar (toEnd idSrc))) nv
+   let nv' = fmap (const (VPar (toEnd idSrc))) nv -- weeTgt is the only thing to replace
    bigSrc <- buildNatVal nv'
    instantiateMeta (InEnd bigTgt) (VNum nv')
    wire (bigSrc, TNat, NamedPort bigTgt "")