It would be nice to be able to see the type mismatch in "Challenge and solution theorem statement do not match"