
   0 | module Idris.Error
   1 | 
   2 | import Core.Env
   3 | 
   4 | import Idris.Doc.String
   5 | import Idris.REPL.Opts
   6 | import Idris.Resugar
   7 | import Idris.Syntax
   8 | import Idris.Pretty
   9 | 
  10 | import Data.List
  11 | import Data.Either
  12 | import Data.List1
  13 | import Data.String
  14 | 
  15 | import Libraries.Data.List.Extra
  16 | import Libraries.Text.PrettyPrint.Prettyprinter.Util
  17 | 
  18 | import System.File
  19 | 
  20 | %default covering
  21 | 
  22 | -- Not fully correct, see e.g. `UnreachableClause` where we don't check the
  23 | -- Envs & Terms because we don't yet have equality instances for these
  24 | export
  25 | Eq Warning where
  26 |   ParserWarning fc1 x1 == ParserWarning fc2 x2 = fc1 == fc2 && x1 == x2
  27 |   UnreachableClause fc1 rho1 s1 == UnreachableClause fc2 rho2 s2 = fc1 == fc2
  28 |   ShadowingGlobalDefs fc1 xs1 == ShadowingGlobalDefs fc2 xs2 = fc1 == fc2 && xs1 == xs2
  29 |   IncompatibleVisibility fc1 x1 y1 n1 == IncompatibleVisibility fc2 x2 y2 n2
  30 |     = fc1 == fc2 && x1 == x2 && y1 == y2 && n1 == n2
  31 |   Deprecated fc1 x1 y1 == Deprecated fc2 x2 y2 = fc1 == fc2 && x1 == x2 && y1 == y2
  32 |   GenericWarn fc1 x1 == GenericWarn fc2 x2 = fc1 == fc2 && x1 == x2
  33 |   _ == _ = False
  34 | 
  35 | export
  36 | Eq TTCErrorMsg where
  37 |   Format x1 y1 z1 == Format x2 y2 z2 = x1 == x2 && y1 == y2 && z1 == z2
  38 |   EndOfBuffer x1 == EndOfBuffer x2 = x1 == x2
  39 |   Corrupt x1 == Corrupt x2 = x1 == x2
  40 |   _ == _ = False
  41 | 
  42 | export
  43 | Eq FileError where
  44 |   GenericFileError x1 == GenericFileError x2 = x1 == x2
  45 |   FileReadError == FileReadError = True
  46 |   FileWriteError == FileWriteError = True
  47 |   FileNotFound == FileNotFound = True
  48 |   PermissionDenied == PermissionDenied = True
  49 |   FileExists == FileExists = True
  50 |   _ == _ = False
  51 | 
  52 | -- Not fully correct, see e.g. `CantConvert` where we don't check the Env
  53 | export
  54 | Eq Error where
  55 |   Fatal err1 == Fatal err2 = err1 == err2
  56 |   CantConvert fc1 gam1 rho1 s1 t1 == CantConvert fc2 gam2 rho2 s2 t2 = fc1 == fc2
  57 |   CantSolveEq fc1 gam1 rho s1 t1 == CantSolveEq fc2 gam2 rho2 s2 t2 = fc1 == fc2
  58 |   PatternVariableUnifies fc1 fct1 rho1 n1 s1 == PatternVariableUnifies fc2 fct2 rho2 n2 s2 = fc1 == fc2 && fct1 == fct2 && n1 == n2
  59 |   CyclicMeta fc1 rho1 n1 s1 == CyclicMeta fc2 rho2 n2 s2 = fc1 == fc2 && n1 == n2
  60 |   WhenUnifying fc1 gam1 rho1 s1 t1 err1 == WhenUnifying fc2 gam2 rho2 s2 t2 err2 = fc1 == fc2 && err1 == err2
  61 |   ValidCase fc1 rho1 x1 == ValidCase fc2 rho2 x2 = fc1 == fc2
  62 |   UndefinedName fc1 n1 == UndefinedName fc2 n2 = fc1 == fc2 && n1 == n2
  63 |   InvisibleName fc1 n1 x1 == InvisibleName fc2 n2 x2 = fc1 == fc2 && n1 == n2 && x1 == x2
  64 |   BadTypeConType fc1 n1 == BadTypeConType fc2 n2 = fc1 == fc2 && n1 == n2
  65 |   BadDataConType fc1 n1 m1 == BadDataConType fc2 n2 m2 = fc1 == fc2 && n1 == n2 && m1 == m2
  66 |   NotCovering fc1 n1 x1 == NotCovering fc2 n2 x2 = fc1 == fc2 && n1 == n2
  67 |   NotTotal fc1 n1 x1 == NotTotal fc2 n2 x2 = fc1 == fc2 && n1 == n2
  68 |   LinearUsed fc1 k1 n1 == LinearUsed fc2 k2 n2 = fc1 == fc2 && k1 == k2 && n1 == n2
  69 |   LinearMisuse fc1 n1 x1 y1 == LinearMisuse fc2 n2 x2 y2 = fc1 == fc2 && n1 == n2 && x1 == x2 && y1 == y2
  70 |   BorrowPartial fc1 rho1 s1 t1 == BorrowPartial fc2 rho2 s2 t2 = fc1 == fc2
  71 |   BorrowPartialType fc1 rho1 s1 == BorrowPartialType fc2 rho2 s2 = fc1 == fc2
  72 |   AmbiguousName fc1 xs1 == AmbiguousName fc2 xs2 = fc1 == fc2 && xs1 == xs2
  73 |   AmbiguousElab fc1 rho1 xs1 == AmbiguousElab fc2 rho2 xs2 = fc1 == fc2
  74 |   AmbiguousSearch fc1 rho1 s1 xs1 == AmbiguousSearch fc2 rho2 s2 xs2 = fc1 == fc2
  75 |   AmbiguityTooDeep fc1 n1 xs1 == AmbiguityTooDeep fc2 n2 xs2 = fc1 == fc2 && n1 == n2 && xs1 == xs2
  76 |   AllFailed xs1 == AllFailed xs2 = assert_total (xs1 == xs2)
  77 |   RecordTypeNeeded fc1 rho1 == RecordTypeNeeded fc2 rho2 = fc1 == fc2
  78 |   DuplicatedRecordUpdatePath fc1 xs1 == DuplicatedRecordUpdatePath fc2 xs2 = fc1 == fc2 && xs1 == xs2
  79 |   NotRecordField fc1 x1 y1 == NotRecordField fc2 x2 y2 = fc1 == fc2 && x1 == x2 && y1 == y2
  80 |   NotRecordType fc1 n1 == NotRecordType fc2 n2 = fc1 == fc2 && n1 == n2
  81 |   IncompatibleFieldUpdate fc1 xs1 == IncompatibleFieldUpdate fc2 xs2 = fc1 == fc2 && xs1 == xs2
  82 |   InvalidArgs fc1 rho1 xs1 s1 == InvalidArgs fc2 rho2 xs2 s2 = fc1 == fc2
  83 |   TryWithImplicits fc1 rho1 xs1 == TryWithImplicits fc2 rho2 xs2 = fc1 == fc2
  84 |   BadUnboundImplicit fc1 rho1 n1 s1 == BadUnboundImplicit fc2 rho2 n2 s2 = fc1 == fc2 && n1 == n2
  85 |   CantSolveGoal fc1 gam1 rho1 s1 x1 == CantSolveGoal fc2 gam2 rho2 s2 x2 = fc1 == fc2
  86 |   DeterminingArg fc1 n1 x1 rho1 s1 == DeterminingArg fc2 n2 x2 rho2 s2 = fc1 == fc2 && n1 == n2 && x1 == x2
  87 |   UnsolvedHoles xs1 == UnsolvedHoles xs2 = xs1 == xs2
  88 |   CantInferArgType fc1 rho1 n1 m1 s1 == CantInferArgType fc2 rho2 n2 m2 s2 = fc1 == fc2 && n1 == n2 && m1 == m2
  89 |   SolvedNamedHole fc1 rho1 n1 s1 == SolvedNamedHole fc2 rho2 n2 s2 = fc1 == fc2 && n1 == n2
  90 |   VisibilityError fc1 x1 n1 y1 m1 == VisibilityError fc2 x2 n2 y2 m2
  91 |     = fc1 == fc2 && x1 == x2 && n1 == n2 && y1 == y2 && m1 == m2
  92 |   NonLinearPattern fc1 n1 == NonLinearPattern fc2 n2 = fc1 == fc2 && n1 == n2
  93 |   BadPattern fc1 n1 == BadPattern fc2 n2 =  fc1 == fc2 && n1 == n2
  94 |   NoDeclaration fc1 n1 == NoDeclaration fc2 n2 = fc1 == fc2 && n1 == n2
  95 |   AlreadyDefined fc1 n1 == AlreadyDefined fc2 n2 = fc1 == fc2 && n1 == n2
  96 |   NotFunctionType fc1 rho1 s1 == NotFunctionType fc2 rho2 s2 = fc1 == fc2
  97 |   RewriteNoChange fc1 rho1 s1 t1 == RewriteNoChange fc2 rho2 s2 t2 = fc1 == fc2
  98 |   NotRewriteRule fc1 rho1 s1 == NotRewriteRule fc2 rho2 s2 = fc1 == fc2
  99 |   CaseCompile fc1 n1 x1 == CaseCompile fc2 n2 x2 = fc1 == fc2 && n1 == n2
 100 |   MatchTooSpecific fc1 rho1 s1 == MatchTooSpecific fc2 rho2 s2 = fc1 == fc2
 101 |   BadDotPattern fc1 rho1 x1 s1 t1 == BadDotPattern fc2 rho2 x2 s2 t2 = fc1 == fc2
 102 |   BadImplicit fc1 x1 == BadImplicit fc2 x2 = fc1 == fc2 && x1 == x2
 103 |   BadRunElab fc1 rho1 s1 d1 == BadRunElab fc2 rho2 s2 d2 = fc1 == fc2 && d1 == d2
 104 |   RunElabFail e1 == RunElabFail e2 = e1 == e2
 105 |   GenericMsg fc1 x1 == GenericMsg fc2 x2 = fc1 == fc2 && x1 == x2
 106 |   GenericMsgSol fc1 x1 y1 z1 == GenericMsgSol fc2 x2 y2 z2 = fc1 == fc2 && x1 == x2 && y1 == y2 && z1 == z2
 107 |   TTCError x1 == TTCError x2 = x1 == x2
 108 |   FileErr x1 y1 == FileErr x2 y2 = x1 == x2 && y1 == y2
 109 |   CantFindPackage x1 == CantFindPackage x2 = x1 == x2
 110 |   LitFail fc1 == LitFail fc2 = fc1 == fc2
 111 |   LexFail fc1 x1 == LexFail fc2 x2 = fc1 == fc2 && x1 == x2
 112 |   ParseFail xs1 == ParseFail xs2 = xs1 == xs2
 113 |   ModuleNotFound fc1 x1 == ModuleNotFound fc2 x2 = fc1 == fc2 && x1 == x2
 114 |   CyclicImports xs1 == CyclicImports xs2 = xs1 == xs2
 115 |   ForceNeeded == ForceNeeded = True
 116 |   InternalError x1 == InternalError x2 = x1 == x2
 117 |   UserError x1 == UserError x2 = x1 == x2
 118 |   NoForeignCC fc1 xs1 == NoForeignCC fc2 xs2 = fc1 == fc2 && xs1 == xs2
 119 |   BadMultiline fc1 x1 == BadMultiline fc2 x2 = fc1 == fc2 && x1 == x2
 120 |   Timeout x1 == Timeout x2 = x1 == x2
 121 |   FailingDidNotFail fc1 == FailingDidNotFail fc2 = fc1 == fc2
 122 |   FailingWrongError fc1 x1 err1 == FailingWrongError fc2 x2 err2
 123 |     = fc1 == fc2 && x1 == x2 && assert_total (err1 == err2)
 124 |   InType fc1 n1 err1 == InType fc2 n2 err2 = fc1 == fc2 && n1 == n2 && err1 == err2
 125 |   InCon n1 err1 == InCon n2 err2 = n1 == n2 && err1 == err2
 126 |   InLHS fc1 n1 err1 == InLHS fc2 n2 err2 = fc1 == fc2 && n1 == n2 && err1 == err2
 127 |   InRHS fc1 n1 err1 == InRHS fc2 n2 err2 = fc1 == fc2 && n1 == n2 && err1 == err2
 128 |   MaybeMisspelling err1 xs1 == MaybeMisspelling err2 xs2 = err1 == err2 && xs1 == xs2
 129 |   WarningAsError wrn1 == WarningAsError wrn2 = wrn1 == wrn2
 130 |   _ == _ = False
 131 | 
 132 | keyword : Doc IdrisAnn -> Doc IdrisAnn
 133 | keyword = annotate (Syntax Keyword)
 134 | 
 135 | -- | Add binding site information if the term is simply a machine-inserted name
 136 | pShowMN : {vars : _} -> Term vars -> Env t vars -> Doc IdrisAnn -> Doc IdrisAnn
 137 | pShowMN t env acc = case t of
 138 |   Local fc _ idx p => case dropAllNS (nameAt p) of
 139 |       MN {} => acc <++> parens ("implicitly bound at" <++> pretty0 (getBinderLoc p env))
 140 |       _ => acc
 141 |   _ => acc
 142 | 
 143 | pshow : {vars : _} ->
 144 |         {auto c : Ref Ctxt Defs} ->
 145 |         {auto s : Ref Syn SyntaxInfo} ->
 146 |         Env Term vars -> Term vars -> Core (Doc IdrisAnn)
 147 | pshow env tm
 148 |     = do defs <- get Ctxt
 149 |          ntm <- normaliseHoles defs env tm
 150 |          itm <- resugar env ntm
 151 |          pure (pShowMN ntm env $ prettyBy Syntax itm)
 152 | 
 153 | pshowNoNorm : {vars : _} ->
 154 |               {auto c : Ref Ctxt Defs} ->
 155 |               {auto s : Ref Syn SyntaxInfo} ->
 156 |               Env Term vars -> Term vars -> Core (Doc IdrisAnn)
 157 | pshowNoNorm env tm
 158 |     = do defs <- get Ctxt
 159 |          itm <- resugar env tm
 160 |          pure (pShowMN tm env $ prettyBy Syntax itm)
 161 | 
 162 | ploc : {auto o : Ref ROpts REPLOpts} ->
 163 |        FC -> Core (Doc IdrisAnn)
 164 | ploc fc = do
 165 |     let Just (fn, s, e) = isNonEmptyFC fc
 166 |         | Nothing => pure emptyDoc
 167 |     let (sr, sc) = mapHom (fromInteger . cast) s
 168 |     let (er, ec) = mapHom (fromInteger . cast) e
 169 |     let nsize = length $ show (er + 1)
 170 |     let head = annotate FileCtxt (pretty0 fc)
 171 |     source <- lines <$> getCurrentElabSource
 172 |     if sr == er
 173 |        then do
 174 |          let emph = spaces (cast $ nsize + sc + 4) <+> annotate Error (pretty0 (replicate (ec `minus` sc) '^'))
 175 |          let firstr = er `minus` 4
 176 |          pure $ vsep ([emptyDoc, head] ++ (addLineNumbers nsize firstr (pretty0 <$> extractRange firstr er source)) ++ [emph]) <+> line
 177 |        else pure $ vsep (emptyDoc :: head :: addLineNumbers nsize sr (pretty0 <$> extractRange sr (Prelude.min er (sr + 5)) source)) <+> line
 178 |   where
 179 |     extractRange : Nat -> Nat -> List String -> List String
 180 |     extractRange s e xs = take ((e `minus` s) + 1) (drop s xs)
 181 |     pad : Nat -> String -> String
 182 |     pad size s = replicate (size `minus` length s) '0' ++ s
 183 |     addLineNumbers : Nat -> Nat -> List (Doc IdrisAnn) -> List (Doc IdrisAnn)
 184 |     addLineNumbers size st xs =
 185 |       snd $ foldl (\(i, s), l => (S i, snoc s (space <+> annotate FileCtxt (pretty0 (pad size $ show $ i + 1) <++> pipe) <++> l))) (st, []) xs
 186 | 
 187 | -- Assumes the two FCs are sorted
 188 | ploc2 : {auto o : Ref ROpts REPLOpts} ->
 189 |         FC -> FC -> Core (Doc IdrisAnn)
 190 | ploc2 fc1 fc2 =
 191 |     do let Just (fn1, s1, e1) = isNonEmptyFC fc1
 192 |            | Nothing => ploc fc2
 193 |        let Just (fn2, s2, e2) = isNonEmptyFC fc2
 194 |            | Nothing => ploc fc1
 195 |        let (sr1, sc1) = mapHom (fromInteger . cast) s1
 196 |        let (sr2, sc2) = mapHom (fromInteger . cast) s2
 197 |        let (er1, ec1) = mapHom (fromInteger . cast) e1
 198 |        let (er2, ec2) = mapHom (fromInteger . cast) e2
 199 |        if (er2 > the Nat (er1 + 5))
 200 |           then pure $ !(ploc (MkFC fn1 s1 e1)) <+> line <+> !(ploc (MkFC fn2 s2 e2))
 201 |           else do let nsize = length $ show (er2 + 1)
 202 |                   let head = annotate FileCtxt (pretty0 $ MkFC fn1 s1 e2)
 203 |                   let firstRow = annotate FileCtxt (spaces (cast $ nsize + 2) <+> pipe)
 204 |                   source <- lines <$> getCurrentElabSource
 205 |                   case (sr1 == er1, sr2 == er2, sr1 == sr2) of
 206 |                        (True, True, True) => do
 207 |                          let line = fileCtxt pipe <++> maybe emptyDoc pretty0 (elemAt source sr1)
 208 |                          let emph = fileCtxt pipe <++> spaces (cast sc1) <+> error (pretty0 (replicate (ec1 `minus` sc1) '^'))
 209 |                                       <+> spaces (cast $ sc2 `minus` ec1) <+> error (pretty0 (replicate (ec2 `minus` sc2) '^'))
 210 |                          pure $ vsep [emptyDoc, head, firstRow, fileCtxt (space <+> byShow (sr1 + 1)) <++> align (vsep [line, emph]), emptyDoc]
 211 |                        (True, True, False) => do
 212 |                          let line1 = fileCtxt pipe <++> maybe emptyDoc pretty0 (elemAt source sr1)
 213 |                          let emph1 = fileCtxt pipe <++> spaces (cast sc1) <+> error (pretty0 (replicate (ec1 `minus` sc1) '^'))
 214 |                          let line2 = fileCtxt pipe <++> maybe emptyDoc pretty0 (elemAt source sr2)
 215 |                          let emph2 = fileCtxt pipe <++> spaces (cast sc2) <+> error (pretty0 (replicate (ec2 `minus` sc2) '^'))
 216 |                          let numbered = if (sr2 `minus` er1) == 1
 217 |                                            then []
 218 |                                            else addLineNumbers nsize (sr1 + 1) (pretty0 <$> extractRange (sr1 + 1) er1 source)
 219 |                          pure $ vsep $ [emptyDoc, head, firstRow, fileCtxt (space <+> byShow (sr1 + 1)) <++> align (vsep [line1, emph1])]
 220 |                             ++ numbered
 221 |                             ++ [fileCtxt (space <+> byShow (sr2 + 1)) <++> align (vsep [line2, emph2]), emptyDoc]
 222 |                        (True, False, _) => do
 223 |                          let line = fileCtxt pipe <++> maybe emptyDoc pretty0 (elemAt source sr1)
 224 |                          let emph = fileCtxt pipe <++> spaces (cast sc1) <+> error (pretty0 (replicate (ec1 `minus` sc1) '^'))
 225 |                          pure $ vsep $ [emptyDoc, head, firstRow, fileCtxt (space <+> byShow (sr1 + 1)) <++> align (vsep [line, emph])]
 226 |                             ++ addLineNumbers nsize (sr1 + 1) (pretty0 <$> extractRange (sr1 + 1) (Prelude.max er1 er2) source)
 227 |                             ++ [emptyDoc]
 228 |                        (False, True, True) => do
 229 |                          let line = fileCtxt pipe <++> maybe emptyDoc pretty0 (elemAt source sr1)
 230 |                          let emph = fileCtxt pipe <++> spaces (cast sc1) <+> error (pretty0 (replicate (ec1 `minus` sc1) '^'))
 231 |                          pure $ vsep $ [emptyDoc, head, firstRow, fileCtxt (space <+> byShow (sr1 + 1)) <++> align (vsep [line, emph])]
 232 |                             ++ addLineNumbers nsize (sr1 + 1) (pretty0 <$> extractRange (sr1 + 1) (Prelude.max er1 er2) source)
 233 |                             ++ [emptyDoc]
 234 |                        (False, True, False) => do
 235 |                          let top = addLineNumbers nsize (sr1 + 1) (pretty0 <$> extractRange (sr1 + 1) er1 source)
 236 |                          let line = fileCtxt pipe <++> maybe emptyDoc pretty0 (elemAt source sr1)
 237 |                          let emph = fileCtxt pipe <++> spaces (cast sc2) <+> error (pretty0 (replicate (ec2 `minus` sc2) '^'))
 238 |                          pure $ vsep $ [emptyDoc, head, firstRow] ++ top ++ [fileCtxt (space <+> byShow (sr2 + 1)) <++> align (vsep [line, emph]), emptyDoc]
 239 |                        (_, _, _) => pure $ vsep (emptyDoc :: head :: addLineNumbers nsize sr1 (pretty0 <$> extractRange sr1 er2 source)) <+> line
 240 |   where
 241 |     extractRange : Nat -> Nat -> List String -> List String
 242 |     extractRange s e xs = take ((e `minus` s) + 1) (drop s xs)
 243 |     pad : Nat -> String -> String
 244 |     pad size s = replicate (size `minus` length s) '0' ++ s
 245 |     addLineNumbers : Nat -> Nat -> List (Doc IdrisAnn) -> List (Doc IdrisAnn)
 246 |     addLineNumbers size st xs =
 247 |       snd $ foldl (\(i, s), l => (S i, snoc s (space <+> annotate FileCtxt (pretty0 (pad size $ show $ i + 1) <++> pipe) <++> l))) (st, []) xs
 248 | 
 249 | export
 250 | pwarningRaw : {auto c : Ref Ctxt Defs} ->
 251 |               {auto s : Ref Syn SyntaxInfo} ->
 252 |               {auto o : Ref ROpts REPLOpts} ->
 253 |               Warning -> Core (Doc IdrisAnn)
 254 | pwarningRaw (ParserWarning fc msg)
 255 |     = pure $ pretty0 msg <+> line <+> !(ploc fc)
 256 | pwarningRaw (UnreachableClause fc env tm)
 257 |     = pure $ errorDesc (reflow "Unreachable clause:"
 258 |         <++> code !(pshow env tm))
 259 |         <+> line <+> !(ploc fc)
 260 | pwarningRaw (ShadowingGlobalDefs fc ns)
 261 |     = pure $ vcat
 262 |     $ reflow "We are about to implicitly bind the following lowercase names."
 263 |    :: reflow "You may be unintentionally shadowing the associated global definitions:"
 264 |    :: map pshadowing (forget ns)
 265 |    `snoc` !(ploc fc)
 266 |   where
 267 |     pshadowing : (Name, List1 Name) -> Doc IdrisAnn
 268 |     pshadowing (n, ns) = indent 2 $ hsep $
 269 |                            pretty0 n
 270 |                         :: reflow "is shadowing"
 271 |                         :: punctuate comma (map pretty0 (forget ns))
 272 | 
 273 | pwarningRaw (IncompatibleVisibility fc vx vy n)
 274 |     = pure $ warning (code (pretty0 (sugarName n))
 275 |         <++> reflow "has been forward-declared with"
 276 |         <++> keyword (pretty0 vx) <++> reflow "visibility, cannot change to"
 277 |         <++> keyword (pretty0 vy) <+> reflow ". This will be an error in a later release.")
 278 |         <+> line <+> !(ploc fc)
 279 | 
 280 | pwarningRaw (ShadowingLocalBindings fc ns)
 281 |     = pure $ vcat
 282 |     [ reflow "You may be unintentionally shadowing the following local bindings:"
 283 |     , indent 2 $ concatWith (surround (comma <+> space)) $ map (code . pretty0 . fst) $ forget ns
 284 |     , !(ploc fc)
 285 |     ]
 286 | 
 287 | pwarningRaw (Deprecated fc s fcAndName)
 288 |     = do docs <- traverseOpt (\(fc, name) => getDocsForName fc name justUserDoc) fcAndName
 289 |          pure . vsep $ catMaybes [ Just $ "Deprecation warning:" <++> pretty0 s
 290 |                                  , reAnnotate (const Pretty.UserDocString) <$> docs
 291 |                                  ]
 292 | pwarningRaw (GenericWarn fc s)
 293 |     = pure $ vcat [pretty0 s, !(ploc fc)]
 294 | 
 295 | export
 296 | pwarning : {auto c : Ref Ctxt Defs} ->
 297 |            {auto s : Ref Syn SyntaxInfo} ->
 298 |            {auto o : Ref ROpts REPLOpts} ->
 299 |            Warning -> Core (Doc IdrisAnn)
 300 | pwarning wrn = pwarningRaw !(toFullNames wrn)
 301 | 
 302 | perrorRaw : {auto c : Ref Ctxt Defs} ->
 303 |             {auto s : Ref Syn SyntaxInfo} ->
 304 |             {auto o : Ref ROpts REPLOpts} ->
 305 |             Error -> Core (Doc IdrisAnn)
 306 | perrorRaw (Fatal err) = perrorRaw err
 307 | perrorRaw (CantConvert fc gam env l r)
 308 |     = do defs <- get Ctxt
 309 |          setCtxt gam
 310 |          let res = errorDesc (hsep [ reflow "Mismatch between" <+> colon
 311 |                   , code !(pshow env l)
 312 |                   , "and"
 313 |                   , code !(pshow env r) <+> dot
 314 |                   ]) <+> line <+> !(ploc fc)
 315 |          put Ctxt defs
 316 |          pure res
 317 | perrorRaw (CantSolveEq fc gam env l r)
 318 |     = do defs <- get Ctxt
 319 |          setCtxt gam
 320 |          let res = errorDesc (hsep [ reflow "Can't solve constraint between" <+> colon
 321 |                       , code !(pshow env l)
 322 |                       , "and"
 323 |                       , code !(pshow env r) <+> dot
 324 |                       ]) <+> line <+> !(ploc fc)
 325 |          put Ctxt defs
 326 |          pure res
 327 | perrorRaw (PatternVariableUnifies fc fct env n tm)
 328 |     = do let (min, max) = order fc fct
 329 |          pure $ errorDesc (hsep [ reflow "Pattern variable"
 330 |                   , code (prettyVar n)
 331 |                   , reflow "unifies with" <+> colon
 332 |                   , code !(pshow env tm) <+> dot
 333 |                   ]) <+> line <+> !(ploc2 min max) <+> line
 334 |                      <+> reflow "Suggestion: Use the same name for both pattern variables, since they unify."
 335 |   where
 336 |     prettyVar : Name -> Doc IdrisAnn
 337 |     prettyVar (PV n _) = prettyVar n
 338 |     prettyVar n = pretty0 n
 339 |     order : FC -> FC -> (FC, FC)
 340 |     order fc1 fc2 =
 341 |       let Just (_, sr1, sc1) = isNonEmptyFC fc1
 342 |            | Nothing => (EmptyFC, fc2)
 343 |           Just (_, sr2, sc2) = isNonEmptyFC fc2
 344 |            | Nothing => (fc1, EmptyFC)
 345 |       in if sr1 < sr2 then (fc1, fc2) else if sr1 == sr2 && sc1 < sc2 then (fc1, fc2) else (fc2, fc1)
 346 | perrorRaw (CyclicMeta fc env n tm)
 347 |     = pure $ errorDesc (reflow "Cycle detected in solution of metavariable"
 348 |         <++> meta (pretty0 !(prettyName n)) <++> equals
 349 |         <++> code !(pshow env tm)) <+> line <+> !(ploc fc)
 350 | perrorRaw (WhenUnifying _ gam env x y err)
 351 |     = do defs <- get Ctxt
 352 |          setCtxt gam
 353 |          let res = errorDesc (reflow "When unifying:" <+> line
 354 |                    <+> "    " <+> code !(pshow env x) <+> line <+> "and:" <+> line
 355 |                    <+> "    " <+> code !(pshow env y)) <+> line <+> !(perrorRaw err)
 356 |          put Ctxt defs
 357 |          pure res
 358 | perrorRaw (ValidCase fc env (Left tm))
 359 |     = pure $ errorDesc (code !(pshow env tm) <++> reflow "is not a valid impossible case.")
 360 |         <+> line <+> !(ploc fc)
 361 | perrorRaw (ValidCase _ env (Right err))
 362 |     = pure $ errorDesc (reflow "Impossible pattern gives an error" <+> colon) <+> line <+> !(perrorRaw err)
 363 | perrorRaw (UndefinedName fc x)
 364 |     = pure $ errorDesc (reflow "Undefined name" <++> code (pretty0 x) <+> dot) <++> line <+> !(ploc fc)
 365 | perrorRaw (InvisibleName fc n (Just ns))
 366 |     = pure $ errorDesc ("Name" <++> code (pretty0 n) <++> reflow "is inaccessible since"
 367 |         <++> code (pretty0 ns) <++> reflow "is not explicitly imported.")
 368 |         <+> line <+> !(ploc fc)
 369 |         <+> line <+> reflow "Suggestion: add an explicit" <++> keyword "export" <++> "or" <++> keyword ("public" <++> "export")
 370 |         <++> reflow "modifier. By default, all names are" <++> keyword "private" <++> reflow "in namespace blocks."
 371 | perrorRaw (InvisibleName fc x Nothing)
 372 |     = pure $ errorDesc ("Name" <++> code (pretty0 x) <++> reflow "is private.") <+> line <+> !(ploc fc)
 373 |         <+> line <+> reflow "Suggestion: add an explicit" <++> keyword "export" <++> "or" <++> keyword ("public" <++> "export")
 374 |         <++> reflow "modifier. By default, all names are" <++> keyword "private" <++> reflow "in namespace blocks."
 375 | perrorRaw (BadTypeConType fc n)
 376 |     = pure $ errorDesc (reflow "Return type of" <++> code (pretty0 n) <++> reflow "must be" <++> code "Type"
 377 |         <+> dot) <+> line <+> !(ploc fc)
 378 | perrorRaw (BadDataConType fc n fam)
 379 |     = pure $ errorDesc (reflow "Return type of" <++> code (pretty0 n) <++> reflow "must be in"
 380 |         <++> code (pretty0 fam)) <++> line <+> !(ploc fc)
 381 | perrorRaw (NotCovering fc n IsCovering)
 382 |     = pure $ errorDesc (reflow "Internal error" <++> parens (reflow "Coverage of" <++> code (pretty0 n)))
 383 | perrorRaw (NotCovering fc n (MissingCases cs))
 384 |     = pure $ errorDesc (code (pretty0 !(prettyName n)) <++> reflow "is not covering.")
 385 |         <+> line <+> !(ploc fc) <+> line
 386 |         <+> reflow "Missing cases" <+> colon <+> line
 387 |         <+> indent 4 (vsep !(traverse (pshow Env.empty) cs)) <+> line
 388 | perrorRaw (NotCovering fc n (NonCoveringCall ns))
 389 |     = pure $ errorDesc (pretty0 !(prettyName n) <++> reflow "is not covering.")
 390 |         <+> line <+> !(ploc fc) <+> line
 391 |         <+> reflow "Calls non covering function" <+>
 392 |         case ns of
 393 |              [fn] => space <+> pretty0 fn
 394 |              _ => pretty0 's' <+> colon <++> concatWith (surround (comma <+> space)) (pretty0 <$> ns)
 395 | perrorRaw (NotTotal fc n r)
 396 |     = pure $ errorDesc (code (pretty0 !(prettyName n)) <++> reflow "is not total," <++> pretty0 r)
 397 |         <+> line <+> !(ploc fc)
 398 | perrorRaw ImpossibleCase
 399 |     = pure $ errorDesc (reflow "<ImpossibleCase: this should never be displayed>")
 400 | perrorRaw (LinearUsed fc count n)
 401 |     = pure $ errorDesc (reflow "There are" <++> byShow count <++> reflow "uses of linear name"
 402 |         <++> code (pretty0 (sugarName n)) <+> dot)
 403 |         <++> line <+> !(ploc fc)
 404 |         <+> line <+> reflow "Suggestion: linearly bounded variables must be used exactly once."
 405 | perrorRaw (LinearMisuse fc n exp ctx)
 406 |     = if isErased exp
 407 |          then pure $ errorDesc (code (pretty0 n) <++> reflow "is not accessible in this context.")
 408 |                 <+> line <+> !(ploc fc)
 409 |          else pure $ errorDesc (reflow "Trying to use" <++> prettyRig exp <++> "name"
 410 |                 <++> code (pretty0 (sugarName n)) <++> "in" <++> prettyRel ctx <++> "context.")
 411 |                 <+> line <+> !(ploc fc)
 412 |   where
 413 |     prettyRig : RigCount -> Doc ann
 414 |     prettyRig = elimSemi "irrelevant"
 415 |                          "linear"
 416 |                          (const "unrestricted")
 417 | 
 418 |     prettyRel : RigCount -> Doc ann
 419 |     prettyRel = elimSemi "irrelevant"
 420 |                          "relevant"
 421 |                          (const "non-linear")
 422 | perrorRaw (BorrowPartial fc env tm arg)
 423 |     = pure $ errorDesc (code !(pshow env tm) <++> reflow "borrows argument" <++> code !(pshow env arg)
 424 |         <++> reflow "so must be fully applied.")
 425 |         <+> line <+> !(ploc fc)
 426 | perrorRaw (BorrowPartialType fc env tm)
 427 |     = pure $ errorDesc (code !(pshow env tm) <++>
 428 |         reflow "borrows, so must return a concrete type.") <+> line <+> !(ploc fc)
 429 | perrorRaw (AmbiguousName fc ns)
 430 |     = pure $ errorDesc (reflow "Ambiguous name" <++> code (cast $ prettyList ns))
 431 |         <+> line <+> !(ploc fc)
 432 | perrorRaw (AmbiguousElab fc env ts_in)
 433 |     = do pp <- getPPrint
 434 |          setPPrint ({ fullNamespace := True } pp)
 435 |          ts_show <- traverse (\ (gam, t) =>
 436 |                                   do defs <- get Ctxt
 437 |                                      setCtxt gam
 438 |                                      res <- pshow env t
 439 |                                      put Ctxt defs
 440 |                                      pure res) ts_in
 441 |          let res = vsep [ errorDesc (reflow "Ambiguous elaboration. Possible results" <+> colon)
 442 |                         , indent 4 (vsep ts_show)
 443 |                         ] <+> line <+> !(ploc fc)
 444 |          setPPrint pp
 445 |          pure res
 446 | perrorRaw (AmbiguousSearch fc env tgt ts)
 447 |     = pure $ vsep [ errorDesc (reflow "Multiple solutions found in search of" <+> colon)
 448 |                   , indent 4 !(pshowNoNorm env tgt)
 449 |                   , !(ploc fc)
 450 |                   , reflow "Possible correct results" <+> colon
 451 |                   , indent 4 (vsep !(traverse (pshowNoNorm env) ts))
 452 |                   ]
 453 | perrorRaw (AmbiguityTooDeep fc n ns)
 454 |     = pure $ errorDesc (reflow "Maximum ambiguity depth exceeded in" <++> code (pretty0 !(getFullName n))
 455 |         <+> colon) <+> line <+> concatWith (surround " --> ") (pretty0 <$> !(traverse getFullName ns))
 456 |         <++> line <+> !(ploc fc)
 457 |         <+> line <+> reflow "Suggestion: the default ambiguity depth limit is 3, the" <++> code "%ambiguity_depth"
 458 |         <++> reflow "pragma can be used to extend this limit, but beware compilation times can be severely impacted."
 459 | perrorRaw (AllFailed ts)
 460 |     = case allUndefined ts of
 461 |            Just e => perrorRaw e
 462 |            _ => pure $ errorDesc (reflow "Sorry, I can't find any elaboration which works. All errors" <+> colon) <+> line
 463 |                   <+> vsep !(traverse pAlterror ts)
 464 |   where
 465 |     pAlterror : (Maybe Name, Error) -> Core (Doc IdrisAnn)
 466 |     pAlterror (Just n, err)
 467 |        = pure $ "If" <++> code (pretty0 !(aliasName !(getFullName n))) <+> colon <++> !(perrorRaw err)
 468 |     pAlterror (Nothing, err)
 469 |        = pure $ reflow "Possible error" <+> colon <+> line <+> indent 4 !(perrorRaw err)
 470 | 
 471 |     allUndefined : List (Maybe Name, Error) -> Maybe Error
 472 |     allUndefined [] = Nothing
 473 |     allUndefined [(_, err@(UndefinedName {}))] = Just err
 474 |     allUndefined ((_, err@(UndefinedName {})) :: es) = allUndefined es
 475 |     allUndefined _ = Nothing
 476 | perrorRaw (RecordTypeNeeded fc _)
 477 |     = pure $ errorDesc (reflow "Can't infer type for this record update.") <+> line <+> !(ploc fc)
 478 | perrorRaw (DuplicatedRecordUpdatePath fc ps)
 479 |     = pure $ vcat $
 480 |       errorDesc (reflow "Duplicated record update paths:")
 481 |       :: map (indent 2 . reAnnotate Syntax . prettyFieldPath) ps
 482 |       ++ [line <+> !(ploc fc)]
 483 | perrorRaw (NotRecordField fc fld Nothing)
 484 |     = pure $ errorDesc (code (pretty0 fld) <++> reflow "is not part of a record type.") <+> line <+> !(ploc fc)
 485 | perrorRaw (NotRecordField fc fld (Just ty))
 486 |     = pure $ errorDesc (reflow "Record type" <++> code (pretty0 !(getFullName ty)) <++> reflow "has no field"
 487 |         <++> code (pretty0 fld) <+> dot) <+> line <+> !(ploc fc)
 488 | perrorRaw (NotRecordType fc ty)
 489 |     = pure $ errorDesc (code (pretty0 !(getFullName ty)) <++> reflow "is not a record type.") <+> line <+> !(ploc fc)
 490 | perrorRaw (IncompatibleFieldUpdate fc flds)
 491 |     = pure $ reflow "Field update" <++> reAnnotate Syntax (prettyFieldPath flds)
 492 |              <++> reflow "not compatible with other updates at" <+> colon <+> line <+> !(ploc fc)
 493 | perrorRaw (InvalidArgs fc env [n] tm)
 494 |     = pure $ errorDesc (code (pretty0 n) <++> reflow "is not a valid argument in" <++> !(pshow env tm)
 495 |         <+> dot) <+> line <+> !(ploc fc)
 496 | perrorRaw (InvalidArgs fc env ns tm)
 497 |     = pure $ errorDesc (concatWith (surround (comma <+> space)) (code . pretty0 <$> ns)
 498 |         <++> reflow "are not valid arguments in" <++> !(pshow env tm) <+> dot)
 499 |         <+> line <+> !(ploc fc)
 500 | perrorRaw (TryWithImplicits fc env imps)
 501 |     = pure $ errorDesc (reflow "Need to bind implicits"
 502 |         <++> concatWith (surround (comma <+> space)) !(traverse (tshow env) imps) <+> dot)
 503 |         <+> line <+> !(ploc fc)
 504 |   where
 505 |     tshow : {vars : _} ->
 506 |             Env Term vars -> (Name, Term vars) -> Core (Doc IdrisAnn)
 507 |     tshow env (n, ty) = pure $ pretty0 n <++> colon <++> code !(pshow env ty)
 508 | perrorRaw (BadUnboundImplicit fc env n ty)
 509 |     = pure $ errorDesc (reflow "Can't bind name" <++> code (pretty0 (nameRoot n))
 510 |         <++> reflow "with type" <++> code !(pshow env ty)
 511 |         <+> colon) <+> line <+> !(ploc fc) <+> line <+> reflow "Suggestion: try an explicit bind."
 512 | perrorRaw (CantSolveGoal fc gam env g reason)
 513 |     = do defs <- get Ctxt
 514 |          setCtxt gam
 515 |          let (_ ** (env', g')) = dropEnv env g
 516 |          let res = errorDesc (reflow "Can't find an implementation for" <++> code !(pshow env' g')
 517 |                      <+> dot) <+> line <+> !(ploc fc)
 518 |          put Ctxt defs
 519 |          case reason of
 520 |               Nothing => pure res
 521 |               Just r => do rdesc <- perrorRaw r
 522 |                            pure (res <+> line <+>
 523 |                                  (reflow "Possible cause:" <++> rdesc))
 524 |   where
 525 |     -- For display, we don't want to see the full top level type; just the
 526 |     -- return type
 527 |     dropEnv : {vars : _} ->
 528 |               Env Term vars -> Term vars ->
 529 |               (ns ** (Env Term ns, Term ns))
 530 |     dropEnv env (Bind _ n b@(Pi {}) sc) = dropEnv (b :: env) sc
 531 |     dropEnv env (Bind _ n b@(Let {}) sc) = dropEnv (b :: env) sc
 532 |     dropEnv env tm = (_ ** (env, tm))
 533 | 
 534 | perrorRaw (DeterminingArg fc n i env g)
 535 |     = pure $ errorDesc (reflow "Can't find an implementation for" <++> code !(pshow env g) <+> line
 536 |         <+> reflow "since I can't infer a value for argument" <++> code (pretty0 n) <+> dot)
 537 |         <+> line <+> !(ploc fc)
 538 | perrorRaw (UnsolvedHoles hs)
 539 |     = pure $ errorDesc (reflow "Unsolved holes" <+> colon) <+> line <+> !(prettyHoles hs)
 540 |   where
 541 |     prettyHoles : List (FC, Name) -> Core (Doc IdrisAnn)
 542 |     prettyHoles [] = pure emptyDoc
 543 |     prettyHoles ((fc, n) :: hs)
 544 |         = pure $ meta (pretty0 n) <++> reflow "introduced at:" <++> !(ploc fc) <+> !(prettyHoles hs)
 545 | perrorRaw (CantInferArgType fc env n h ty)
 546 |     = pure $ errorDesc (reflow "Can't infer type for argument" <++> code (pretty0 n)) <+> line
 547 |         <+> "Got" <++> code !(pshow env ty) <++> reflow "with hole" <++> meta (pretty0 h) <+> dot
 548 |         <+> line <+> !(ploc fc)
 549 | perrorRaw (SolvedNamedHole fc env h tm)
 550 |     = pure $ errorDesc (reflow "Named hole" <++> meta (pretty0 h)
 551 |         <++> reflow "has been solved by unification.") <+> line
 552 |         <+> "Result" <+> colon <++> code !(pshow env tm)
 553 |         <+> line <+> !(ploc fc)
 554 | perrorRaw (VisibilityError fc vx x vy y)
 555 |     = pure $ errorDesc (keyword (pretty0 vx) <++> code (pretty0 (sugarName x))
 556 |         <++> reflow "cannot refer to" <++> keyword (pretty0 vy) <++> code (pretty0 (sugarName y)))
 557 |         <+> line <+> !(ploc fc)
 558 | perrorRaw (NonLinearPattern fc n)
 559 |     = pure $ errorDesc (reflow "Non linear pattern" <++> code (pretty0 (sugarName n)) <+> dot)
 560 |         <+> line <+> !(ploc fc)
 561 | perrorRaw (BadPattern fc n)
 562 |     = pure $ errorDesc (reflow "Pattern not allowed here" <+> colon <++> code (pretty0 n) <+> dot)
 563 |         <+> line <+> !(ploc fc)
 564 | perrorRaw (NoDeclaration fc n)
 565 |     = pure $ errorDesc (reflow "No type declaration for" <++> code (pretty0 n) <+> dot)
 566 |         <+> line <+> !(ploc fc)
 567 | perrorRaw (AlreadyDefined fc n)
 568 |     = pure $ errorDesc (code (pretty0 n) <++> reflow "is already defined.")
 569 |         <+> line <+> !(ploc fc)
 570 | perrorRaw (NotFunctionType fc env tm)
 571 |     = pure $ errorDesc (code !(pshow env tm) <++> reflow "is not a function type.")
 572 |         <+> line <+> !(ploc fc)
 573 | perrorRaw (RewriteNoChange fc env rule ty)
 574 |     = pure $ errorDesc (reflow "Rewriting by" <++> code !(pshow env rule)
 575 |         <++> reflow "did not change type" <++> code !(pshow env ty) <+> dot)
 576 |         <+> line <+> !(ploc fc)
 577 | perrorRaw (NotRewriteRule fc env rule)
 578 |     = pure $ errorDesc (code !(pshow env rule) <++> reflow "is not a rewrite rule type.")
 579 |         <+> line <+> !(ploc fc)
 580 | perrorRaw (CaseCompile fc n DifferingArgNumbers)
 581 |     = pure $ errorDesc (reflow "Patterns for" <++> code (pretty0 !(prettyName n))
 582 |        <++> reflow "have differing numbers of arguments.")
 583 |         <+> line <+> !(ploc fc)
 584 | perrorRaw (CaseCompile fc n DifferingTypes)
 585 |     = pure $ errorDesc (reflow "Patterns for" <++> code (pretty0 !(prettyName n))
 586 |        <++> reflow "require matching on different types.")
 587 |         <+> line <+> !(ploc fc)
 588 | perrorRaw (CaseCompile fc n UnknownType)
 589 |     = pure $ errorDesc (reflow "Can't infer type to match in"
 590 |        <++> code (pretty0 !(prettyName n)) <+> dot)
 591 |         <+> line <+> !(ploc fc)
 592 | perrorRaw (CaseCompile fc n (NotFullyApplied cn))
 593 |     = pure $ errorDesc ("Constructor" <++> code (pretty0 cn) <++> reflow "is not fully applied.")
 594 |          <+> line <+> !(ploc fc)
 595 | perrorRaw (CaseCompile fc n (MatchErased (_ ** (env, tm))))
 596 |     = pure $ errorDesc (reflow "Attempt to match on erased argument" <++> code !(pshow env tm) <++> "in"
 597 |         <++> code (pretty0 !(prettyName n)) <+> dot) <+> line <+> !(ploc fc)
 598 | perrorRaw (BadDotPattern fc env reason x y)
 599 |     = pure $ errorDesc (reflow "Can't match on" <++> code !(pshow env x)
 600 |         <++> parens (pretty reason) <+> dot) <+> line <+> !(ploc fc)
 601 | perrorRaw (MatchTooSpecific fc env tm)
 602 |     = pure $ errorDesc (reflow "Can't match on" <++> code !(pshow env tm)
 603 |         <++> reflow "as it must have a polymorphic type.") <+> line <+> !(ploc fc)
 604 | perrorRaw (BadImplicit fc str)
 605 |     = pure $ errorDesc (reflow "Can't infer type for unbound implicit name" <++> code (pretty0 str) <+> dot)
 606 |         <+> line <+> !(ploc fc) <+> line <+> reflow "Suggestion: try making it a bound implicit."
 607 | perrorRaw (BadRunElab fc env script desc)
 608 |     = pure $ errorDesc (reflow "Bad elaborator script" <++> code !(pshow env script)
 609 |        <++> parens (pretty0 desc) <+> dot)
 610 |         <+> line <+> !(ploc fc)
 611 |         <+> !(let scriptFC = getLoc script in
 612 |           if isJust (isNonEmptyFC scriptFC)
 613 |             then pure $ line <+> reflow "Stuck place in the script:" <+> line <+> !(ploc scriptFC)
 614 |             else pure emptyDoc)
 615 | perrorRaw (RunElabFail e)
 616 |     = pure $ reflow "Error during reflection" <+> colon <++> !(perrorRaw e)
 617 | perrorRaw (GenericMsg fc str) = pure $ pretty0 str <+> line <+> !(ploc fc)
 618 | perrorRaw (GenericMsgSol fc header solutionHeader solutions)
 619 |     = pure $ pretty0 header <+> line <+> !(ploc fc)
 620 |        <+> line
 621 |        <+> fromString "\{solutionHeader}:" <+> line
 622 |        <+> indent 1 (vsep (map (\s => "-" <++> pretty0 s) solutions))
 623 | perrorRaw (OperatorBindingMismatch fc {print=p} expected actual opName rhs candidates)
 624 |     = pure $ "Operator" <++> pretty0 !(getFullName (fromEither opName)) <++> "is"
 625 |        <++> printBindingInfo expected-- .bindingInfo
 626 |        <++> "operator, but is used as" <++> printBindingModifier actual.getBinder
 627 |        <++> "operator."
 628 |        <+> line <+> !(ploc fc)
 629 |        <+> "Explanation: regular, typebind and autobind operators all use a slightly different"
 630 |        <++> "syntax, typebind looks like this: '(name : type)" <++> infixOpName
 631 |        <++> "expr', autobind looks like this: '(name <- expr)" <++> infixOpName
 632 |        <++> "expr'."
 633 |        <+> line <+> line
 634 |        <+> "Possible solutions:" <+> line
 635 |        <+> indent 1 (vsep (map ("-" <++>)
 636 |            (expressionDiagnositc ++ [fixityDiagnostic, moduleDiagnostic] ++ spellingCandidates)))
 637 |     where
 638 |       spellingCandidates : List (Doc IdrisAnn)
 639 |       spellingCandidates = case candidates of
 640 |                               [] => []
 641 |                               [x] => ["Did you mean" <++> enclose "'" "'" (pretty0 x) <++> "?"]
 642 |                               xs => ["Did you mean either of:" <++> hcat (punctuate ", "
 643 |                                        (map (enclose "'" "'" . pretty0) xs)) <++> "?"]
 644 | 
 645 | 
 646 |       moduleDiagnostic : Doc IdrisAnn
 647 |       moduleDiagnostic = case expected of
 648 |                               UndeclaredFixity => "Import a module that exports a suitable fixity."
 649 |                               (DeclaredFixity e) => "Hide or remove the fixity at" <++> byShow e.fc
 650 |                                   <++> "and import a module that exports a compatible fixity."
 651 | 
 652 |       infixOpName : Doc IdrisAnn
 653 |       infixOpName = case opName of
 654 |                          Left backtickedOp => enclose "`" "`" (byShow backtickedOp)
 655 |                          Right symbolOp => byShow symbolOp
 656 | 
 657 |       displayFixityInfo : FixityInfo -> BindingModifier -> Doc IdrisAnn
 658 |       displayFixityInfo (MkFixityInfo fc1 vis _ fix precedence) NotBinding
 659 |         = byShow vis <++> byShow fix <++> byShow precedence <++> pretty0 (fromEither opName)
 660 |       displayFixityInfo (MkFixityInfo _ vis _ fix precedence) usedBinder
 661 |         = byShow vis <++> byShow usedBinder <++> byShow fix <++> byShow precedence <++> pretty0 (fromEither opName)
 662 | 
 663 |       printE : ? -> Doc IdrisAnn
 664 |       printE x = reAnnotate (const Code) (p x)
 665 | 
 666 |       expressionDiagnositc : List (Doc IdrisAnn)
 667 |       expressionDiagnositc = case expected of
 668 |           UndeclaredFixity => []
 669 |           DeclaredFixity e => let sentence = "Write the expression using" <++> byShow e.bindingInfo <++> "syntax:"
 670 |             in pure $ sentence <++> enclose "'" "'" (case e.bindingInfo of
 671 |                     NotBinding =>
 672 |                        printE actual.getLhs <++> infixOpName <++> printE rhs
 673 |                     Autobind =>
 674 |                        parens (maybe "_" printE actual.getBoundPat <++> "<-"
 675 |                                <++> printE actual.getLhs)
 676 |                        <++> infixOpName <++> printE rhs
 677 |                     Typebind =>
 678 |                        parens (maybe "_" printE actual.getBoundPat <++> ":"
 679 |                                <++> printE actual.getLhs)
 680 |                        <++> infixOpName <++> printE rhs
 681 |                     ) <+> dot
 682 | 
 683 | 
 684 |       fixityDiagnostic : Doc IdrisAnn
 685 |       fixityDiagnostic = case expected of
 686 |            UndeclaredFixity => "Define a new fixity:" <++> "infixr 0" <++> infixOpName
 687 |            (DeclaredFixity fix) =>
 688 |             "Change the fixity defined at" <++> pretty0 fix.fc <++> "to"
 689 |             <++> enclose "'" "'" (displayFixityInfo fix actual.getBinder)
 690 |             <+> dot
 691 | 
 692 |       printBindingModifier : BindingModifier -> Doc IdrisAnn
 693 |       printBindingModifier NotBinding = "a regular"
 694 |       printBindingModifier Typebind = "a type-binding (typebind)"
 695 |       printBindingModifier Autobind = "an automatically-binding (autobind)"
 696 | 
 697 |       printBindingInfo : FixityDeclarationInfo -> Doc IdrisAnn
 698 |       printBindingInfo UndeclaredFixity = "a regular"
 699 |       printBindingInfo (DeclaredFixity x) = printBindingModifier x.bindingInfo
 700 | 
 701 | 
 702 | perrorRaw (TTCError msg)
 703 |     = pure $ errorDesc (reflow "Error in TTC file" <+> colon <++> byShow msg)
 704 |         <++> parens "the most likely case is that the ./build directory in your current project contains files from a previous build of idris2 or the idris2 executable is from a different build than the installed .ttc files"
 705 | perrorRaw (FileErr fname err)
 706 |     = pure $ errorDesc (reflow "File error in" <++> pretty0 fname <++> colon)
 707 |        <++> byShow err
 708 | perrorRaw (CantFindPackage fname)
 709 |     = pure $ errorDesc (reflow "Can't find package " <++> pretty0 fname)
 710 | perrorRaw (LazyImplicitFunction fc)
 711 |     = pure $ errorDesc (reflow "Implicit lazy functions are not yet supported.") <+> line <+> !(ploc fc)
 712 | perrorRaw (LazyPatternVar fc)
 713 |     = pure $ errorDesc (reflow "Defining lazy functions via pattern matching is not yet supported.") <+> line <+> !(ploc fc)
 714 | perrorRaw (LitFail fc)
 715 |     = pure $ errorDesc (reflow "Can't parse literate.")
 716 |         <+> line <+> !(ploc fc)
 717 | perrorRaw (LexFail fc msg)
 718 |     = pure $ errorDesc (pretty0 msg) <+> line <+> !(ploc fc)
 719 | perrorRaw (ParseFail ((fc, msg) ::: Nil))
 720 |     = pure $ errorDesc (pretty0 msg) <+> line <+> !(ploc fc)
 721 | perrorRaw (ParseFail errs)
 722 |     = pure $ errorDesc (reflow "Couldn't parse any alternatives" <+> colon) <+> line <+> !listErrors
 723 |   where
 724 |     prettyErrors : Nat -> Nat -> List (FC, String) -> Core (Doc IdrisAnn)
 725 |     prettyErrors showCount _ []   = pure emptyDoc
 726 |     prettyErrors showCount 0 errs = pure $ meta (pretty0 "... (\{show $ length errs} others)")
 727 |     prettyErrors showCount (S k) ((fc, msg) :: hs)
 728 |         = do let idx = show $ showCount `minus` k
 729 |              pure $ warning (pretty0 "\{idx}: \{msg}")
 730 |                <+> line <+> !(ploc fc)
 731 |                <+> !(prettyErrors showCount k hs)
 732 | 
 733 |     listErrors : Core (Doc IdrisAnn)
 734 |     listErrors = do showCount <- logErrorCount . session . options <$> get Ctxt
 735 |                     prettyErrors showCount showCount . nub . reverse $ forget errs
 736 | perrorRaw (ModuleNotFound fc ns)
 737 |     = pure $ errorDesc ("Module" <++> annotate FileCtxt (pretty0 ns) <++> reflow "not found")
 738 |         <+> line <+> !(ploc fc)
 739 | perrorRaw (CyclicImports ns)
 740 |     = pure $ errorDesc (reflow "Module imports form a cycle" <+> colon)
 741 |         <++> concatWith (surround " -> ") (pretty0 <$> ns)
 742 | perrorRaw ForceNeeded = pure $ errorDesc (reflow "Internal error when resolving implicit laziness")
 743 | perrorRaw (InternalError str) = pure $ errorDesc (reflow "INTERNAL ERROR" <+> colon) <++> pretty0 str
 744 | perrorRaw (UserError str) = pure . errorDesc $ pretty0 str
 745 | perrorRaw (NoForeignCC fc specs) = do
 746 |     let cgs = fst <$> availableCGs (options !(get Ctxt))
 747 |     let res = vsep [ errorDesc (reflow ("The given specifier '" ++ show specs ++ "' was not accepted by any backend. Available backends") <+> colon)
 748 |                    , indent 2 (concatWith (\ x, y => x <+> ", " <+> y) (map reflow cgs))
 749 |                    , reflow "Some backends have additional specifier rules, refer to their documentation."
 750 |                    ] <+> line <+> !(ploc fc)
 751 |     pure res
 752 | perrorRaw (BadMultiline fc str)
 753 |   = pure $ errorDesc (reflow "While processing multi-line string" <+> dot <++> pretty0 str <+> dot)
 754 |       <+> line <+> !(ploc fc)
 755 | perrorRaw (Timeout str) = pure $ errorDesc (reflow "Timeout in" <++> pretty0 str)
 756 | 
 757 | perrorRaw (FailingDidNotFail fc)
 758 |   = pure $ errorDesc (reflow "Failing block did not fail" <+> dot)
 759 |     <+> line <+> !(ploc fc)
 760 | perrorRaw (FailingWrongError fc msg err)
 761 |   = pure $ vcat [ errorDesc (reflow "Failing block failed with the wrong error" <+> dot)
 762 |                 , "Expected" <++> dquote <+> pretty0 msg <+> dquote <++> "but got:"
 763 |                 , vsep !(traverse perrorRaw (forget err))
 764 |                 ]
 765 | 
 766 | perrorRaw (InType fc n err)
 767 |     = pure $ hsep [ errorDesc (reflow "While processing type of" <++> code (pretty0 !(prettyName n))) <+> dot
 768 |                   , !(perrorRaw err)
 769 |                   ]
 770 | perrorRaw (InCon n err)
 771 |     = pure $ hsep [ errorDesc (reflow "While processing constructor" <++> code (pretty0 !(prettyName n.val))) <+> dot
 772 |                   , !(perrorRaw err)
 773 |                   ]
 774 | perrorRaw (InLHS fc n err)
 775 |     = pure $ hsep [ errorDesc (reflow "While processing left hand side of" <++> code (pretty0 !(prettyName n))) <+> dot
 776 |                   , !(perrorRaw err)
 777 |                   ]
 778 | perrorRaw (InRHS fc n err)
 779 |     = pure $ hsep [ errorDesc (reflow "While processing right hand side of" <++> code (pretty0 !(prettyName n))) <+> dot
 780 |                   , !(perrorRaw err)
 781 |                   ]
 782 | 
 783 | perrorRaw (MaybeMisspelling err ns) = pure $ !(perrorRaw err) <+> case ns of
 784 |   (n ::: []) => reflow "Did you mean:" <++> code (pretty0 n) <+> "?"
 785 |   _ => let (xs, x) = unsnoc ns in
 786 |        reflow "Did you mean any of:"
 787 |        <++> concatWith (surround (comma <+> space)) (map (code . pretty0) xs)
 788 |        <+> comma <++> "or" <++> code (pretty0 x) <+> "?"
 789 | perrorRaw (WarningAsError warn) = pwarningRaw warn
 790 | 
 791 | export
 792 | perror : {auto c : Ref Ctxt Defs} ->
 793 |          {auto s : Ref Syn SyntaxInfo} ->
 794 |          {auto o : Ref ROpts REPLOpts} ->
 795 |          Error -> Core (Doc IdrisAnn)
 796 | perror err = perrorRaw !(toFullNames err)
 797 | 
 798 | ||| Check (in a whitespace-insensitive manner) that the msg is
 799 | ||| contained in the error.
 800 | export
 801 | checkError :
 802 |   {auto c : Ref Ctxt Defs} ->
 803 |   {auto s : Ref Syn SyntaxInfo} ->
 804 |   {auto o : Ref ROpts REPLOpts} ->
 805 |   (msg : String) -> Error -> Core Bool
 806 | checkError msg err = do
 807 |   -- Kill the locations so that we don't get source code excerpts
 808 |   let err = killErrorLoc err
 809 |   -- Show the error as a string
 810 |   str <- show <$> perror err
 811 |   -- Normalise the two strings. This ensures comparison is whitespace
 812 |   -- insentitive (error messages' layout depend on terminal width)
 813 |   let msg = unwords (words msg)
 814 |   let str = unwords (words str)
 815 |   pure (msg `isInfixOf` str)
 816 | 
 817 | prettyMaybeLoc : Maybe FC -> Doc IdrisAnn
 818 | prettyMaybeLoc Nothing = emptyDoc
 819 | prettyMaybeLoc (Just fc) = annotate FileCtxt (pretty0 fc) <+> colon
 820 | 
 821 | export
 822 | display : {auto c : Ref Ctxt Defs} ->
 823 |           {auto s : Ref Syn SyntaxInfo} ->
 824 |           {auto o : Ref ROpts REPLOpts} ->
 825 |           Error -> Core (Doc IdrisAnn)
 826 | display err = do
 827 |   pure $ annotate Error "Error:" <++> !(perror err)
 828 | 
 829 | export
 830 | displayWarning : {auto c : Ref Ctxt Defs} ->
 831 |                  {auto s : Ref Syn SyntaxInfo} ->
 832 |                  {auto o : Ref ROpts REPLOpts} ->
 833 |                  Warning -> Core (Doc IdrisAnn)
 834 | displayWarning w
 835 |     = pure $ annotate Warning "Warning:" <++> !(pwarning w)
 836 |