@@ -165,8 +165,8 @@ pprintErr' i (InternalMsg s) =
165165 text ("Please consider reporting at " ++ bugaddr)
166166 ]
167167pprintErr' i (CantUnify _ x y e sc s) =
168− text "Can't unify" <> indented (pprintTerm' i (map (\ (n, b) -> (n, False)) sc) (delab i x)) <$>
169− text "with" <> indented (pprintTerm' i (map (\ (n, b) -> (n, False)) sc) (delab i y)) <>
168+ text "Can't unify" <> indented (annTm x (pprintTerm' i (map (\ (n, b) -> (n, False)) sc) (delab i x))) <$>
169+ text "with" <> indented (annTm y (pprintTerm' i (map (\ (n, b) -> (n, False)) sc) (delab i y))) <>
170170 case e of
171171 Msg "" -> empty
172172 _ -> line <> line <> text "Specifically:" <>
@@ -174,46 +174,46 @@ pprintErr' i (CantUnify _ x y e sc s) =
174174 if (opt_errContext (idris_options i)) then showSc i sc else empty
175175pprintErr' i (CantConvert x y env) =
176176 text "Can't convert" <>
177− indented (pprintTerm' i (map (\ (n, b) -> (n, False)) env) (delab i x)) <$>
177+ indented (annTm x (pprintTerm' i (map (\ (n, b) -> (n, False)) env) (delab i x))) <$>
178178 text "with" <>
179− indented (pprintTerm' i (map (\ (n, b) -> (n, False)) env) (delab i y)) <>
179+ indented (annTm y (pprintTerm' i (map (\ (n, b) -> (n, False)) env) (delab i y))) <>
180180 if (opt_errContext (idris_options i)) then line <> showSc i env else empty
181181pprintErr' i (CantSolveGoal x env) =
182182 text "Can't solve goal " <>
183− indented (pprintTerm' i (map (\ (n, b) -> (n, False)) env) (delab i x)) <>
183+ indented (annTm x (pprintTerm' i (map (\ (n, b) -> (n, False)) env) (delab i x))) <>
184184 if (opt_errContext (idris_options i)) then line <> showSc i env else empty
185185pprintErr' i (UnifyScope n out tm env) =
186186 text "Can't unify" <> indented (annName n) <+>
187− text "with" <> indented (pprintTerm' i (map (\ (n, b) -> (n, False)) env) (delab i tm)) <+>
188− text "as" <> indented (annName out) <> text "is not in scope" <>
187+ text "with" <> indented (annTm tm (pprintTerm' i (map (\ (n, b) -> (n, False)) env) (delab i tm))) <+>
188+ text "as" <> indented (annName out) <> text "is not in scope" <>
189189 if (opt_errContext (idris_options i)) then line <> showSc i env else empty
190190pprintErr' i (CantInferType t) = text "Can't infer type for" <+> text t
191191pprintErr' i (NonFunctionType f ty) =
192− pprintTerm i (delab i f) <+>
192+ annTm f (pprintTerm i (delab i f)) <+>
193193 text "does not have a function type" <+>
194194 parens (pprintTerm i (delab i ty))
195195pprintErr' i (NotEquality tm ty) =
196− pprintTerm i (delab i tm) <+>
196+ annTm tm (pprintTerm i (delab i tm)) <+>
197197 text "does not have an equality type" <+>
198− parens (pprintTerm i (delab i ty))
198+ annTm ty (parens (pprintTerm i (delab i ty)))
199199pprintErr' i (TooManyArguments f) = text "Too many arguments for" <+> annName f
200200pprintErr' i (CantIntroduce ty) =
201− text "Can't use lambda here: type is" <+> pprintTerm i (delab i ty)
201+ text "Can't use lambda here: type is" <+> annTm ty (pprintTerm i (delab i ty))
202202pprintErr' i (InfiniteUnify x tm env) =
203203 text "Unifying" <+> annName' x (showbasic x) <+> text "and" <+>
204− pprintTerm' i (map (\ (n, b) -> (n, False)) env) (delab i tm) <+>
204+ annTm tm (pprintTerm' i (map (\ (n, b) -> (n, False)) env) (delab i tm)) <+>
205205 text "would lead to infinite value" <>
206206 if (opt_errContext (idris_options i)) then line <> showSc i env else empty
207207pprintErr' i (NotInjective p x y) =
208− text "Can't verify injectivity of" <+> pprintTerm i (delab i p) <+>
209− text " when unifying" <+> pprintTerm i (delab i x) <+> text "and" <+>
210− pprintTerm i (delab i y)
208+ text "Can't verify injectivity of" <+> annTm p (pprintTerm i (delab i p)) <+>
209+ text " when unifying" <+> annTm x (pprintTerm i (delab i x)) <+> text "and" <+>
210+ annTm y (pprintTerm i (delab i y))
211211pprintErr' i (CantResolve c) = text "Can't resolve type class" <+> pprintTerm i (delab i c)
212212pprintErr' i (CantResolveAlts as) = text "Can't disambiguate name:" <+>
213213 align (cat (punctuate (comma <> space) (map (fmap (fancifyAnnots i) . annName) as)))
214214pprintErr' i (NoTypeDecl n) = text "No type declaration for" <+> annName n
215215pprintErr' i (NoSuchVariable n) = text "No such variable" <+> annName n
216−pprintErr' i (IncompleteTerm t) = text "Incomplete term" <+> pprintTerm i (delab i t)
216+pprintErr' i (IncompleteTerm t) = text "Incomplete term" <+> annTm t (pprintTerm i (delab i t))
217217pprintErr' i UniverseError = text "Universe inconsistency"
218218pprintErr' i ProgramLineComment = text "Program line next to comment"
219219pprintErr' i (Inaccessible n) = annName n <+> text "is not an accessible pattern variable"
@@ -222,7 +222,7 @@ pprintErr' i (NonCollapsiblePostulate n) = text "The return type of postulate" <
222222pprintErr' i (AlreadyDefined n) = annName n<+>
223223 text "is already defined"
224224pprintErr' i (ProofSearchFail e) = pprintErr' i e
225−pprintErr' i (NoRewriting tm) = text "rewrite did not change type" <+> pprintTerm i (delab i tm)
225+pprintErr' i (NoRewriting tm) = text "rewrite did not change type" <+> annTm tm (pprintTerm i (delab i tm))
226226pprintErr' i (At f e) = annotate (AnnFC f) (text (show f)) <> colon <> pprintErr' i e
227227pprintErr' i (Elaborating s n e) = text "When elaborating" <+> text s <>
228228 annName' n (showqual i n) <> colon <$>
@@ -273,6 +273,9 @@ annName n = annName' n (showbasic n)
273273annName' :: Name -> String -> Doc OutputAnnotation
274274annName' n str = annotate (AnnName n Nothing Nothing Nothing) (text str)
275275
276+annTm :: Term -> Doc OutputAnnotation -> Doc OutputAnnotation
277+annTm tm = annotate (AnnTerm tm)
278+
276279fancifyAnnots :: IState -> OutputAnnotation -> OutputAnnotation
277280fancifyAnnots ist annot@(AnnName n _ _ _) =
278281 do let ctxt = tt_ctxt ist