Error reflection now supports specific function arguments

FunErrTest.idr

import Language.Reflection.Errors
import Language.Reflection.Utils

%language ErrorReflection

total
cadr :  (xs : List a)
     -> {auto cons1 : isCons xs = True}
     -> {auto cons2 : isCons (tail xs cons1) = True}
     -> a
cadr (x :: (y :: _)) {cons1=refl} {cons2=refl} = y
cadr (x :: [])       {cons1=refl} {cons2=refl} impossible

extractList : TT -> Maybe TT
extractList (App (App reflCon (App isCons lst)) _) = Just lst
extractList _ = Nothing


total
has2elts : Err -> Maybe (List ErrorReportPart)
has2elts (CantSolveGoal tm _) = do lst <- extractList tm
                                   return [ TextPart "Could not prove that"
                                          , TermPart lst
                                          , TextPart "has at least two elements."
                                          ]
has2elts e = Just [TextPart (show e)]

%error_handlers cadr cons1 has2elts
%error_handlers cadr cons2 has2elts

REPL session

*FunErrTest> cadr []
Could not prove that [] has at least two elements.
Original error:

	Can't solve goal 
		isCons [] = True

*FunErrTest> \ xs : List Int => cadr xs
Could not prove that xs has at least two elements.
Original error:

	Can't solve goal 
		isCons xs = True