b6c0ae4 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Fix error when error reflection fails

Error reflection could fail legitimately with a type error, if the reflected function is not directly imported but available via an imported module. In this case, display the original error.

commitb6c0ae490d5096a14ace4be5abc70a44407c8041 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateWed 19 Jul 2017, 18:10 (9 years ago) parent97805c4

1 file changed+4−2

compare with master

unifiedsplit

src/Idris/Elab/Term.hs+4−2

src/Idris/Elab/Term.hs+4−2

@@ -2658,9 +2658,11 @@ withErrorReflection x = idrisCatch x (\ e -> handle e >>= ierror)

26582658 concat (intersperse ", " (map show handlers))

26592659 let reports = map (\n -> RApp (Var n) (reflectErr err)) handlers

26602660

2661− -- Typecheck error handlers - if this fails, then something else was wrong earlier!

2661+ -- Typecheck error handlers - if this fails, most

2662+ -- likely something which is needed by it has not

2663+ -- been imported, so keep the original error.

26622664 handlers <- case mapM (check (tt_ctxt ist) []) reports of

2663− Error e -> ierror $ ReflectionFailed "Type error while constructing reflected error" e

2665+ Error _ -> return [] -- ierror $ ReflectionFailed "Type error while constructing reflected error" e

26642666 OK hs -> return hs

26652667

26662668 -- Normalize error handler terms to produce the new messages