@@ -127,7 +127,10 @@ indented :: Doc a -> Doc a
127127indented = nest errorIndent . (line <>)
128128
129129pprintTerm :: IState -> PTerm -> Doc OutputAnnotation
130−pprintTerm ist = prettyImp (opt_showimp (idris_options ist))
130+pprintTerm ist = pprintTerm' ist []
131+
132+pprintTerm' :: IState -> [(Name, Bool)] -> PTerm -> Doc OutputAnnotation
133+pprintTerm' ist = pprintPTerm (opt_showimp (idris_options ist))
131134
132135pshow :: IState -> Err -> String
133136pshow ist err = displayDecorated (consoleDecorate ist) .
@@ -144,23 +147,26 @@ pprintErr' i (InternalMsg s) =
144147 text ("Please consider reporting at " ++ bugaddr)
145148 ]
146149pprintErr' i (CantUnify _ x y e sc s) =
147− text "Can't unify" <> indented (pprintTerm i (delab i x)) <$>
148− text "with" <> indented (pprintTerm i (delab i y)) <>
150+ text "Can't unify" <> indented (pprintTerm' i (map (\ (n, b) -> (n, False)) sc) (delab i x)) <$>
151+ text "with" <> indented (pprintTerm' i (map (\ (n, b) -> (n, False)) sc) (delab i y)) <>
149152 case e of
150153 Msg "" -> empty
151154 _ -> line <> line <> text "Specifically:" <>
152155 indented (pprintErr' i e) <>
153156 if (opt_errContext (idris_options i)) then text $ showSc i sc else empty
154157pprintErr' i (CantConvert x y env) =
155− text "Can't convert" <> indented (pprintTerm i (delab i x)) <$>
156− text "with" <> indented (pprintTerm i (delab i y)) <>
158+ text "Can't convert" <>
159+ indented (pprintTerm' i (map (\ (n, b) -> (n, False)) env) (delab i x)) <$>
160+ text "with" <>
161+ indented (pprintTerm' i (map (\ (n, b) -> (n, False)) env) (delab i y)) <>
157162 if (opt_errContext (idris_options i)) then line <> text (showSc i env) else empty
158163pprintErr' i (CantSolveGoal x env) =
159− text "Can't solve goal " <> indented (pprintTerm i (delab i x)) <>
164+ text "Can't solve goal " <>
165+ indented (pprintTerm' i (map (\ (n, b) -> (n, False)) env) (delab i x)) <>
160166 if (opt_errContext (idris_options i)) then line <> text (showSc i env) else empty
161167pprintErr' i (UnifyScope n out tm env) =
162168 text "Can't unify" <> indented (annName n) <+>
163− text "with" <> indented (pprintTerm i (delab i tm)) <+>
169+ text "with" <> indented (pprintTerm' i (map (\ (n, b) -> (n, False)) env) (delab i tm)) <+>
164170 text "as" <> indented (annName out) <> text "is not in scope" <>
165171 if (opt_errContext (idris_options i)) then line <> text (showSc i env) else empty
166172pprintErr' i (CantInferType t) = text "Can't infer type for" <+> text t
@@ -176,7 +182,8 @@ pprintErr' i (TooManyArguments f) = text "Too many arguments for" <+> annName f
176182pprintErr' i (CantIntroduce ty) =
177183 text "Can't use lambda here: type is" <+> pprintTerm i (delab i ty)
178184pprintErr' i (InfiniteUnify x tm env) =
179− text "Unifying" <+> annName' x (showbasic x) <+> text "and" <+> pprintTerm i (delab i tm) <+>
185+ text "Unifying" <+> annName' x (showbasic x) <+> text "and" <+>
186+ pprintTerm' i (map (\ (n, b) -> (n, False)) env) (delab i tm) <+>
180187 text "would lead to infinite value" <>
181188 if (opt_errContext (idris_options i)) then line <> text (showSc i env) else empty
182189pprintErr' i (NotInjective p x y) =