New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Issue #3435 #3455
Issue #3435 #3455
Conversation
Distinguish between candidates that fail because they have the wrong type and candidates that fail due to some constraints. If there's a single one of the latter candidates (and on valid instance is found) report the error from the constraint. If there are multiple of the latter report the candidates together with the corresponding error.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Looks very good! Just one minor complaint: I don't really like the way you handle the InstanceCandidateFailed
error, it feels like you could just directly construct the YesNoMaybe
value instead of throwing a global exception and catching it again almost immediately.
@@ -135,23 +135,31 @@ whenConstraints action handler = | |||
stealConstraints pid | |||
handler | |||
|
|||
wakeConstraints' :: (ProblemConstraint -> TCM Bool) -> TCM () |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I don't want to nitpick but some comment for the extra argument here would be nice.
solveAwakeConstraints' force = do | ||
solveAwakeConstraints' = solveSomeAwakeConstraints (const True) | ||
|
||
solveSomeAwakeConstraints :: (ProblemConstraint -> Bool) -> Bool -> TCM () |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Same here
src/full/Agda/TypeChecking/Errors.hs
Outdated
vcat [ prettyTCM term <?> text "was ruled out because" | ||
, prettyTCM err ] | ||
|
||
InstanceCandidateFailed{} -> __IMPOSSIBLE__ -- Only used internally by instance search |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Maybe a local ExceptT
for instance search would be a better solution.
@@ -330,16 +347,19 @@ dropSameCandidates m cands0 = verboseBracket "tc.instance" 30 "dropSameCandidate | |||
{- else -} (\ _ -> return False) | |||
`catchError` (\ _ -> return False) | |||
|
|||
data YesNoMaybe = Yes | No | Maybe | HellNo TCErr | |||
data YesNoMaybe = Yes | No | NoBecause TCErr | Maybe | HellNo TCErr |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
It's probably time to give a different name to this type
Fix performance regression in #3435 by delaying solving of instance constraints.