7afa03a · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Need to resolve autos in each 'try' branch

If the branch solves an implicit which makes the auto solvable, we need to try to resolve it straight away so we know whether the branch is valid or not. We need this especially when using 'try' to implement implicit coercions.

commit7afa03a8b7939ccf65b1cea2afa49388747ebb23 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateThu 4 Dec 2014, 14:39 (12 years ago) parentb0a0c0c

1 file changed+2−1

compare with master

unifiedsplit

src/Idris/ElabTerm.hs+2−1

src/Idris/ElabTerm.hs+2−1

@@ -348,7 +348,8 @@ elab ist info emode opts fn tm

348348 try' e1 (trySeq' e1 xs) True

349349 trySeq' deferr [] = proofFail deferr

350350 trySeq' deferr (x : xs)

351− = try' (elab' ina fc x) (trySeq' deferr xs) True

351+ = try' (do elab' ina fc x

352+ solveAutos ist fn False) (trySeq' deferr xs) True

352353 elab' ina _ (PPatvar fc n) | bindfree = do patvar n; -- update_term liftPats

353354-- elab' (_, _, inty) (PRef fc f)

354355-- | isTConName f (tt_ctxt ist) && pattern && not reflection && not inty