is cc necessary for handling unsolved_constraint exception

[chenkai036]

Whenever an unsolved_constraint exception is raised, hi attempts to verify the constraints another time by calling satisfied. It seems unnecessary as the exception itself shall contain those already non-satisfied constraints? User code may just catch std::exception and rely on what() to report hobbes compile errors (even if users explicit catch unsolved_constraint, it requires them to keep track of a cc instance). If the above redundancy could be safely removed, we could override what to achieve a uniform / canonical interface in exception handling.

[kthielen]

Well, as it is right now, yes it does need to do that level of filtering. The reason is that if you see where we detect that some constraints are unresolved, we expand implied constraints from hidden type classes and don't filter them:

https://github.com/Morgan-Stanley/hobbes/blob/master/lib/hobbes/eval/cc.C#L241

These hidden type classes are generated when you make a polymorphic function and they keep track of all of the constraints that are relevant to your function for you (without you having to know about it).

For example, this function:

sum xs = foldl((+),zero,xs)

Would be reported as having type '(HasZero t, Add t t t) => [t] -> t', but actually its type would be like '(.genc.8675309 t) => [t] -> t' where the weird name is just a type class generated behind the scenes.

But when we go to report errors to users, they won't understand it if we give them '.genc.8675309 chicken' and might tell us that we are the ones who are bad/wrong, but if the implied constraints get expanded out then they can see that they asked for 'HasZero chicken' and 'Add chicken chicken chicken' which obviously can't be true (probably).

Maybe that's too much info, but that's the backstory on what's going on. In terms of where that filtering happens, you're probably right that we should do it before raising the exception instead of having the code that catches the exception have to do that. That place in cc.C would be the place to change it.

[chenkai036]

I see, thanks for the internals :) It's worthwhile to locate an appropriate place to perform the filtering, I will take a closer look of cc and get back later.