@@ -152,17 +152,17 @@ pprintErr' i (CantUnify _ x y e sc s) =
152 indented (pprintErr' i e) <>
152 indented (pprintErr' i e) <>
153 if (opt_errContext (idris_options i)) then text $ showSc i sc else empty
153 if (opt_errContext (idris_options i)) then text $ showSc i sc else empty
154pprintErr' i (CantConvert x y env) =
154pprintErr' i (CantConvert x y env) =
155− text "Can't convert" <> indented (pprintTerm i (delab i x)) <>
155+ text "Can't convert" <> indented (pprintTerm i (delab i x)) <$>
156 text "with" <> indented (pprintTerm i (delab i y)) <>
156 text "with" <> indented (pprintTerm i (delab i y)) <>
157− if (opt_errContext (idris_options i)) then text (showSc i env) else empty
157+ if (opt_errContext (idris_options i)) then line <> text (showSc i env) else empty
158pprintErr' i (CantSolveGoal x env) =
158pprintErr' i (CantSolveGoal x env) =
159 text "Can't solve goal " <> indented (pprintTerm i (delab i x)) <>
159 text "Can't solve goal " <> indented (pprintTerm i (delab i x)) <>
160− if (opt_errContext (idris_options i)) then text (showSc i env) else empty
160+ if (opt_errContext (idris_options i)) then line <> text (showSc i env) else empty
161pprintErr' i (UnifyScope n out tm env) =
161pprintErr' i (UnifyScope n out tm env) =
162 text "Can't unify" <> indented (annName n) <+>
162 text "Can't unify" <> indented (annName n) <+>
163 text "with" <> indented (pprintTerm i (delab i tm)) <+>
163 text "with" <> indented (pprintTerm i (delab i tm)) <+>
164 text "as" <> indented (annName out) <> text "is not in scope" <>
164 text "as" <> indented (annName out) <> text "is not in scope" <>
165− if (opt_errContext (idris_options i)) then text (showSc i env) else empty
165+ if (opt_errContext (idris_options i)) then line <> text (showSc i env) else empty
166pprintErr' i (CantInferType t) = text "Can't infer type for" <+> text t
166pprintErr' i (CantInferType t) = text "Can't infer type for" <+> text t
167pprintErr' i (NonFunctionType f ty) =
167pprintErr' i (NonFunctionType f ty) =
168 pprintTerm i (delab i f) <+>
168 pprintTerm i (delab i f) <+>
@@ -178,7 +178,7 @@ pprintErr' i (CantIntroduce ty) =
178pprintErr' i (InfiniteUnify x tm env) =
178pprintErr' i (InfiniteUnify x tm env) =
179 text "Unifying" <+> annName' x (showbasic x) <+> text "and" <+> pprintTerm i (delab i tm) <+>
179 text "Unifying" <+> annName' x (showbasic x) <+> text "and" <+> pprintTerm i (delab i tm) <+>
180 text "would lead to infinite value" <>
180 text "would lead to infinite value" <>
181− if (opt_errContext (idris_options i)) then text (showSc i env) else empty
181+ if (opt_errContext (idris_options i)) then line <> text (showSc i env) else empty
182pprintErr' i (NotInjective p x y) =
182pprintErr' i (NotInjective p x y) =
183 text "Can't verify injectivity of" <+> pprintTerm i (delab i p) <+>
183 text "Can't verify injectivity of" <+> pprintTerm i (delab i p) <+>
184 text " when unifying" <+> pprintTerm i (delab i x) <+> text "and" <+>
184 text " when unifying" <+> pprintTerm i (delab i x) <+> text "and" <+>