on master help sign in
Give resugared names in incomplete term errors
c4e6eafEdwin Brady
src/Idris/Delaborate.hs+4−4
@@ -354,11 +354,11 @@ pprintErr' i (IncompleteTerm t)
354 = align (cat (punctuate (comma <> space)
354 = align (cat (punctuate (comma <> space)
355 (map pprintIncomplete (nub $ getMissing [] [] t))))
355 (map pprintIncomplete (nub $ getMissing [] [] t))))
356 where
356 where
357− pprintIncomplete (fn, arg)
357+ pprintIncomplete (tm, arg)
358 = text "Can't infer argument" <+> annName arg <+> text "to" <+>
358 = text "Can't infer argument" <+> annName arg <+> text "to" <+>
359− annName fn
359+ annTm tm (pprintTerm i (delabSugared i tm))
360
360
361− getMissing :: [Name] -> [Name] -> Term -> [(Name, Name)]
361+ getMissing :: [Name] -> [Name] -> Term -> [(Term, Name)]
362 getMissing hs env (Bind n (Hole ty) sc)
362 getMissing hs env (Bind n (Hole ty) sc)
363 = getMissing (n : hs) (n : env) sc
363 = getMissing (n : hs) (n : env) sc
364 getMissing hs env (Bind n (Guess _ _) sc)
364 getMissing hs env (Bind n (Guess _ _) sc)
@@ -371,7 +371,7 @@ pprintErr' i (IncompleteTerm t)
371 = getMissing hs env (binderTy b) ++
371 = getMissing hs env (binderTy b) ++
372 getMissing hs (n : env) sc
372 getMissing hs (n : env) sc
373 getMissing hs env ap@(App _ _ _)
373 getMissing hs env ap@(App _ _ _)
374− | (P _ n _, args) <- unApply ap = getMissingArgs n args
374+ | (fn@(P _ n _), args) <- unApply ap = getMissingArgs fn args
375 where
375 where
376 getMissingArgs n [] = []
376 getMissingArgs n [] = []
377 getMissingArgs n (V i : as)
377 getMissingArgs n (V i : as)