@@ -766,14 +766,17 @@ elabClause info opts (cnum, PClause fc fname lhs_in_as withs rhs_in_as wherebloc
766 Error e -> ierror (At fc (CantUnify False (clhsty, Nothing) (crhsty, Nothing) e [] 0))
766 Error e -> ierror (At fc (CantUnify False (clhsty, Nothing) (crhsty, Nothing) e [] 0))
767 i <- getIState
767 i <- getIState
768 checkInferred fc (delab' i crhs True True) rhs
768 checkInferred fc (delab' i crhs True True) rhs
769− -- if the function is declared '%error_reverse', or its type,
769+ -- if the function is declared '%error_reverse',
770 -- then we'll try running it in reverse to improve error messages
770 -- then we'll try running it in reverse to improve error messages
771+ -- Also if the type is '%error_reverse' and the LHS is smaller than
771 let (ret_fam, _) = unApply (getRetTy crhsty)
773 let (ret_fam, _) = unApply (getRetTy crhsty)
772 rev <- case ret_fam of
774 rev <- case ret_fam of
773 P _ rfamn _ ->
775 P _ rfamn _ ->
774 case lookupCtxt rfamn (idris_datatypes i) of
776 case lookupCtxt rfamn (idris_datatypes i) of
775 [TI _ _ dopts _ _] ->
777 [TI _ _ dopts _ _] ->
776− return (DataErrRev `elem` dopts)
778+ return (DataErrRev `elem` dopts &&
779+ size clhs <= size crhs)
777 _ -> return False
780 _ -> return False
778 _ -> return False
781 _ -> return False