d439b10 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Tweak %error_reverse heuristic

If not given explicitly, but just taken from an %error_reverse on a type, only add a rule to reverse normalisation if the RHS of the rule is no bigger than the LHS of the rule

commitd439b107e7109d4e8f9236a982266e9ac376bd45 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateSat 8 Oct 2016, 17:21 (10 years ago) parent75248d6

1 file changed+5−2

compare with master

unifiedsplit

src/Idris/Elab/Clause.hs+5−2

src/Idris/Elab/Clause.hs+5−2

@@ -766,14 +766,17 @@ elabClause info opts (cnum, PClause fc fname lhs_in_as withs rhs_in_as wherebloc

766766 Error e -> ierror (At fc (CantUnify False (clhsty, Nothing) (crhsty, Nothing) e [] 0))

767767 i <- getIState

768768 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',

770770 -- 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

772+ -- the RHS

771773 let (ret_fam, _) = unApply (getRetTy crhsty)

772774 rev <- case ret_fam of

773775 P _ rfamn _ ->

774776 case lookupCtxt rfamn (idris_datatypes i) of

775777 [TI _ _ dopts _ _] ->

776− return (DataErrRev `elem` dopts)

778+ return (DataErrRev `elem` dopts &&

779+ size clhs <= size crhs)

777780 _ -> return False

778781 _ -> return False

779782