Pretty printing of "Can't disambiguate" error
commit102f888ba8908f9b8ce08dba64734fe51bd8ddeb
authorEdwin Brady <ecb10@st-andrews.ac.uk>
dateThu 30 Jan 2014, 12:12 (13 years ago)
parent72b9990
src/Idris/Delaborate.hs+1−1
@@ -185,7 +185,7 @@ pprintErr' i (NotInjective p x y) =
185185 pprintTerm i (delab i y)
186186pprintErr' i (CantResolve c) = text "Can't resolve type class" <+> pprintTerm i (delab i c)
187187pprintErr' i (CantResolveAlts as) = text "Can't disambiguate name:" <+>
188− cat (punctuate comma (map text as))
188+ cat (punctuate (comma <> space) (map text as))
189189pprintErr' i (NoTypeDecl n) = text "No type declaration for" <+> annName n
190190pprintErr' i (NoSuchVariable n) = text "No such variable" <+> annName n
191191pprintErr' i (IncompleteTerm t) = text "Incomplete term" <+> pprintTerm i (delab i t)
src/Idris/ElabTerm.hs+3−1
@@ -223,7 +223,9 @@ elab ist info pattern opts fn tm
223223 let (tc, _) = unApply ty
224224 let as' = pruneByType tc ctxt as
225225 tryAll (zip (map (elab' ina) as') (map showHd as'))
226− where showHd (PApp _ h _) = show h
226+ where showHd (PApp _ (PRef _ n) _) = show n
227+ showHd (PRef _ n) = show n
228+ showHd (PApp _ h _) = show h
227229 showHd x = show x
228230 elab' ina (PAlternative False as)
229231 = trySeq as