102f888 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Pretty printing of "Can't disambiguate" error

102f888Edwin Brady13 years ago

src/Idris/Delaborate.hs+1−1

@@ -185,7 +185,7 @@ pprintErr' i (NotInjective p x y) =

185 pprintTerm i (delab i y)

186pprintErr' i (CantResolve c) = text "Can't resolve type class" <+> pprintTerm i (delab i c)

187pprintErr' i (CantResolveAlts as) = text "Can't disambiguate name:" <+>

188− cat (punctuate comma (map text as))

188+ cat (punctuate (comma <> space) (map text as))

189pprintErr' i (NoTypeDecl n) = text "No type declaration for" <+> annName n

190pprintErr' i (NoSuchVariable n) = text "No such variable" <+> annName n

191pprintErr' 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

223 let (tc, _) = unApply ty

224 let as' = pruneByType tc ctxt as

225 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

227 showHd x = show x

229 showHd x = show x

228 elab' ina (PAlternative False as)

230 elab' ina (PAlternative False as)

229 = trySeq as

231 = trySeq as