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

git.iko.soy/Idris-dev

on master help sign in

Errors for inspecting a _ in case/with

9eb843dEdwin Brady10 years ago

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)

1027

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

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

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 $

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

1035+ addImplBound i (map fst bargs) wval_in

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

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

1032 -- Elaborate wval in this context

1037 -- Elaborate wval in this context

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

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

src/Idris/Elab/Term.hs+3

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

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

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

1041 = 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.")

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

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

1043 = do attack

1046 = do attack

1044

1047