9eb843d · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Errors for inspecting a _ in case/with

These are likely if checking something generated by interactive editing, so it's better that we know about the possibility and report helpfully. Fixes #3280

commit9eb843d6cc80c9d2f5d1d5561207511013d986ef authorEdwin Brady <ecb10@st-andrews.ac.uk> dateMon 12 Dec 2016, 10:37 (10 years ago) parent32c2467

2 files changed+9−1

compare with master

unifiedsplit

src/Idris/Elab/Clause.hs+6−1 src/Idris/Elab/Term.hs+3

src/Idris/Elab/Clause.hs+6−1

@@ -1027,7 +1027,12 @@ elabClause info opts (_, PWith fc fname lhs_in withs wval_in pn_in withblock)

10271027

10281028 logElab 5 ("Checked " ++ show clhs)

10291029 let bargs = getPBtys (explicitNames (normalise ctxt [] lhs_tm))

1030− let wval = rhs_trans info $ addImplBound i (map fst bargs) wval_in

1030+ wval <- case wval_in of

1031+ Placeholder -> ierror $ At fc $

1032+ Msg "No expression for the with block to inspect.\nYou need to replace the _ with an expression."

1033+ _ -> return $

1034+ rhs_trans info $

1035+ addImplBound i (map fst bargs) wval_in

10311036 logElab 5 ("Checking " ++ showTmImpls wval)

10321037 -- Elaborate wval in this context

10331038 ((wvalElab, defer, is, ctxt', newDecls, highlights, newGName), _) <-

src/Idris/Elab/Term.hs+3

@@ -1039,6 +1039,9 @@ elab ist info emode opts fn tm

10391039 elab' ina fc (PElabError e) = lift $ tfail e

10401040 elab' ina mfc (PRewrite fc substfn rule sc newg)

10411041 = elabRewrite (elab' ina mfc) ist fc substfn rule sc newg

1042+ -- A common error case if trying to typecheck an autogenerated case block

1043+ elab' ina _ c@(PCase fc Placeholder opts)

1044+ = lift $ tfail (Msg "No expression for the case to inspect.\nYou need to replace the _ with an expression.")

10421045 elab' ina _ c@(PCase fc scr opts)

10431046 = do attack

10441047