Skip to content

Add Error variants#115

Closed
croyzor wants to merge 4 commits into
mainfrom
cr/yield-err-msg
Closed

Add Error variants#115
croyzor wants to merge 4 commits into
mainfrom
cr/yield-err-msg

Conversation

@croyzor

@croyzor croyzor commented Apr 28, 2026

Copy link
Copy Markdown
Collaborator

Add an error message to Yield to print when typechecking ends with us getting stuck.

@croyzor croyzor requested a review from acl-cqc April 28, 2026 08:26

@acl-cqc acl-cqc left a comment

Copy link
Copy Markdown
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Generally yes, but I think the API could be better (and maybe even less change if we keep the string)....

Comment thread brat/Brat/Error.hs Outdated
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]

Copy link
Copy Markdown
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

funny to read as the AND WORSE is, it's not necessarily true is it? There's no ordering or reason for the second to be worse than the first, is there? Should we just go with "AND ALSO" ?

Comment thread brat/Brat/Error.hs Outdated
| ThunkLeftUnders String
| BracketErr BracketErrMsg
| RemainingNatHopes [String]
| NeedToKnow End

Copy link
Copy Markdown
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Why not make this take a Set of Ends?

Comment thread brat/Brat/Checker/Monad.hs Outdated

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 ()

Copy link
Copy Markdown
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

If NeedToKnow took a set of ends, you could drop this ErrorMsg param from mkYield and have it construct a NeedToKnow using the set it's given.

You might then keep the string, this seems useful as a hint as to where in the code we are blocked.

Comment thread brat/Brat/Checker/Monad.hs Outdated
++ "":"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

Copy link
Copy Markdown
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Whether you store err in Yield and use that here, or build NeedToKnow ends here, I don't really mind....

@croyzor

croyzor commented May 15, 2026

Copy link
Copy Markdown
Collaborator Author

Couldn't agree more! Much nicer now

@croyzor croyzor requested a review from acl-cqc May 15, 2026 13:00
@croyzor croyzor changed the title Add error message to Yield Add Error variants May 15, 2026
@acl-cqc

acl-cqc commented May 15, 2026

Copy link
Copy Markdown
Collaborator

Oh!! I hadn't actually realized that quite that much of the PR will disappear....i.e. that Both and NeedToKnow are no longer used at all. Sorry for repeated rework. I guess at this point it does look like smuggling these in will be the right thing, i.e. if they are actually used???

@croyzor croyzor closed this May 29, 2026
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants