Add error message to Yield

brat/Brat/Checker/Helpers.hs

@@ -46,7 +46,7 @@ simpleCheck my ty tm = case (my, ty) of
     else isSkolem e >>= \case
       SkolemConst -> throwLeft $ helper Braty ty tm
       Definable -> do
-        mkYield "simpleCheck" (S.singleton e)
+        mkYield (NeedToKnow e) "simpleCheck" (S.singleton e)
         ty <- eval S0 ty
         simpleCheck Braty ty tm
   _ -> throwLeft $ helper my ty tm
@@ -731,7 +731,7 @@ mineToSolve = allowedToSolve <$> whoAmI
 -- defined is passed in.
 awaitTypeDefinition :: Val Z -> Checking (Val Z)
 awaitTypeDefinition ty = eval S0 ty >>= \case
-  VApp (VPar e) _ -> mkYield "awaitTypeDefinition" (S.singleton e) >> awaitTypeDefinition ty
+  VApp (VPar e) _ -> mkYield (NeedToKnow e) "awaitTypeDefinition" (S.singleton e) >> awaitTypeDefinition ty
   ty -> pure ty
 
 mkGraph :: TypeKind -> Val Z -> Checking Src

brat/Brat/Checker/Monad.hs

@@ -82,8 +82,8 @@ data Context = Ctx { globalVEnv :: VEnv
 mkFork :: String -> Free sig () -> Free sig ()
 mkFork d par = thTrace ("Forking " ++ d) $ Fork d par $ pure ()
 
-mkYield :: String -> S.Set End -> Free sig ()
-mkYield desc es = thTrace ("Yielding in " ++ desc ++ "\n  " ++ show es) $ Yield (AwaitingAny es) (\_ -> trackM ("woke up " ++ desc) >> Ret ())
+mkYield :: ErrorMsg -> String -> S.Set End -> Free sig ()
+mkYield err desc es = thTrace ("Yielding in " ++ desc ++ "\n  " ++ show es) $ Yield err (AwaitingAny es) (\n -> trackM ("woke up " ++ desc ++ "\n" ++ show n) >> Ret ())
 
 -- Commands for synchronous operations
 data CheckingSig ty where
@@ -127,7 +127,7 @@ wrapper f (Req s k) = f s >>= \case
   Just v -> wrapper f (k v)
   Nothing -> Req s (wrapper f . k)
 wrapper f (Define lbl v e k) = Define lbl v e (wrapper f . k)
-wrapper f (Yield st k) = Yield st (wrapper f . k)
+wrapper f (Yield err st k) = Yield err st (wrapper f . k)
 wrapper f (Fork d par c) = Fork d (wrapper f par) (wrapper f c)
 
 wrapper2 :: (forall a. CheckingSig a -> Maybe a) -> Checking v -> Checking v
@@ -238,7 +238,7 @@ localKVar env (Req KDone k) = case [ x | (x,(One,_)) <- M.assocs env ] of
                                               ]
 localKVar env (Req r k) = Req r (localKVar env . k)
 localKVar env (Define lbl e v k) = Define lbl e v (localKVar env . k)
-localKVar env (Yield st k) = Yield st (localKVar env . k)
+localKVar env (Yield err st k) = Yield err st (localKVar env . k)
 localKVar env (Fork desc par c) =
   -- can't send end both ways, so until we can join (TODO), restrict Forks to local scope
   thTrace ("Spawning(LKV) " ++ desc) $ localKVar env $ par *> c
@@ -253,7 +253,7 @@ catchErr (Ret t) = Ret (Right t)
 catchErr (Req (Throw e) _) = pure $ Left e
 catchErr (Req r k) = Req r (catchErr . k)
 catchErr (Define lbl e v k) = Define lbl e v (catchErr . k)
-catchErr (Yield st k) = Yield st (catchErr . k)
+catchErr (Yield err st k) = Yield err st (catchErr . k)
 catchErr (Fork desc par c) = thTrace ("Spawning(catch) " ++ desc) $ catchErr $ par *> c
 
 handler :: Free CheckingSig v
@@ -347,10 +347,13 @@ handler (Define lbl end v k) ctx g = let st@Store{typeMap=tm, valueMap=vm} = sto
                                                  (M.delete inport (dynamicSet ctx))
                                         Nothing -> dynamicSet ctx
                           }) g
-handler (Yield Unstuck k) ctx g = handler (k mempty) ctx g
-handler (Yield (AwaitingAny ends) _k) ctx _ = Left $ dumbErr $ TypeErr $ unlines $
+handler (Yield _err Unstuck k) ctx g = handler (k mempty) ctx g
+handler (Yield err (AwaitingAny ends) _k) ctx _ = Left $ dumbErr $ Both
+                                                                   (TypeErr $ unlines $
   ("Typechecking blocked on:":(show <$> S.toList ends))
-  ++ "":"Dynamic set is":(show <$> M.keys (dynamicSet ctx)) ++ ["Try writing more types! :-)"]
+  ++ "":"Dynamic set is":(show <$> M.keys (dynamicSet ctx))
+  ++ "":["Try writing more types! :-)"])
+ err
 handler (Fork desc par c) ctx g = handler (thTrace ("Spawning " ++ desc) $ par *> c) ctx g
 
 type Checking = Free CheckingSig
@@ -404,7 +407,7 @@ localNS ns (Req (SplitNS str) k) = let (subSpace, newRoot) = split str ns in
 localNS ns (Req AskNS k) = localNS ns (k (fst ns))
 localNS ns (Req c k) = Req c (localNS ns . k)
 localNS ns (Define lbl e v k) = Define lbl e v (localNS ns . k)
-localNS ns (Yield st k) = Yield st (localNS ns . k)
+localNS ns (Yield err st k) = Yield err st (localNS ns . k)
 localNS ns (Fork desc par c) = let (subSpace, newRoot) = split desc ns in
                                  Fork desc (localNS subSpace par) (localNS newRoot c)
 

brat/Brat/Checker/SolveHoles.hs

@@ -93,7 +93,7 @@ typeEqEta tm stuff@(ny :* _ks :* _sems) _ k exp act = do
   unless (exp == act) $ case flexes act ++ flexes exp of
     [] -> typeEqRigid tm stuff k exp act -- easyish, both rigid i.e. already defined
     -- tricky: must wait for one or other to become more defined
-    es -> mkYield "typeEqEta" (S.fromList es) >> typeEq' tm stuff k exp act
+    es@(e:_) -> mkYield (NeedToKnow e) "typeEqEta" (S.fromList es) >> typeEq' tm stuff k exp act
 
 typeEqs :: String -> (Ny :* Stack Z TypeKind :* Stack Z Sem) n -> [TypeKind] -> [Val n] -> [Val n] -> Checking ()
 typeEqs _ _ [] [] [] = pure ()

brat/Brat/Checker/SolveNumbers.hs

@@ -105,11 +105,11 @@ unifyNum' mine (NumValue lup lgro) (NumValue rup rgro)
        | Just _ <- mine e' -> do
           req (Wire (dangling, TNat, p))
           defineSrc' ("flex-flex In Ex") (NamedPort dangling "") (VNum (nVar v))
-       | otherwise -> mkYield "flexFlex" (S.singleton e) >> unifyNum mine (nVar v) (nVar v')
+       | otherwise -> mkYield (NeedToKnow e) "flexFlex" (S.singleton e) >> unifyNum mine (nVar v) (nVar v')
       (VPar e@(InEnd p), VPar e'@(InEnd p'))
        | Just _ <- mine e -> defineTgt' "flex-flex In In1" (NamedPort p "") (VNum (nVar v'))
        | Just _ <- mine e' -> defineTgt' "flex-flex In In0"(NamedPort p' "") (VNum (nVar v))
-       | otherwise -> mkYield "flexFlex" (S.fromList [e, e']) >> unifyNum mine (nVar v) (nVar v')
+       | otherwise -> mkYield (Both (NeedToKnow e) (NeedToKnow e')) "flexFlex" (S.fromList [e, e']) >> unifyNum mine (nVar v) (nVar v')
 
   lhsStrictMono :: StrictMono (VVar Z) -> NumVal (VVar Z) -> Checking ()
   lhsStrictMono (StrictMono 0 mono) num = lhsMono mono num
@@ -123,13 +123,13 @@ unifyNum' mine (NumValue lup lgro) (NumValue rup rgro)
   lhsMono lhs@(Linear (VPar e)) num | [e'] <- numVars num, e == e' = case num of
     (NumValue 0 (StrictMonoFun sm)) -> case anyDoubsAnyFulls sm of
       (True, _) -> lhsMono lhs (nConstant 0)
-      (False, True) -> mkYield "lhsMono2Sols" (S.singleton e) >>
+      (False, True) -> mkYield (NeedToKnow e) "lhsMono2Sols" (S.singleton e) >>
                        unifyNum mine (nVar (VPar e)) num
       (False, False) -> pure ()
     _ -> err . UnificationError $ "Can't make " ++ show e ++ " = " ++ show num
   lhsMono (Linear (VPar e)) num = case mine e of
     Just loc -> loc -! solveNumMeta mine e num
-    _ -> mkYield "lhsMono" (S.singleton e) >>
+    _ -> mkYield (NeedToKnow e) "lhsMono" (S.singleton e) >>
          unifyNum mine (nVar (VPar e)) num
   lhsMono (Full sm) (NumValue 0 (StrictMonoFun (StrictMono 0 (Full sm'))))
     = lhsFun00 (StrictMonoFun sm) (NumValue 0 (StrictMonoFun sm'))
@@ -169,7 +169,7 @@ unifyNum' mine (NumValue lup lgro) (NumValue rup rgro)
   -- = 2^k + 2^(k + 1) * full(n)
 
     | otherwise = do
-      mkYield "demandSucc" (S.singleton e)
+      mkYield (NeedToKnow e) "demandSucc" (S.singleton e)
       nv <- quoteNum Zy <$> numEval S0 mono
       demandSucc nv
 
@@ -196,7 +196,7 @@ unifyNum' mine (NumValue lup lgro) (NumValue rup rgro)
           half <- traceChecking "makeHalf" makeHalf e
           pure (NumValue 0 (StrictMonoFun (StrictMono 0 (Linear (VPar half)))))
         | otherwise -> do
-          mkYield "evenGro" (S.singleton e)
+          mkYield (NeedToKnow e) "evenGro" (S.singleton e)
           nv <- quoteNum Zy <$> numEval S0 mono
           demandEven nv
       Full sm -> nConstant 0 <$ demand0 (NumValue 0 (StrictMonoFun sm))

brat/Brat/Error.hs

@@ -11,7 +11,7 @@
 
 import Brat.FC
 import Data.Bracket
-import Brat.Syntax.Port (PortName)
+import Brat.Syntax.Port (End, PortName)
 
 import Data.List (intercalate)
 import System.Exit
@@ -109,6 +109,9 @@
  | ThunkLeftUnders String
  | BracketErr BracketErrMsg
  | RemainingNatHopes [String]
+ | NeedToKnow End
+ | Both ErrorMsg ErrorMsg
+ | WaitingForConstraint String
 
 instance Show ErrorMsg where
   show (TypeErr x) = "Type error: " ++ x
@@ -194,6 +197,10 @@
   show (ThunkLeftUnders unders) = "Expected function to return additional values of type: " ++ unders
   show (BracketErr msg) = show msg
   show (RemainingNatHopes hs) = unlines ("Expected to work out values for these holes:":(("    " ++) <$> hs))
+  show (NeedToKnow end) = unlines ["I wanna know what:", ' ':show end,"is."]
+  show (Both err1 err2) = unlines [show err1,""," AND WORSE","",show err2]
+  show (WaitingForConstraint msg) = "Waiting for constraint:\n " ++ msg
+
 
 data Error = Err { fc  :: Maybe FC
                  , msg :: ErrorMsg
@@ -240,8 +247,8 @@
     ls = lines contents
   in case endLineN - startLineN of
        0 -> [ls!!startLineN, highlightSection startCol endCol]
        n | n > 0 -> let (first:rest) = drop (startLineN - 1) $ take (endLineN + 1) ls
                         (last:rmid) = reverse rest
                     in [first, highlightSection startCol (length first)]
                        ++ (reverse rmid >>= (\l -> [l, highlightSection 0 (length l)]))
                        ++ [last, highlightSection 0 endCol]

brat/Control/Monad/Freer.hs

@@ -1,5 +1,6 @@
 module Control.Monad.Freer where
 
+import Brat.Error (ErrorMsg(..))
 import Brat.Syntax.Port (End)
 import Brat.Syntax.Value (Val)
 import Hasochism (N(..))
@@ -13,7 +14,7 @@ import qualified Data.Set as S
 --  * e -> Unstuck means e has been solved
 --  * e -> Awaiting es means the problem's been transferred
 --  * e not in news means no change to e
-newtype News = News (M.Map End Stuck)
+newtype News = News (M.Map End Stuck) deriving Show
 
 updateEnd :: News -> End -> Stuck
 updateEnd (News m) e = case M.lookup e m of
@@ -44,14 +45,14 @@ data Free (sig :: Type -> Type) (v :: Type) where
   Ret :: v -> Free sig v
   Req ::  sig t -> (t -> Free sig v) -> Free sig v
   Define :: String -> End -> Val Z -> (News -> Free sig v) -> Free sig v
-  Yield :: Stuck -> (News -> Free sig v) -> Free sig v
+  Yield :: ErrorMsg -> Stuck -> (News -> Free sig v) -> Free sig v
   Fork :: String -> Free sig () -> Free sig v -> Free sig v
 
 instance Functor (Free sig) where
   fmap f (Ret v) = Ret (f v)
   fmap f (Req sig k) = Req sig (fmap f . k)
   fmap f (Define lbl e v k) = Define lbl e v (fmap f . k)
-  fmap f (Yield st k) = Yield st (fmap f . k)
+  fmap f (Yield err st k) = Yield err st (fmap f . k)
   fmap f (Fork d par c) = Fork d par (fmap f c)
 
 class NewsWatcher t where
@@ -68,16 +69,16 @@ instance NewsWatcher (Free sig v) where
   Ret v /// _ = Ret v
   Req sig k /// n = Req sig $ \v -> k v /// n
   Define lbl e v k /// n = Define lbl e v (k /// n)
-  Yield st k /// n = Yield (st /// n) (k /// n)
+  Yield err st k /// n = Yield err (st /// n) (k /// n)
   Fork d par c /// n = Fork d (par /// n) (c /// n)
 
 instance Applicative (Free sig) where
   pure = Ret
 
   -- Left biased scheduling of commands:
   -- First, get rid of Yield Unstuck
-  Yield Unstuck k <*> a = k mempty <*> a
-  f <*> Yield Unstuck k = f <*> k mempty
+  Yield _ Unstuck k <*> a = k mempty <*> a
+  f <*> Yield _ Unstuck k = f <*> k mempty
 
   -- Aggressively forward Forks
   Fork d par c <*> ma = Fork d par (c <*> ma)
@@ -91,15 +92,15 @@ instance Applicative (Free sig) where
   -- What happens when Yield is on the left
   y <*> Ret v = fmap ($ v) y
   y <*> Req sig k = Req sig $ \v -> y <*> k v
-  y1@(Yield st1 _) <*> y2@(Yield st2 _) = Yield (st1 <> st2) $
+  y1@(Yield err1 st1 _) <*> y2@(Yield err2 st2 _) = Yield (Both err1 err2) (st1 <> st2) $
     \n -> (y1 /// n) <*> (y2 /// n)
   y <*> Define lbl e v k = Define lbl e v $ \n -> (y /// n) <*> k n
 
 instance Monad (Free sig) where
   Ret v >>= k = k v
   Req r j >>= k = Req r (j >=> k)
   Define lbl e v k1 >>= k2 = Define lbl e v (k1 >=> k2)
-  Yield st k1 >>= k2 = Yield st (k1 >=> k2)
+  Yield err st k1 >>= k2 = Yield err st (k1 >=> k2)
   --- equivalent to
   -- Yield st k1 >>= k2 = Yield st (\n -> (k1 n) >>= k2)
   Fork d par k1 >>= k2 = Fork d par (k1 >>= k2)

brat/test/Main.hs

@@ -35,7 +35,7 @@ coroT1 = do
           Just _ -> err $ InternalError "already defined"
           Nothing -> defineEnd "test" e (VCon (PrefixName [] "nil") [])
       )
-  mkYield "coroT1" (S.singleton e) >> pure ()
+  mkYield (TypeErr "coroT1") "coroT1" (S.singleton e) >> pure ()
   --traceM "Yield continued"
   v <- req $ ELup e
   case v of
@@ -48,7 +48,7 @@ coroT2 = do
   let e = InEnd $ In name 0
   req $ Declare e Braty (Left $ Star []) Definable
   v <- do
-    mkYield "coroT2" (S.singleton e)
+    mkYield (TypeErr "coroT2") "coroT2" (S.singleton e)
     req $ ELup e
   -- No way to execute this without a 'v'
   mkFork "t2" $ defineEnd "test" e (VCon (PrefixName [] "nil") [])