45a3f93 · Idris-dev · git.iko.soy

CHANGELOG.md+15−3

@@ -83,9 +83,21 @@

8383 as they were given in the source files.

8484+ Backslash, braces and percent symbols are now correctly pretty printed

8585 in LaTeX.

86−+ Parse errors have a new format, similar to GHC 8.2's default, due to a

87− switch from Trifecta to Megaparsec for parsing. This could possibly cause

88− some subtle deviations in parsing from previous versions of Idris.

86++ Errors and warnings now consistently have the following format:

87+ ```idris

88+ reg068.idr:1:6-8:

89+ |

90+ 1 | data nat : Type where --error

91+ | ~~~

92+ Main.nat has a name which may be implicitly bound.

93+ This is likely to lead to problems!

94+ ```

95+ The code is highlighted when highlighting information is available. How

96+ much highlighting information is available depends on where the error

97+ occurred.

98++ The parser provider has been switched from Trifecta to Megaparsec. This

99+ could possibly cause some subtle deviations in parsing from previous

100+ versions of Idris.

89101+ Many more errors now report beginning *and* ending position (which may be

90102 on different lines), instead of just a single point. The format is

91103 `Foo.idr:9:7-15:` if ending column is on the same line or

src/Idris/Elab/Clause.hs+3−4

@@ -28,7 +28,7 @@ import Idris.Elab.Type

2828import Idris.Elab.Utils

2929import Idris.Error

3030import Idris.Options

31−import Idris.Output (iputStrLn, pshow, sendHighlighting)

31+import Idris.Output (iWarn, pshow, sendHighlighting)

3232import Idris.PartialEval

3333import Idris.Termination

3434import Idris.Transforms

@@ -205,9 +205,8 @@ elabClauses info' fc opts n_in cs =

205205 case tree of

206206 CaseDef _ _ [] -> return ()

207207 CaseDef _ _ xs -> mapM_ (\x ->

208− iputStrLn $ show fc ++

209− ":warning - Unreachable case: " ++

210− show (delab ist x)) xs

208+ iWarn fc $ text "Unreachable case:" </> text (show (delab ist x))

209+ ) xs

211210 let knowncovering = (pcover && cov) || AssertTotal `elem` opts

212211 let defaultcase = if knowncovering

213212 then STerm Erased

src/Idris/Main.hs+3−3

@@ -195,7 +195,7 @@ idrisMain opts =

195195 mapM_ (\str -> do ist <- getIState

196196 c <- colourise

197197 case parseExpr ist str of

198− Left err -> do iputStrLn . show . fixColour c . parseErrorDoc $ err

198+ Left err -> do emitWarning err

199199 runIO $ exitWith (ExitFailure 1)

200200 Right e -> process "" (Eval e))

201201 exprs

@@ -272,7 +272,7 @@ execScript :: String -> Idris ()

272272execScript expr = do i <- getIState

273273 c <- colourise

274274 case parseExpr i expr of

275− Left err -> do iputStrLn . show . fixColour c . parseErrorDoc $ err

275+ Left err -> do emitWarning err

276276 runIO $ exitWith (ExitFailure 1)

277277 Right term -> do ctxt <- getContext

278278 (tm, _) <- elabVal (recinfo (fileFC "toplevel")) ERHS term

@@ -299,7 +299,7 @@ initScript = do script <- runIO $ getIdrisInitScript

299299 runInit h

300300 processLine i cmd input clr =

301301 case parseCmd i input cmd of

302− Left err -> runIO . print . fixColour clr . parseErrorDoc $ err

302+ Left err -> emitWarning err

303303 Right (Right Reload) -> iPrintError "Init scripts cannot reload the file"

304304 Right (Right (Load f _)) -> iPrintError "Init scripts cannot load files"

305305 Right (Right (ModImport f)) -> iPrintError "Init scripts cannot import modules"

src/Idris/Output.hs+140−14

@@ -9,12 +9,13 @@ Maintainer : The Idris Community.

99{-# LANGUAGE FlexibleInstances #-}

1010{-# OPTIONS_GHC -fwarn-incomplete-patterns #-}

1111

12−module Idris.Output (clearHighlights, idemodePutSExp, iPrintError, iPrintFunTypes,

13− iPrintResult, iPrintTermWithType, iputGoal, iputStr, iputStrLn,

14− iRender, iRenderError, iRenderOutput, iRenderResult, iWarn,

15− prettyDocumentedIst, printUndefinedNames, pshow, renderExternal,

16− sendHighlighting, sendParserHighlighting, warnTotality,

17− writeHighlights) where

12+module Idris.Output (clearHighlights, emitWarning, formatMessage, idemodePutSExp,

13+ iPrintError, iPrintFunTypes, iPrintResult, iPrintTermWithType,

14+ iputGoal, iputStr, iputStrLn, iRender, iRenderError,

15+ iRenderOutput, iRenderResult, iWarn, prettyDocumentedIst,

16+ printUndefinedNames, pshow, renderExternal, sendHighlighting,

17+ sendParserHighlighting, warnTotality, writeHighlights,

18+ OutputDoc(..), Message(..)) where

1819

1920import Idris.AbsSyntax

2021import Idris.Colours (hEndColourise, hStartColourise)

@@ -31,13 +32,15 @@ import Util.System (isATTY)

3132

3233import Prelude hiding ((<$>))

3334

35+import Control.Arrow (first)

3436import Control.Monad.Trans.Except (ExceptT(ExceptT), runExceptT)

3537import Data.List (intersperse, nub)

36−import Data.Maybe (fromMaybe)

38+import Data.Maybe (fromJust, fromMaybe, isJust, listToMaybe)

3739import System.Console.Haskeline.MonadException (MonadException(controlIO),

3840 RunIO(RunIO))

3941import System.FilePath (replaceExtension)

4042import System.IO (Handle, hPutStr, hPutStrLn)

43+import System.IO.Error (tryIOError)

4144

4245instance MonadException m => MonadException (ExceptT Err m) where

4346 controlIO f = ExceptT $ controlIO $ \(RunIO run) -> let

@@ -49,18 +52,141 @@ pshow ist err = displayDecorated (consoleDecorate ist) .

4952 renderPretty 1.0 80 .

5053 fmap (fancifyAnnots ist True) $ pprintErr ist err

5154

52−iWarn :: FC -> Doc OutputAnnotation -> Idris ()

53−iWarn fc err =

55+type OutputDoc = Doc OutputAnnotation

56+

57+class Message a where

58+ messageExtent :: a -> FC

59+ messageText :: a -> OutputDoc

60+ messageSource :: a -> Maybe String

61+

62+data Ann = AText String | ATagged OutputAnnotation Ann | ASplit Ann Ann

63+

64+data SimpleWarning = SimpleWarning FC OutputDoc

65+instance Message SimpleWarning where

66+ messageExtent (SimpleWarning extent _) = extent

67+ messageText (SimpleWarning _ msg) = msg

68+ messageSource _ = Nothing

69+

70+formatMessage :: Message w => w -> Idris OutputDoc

71+formatMessage w = do

72+ i <- getIState

73+ maybeSource <- case messageSource w of

74+ Just src -> pure (Just src)

75+ Nothing -> readSource fc

76+ let maybeFormattedSource = maybeSource >>= layoutSource fc (idris_highlightedRegions i)

77+ return $ layoutMessage (layoutFC fc) maybeFormattedSource (messageText w)

78+ where

79+ fc :: FC

80+ fc = messageExtent w

81+

82+ layoutFC :: FC -> OutputDoc

83+ layoutFC fc@(FC fn _ _) | fn /= "" = text (show $ fc) <> colon

84+ layoutFC _ = empty

85+

86+ readSource :: FC -> Idris (Maybe String)

87+ readSource (FC fn _ _) = do

88+ result <- runIO $ tryIOError (readFile fn)

89+ case result of

90+ Left _ -> pure Nothing

91+ Right v -> pure (Just v)

92+ readSource _ = pure Nothing

93+

94+ layoutSource :: FC -> [(FC, OutputAnnotation)] -> String -> Maybe OutputDoc

95+ layoutSource (FC fn (si, sj) (ei, ej)) highlights src =

96+ if haveSource

97+ then Just source

98+ else Nothing

99+ where

100+ sourceLine :: Maybe String

101+ sourceLine = listToMaybe . drop (si - 1) . (++ ["<end of file>"]) . lines $ src

102+

103+ haveSource :: Bool

104+ haveSource = isJust sourceLine

105+

106+ line1 :: OutputDoc

107+ line1 = text $ replicate (length (show si)) ' ' ++ " |"

108+

109+ lineFC :: FC

110+ lineFC = FC fn (si, 1) (si, length (fromJust sourceLine))

111+

112+ intersects :: FC -> FC -> Bool

113+ intersects (FC fn1 s1 e1) (FC fn2 s2 e2)

114+ | fn1 /= fn2 = False

115+ | e1 < s2 = False

116+ | e2 < s1 = False

117+ | otherwise = True

118+ intersects _ _ = False

119+

120+ intersection :: FC -> FC -> FC

121+ intersection fc1@(FC fn1 s1 e1) fc2@(FC _ s2 e2)

122+ | intersects fc1 fc2 = FC fn1 (max s1 s2) (min e1 e2)

123+ | otherwise = NoFC

124+ intersection _ _ = NoFC

125+

126+ width :: Ann -> Int

127+ width (AText s) = length s

128+ width (ATagged _ n) = width n

129+ width (ASplit l r) = width l + width r

130+

131+ sourceDoc :: Ann -> OutputDoc

132+ sourceDoc (AText s) = text s

133+ sourceDoc (ATagged a n) = annotate a (sourceDoc n)

134+ sourceDoc (ASplit l r) = sourceDoc l <> sourceDoc r

135+

136+ insertAnnotation :: ((Int, Int), OutputAnnotation) -> Ann -> Ann

137+ insertAnnotation ((sj, ej), oa) (ATagged tag n) = ATagged tag (insertAnnotation ((sj, ej), oa) n)

138+ insertAnnotation ((sj, ej), oa) (ASplit l r)

139+ | w <- width l = ASplit (insertAnnotation ((sj, ej), oa) l) (insertAnnotation ((sj - w, ej - w), oa) r)

140+ insertAnnotation ((sj, ej), oa) a@(AText t)

141+ | sj <= 1, ej >= width a = ATagged oa a

142+ | sj > 1, sj <= width a = ASplit (AText $ take (sj - 1) t) (insertAnnotation ((1, ej - sj + 1), oa) (AText $ drop (sj - 1) t))

143+ | sj == 1, ej >= 1, ej < width a = ASplit (insertAnnotation ((1, ej), oa) (AText $ take ej t)) (AText $ drop ej t)

144+ | otherwise = a

145+

146+ highlightedSource :: OutputDoc

147+ highlightedSource = sourceDoc .

148+ foldr insertAnnotation (AText $ fromJust sourceLine) .

149+ map (\(FC _ (_, sj) (_, ej), ann) -> ((sj, ej), ann)) .

150+ map (first (intersection lineFC)) .

151+ filter (intersects lineFC . fst) $

152+ highlights

153+

154+ line2 :: OutputDoc

155+ line2 = text (show si ++ " | ") <> highlightedSource

156+

157+ indicator :: OutputDoc

158+ indicator = text (replicate (end - sj + 1) ch) <> ellipsis

159+ where

160+ (end, ch, ellipsis) = case (si == ei, sj == ej) of

161+ (True , True ) -> (ej, '^', empty)

162+ (True , False) -> (ej, '~', empty)

163+ (False, _ ) -> (length (fromJust sourceLine), '~', text " ...")

164+

165+ line3 :: OutputDoc

166+ line3 = line1 <> text (replicate sj ' ') <> indicator

167+

168+ source :: OutputDoc

169+ source = line1 <$$> line2 <$$> line3

170+ layoutSource _ _ _ = Nothing

171+

172+ layoutMessage :: OutputDoc -> Maybe OutputDoc -> OutputDoc -> OutputDoc

173+ layoutMessage loc (Just src) err = loc <$$> src <$$> err <$$> empty

174+ layoutMessage loc Nothing err = loc </> err

175+

176+iWarn :: FC -> OutputDoc -> Idris ()

177+iWarn fc err = emitWarning $ SimpleWarning fc err

178+

179+emitWarning :: Message w => w -> Idris ()

180+emitWarning w =

54181 do i <- getIState

55182 case idris_outputmode i of

56183 RawOutput h ->

57− do err' <- iRender . fmap (fancifyAnnots i True) $

58− case fc of

59− FC fn _ _ | fn /= "" -> text (show fc) <> colon <//> err

60− _ -> err

184+ do formattedErr <- formatMessage w

185+ err' <- iRender . fmap (fancifyAnnots i True) $ formattedErr

61186 hWriteDoc h i err'

62187 IdeMode n h ->

63− do err' <- iRender . fmap (fancifyAnnots i True) $ err

188+ do err' <- iRender . fmap (fancifyAnnots i True) $ messageText w

189+ let fc = messageExtent w

64190 let (str, spans) = displaySpans err'

65191 runIO . hPutStrLn h $

66192 convSExp "warning" (fc_fname fc, fc_start fc, fc_end fc, str, spans) n

src/Idris/Parser.hs+18−21

@@ -36,7 +36,6 @@ import Idris.Parser.Ops

3636import Idris.Termination

3737import Idris.Unlit

3838

39−import qualified Util.Pretty

4039import Util.System (readSource)

4140

4241import Prelude hiding (pi)

@@ -1062,15 +1061,15 @@ RHS ::= '=' Expr

10621061RHSName ::= '{' FnName '}';

10631062@

10641063-}

1065−rhs :: SyntaxInfo -> Name -> IdrisParser PTerm

1064+rhs :: SyntaxInfo -> Name -> IdrisParser (PTerm, FC)

10661065rhs syn n = do lchar '='

10671066 indentGt

1068− expr syn

1067+ withExtent $ expr syn

10691068 <|> do symbol "?=";

10701069 (name, fc) <- withExtent $ P.option n' (symbol "{" *> fnName <* symbol "}")

10711070 r <- expr syn

1072− return (addLet fc name r)

1073− <|> impossible

1071+ return (addLet fc name r, fc)

1072+ <|> withExtent impossible

10741073 <?> "function right hand side"

10751074 where mkN :: Name -> Name

10761075 mkN (UN x) = if (tnull x || not (isAlpha (thead x)))

@@ -1112,33 +1111,34 @@ WhereOrTerminator ::= WhereBlock | Terminator;

11121111clause :: SyntaxInfo -> IdrisParser PClause

11131112clause syn

11141113 -- unnamed with or function clause (inside a with)

1115− = appExtent (do

1116− wargs <- P.try (do pushIndent; some (wExpr syn))

1114+ = do wargs <- P.try (do pushIndent; some (wExpr syn))

11171115 ist <- get

11181116 n <- case lastParse ist of

11191117 Just t -> return t

11201118 Nothing -> fail "Invalid clause"

1121− (do r <- rhs syn n

1119+ (do (r, fc) <- rhs syn n

11221120 let wsyn = syn { syn_namespace = [], syn_toplevel = False }

11231121 (wheres, nmap) <- whereBlock n wsyn <* popIndent

11241122 <|> ([], []) <$ terminator

1125− return $ \fc -> PClauseR fc wargs r wheres) <|> (do

1123+ return $ PClauseR fc wargs r wheres) <|> (do

11261124 popIndent

1127− keyword "with"

1128− wval <- simpleExpr syn

1129− pn <- optProof

1125+ ((wval, pn), fc) <- withExtent $ do

1126+ keyword "with"

1127+ wval <- bracketed syn

1128+ pn <- optProof

1129+ return (wval, pn)

11301130 openBlock

11311131 ds <- some $ fnDecl syn

11321132 let withs = concat ds

11331133 closeBlock

1134− return $ \fc -> PWithR fc wargs wval pn withs))

1134+ return $ PWithR fc wargs wval pn withs)

11351135 -- <==

11361136 <|> do ty <- P.try (do pushIndent

11371137 ty <- simpleExpr syn

11381138 symbol "<=="

11391139 return ty)

11401140 (n, fc) <- withExtent (expandNS syn <$> fnName)

1141− r <- rhs syn n

1141+ (r, _) <- rhs syn n

11421142 let wsyn = syn { syn_namespace = [] }

11431143 (wheres, nmap) <- whereBlock n wsyn <* popIndent

11441144 <|> ([], []) <$ terminator

@@ -1153,7 +1153,7 @@ clause syn

11531153 <|> do pushIndent

11541154 (n, nfc, capp, wargs) <- lhs

11551155 modify $ \ist -> ist { lastParse = Just n }

1156− (do (rs, fc) <- withExtent (rhs syn n)

1156+ (do (rs, fc) <- rhs syn n

11571157 let wsyn = syn { syn_namespace = [] }

11581158 (wheres, nmap) <- whereBlock n wsyn <* popIndent

11591159 <|> ([], []) <$ terminator

@@ -1480,7 +1480,7 @@ parseImports :: FilePath -> String -> Idris (Maybe (Docstring ()), [String], [Im

14801480parseImports fname input

14811481 = do i <- getIState

14821482 case runparser imports i fname input of

1483− Left err -> ifail . show . parseErrorDoc $ err

1483+ Left err -> formatMessage err >>= ifail . show

14841484 Right (x, annots, i) ->

14851485 do putIState i

14861486 fname' <- runIO $ Dir.makeAbsolute fname

@@ -1525,12 +1525,9 @@ parseProg :: SyntaxInfo -> FilePath -> String -> Maybe Mark -> Idris [PDecl]

15251525parseProg syn fname input mrk

15261526 = do i <- getIState

15271527 case runparser mainProg i fname input of

1528− Left err -> do let fc = errorExtent err

1528+ Left err -> do emitWarning err

15291529 i <- getIState

1530− case idris_outputmode i of

1531− RawOutput h -> iputStrLn (show . fixColour (idris_colourRepl i) . parseErrorDoc $ err)

1532− IdeMode n h -> iWarn fc (Util.Pretty.text $ errorMessage err)

1533− putIState (i { errSpan = Just fc })

1530+ putIState (i { errSpan = Just (messageExtent err) })

15341531 return []

15351532 Right (x, i) -> do putIState i

15361533 reportParserWarnings

src/Idris/Parser/Stack.hs+8−11

@@ -13,8 +13,6 @@ module Idris.Parser.Stack

1313 , runparser

1414 -- * Parse errors

1515 , ParseError

16− , errorExtent

17− , errorMessage

1816 , prettyError

1917 -- * Mark and restore

2018 , Mark

@@ -35,6 +33,7 @@ module Idris.Parser.Stack

3533where

3634

3735import Idris.Core.TT (FC(..))

36+import Idris.Output (Message(..))

3837

3938import Control.Arrow (app)

4039import Control.Monad.State.Strict (StateT(..), evalStateT)

@@ -44,6 +43,7 @@ import qualified Data.List.NonEmpty as NonEmpty

4443import Data.Void (Void(..))

4544import System.FilePath (addTrailingPathSeparator, splitFileName)

4645import qualified Text.Megaparsec as P

46+import qualified Util.Pretty as PP

4747

4848{- * Parsing -}

4949

@@ -64,15 +64,12 @@ runparser p i inputname s =

6464

6565data ParseError = ParseError String (P.ParseError (P.Token String) Void)

6666

67−-- | Retrieve a parse error's FC

68−errorExtent :: ParseError -> FC

69−errorExtent (ParseError _ err) = sourcePositionFC pos

70− where

71− (pos NonEmpty.:| _) = P.errorPos err

72−

73−-- | A single-line parse error message, including location.

74−errorMessage :: ParseError -> String

75−errorMessage (ParseError _ err) = P.parseErrorTextPretty err

67+instance Message ParseError where

68+ messageExtent (ParseError _ err) = sourcePositionFC pos

69+ where

70+ (pos NonEmpty.:| _) = P.errorPos err

71+ messageText (ParseError _ err) = PP.text . init . P.parseErrorTextPretty $ err

72+ messageSource (ParseError src _) = Just src

7673

7774-- | A fully formatted parse error, with caret and bar, etc.

7875prettyError :: ParseError -> String

src/Idris/Prover.hs+6−3

@@ -317,8 +317,9 @@ elabloop info fn d prompt prf e prev h env

317317 (d, prev', st, done, prf', env', res) <-

318318 idrisCatch

319319 (case cmd of

320− Left err ->

321− return (False, prev, e, False, prf, env, Left . Msg . show . fixColour (idris_colourRepl ist) . parseErrorDoc $ err)

320+ Left err -> do

321+ msg <- fmap (Left . Msg . show) (formatMessage err)

322+ return (False, prev, e, False, prf, env, msg)

322323 Right (Left cmd') ->

323324 case cmd' of

324325 EQED -> do hs <- lifte e get_holes

@@ -433,7 +434,9 @@ ploop fn d prompt prf e h

433434 _ -> return ()

434435 (d, st, done, prf', res) <- idrisCatch

435436 (case cmd of

436− Left err -> return (False, e, False, prf, Left . Msg . show . fixColour (idris_colourRepl i) . parseErrorDoc $ err)

437+ Left err -> do

438+ msg <- fmap (Left . Msg . show) (formatMessage err)

439+ return (False, e, False, prf, msg)

437440 Right Undo -> do (_, st) <- elabStep e loadState

438441 return (True, st, False, init prf, Right $ iPrintResult "")

439442 Right ProofState -> return (True, e, False, prf, Right $ iPrintResult "")

src/Idris/REPL.hs+1−2

@@ -725,9 +725,8 @@ processInput cmd orig inputs efile

725725 let opts = idris_options i

726726 let quiet = opt_quiet opts

727727 let fn = fromMaybe "" (listToMaybe inputs)

728− c <- colourise

729728 case parseCmd i "(input)" cmd of

730− Left err -> Just inputs <$ iputStrLn (show . fixColour c . parseErrorDoc $ err)

729+ Left err -> Just inputs <$ emitWarning err

731730 Right (Right Reload) ->

732731 reload orig inputs

733732 Right (Right Watch) ->

test/basic002/expected+8

@@ -1,5 +1,13 @@

11test006.idr:25:23-27:

2+ |

3+25 | Main.parity_lemma_2 = proof {

4+ | ~~~~~

25This style of tactic proof is deprecated. See %runElab for the replacement.

6+

37test006.idr:32:23-27:

8+ |

9+32 | Main.parity_lemma_1 = proof {

10+ | ~~~~~

411This style of tactic proof is deprecated. See %runElab for the replacement.

12+

513[False, True, False, True, False, True]

test/basic006/expected+6−1

@@ -1,4 +1,8 @@

1−test020a.idr:16:10-19:When checking right hand side of foo with expected type

1+test020a.idr:16:10-19:

2+ |

3+16 | foo xs = reverse xs

4+ | ~~~~~~~~~~

5+When checking right hand side of foo with expected type

26 List a

37

48When checking an application of function Prelude.List.reverse:

@@ -6,5 +10,6 @@ When checking an application of function Prelude.List.reverse:

610 Vect n a (Type of xs)

711 and

812 List a (Expected type)

13+

914[3, 2, 1]

1015"Number 42"

test/basic009/expected+18−3

@@ -1,7 +1,16 @@

11MAIN-PASS

2−Faulty.idr:6:9-11:num is bound as an implicit

2+Faulty.idr:6:9-11:

3+ |

4+6 | fault : num = Z

5+ | ~~~

6+num is bound as an implicit

37 Did you mean to refer to A.num?

4−Faulty.idr:7:7-12:When checking right hand side of fault with expected type

8+

9+Faulty.idr:7:9-12:

10+ |

11+7 | fault = Refl

12+ | ~~~~

13+When checking right hand side of fault with expected type

514 num = 0

615

716Type mismatch between

@@ -14,4 +23,10 @@ Specifically:

1423 0

1524 and

1625 num

17−Multiple.idr:3:21:import alias not unique: "X"

26+

27+Multiple.idr:3:21:

28+ |

29+3 | import Data.Vect as X

30+ | ^

31+import alias not unique: "X"

32+

test/basic016/expected+1−1

@@ -1 +1 @@

1−Cycle detected in imports: CycleA.idr -> CycleB -> CycleC -> CycleA -> CycleB

1+ Cycle detected in imports: CycleA.idr -> CycleB -> CycleC -> CycleA -> CycleB

test/basic017/expected+6−1

@@ -1,3 +1,8 @@

1−basic017a.idr:11:8:When checking type of Main.append:

1+basic017a.idr:11:8:

2+ |

3+11 | append : Vect n a -> Vect m a -> Vect (n + m) a

4+ | ^

5+When checking type of Main.append:

26When checking an application of Main.Vect:

37 No such variable n

8+

test/basic018/expected+14−1

@@ -1,10 +1,22 @@

11basic018.idr:7:12-16:

2+ |

3+7 | Vect thing elem

4+ | ~~~~~

25thing is bound as an implicit

36 Did you mean to refer to Main.thing?

7+

48basic018.idr:12:8-12:

9+ |

10+12 | test : thing = S 41

11+ | ~~~~~

512thing is bound as an implicit

613 Did you mean to refer to Main.thing?

7−basic018.idr:13:6-11:When checking right hand side of test with expected type

14+

15+basic018.idr:13:8-11:

16+ |

17+13 | test = Refl

18+ | ~~~~

19+When checking right hand side of test with expected type

820 thing = S 41

921

1022Type mismatch between

@@ -17,3 +29,4 @@ Specifically:

1729 42

1830 and

1931 thing

32+

test/directives001/expected+36−6

@@ -1,12 +1,42 @@

1−directives001.idr:14:7:Use of deprecated name directives001.Foo

1+directives001.idr:14:7:

2+ |

3+14 | mkFoo : String -> Foo

4+ | ^

5+Use of deprecated name directives001.Foo

26To be replaced with `Bar`.

3−directives001.idr:14:7:Use of deprecated name directives001.Foo

7+

8+directives001.idr:14:7:

9+ |

10+14 | mkFoo : String -> Foo

11+ | ^

12+Use of deprecated name directives001.Foo

413To be replaced with `Bar`.

5−directives001.idr:15:7-13:Use of deprecated name directives001.Foo

14+

15+directives001.idr:15:9-13:

16+ |

17+15 | mkFoo = MkFoo

18+ | ~~~~~

19+Use of deprecated name directives001.Foo

620To be replaced with `Bar`.

7−directives001.idr:15:7-13:Use of deprecated name directives001.Foo

21+

22+directives001.idr:15:9-13:

23+ |

24+15 | mkFoo = MkFoo

25+ | ~~~~~

26+Use of deprecated name directives001.Foo

827To be replaced with `Bar`.

9−directives001.idr:26:8-28:28:Use of a fragile construct directives001.mkBar

28+

29+directives001.idr:26:10-28:28:

30+ |

31+26 | main = do

32+ | ~~ ...

33+Use of a fragile construct directives001.mkBar

1034How `Bar`s are to be created is still being discussed, `mkBar` is subject to change.

11−directives001.idr:26:8-28:28:Use of a fragile construct directives001.mkBar

35+

36+directives001.idr:26:10-28:28:

37+ |

38+26 | main = do

39+ | ~~ ...

40+Use of a fragile construct directives001.mkBar

1241How `Bar`s are to be created is still being discussed, `mkBar` is subject to change.

42+

test/directives002/expected+4

@@ -1,2 +1,6 @@

11directives002.idr:12:3-14:28:

2+ |

3+12 | main = do

4+ | ~~~~~~~~~ ...

25directives002.Main.main is possibly not total due to: directives002.loop

6+

test/effects003/expected+4

@@ -1,5 +1,9 @@

11hangman.idr:204:8-12:

2+ |

3+204 | wlen = proof search

4+ | ~~~~~

25This style of tactic proof is deprecated. See %runElab for the replacement.

6+

37------------

48

596 guesses left

test/error001/expected+6−1

@@ -1,4 +1,8 @@

1−test002.idr:1:6:Universe inconsistency.

1+test002.idr:1:6:

2+ |

3+1 | myid : (a : Type) -> a -> a

4+ | ^

5+Universe inconsistency.

26 Working on: ./test002.idr.z

37 Old domain: (6,6)

48 New domain: (6,5)

@@ -6,3 +10,4 @@ test002.idr:1:6:Universe inconsistency.

610 ConstraintFC {uconstraint = ./test002.idr.z <= ./test002.idr.a1, ufc = test002.idr:1:6}

711 ConstraintFC {uconstraint = ./test002.idr.y < ./test002.idr.z, ufc = test002.idr:1:6}

812 ConstraintFC {uconstraint = ./test002.idr.z <= ./test002.idr.a1, ufc = test002.idr:1:6}

13+

test/error003/expected+5−1

@@ -1,5 +1,9 @@

1−ErrorReflection.idr:68:5-20:

1+ErrorReflection.idr:68:7-20:

2+ |

3+68 | bad = Lam (Var Here)

4+ | ~~~~~~~~~~~~~~

25When checking right hand side of bad with expected type

36 Tm [] TUnit

47

58DSL type error: (t(504) => t'(503)) doesn't match ()

9+

test/error004/expected+8

@@ -1,12 +1,20 @@

11FunErrTest.idr:35:12-18:

2+ |

3+35 | badCadr1 = cadr []

4+ | ~~~~~~~

25When checking right hand side of badCadr1 with expected type

36 Int

47

58When checking argument cons2 to function FunErrTest.cadr:

69 Could not prove that [] has at least two elements.

10+

711FunErrTest.idr:38:12-19:

12+ |

13+38 | badCadr2 = cadr [1]

14+ | ~~~~~~~~

815When checking right hand side of badCadr2 with expected type

916 Int

1017

1118When checking argument cons2 to function FunErrTest.cadr:

1219 Could not prove that [] has at least two elements.

20+

test/error005/expected+30−5

@@ -1,31 +1,56 @@

1−error005.idr:11:7:When checking right hand side of two with expected type

1+error005.idr:11:7:

2+ |

3+11 | two = 2

4+ | ^

5+When checking right hand side of two with expected type

26 Fin 2

37

48When checking argument prf to function Data.Fin.fromInteger:

59 When using 2 as a literal for a Fin 2

610 2 is not strictly less than 2

7−error005.idr:14:12:When checking right hand side of hahaha with expected type

11+

12+error005.idr:14:12:

13+ |

14+14 | hahaha n = 0

15+ | ^

16+When checking right hand side of hahaha with expected type

817 Fin n

918

1019When checking argument prf to function Data.Fin.fromInteger:

1120 When using 0 as a literal for a Fin n

1221 0 is not strictly less than n

13−error005.idr:20:11:When checking right hand side of notOk with expected type

22+

23+error005.idr:20:11:

24+ |

25+20 | notOk n = 2

26+ | ^

27+When checking right hand side of notOk with expected type

1428 Fin (plus 2 n)

1529

1630When checking argument prf to function Data.Fin.fromInteger:

1731 When using 2 as a literal for a Fin (S (S n))

1832 2 is not strictly less than S (S n)

19−error005.idr:23:12-24:When checking right hand side of b0rken with expected type

33+

34+error005.idr:23:12-24:

35+ |

36+23 | b0rken n = fromInteger n

37+ | ~~~~~~~~~~~~~

38+When checking right hand side of b0rken with expected type

2039 Fin 3

2140

2241When checking argument prf to function Data.Fin.fromInteger:

2342 When using n as a literal for a Fin 3

2443 Could not show that n is less than 3 because n is a bound

2544 variable instead of a constant Integer

26−error005.idr:26:17:When checking right hand side of x with expected type

45+

46+error005.idr:26:17:

47+ |

48+26 | x = the (Fin 4) 5

49+ | ^

50+When checking right hand side of x with expected type

2751 Fin 4

2852

2953When checking argument prf to function Data.Fin.fromInteger:

3054 When using 5 as a literal for a Fin 4

3155 5 is not strictly less than 4

56+

test/error006/expected+6−1

@@ -1,2 +1,7 @@

1−WithPatsNoWith.idr:4:1-13:When checking left hand side of foo:

1+WithPatsNoWith.idr:4:1-13:

2+ |

3+4 | foo 1 | 2 | 3 = True

4+ | ~~~~~~~~~~~~~

5+When checking left hand side of foo:

26unexpected patterns outside of "with" block

7+

test/error007/expected+4

@@ -1,4 +1,7 @@

11error007.idr:26:7-29:

2+ |

3+26 | send_page conn str code -- (prim__zextB32_Int code)

4+ | ~~~~~~~~~~~~~~~~~~~~~~~

25When checking right hand side of answer_to_connection with expected type

36 IO Int

47

@@ -13,3 +16,4 @@ When checking argument code to function Main.send_page:

1316 Bits32

1417 and

1518 Int

19+

test/error008/expected+12−2

@@ -1,4 +1,14 @@

1−error008.idr:3:4:When checking type of Main.s2:

1+error008.idr:3:4:

2+ |

3+3 | s2 : x + sum Nil = x * fromInteger 0

4+ | ^

5+When checking type of Main.s2:

26Can't disambiguate name: Prelude.List.Nil, Data.Vect.Nil

3−error008a.idr:3:4:When checking type of Main.s1:

7+

8+error008a.idr:3:4:

9+ |

10+3 | s1 : Num a => {x : a} -> x + sum {a} Nil = x -- * fromInteger 0

11+ | ^

12+When checking type of Main.s1:

413Can't disambiguate name: Prelude.List.Nil, Data.Vect.Nil

14+

test/ffi002/expected+6−1

@@ -1 +1,6 @@

1−test023.idr:20:26-36:Type provider error: Always fails

1+test023.idr:20:26-36:

2+ |

3+20 | %provide (t : Type) with badProvider

4+ | ~~~~~~~~~~~

5+Type provider error: Always fails

6+

test/interfaces008/expected+4

@@ -1,2 +1,6 @@

11interfaces008.idr:20:18-23:

2+ |

3+20 | implementation Foo2 a where

4+ | ~~~~~~

25Default implementations must be for a super interface constraint on the containing interface.

6+

test/layout001/expected+23−13

@@ -1,72 +1,82 @@

1−./layout001a.idr:5:1:

1+layout001a.idr:5:1:

22 |

335 | y

44 | ^

55Wrong indention: should be greater than context indentation

66

7−./layout001b.idr:5:3:

7+layout001b.idr:5:3:

88 |

995 | = y

1010 | ^

1111Wrong indention: should be greater than context indentation

1212

13−./layout001c.idr:3:1:

13+layout001c.idr:3:1:

1414 |

15153 | 2

1616 | ^

1717Wrong indention: should be greater than context indentation

1818

19−./layout001e.idr:6:1:

19+layout001e.idr:6:1:

2020 |

21216 | 3

2222 | ^

2323Wrong indention: should be greater than context indentation

2424

25−./layout001f.idr:6:2:

25+layout001f.idr:6:2:

2626 |

27276 | 3

2828 | ^

2929Wrong indention: should be greater than context indentation

3030

31−./layout001g.idr:6:3:

31+layout001g.idr:6:3:

3232 |

33336 | 3

3434 | ^

3535Wrong indention: should be greater than context indentation

3636

37−./layout001h.idr:6:3:

37+layout001h.idr:6:3:

3838 |

39396 | 3

4040 | ^

4141Wrong indention: should be greater than context indentation

4242

43−./layout001i.idr:6:4:

43+layout001i.idr:6:4:

4444 |

45456 | 3

4646 | ^

4747Wrong indention: should be greater than context indentation

4848

49−./layout001j.idr:6:5:

49+layout001j.idr:6:5:

5050 |

51516 | 3

5252 | ^

5353Wrong indention: should be greater than context indentation

5454

55−./layout001l.idr:6:1:

55+layout001l.idr:6:1:

5656 |

57576 | y

5858 | ^

5959Wrong indention: should be greater than context indentation

6060

61−mplus1.idr:13:31-17:49:When checking right hand side of term with expected type

61+mplus1.idr:13:34-17:49:

62+ |

63+13 | term = do f <- factor

64+ | ~~~~~~~~~~~~~~ ...

65+When checking right hand side of term with expected type

6266 Maybe Int

6367

6468When checking an application of function Prelude.Applicative.pure:

6569 No such variable f

66−./mplus2.idr:17:37:

70+

71+mplus2.idr:17:37:

6772 |

687317 | `mplus` pure f

6974 | ^

7075not end of block

7176

72−mplus3.idr:11:1-16:warning - Unreachable case: term

77+mplus3.idr:11:1-16:

78+ |

79+11 | term = ?term_rhs

80+ | ~~~~~~~~~~~~~~~~

81+Unreachable case: term

82+

test/literate001/expected+6−1

@@ -1,4 +1,9 @@

1−./test003a.lidr:1:0:Program line next to comment

1+./test003a.lidr:1:0:

2+ |

3+1 | Broken

4+ |^

5+Program line next to comment

6+

27'a'

38'd'

49zabcdefg

test/meta002/expected+14−2

@@ -1,13 +1,25 @@

11DataDef.idr:74:1-8:

2+ |

3+74 | %runElab nope

4+ | ~~~~~~~~

25While running an elaboration script, the following error occurred:

36Prelude.Either.Either is already defined as a datatype.

4−Tacs.idr:299:15-300:78:

7+

8+Tacs.idr:299:17-300:78:

9+ |

10+299 | testElab3 = %runElab (elaborateSTLC (App (Lam "x" (App (Var 0) (Var 0)))

11+ | ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ ...

512When checking right hand side of testElab3 with expected type

613 DPair Ty (Tm [])

714

815Unifying ty and ARR ty t would lead to infinite value

9−AgdaStyleReflection.idr:315:5-20:

16+

17+AgdaStyleReflection.idr:315:7-20:

18+ |

19+315 | baz = tactic trivial

20+ | ~~~~~~~~~~~~~~

1021When checking right hand side of baz with expected type

1122 (Nat, Void)

1223

1324PROOF SEARCH FAILURE is not defined.

25+

test/meta003/expected+4

@@ -1,6 +1,10 @@

11BadDef.idr:14:1-8:

2+ |

3+14 | %runElab mkBadDef1

4+ | ~~~~~~~~

25While running an elaboration script, the following error occurred:

36Type mismatch between

47 ()

58and

69 String

10+

test/meta004/expected+4

@@ -1,3 +1,7 @@

11meta004.idr:50:1-8:

2+ |

3+50 | %runElab domore

4+ | ~~~~~~~~

25While running an elaboration script, the following error occurred:

36Not an impossible case

7+

test/proof001/expected+8

@@ -1,4 +1,12 @@

11test029.idr:29:25-29:

2+ |

3+29 | simple.append_lemma_2 = proof {

4+ | ~~~~~

25This style of tactic proof is deprecated. See %runElab for the replacement.

6+

37test029.idr:36:25-29:

8+ |

9+36 | simple.append_lemma_1 = proof {

10+ | ~~~~~

411This style of tactic proof is deprecated. See %runElab for the replacement.

12+

test/proof002/expected+16

@@ -1,10 +1,25 @@

11Reflect.idr:175:21-25:

2+ |

3+175 | Reflect.appRExpr1 = proof {

4+ | ~~~~~

25This style of tactic proof is deprecated. See %runElab for the replacement.

6+

37Reflect.idr:184:21-25:

8+ |

9+184 | Reflect.appRExpr2 = proof {

10+ | ~~~~~

411This style of tactic proof is deprecated. See %runElab for the replacement.

12+

513Reflect.idr:192:15-19:

14+ |

15+192 | Reflect.bp1 = proof {

16+ | ~~~~~

617This style of tactic proof is deprecated. See %runElab for the replacement.

18+

719test030a.idr:12:26-37:

20+ |

21+12 | testReflect1 {a} xs ys = AssocProof a

22+ | ~~~~~~~~~~~~

823When checking right hand side of testReflect1 with expected type

924 ys ++ x :: ys ++ xs = (xs ++ [x]) ++ ys ++ xs

1025

@@ -19,3 +34,4 @@ When checking an application of function Reflect.getJust:

1934 Just x

2035 and

2136 Nothing

37+

test/proof003/expected+24

@@ -1,15 +1,39 @@

11Parity.idr:17:18-22:

2+ |

3+17 | parity_lemma_2 = proof {

4+ | ~~~~~

25This style of tactic proof is deprecated. See %runElab for the replacement.

6+

37Parity.idr:24:18-22:

8+ |

9+24 | parity_lemma_1 = proof {

10+ | ~~~~~

411This style of tactic proof is deprecated. See %runElab for the replacement.

12+

513test015.idr:88:15-19:

14+ |

15+88 | Main.ntbOdd = proof {

16+ | ~~~~~

617This style of tactic proof is deprecated. See %runElab for the replacement.

18+

719test015.idr:97:16-20:

20+ |

21+97 | Main.ntbEven = proof {

22+ | ~~~~~

823This style of tactic proof is deprecated. See %runElab for the replacement.

24+

925test015.idr:107:20-24:

26+ |

27+107 | Main.adc_lemma_2 = proof {

28+ | ~~~~~

1029This style of tactic proof is deprecated. See %runElab for the replacement.

30+

1131test015.idr:142:20-24:

32+ |

33+142 | Main.adc_lemma_1 = proof {

34+ | ~~~~~

1235This style of tactic proof is deprecated. See %runElab for the replacement.

36+

133700101010

143801011001

1539010000011

test/proof007/expected+5−1

@@ -1,6 +1,10 @@

1−DefaultArgUnknownName.idr:9:6-23:

1+DefaultArgUnknownName.idr:9:8-23:

2+ |

3+9 | test = funWithBadDefArg

4+ | ~~~~~~~~~~~~~~~~

25When checking right hand side of test with expected type

36 ()

47

58When checking argument arg to function DefaultArgUnknownName.funWithBadDefArg:

69 No such variable sadgjhsag

10+

test/proof008/expected+4

@@ -1,2 +1,6 @@

11ClaimAndUnfocus.idr:8:27-31:

2+ |

3+8 | ClaimAndUnfocus.foo_rhs = proof

4+ | ~~~~~

25This style of tactic proof is deprecated. See %runElab for the replacement.

6+

test/proof011/expected+10−2

@@ -1,4 +1,7 @@

1−proof011.idr:20:5-21:18:

1+proof011.idr:20:7-21:18:

2+ |

3+20 | = rewrite vassoc xs ys xs using vreplace in

4+ | ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ ...

25When checking right hand side of vassoc' with expected type

36 (x :: xs) ++ ys ++ zs = ((x :: xs) ++ ys) ++ zs

47

@@ -8,7 +11,11 @@ rewriting xs ++ ys ++ xs to (xs ++ ys) ++ xs did not change type x ::

811 x ::

912 (xs ++ ys) ++

1013 zs

11−proof011a.idr:14:5-37:

14+

15+proof011a.idr:14:7-37:

16+ |

17+14 | = rewrite vassoc xs ys xs in Refl

18+ | ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

1219When checking right hand side of vassoc' with expected type

1320 (x :: xs) ++ ys ++ zs = ((x :: xs) ++ ys) ++ zs

1421

@@ -18,3 +25,4 @@ rewriting xs ++ ys ++ xs to (xs ++ ys) ++ xs did not change type x ::

1825 x ::

1926 (xs ++ ys) ++

2027 zs

28+

test/quasiquote003/expected+6−1

@@ -1,4 +1,9 @@

1−NoInfer.idr:11:5-11:When checking right hand side of zzz with expected type

1+NoInfer.idr:11:7-11:

2+ |

3+11 | zzz = `(FZ)

4+ | ~~~~~

5+When checking right hand side of zzz with expected type

26 TT

37

48No such variable k

9+

test/quasiquote004/expected+17−1

@@ -1,11 +1,27 @@

11Quasiquote004.idr:39:26-30:

2+ |

3+39 | Quasiquote004.getMeNat = proof

4+ | ~~~~~

25This style of tactic proof is deprecated. See %runElab for the replacement.

6+

37Quasiquote004.idr:42:28-32:

8+ |

9+42 | Quasiquote004.fizzyIsAOK = proof

10+ | ~~~~~

411This style of tactic proof is deprecated. See %runElab for the replacement.

12+

513Quasiquote004.idr:50:27-31:

14+ |

15+50 | Quasiquote004.getMeNat' = proof

16+ | ~~~~~

617This style of tactic proof is deprecated. See %runElab for the replacement.

7−Quasiquote004.idr:50:25-51:18:

18+

19+Quasiquote004.idr:50:27-51:18:

20+ |

21+50 | Quasiquote004.getMeNat' = proof

22+ | ~~~~~ ...

823When checking right hand side of Quasiquote004.getMeNat' with expected type

924 String

1025

1126Not a Nat goal

27+

test/quasiquote006/expected+16−4

@@ -1,19 +1,31 @@

1−quasiquote006.idr:9:3-10:

1+quasiquote006.idr:9:5-10:

2+ |

3+9 | b = `{Nil}

4+ | ~~~~~~

25When checking right hand side of b with expected type

36 TTName

47

58Can't disambiguate name: ForeignEnv.Nil,

69 Prelude.List.Nil

7−quasiquote006.idr:12:3-17:

10+

11+quasiquote006.idr:12:5-17:

12+ |

13+12 | c = `{alsdkjflkj}

14+ | ~~~~~~~~~~~~~

815When checking right hand side of c with expected type

916 TTName

1017

1118No such variable alsdkjflkj

12−quasiquote006.idr:15:3-11:

19+

20+quasiquote006.idr:15:5-11:

21+ |

22+15 | d = `{(::)}

23+ | ~~~~~~~

1324When checking right hand side of d with expected type

1425 TTName

1526

1627Can't disambiguate name: ForeignEnv.::,

1728 Prelude.List.::,

1829 Prelude.Stream.::

19−quasiquote006.idr:17:3:Main.d already defined

30+

31+ quasiquote006.idr:17:3:Main.d already defined

test/reg017/expected+8

@@ -1,5 +1,13 @@

11reg017.idr:5:17-23:

2+ |

3+5 | { default tactics { refine Refl; solve; } prfA : a = a } ->

4+ | ~~~~~~~

25This style of tactic proof is deprecated. See %runElab for the replacement.

6+

37reg017.idr:8:17-23:

8+ |

9+8 | { default tactics { refine Refl; solve; } prfBC : b = c } ->

10+ | ~~~~~~~

411This style of tactic proof is deprecated. See %runElab for the replacement.

12+

5134

test/reg027/expected+6−1

@@ -1,2 +1,7 @@

11<<int fn>>

2−reg027a.idr:9:16-30:Overlapping implementation: Show (Int -> a) already defined

2+reg027a.idr:9:16-30:

3+ |

4+9 | implementation Show (Int -> b) where

5+ | ~~~~~~~~~~~~~~~

6+Overlapping implementation: Show (Int -> a) already defined

7+

test/regression002/expected+238−36

@@ -1,13 +1,41 @@

1−reg003a.idr:4:13-38:When checking type of Main.ECons:

1+reg003a.idr:4:13-38:

2+ |

3+4 | ECons : Nat -> OddList -> EvenList

4+ | ~~~~~~~~~~~~~~~~~~~~~~~~~~

5+When checking type of Main.ECons:

26No such variable OddList

3−reg003a.idr:7:13-38:When checking type of Main.OCons:

7+

8+reg003a.idr:7:13-38:

9+ |

10+7 | OCons : Nat -> EvenList -> OddList

11+ | ~~~~~~~~~~~~~~~~~~~~~~~~~~

12+When checking type of Main.OCons:

413No such variable EvenList

5−reg003a.idr:9:6:When checking type of Main.test:

14+

15+reg003a.idr:9:6:

16+ |

17+9 | test : EvenList

18+ | ^

19+When checking type of Main.test:

620No such variable EvenList

21+

722reg006.idr:17:1-23:

23+ |

24+17 | lookup k Leaf = Nothing

25+ | ~~~~~~~~~~~~~~~~~~~~~~~

826RBTree.lookup is possibly not total due to recursive path RBTree.lookup --> RBTree.lookup

9−reg007.lidr:8:3-13:A.n is already defined

10−reg007.lidr:12:13-18:When checking right hand side of hurrah with expected type

27+

28+reg007.lidr:8:3-13:

29+ |

30+8 | > A.n = Z -- This is where it's at!

31+ | ~~~~~~~~~~~

32+A.n is already defined

33+

34+reg007.lidr:12:13-18:

35+ |

36+12 | > hurrah = isSame

37+ | ~~~~~~

38+When checking right hand side of hurrah with expected type

1139 0 = 1

1240

1341Type mismatch between

@@ -20,40 +48,111 @@ Specifically:

2048 1

2149 and

2250 0

51+

2352reg010.idr:5:3-26:

53+ |

54+5 | unsafeSubst P x x px | _ = px

55+ | ~~~~~~~~~~~~~~~~~~~~~~~~

2456When checking left hand side of with block in usubst.unsafeSubst:

2557Can't match on with block in usubst.unsafeSubst warg a P x x px

58+

2659reg018a.idr:16:1-18:

60+ |

61+16 | minusCoNat Z n = Z

62+ | ~~~~~~~~~~~~~~~~~~

2763conat.minusCoNat is possibly not total due to recursive path conat.minusCoNat --> conat.minusCoNat

64+

2865reg018a.idr:21:1-42:

66+ |

67+21 | loopForever = minusCoNat infinity infinity

68+ | ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

2969conat.loopForever is possibly not total due to: conat.minusCoNat

70+

3071reg018b.idr:8:1-28:

72+ |

73+8 | showB (I x) = "I" ++ showB x

74+ | ~~~~~~~~~~~~~~~~~~~~~~~~~~~~

3175A.showB is possibly not total due to recursive path A.showB --> A.showB

76+

3277reg018b.idr:11:1-6:

78+ |

79+11 | Show B where show = showB

80+ | ~~~~~~

3381A.B implementation of Prelude.Show.Show is possibly not total due to: A.showB

82+

3483reg018c.idr:21:1-22:21:

84+ |

85+21 | inf (x :: xs) with (hdtl xs)

86+ | ~~~~~~~~~~~~~~~~~~~~~~~~~~~~ ...

3587CodataTest.inf is possibly not total due to: with block in CodataTest.inf

36−reg018d.idr:8:1-39:Main.pull is not total as there are missing cases

37−reg023.idr:7:5-7:When checking right hand side of bad with expected type

88+

89+reg018d.idr:8:1-39:

90+ |

91+8 | pull {n=Z} _ (x :: xs) = (x, xs)

92+ | ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

93+Main.pull is not total as there are missing cases

94+

95+reg023.idr:7:7:

96+ |

97+7 | bad = Z

98+ | ^

99+When checking right hand side of bad with expected type

38100 f Nat

39101

40102Type mismatch between

41103 Nat (Type of 0)

42104and

43105 f Nat (Expected type)

44−reg028.idr:5:1-9:tbad.bad is possibly not total due to: with block in tbad.bad

106+

107+reg028.idr:5:1-9:

108+ |

109+5 | bad Z = Z

110+ | ~~~~~~~~~

111+tbad.bad is possibly not total due to: with block in tbad.bad

112+

45113reg028a.idr:17:14-18:

114+ |

115+17 | qsortLemma = proof

116+ | ~~~~~

46117This style of tactic proof is deprecated. See %runElab for the replacement.

118+

47119reg028a.idr:11:1-14:

120+ |

121+11 | qsort' [] = []

122+ | ~~~~~~~~~~~~~~

48123tbad.qsort' is possibly not total due to: with block in tbad.qsort'

49−reg034.idr:6:1-14:When checking left hand side of bar:

124+

125+reg034.idr:6:1-14:

126+ |

127+6 | bar xs xs Refl = Refl

128+ | ~~~~~~~~~~~~~~

129+When checking left hand side of bar:

50130Can't match on bar xs xs Refl

51−reg034.idr:9:1-14:When checking left hand side of foo:

131+

132+reg034.idr:9:1-14:

133+ |

134+9 | foo f x x Refl = Refl

135+ | ~~~~~~~~~~~~~~

136+When checking left hand side of foo:

52137Can't match on foo f x x Refl

53−reg035b.idr:8:12-38:No such variable __pi_arg

138+

139+reg035b.idr:8:14-38:

140+ |

141+8 | fins Z = ([] ** (finZEmpty {a=_}))

142+ | ~~~~~~~~~~~~~~~~~~~~~~~~~

143+No such variable __pi_arg

144+

54145reg044.idr:4:6-10:

146+ |

147+4 | pf = proof

148+ | ~~~~~

55149This style of tactic proof is deprecated. See %runElab for the replacement.

56−reg044.idr:4:4-6:13:When checking right hand side of Main.pf with expected type

150+

151+reg044.idr:4:6-6:13:

152+ |

153+4 | pf = proof

154+ | ~~~~~ ...

155+When checking right hand side of Main.pf with expected type

57156 (b : Nat) -> (a : Nat) -> (S a = S b) -> a = b

58157

59158Type mismatch between

@@ -66,73 +165,165 @@ Specifically:

66165 b

67166 and

68167 a

69−reg049.idr:2:11-14:When checking constructor Main.Bogus:

168+

169+reg049.idr:2:11-14:

170+ |

171+2 | Bogus : Void

172+ | ~~~~

173+When checking constructor Main.Bogus:

70174Void is not Main.Foo

71−reg049.idr:5:6-12:When checking right hand side of uhOh with expected type

175+

176+reg049.idr:5:8-12:

177+ |

178+5 | uhOh = Bogus

179+ | ~~~~~

180+When checking right hand side of uhOh with expected type

72181 Void

73182

74183No such variable Bogus

75−./badbangop.idr:7:1:

184+

185+badbangop.idr:7:1:

76186 |

771877 | (!) : List a -> Nat -> Maybe a

78188 | ^

79189! is not a valid operator

80190

81−./baddoublebang.idr:6:28:

191+baddoublebang.idr:6:28:

82192 |

831936 | doubleBang mmn = do pure !!mmn

84194 | ^

85195unexpected Operator without known fixity: !!

86196

87−reg054.idr:18:1-17:When checking left hand side of inf:

197+reg054.idr:18:1-17:

198+ |

199+18 | inf (MkInfer _ Z) = True

200+ | ~~~~~~~~~~~~~~~~~

201+When checking left hand side of inf:

88202When checking an application of constructor Main.MkInfer:

89203 Attempting concrete match on polymorphic argument: 0

90−reg054.idr:34:1-18:When checking left hand side of weird:

204+

205+reg054.idr:34:1-18:

206+ |

207+34 | weird {x = Char} y = '5'

208+ | ~~~~~~~~~~~~~~~~~~

209+When checking left hand side of weird:

91210No explicit types on left hand side: Char

92−reg054.idr:37:1-30:When checking left hand side of weird':

211+

212+reg054.idr:37:1-30:

213+ |

214+37 | weird' {x = Prelude.Nat.Nat} y = Z

215+ | ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

216+When checking left hand side of weird':

93217No explicit types on left hand side: Nat

94−reg054.idr:40:1-7:When checking left hand side of tctrick:

218+

219+reg054.idr:40:1-7:

220+ |

221+40 | tctrick (Just x) = x

222+ | ~~~~~~~

223+When checking left hand side of tctrick:

95224When checking an application of Main.tctrick:

96225 Type mismatch between

97226 Maybe a1 (Type of Just x)

98227 and

99228 a (Expected type)

100−reg055.idr:5:1-7:When checking left hand side of g:

229+

230+reg055.idr:5:1-7:

231+ |

232+5 | g (f Z) = 1

233+ | ~~~~~~~

234+When checking left hand side of g:

101235Can't match on g (f 0)

102−reg055.idr:8:1-5:When checking left hand side of h:

236+

237+reg055.idr:8:1-5:

238+ |

239+8 | h x x = x

240+ | ~~~~~

241+When checking left hand side of h:

103242Can't match on h x x

104−reg055a.idr:8:1-18:When checking left hand side of foo:

243+

244+reg055a.idr:8:1-18:

245+ |

246+8 | foo (CAny Nothing) = 42

247+ | ~~~~~~~~~~~~~~~~~~

248+When checking left hand side of foo:

105249When checking an application of constructor Foo.CAny:

106250 Attempting concrete match on polymorphic argument: Nothing

107−reg055a.idr:13:1-23:When checking left hand side of Foo.apply:

251+

252+reg055a.idr:13:1-23:

253+ |

254+13 | apply (\x => \y => x) a = a

255+ | ~~~~~~~~~~~~~~~~~~~~~~~

256+When checking left hand side of Foo.apply:

108257Can't match on apply (\x, y => x) a

109−reg056.idr:7:16-25:dodgy n m Refl is a valid case

110−reg056.idr:10:11-20:nonk Refl is a valid case

111−reg068.idr:1:6-8:Main.nat has a name which may be implicitly bound.

258+

259+reg056.idr:7:16-25:

260+ |

261+7 | dodgy n m Refl impossible

262+ | ~~~~~~~~~~

263+dodgy n m Refl is a valid case

264+

265+reg056.idr:10:11-20:

266+ |

267+10 | nonk Refl impossible

268+ | ~~~~~~~~~~

269+nonk Refl is a valid case

270+

271+reg068.idr:1:6-8:

272+ |

273+1 | data nat : Type where --error

274+ | ~~~

275+Main.nat has a name which may be implicitly bound.

112276This is likely to lead to problems!

113−reg068.idr:2:8-10:Main.ze has a name which may be implicitly bound.

277+

278+reg068.idr:2:8-10:

279+ |

280+2 | ze : nat --hello.idr:10:6:When checking constructor Main.ze: !!V 0!! is not Main.nat

281+ | ~~~

282+Main.ze has a name which may be implicitly bound.

114283This is likely to lead to problems!

284+

115285reg068.idr:2:8-10:

286+ |

287+2 | ze : nat --hello.idr:10:6:When checking constructor Main.ze: !!V 0!! is not Main.nat

288+ | ~~~

116289nat is bound as an implicit

117290 Did you mean to refer to Main.nat?

118−reg068.idr:2:8-10:When checking constructor Main.ze:

291+

292+reg068.idr:2:8-10:

293+ |

294+2 | ze : nat --hello.idr:10:6:When checking constructor Main.ze: !!V 0!! is not Main.nat

295+ | ~~~

296+When checking constructor Main.ze:

119297Type level variable nat is not Main.nat

120−Mod.idr:11:1-22:public export Mod.natexp can't refer to export Mod.natfn

298+

299+Mod.idr:11:1-22:

300+ |

301+11 | natexp k = S (natfn k)

302+ | ~~~~~~~~~~~~~~~~~~~~~~

303+public export Mod.natexp can't refer to export Mod.natfn

304+

121305reg070.idr:7:1-7:

306+ |

307+7 | Show Te where

308+ | ~~~~~~~

122309Test_show.Te implementation of Prelude.Show.Show is possibly not total due to: Prelude.Show.Test_show.Te implementation of Prelude.Show.Show, method show

123−./reg076.idr:8:1:

310+

311+reg076.idr:8:1:

124312 |

125−8 | <empty line>

313+8 | <end of file>

126314 | ^

127315Missing fixity declaration for Main.:>

128316

129−./reg077.idr:3:1:

317+reg077.idr:3:1:

130318 |

131−3 | <empty line>

319+3 | <end of file>

132320 | ^

133321Missing fixity declaration for Main.:>>

134322

135323DoubleEquality.idr:4:83-103:

324+ |

325+4 | oops = the ((False = True) -> Void) (\Refl impossible) $ cong {f = (>0) . (1/)} $ the (-0.0 = 0.0) Refl

326+ | ~~~~~~~~~~~~~~~~~~~~~

136327When checking right hand side of oops with expected type

137328 Void

138329

@@ -147,5 +338,16 @@ When checking argument value to function Prelude.Basics.the:

147338 -0.0

148339 and

149340 0.0

150−Canonicity.idr:9:1-9:Canonicity.f is not total as there are missing cases

151−Canonicity.idr:12:1-20:Canonicity.NaN is possibly not total due to: Canonicity.f

341+

342+Canonicity.idr:9:1-9:

343+ |

344+9 | f Nil = 0

345+ | ~~~~~~~~~

346+Canonicity.f is not total as there are missing cases

347+

348+Canonicity.idr:12:1-20:

349+ |

350+12 | NaN = f (Cons 0 Nil)

351+ | ~~~~~~~~~~~~~~~~~~~~

352+Canonicity.NaN is possibly not total due to: Canonicity.f

353+

test/sourceLocation001/expected+18−2

@@ -1,17 +1,33 @@

11SourceLoc.idr:12:19-25:

2+ |

3+12 | getLoc : {default tactics { sourceLocation } x : SourceLocation} -> SourceLocation

4+ | ~~~~~~~

25This style of tactic proof is deprecated. See %runElab for the replacement.

6+

37SourceLoc.idr:21:19-23:

8+ |

9+21 | fromProofScript = proof sourceLocation

10+ | ~~~~~

411This style of tactic proof is deprecated. See %runElab for the replacement.

12+

513SourceLoc.idr:41:20-26:

14+ |

15+41 | Die : {default tactics { sourceLocation } loc : SourceLocation} -> Tm ctxt t

16+ | ~~~~~~~

617This style of tactic proof is deprecated. See %runElab for the replacement.

18+

719SourceLoc.idr:99:18-22:

20+ |

21+99 | SourceLoc.meta = proof

22+ | ~~~~~

823This style of tactic proof is deprecated. See %runElab for the replacement.

24+

925Testing using definition

1026FileLoc "SourceLoc.idr" (17, 11) (17, 16)

1127Testing using inline tactics

12−FileLoc "SourceLoc.idr" (21, 17) (21, 38)

28+FileLoc "SourceLoc.idr" (21, 19) (21, 38)

1329Testing using metavariable with later definition

14−FileLoc "SourceLoc.idr" (99, 16) (100, 16)

30+FileLoc "SourceLoc.idr" (99, 18) (100, 16)

1531-----------------------

1632Success!

1733Error at FileLoc "SourceLoc.idr" (73, 23) (73, 25)

test/syntax001/expected+12−2

@@ -1,4 +1,8 @@

1−Syntax.idr:6:7-18:When checking right hand side of foo with expected type

1+Syntax.idr:6:7-18:

2+ |

3+6 | foo = fnord "argh"

4+ | ~~~~~~~~~~~~

5+When checking right hand side of foo with expected type

26 Nat

37

48When checking an application of function Prelude.Interfaces.+:

@@ -6,7 +10,12 @@ When checking an application of function Prelude.Interfaces.+:

610 String (Type of "argh")

711 and

812 Nat (Expected type)

9−SyntaxTest.idr:5:7-18:When checking right hand side of foo with expected type

13+

14+SyntaxTest.idr:5:7-18:

15+ |

16+5 | foo = fnord "argh"

17+ | ~~~~~~~~~~~~

18+When checking right hand side of foo with expected type

1019 Nat

1120

1221When checking an application of function Prelude.Interfaces.+:

@@ -14,3 +23,4 @@ When checking an application of function Prelude.Interfaces.+:

1423 String (Type of "argh")

1524 and

1625 Nat (Expected type)

26+

test/totality001/expected+18−3

@@ -1,3 +1,18 @@

1−test010.idr:15:1-30:Main.foo is possibly not total due to: Main.MkBad

2−test010a.idr:9:1-23:main.bar is possibly not total due to: main.MkBad

3−test010b.idr:9:1-23:main.bar is possibly not total due to: main.MkBad

1+test010.idr:15:1-30:

2+ |

3+15 | foo (MkBad f i) = f (MkBad' i)

4+ | ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

5+Main.foo is possibly not total due to: Main.MkBad

6+

7+test010a.idr:9:1-23:

8+ |

9+9 | bar = MkBad (\x => 3) 3

10+ | ~~~~~~~~~~~~~~~~~~~~~~~

11+main.bar is possibly not total due to: main.MkBad

12+

13+test010b.idr:9:1-23:

14+ |

15+9 | bar = MkBad (\x => 3) 3

16+ | ~~~~~~~~~~~~~~~~~~~~~~~

17+main.bar is possibly not total due to: main.MkBad

18+

test/totality002/expected+14−1

@@ -1,5 +1,18 @@

11test017.idr:94:26-30:

2+ |

3+94 | maxCommutativeStepCase = proof {

4+ | ~~~~~

25This style of tactic proof is deprecated. See %runElab for the replacement.

6+

37test017a.idr:7:1-24:

8+ |

9+7 | vtrans [] _ = []

10+ | ~~~~~~~~~~~~~~~~~~~~~~~~

411scg.vtrans is possibly not total due to recursive path scg.vtrans --> scg.vtrans

5−test017b.idr:4:1-9:foo.foo is possibly not total due to recursive path foo.foo

12+

13+test017b.idr:4:1-9:

14+ |

15+4 | foo = foo

16+ | ~~~~~~~~~

17+foo.foo is possibly not total due to recursive path foo.foo

18+

test/totality003/expected+4

@@ -1,2 +1,6 @@

11totality003a.idr:5:1-13:

2+ |

3+5 | qsort [] = []

4+ | ~~~~~~~~~~~~~

25smaller.qsort is possibly not total due to recursive path smaller.qsort --> smaller.qsort --> smaller.qsort

6+

test/totality004/expected+10−1

@@ -1,4 +1,13 @@

11[1, 2, 2, 4, 3, 6, 4, 8, 5, 10]

22totality004a.idr:13:1-44:

3+ |

4+13 | process (Get f) (x :: xs) = process (f x) xs

5+ | ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

36Main.process is possibly not total due to recursive path Main.process --> Main.process --> Main.process

4−totality004a.idr:24:1-60:Main.main is possibly not total due to: Main.process

7+

8+totality004a.idr:24:1-60:

9+ |

10+24 | main = printLn (take 10 (process doubleInt (countStream 1)))

11+ | ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

12+Main.main is possibly not total due to: Main.process

13+

test/totality006/expected+16−2

@@ -1,4 +1,18 @@

1−totality006.idr:8:1-29:Main.prf is not total as there are missing cases

2−totality006a.idr:11:21-30:prf' (S _) (S _) Oh is a valid case

1+totality006.idr:8:1-29:

2+ |

3+8 | prf Z Z Oh impossible

4+ | ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

5+Main.prf is not total as there are missing cases

6+

7+totality006a.idr:11:21-30:

8+ |

9+11 | prf' (S _) (S _) Oh impossible

10+ | ~~~~~~~~~~

11+prf' (S _) (S _) Oh is a valid case

12+

313totality006b.idr:10:1-34:

14+ |

15+10 | blargh [] (y :: xs) so = absurd so

16+ | ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

417totality006b.blargh is not total as there are missing cases

18+

test/totality007/expected+4

@@ -1,5 +1,9 @@

11Entering directory `./src'

22Totality.idr:4:1-9:

3+ |

4+4 | foo Z = Z

5+ | ~~~~~~~~~

36Totality.foo is not total as there are missing cases

7+

48Totality.idr:4:1-9:Could not build: Totality.foo is not total as there are missing cases

59Leaving directory `./src'

test/totality008/expected+6−1

@@ -1 +1,6 @@

1−totality008.idr:7:1-14:Main.ElimT is possibly not total due to: Main.C2

1+totality008.idr:7:1-14:

2+ |

3+7 | ElimT _ C1 = 3

4+ | ~~~~~~~~~~~~~~

5+Main.ElimT is possibly not total due to: Main.C2

6+

test/totality009/expected+60−10

@@ -1,10 +1,60 @@

1−TestLambdaPossible.idr:9:25-34:Warning - TestLambdaPossible.case block in wrongPossible at TestLambdaPossible.idr:9:25-34 is not total as there are missing cases

2−TestLambdaPossible.idr:9:1-35:Warning - TestLambdaPossible.wrongPossible is possibly not total due to: TestLambdaPossible.case block in wrongPossible at TestLambdaPossible.idr:9:25-34

3−TestLambdaPossible.idr:12:25:Warning - TestLambdaPossible.case block in wrongPossible' at TestLambdaPossible.idr:12:25 is not total as there are missing cases

4−TestLambdaPossible.idr:12:1-13:40:Warning - TestLambdaPossible.wrongPossible' is possibly not total due to: TestLambdaPossible.case block in wrongPossible' at TestLambdaPossible.idr:12:25

5−TestLambdaPossible.idr:9:15-35:Warning - TestLambdaPossible.case block in wrongPossible at TestLambdaPossible.idr:9:25-34 is not total as there are missing cases

6−TestLambdaPossible.idr:9:1-35:Warning - TestLambdaPossible.wrongPossible is possibly not total due to: TestLambdaPossible.case block in wrongPossible at TestLambdaPossible.idr:9:25-34

7−TestLambdaPossible.idr:12:18-13:40:Warning - TestLambdaPossible.case block in wrongPossible' at TestLambdaPossible.idr:12:25 is not total as there are missing cases

8−TestLambdaPossible.idr:12:1-13:40:Warning - TestLambdaPossible.wrongPossible' is possibly not total due to: TestLambdaPossible.case block in wrongPossible' at TestLambdaPossible.idr:12:25

9−TestLambdaPossible2.idr:10:1-35:TestLambdaPossible.wrongPossible is possibly not total due to: TestLambdaPossible.case block in wrongPossible at TestLambdaPossible2.idr:10:25-34

10−TestLambdaPossible2.idr:14:1-15:40:TestLambdaPossible.wrongPossible' is possibly not total due to: TestLambdaPossible.case block in wrongPossible' at TestLambdaPossible2.idr:14:25

1+TestLambdaPossible.idr:9:25-34:

2+ |

3+9 | wrongPossible = (\Flase impossible)

4+ | ~~~~~~~~~~

5+Warning - TestLambdaPossible.case block in wrongPossible at TestLambdaPossible.idr:9:25-34 is not total as there are missing cases

6+

7+TestLambdaPossible.idr:9:1-35:

8+ |

9+9 | wrongPossible = (\Flase impossible)

10+ | ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

11+Warning - TestLambdaPossible.wrongPossible is possibly not total due to: TestLambdaPossible.case block in wrongPossible at TestLambdaPossible.idr:9:25-34

12+

13+TestLambdaPossible.idr:12:25:

14+ |

15+12 | wrongPossible' x = case x of

16+ | ^

17+Warning - TestLambdaPossible.case block in wrongPossible' at TestLambdaPossible.idr:12:25 is not total as there are missing cases

18+

19+TestLambdaPossible.idr:12:1-13:40:

20+ |

21+12 | wrongPossible' x = case x of

22+ | ~~~~~~~~~~~~~~~~~~~~~~~~~~~~ ...

23+Warning - TestLambdaPossible.wrongPossible' is possibly not total due to: TestLambdaPossible.case block in wrongPossible' at TestLambdaPossible.idr:12:25

24+

25+TestLambdaPossible.idr:9:17-35:

26+ |

27+9 | wrongPossible = (\Flase impossible)

28+ | ~~~~~~~~~~~~~~~~~~~

29+Warning - TestLambdaPossible.case block in wrongPossible at TestLambdaPossible.idr:9:25-34 is not total as there are missing cases

30+

31+TestLambdaPossible.idr:9:1-35:

32+ |

33+9 | wrongPossible = (\Flase impossible)

34+ | ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

35+Warning - TestLambdaPossible.wrongPossible is possibly not total due to: TestLambdaPossible.case block in wrongPossible at TestLambdaPossible.idr:9:25-34

36+

37+TestLambdaPossible.idr:12:20-13:40:

38+ |

39+12 | wrongPossible' x = case x of

40+ | ~~~~~~~~~ ...

41+Warning - TestLambdaPossible.case block in wrongPossible' at TestLambdaPossible.idr:12:25 is not total as there are missing cases

42+

43+TestLambdaPossible.idr:12:1-13:40:

44+ |

45+12 | wrongPossible' x = case x of

46+ | ~~~~~~~~~~~~~~~~~~~~~~~~~~~~ ...

47+Warning - TestLambdaPossible.wrongPossible' is possibly not total due to: TestLambdaPossible.case block in wrongPossible' at TestLambdaPossible.idr:12:25

48+

49+TestLambdaPossible2.idr:10:1-35:

50+ |

51+10 | wrongPossible = (\Flase impossible)

52+ | ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

53+TestLambdaPossible.wrongPossible is possibly not total due to: TestLambdaPossible.case block in wrongPossible at TestLambdaPossible2.idr:10:25-34

54+

55+TestLambdaPossible2.idr:14:1-15:40:

56+ |

57+14 | wrongPossible' x = case x of

58+ | ~~~~~~~~~~~~~~~~~~~~~~~~~~~~ ...

59+TestLambdaPossible.wrongPossible' is possibly not total due to: TestLambdaPossible.case block in wrongPossible' at TestLambdaPossible2.idr:14:25

60+

test/totality010/expected+12−2

@@ -1,2 +1,12 @@

1−totality010.idr:27:1-35:Main.evenNotS is not total as there are missing cases

2−totality010.idr:30:1-40:Main.bad is possibly not total due to: Main.evenNotS

1+totality010.idr:27:1-35:

2+ |

3+27 | evenNotS MkEven ZeroEven impossible

4+ | ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

5+Main.evenNotS is not total as there are missing cases

6+

7+totality010.idr:30:1-40:

8+ |

9+30 | bad = evenNotS ZeroEven $ MkBad ZeroEven

10+ | ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

11+Main.bad is possibly not total due to: Main.evenNotS

12+

test/totality011/expected+4

@@ -1,2 +1,6 @@

11totality011.lidr:22:3-57:

2+ |

3+22 | > weCanOnlyGetOlder {t'' = Z} {t = Z} _ _ _ = LTEZero

4+ | ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

25Main.weCanOnlyGetOlder is not total as there are missing cases

6+

test/totality012/expected+8

@@ -1,4 +1,12 @@

11totality012a.idr:9:1-10:27:

2+ |

3+9 | echo2 x = if (x == "quit") then PutStr "Bye!\n"

4+ | ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ ...

25Main.echo2 is possibly not total due to recursive path Main.echo2 --> Main.echo2

6+

37totality012b.idr:11:1-17:33:

8+ |

9+11 | echo = do PutStr "$ "

10+ | ~~~~~~~~~~~~~~~~~~~~~ ...

411Main.echo is possibly not total due to recursive path Main.echo

12+

test/totality013/expected+10−1

@@ -1,3 +1,12 @@

11totality013a.idr:5:3-49:

2+ |

3+5 | foo order x xs y ys _ = mtot order (x :: xs) ys

4+ | ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

25Main.foo is possibly not total due to recursive path Main.foo --> Main.mtot --> Main.mtot --> Main.mtot

3−totality013a.idr:9:3-36:Main.mtot is possibly not total due to: Main.foo

6+

7+totality013a.idr:9:3-36:

8+ |

9+9 | mtot order [] right = right

10+ | ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

11+Main.mtot is possibly not total due to: Main.foo

12+

test/totality014/expected+7−2

@@ -1,8 +1,13 @@

1−totality014.idr:1:6-9:Universe inconsistency.

1+totality014.idr:1:6-9:

2+ |

3+1 | data Con2 : Type where

4+ | ~~~~

5+Universe inconsistency.

26 Working on: ./totality014.idr.w

37 Old domain: (5,5)

48 New domain: (5,4)

59 Involved constraints:

610 ConstraintFC {uconstraint = ./totality014.idr.w < ./totality014.idr.u, ufc = totality014.idr:1:6-9}

711 ConstraintFC {uconstraint = ./totality014.idr.w < ./totality014.idr.u, ufc = totality014.idr:1:6-9}

8− ConstraintFC {uconstraint = ./totality014.idr.u <= ./totality014.idr.w, ufc = totality014.idr:6:27-29}

12+ ConstraintFC {uconstraint = ./totality014.idr.u <= ./totality014.idr.w, ufc = totality014.idr:6:29}

13+

test/totality015/expected+16−2

@@ -1,4 +1,18 @@

11totality015a.idr:52:3-53:

2+ |

3+52 | quiz (num1 :: num2 :: nums) score = quiz nums score

4+ | ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

25Main.quiz is possibly not total due to recursive path Main.quiz --> Main.quiz

3−totality015a.idr:42:3-44:36:Main.correct is possibly not total due to: Main.quiz

4−totality015a.idr:47:3-49:28:Main.wrong is possibly not total due to: Main.quiz

6+

7+totality015a.idr:42:3-44:36:

8+ |

9+42 | correct nums score

10+ | ~~~~~~~~~~~~~~~~~~ ...

11+Main.correct is possibly not total due to: Main.quiz

12+

13+totality015a.idr:47:3-49:28:

14+ |

15+47 | wrong nums ans score

16+ | ~~~~~~~~~~~~~~~~~~~~ ...

17+Main.wrong is possibly not total due to: Main.quiz

18+

test/totality016/expected+54−9

@@ -1,9 +1,54 @@

1−totality016.idr:15:1-21:Main.f1 is not total as there are missing cases

2−totality016.idr:19:1-24:Main.f2 is not total as there are missing cases

3−totality016.idr:23:1-29:Main.f3 is not total as there are missing cases

4−totality016.idr:27:1-14:Main.g1 is not total as there are missing cases

5−totality016.idr:31:1-17:Main.g2 is not total as there are missing cases

6−totality016.idr:35:1-16:Main.h1 is not total as there are missing cases

7−totality016.idr:39:1-19:Main.h2 is not total as there are missing cases

8−totality016.idr:43:1-25:Main.h3 is not total as there are missing cases

9−totality016.idr:47:1-30:Main.h4 is not total as there are missing cases

1+totality016.idr:15:1-21:

2+ |

3+15 | f1 (MkTP T1 x) = True

4+ | ~~~~~~~~~~~~~~~~~~~~~

5+Main.f1 is not total as there are missing cases

6+

7+totality016.idr:19:1-24:

8+ |

9+19 | f2 (MkTP T1 x, _) = True

10+ | ~~~~~~~~~~~~~~~~~~~~~~~~

11+Main.f2 is not total as there are missing cases

12+

13+totality016.idr:23:1-29:

14+ |

15+23 | f3 ((MkTP T1 x, _), _) = True

16+ | ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

17+Main.f3 is not total as there are missing cases

18+

19+totality016.idr:27:1-14:

20+ |

21+27 | g1 T1 x = True

22+ | ~~~~~~~~~~~~~~

23+Main.g1 is not total as there are missing cases

24+

25+totality016.idr:31:1-17:

26+ |

27+31 | g2 (T1, x) = True

28+ | ~~~~~~~~~~~~~~~~~

29+Main.g2 is not total as there are missing cases

30+

31+totality016.idr:35:1-16:

32+ |

33+35 | h1 True x = True

34+ | ~~~~~~~~~~~~~~~~

35+Main.h1 is not total as there are missing cases

36+

37+totality016.idr:39:1-19:

38+ |

39+39 | h2 (True, x) = True

40+ | ~~~~~~~~~~~~~~~~~~~

41+Main.h2 is not total as there are missing cases

42+

43+totality016.idr:43:1-25:

44+ |

45+43 | h3 (MkTP2 (T1, x)) = True

46+ | ~~~~~~~~~~~~~~~~~~~~~~~~~

47+Main.h3 is not total as there are missing cases

48+

49+totality016.idr:47:1-30:

50+ |

51+47 | h4 (MkTP2 (T1, x), _) _ = True

52+ | ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

53+Main.h4 is not total as there are missing cases

54+

test/totality017/expected+36−6

@@ -1,6 +1,36 @@

1−totality017.idr:19:1-15:Main.g1 is not total as there are missing cases

2−totality017.idr:25:1-17:Main.g2 is not total as there are missing cases

3−totality017.idr:31:1-13:Main.g3 is not total as there are missing cases

4−totality017.idr:37:1-36:Main.g4 is not total as there are missing cases

5−totality017.idr:42:1-11:Main.f' is not total as there are missing cases

6−totality017.idr:47:1-17:Main.f is not total as there are missing cases

1+totality017.idr:19:1-15:

2+ |

3+19 | g1 T1 T1 = True

4+ | ~~~~~~~~~~~~~~~

5+Main.g1 is not total as there are missing cases

6+

7+totality017.idr:25:1-17:

8+ |

9+25 | g2 T1' T1' = True

10+ | ~~~~~~~~~~~~~~~~~

11+Main.g2 is not total as there are missing cases

12+

13+totality017.idr:31:1-13:

14+ |

15+31 | g3 T1' = True

16+ | ~~~~~~~~~~~~~

17+Main.g3 is not total as there are missing cases

18+

19+totality017.idr:37:1-36:

20+ |

21+37 | g4 (MkTTPP (MkPP 0) (MkPP 0)) = True

22+ | ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

23+Main.g4 is not total as there are missing cases

24+

25+totality017.idr:42:1-11:

26+ |

27+42 | f' 0 = True

28+ | ~~~~~~~~~~~

29+Main.f' is not total as there are missing cases

30+

31+totality017.idr:47:1-17:

32+ |

33+47 | f (MkPP 0) = True

34+ | ~~~~~~~~~~~~~~~~~

35+Main.f is not total as there are missing cases

36+

test/totality018/expected+6−1

@@ -1 +1,6 @@

1−totality018.idr:12:1-10:Main.bar is not total as there are missing cases

1+totality018.idr:12:1-10:

2+ |

3+12 | bar FZ = 0

4+ | ~~~~~~~~~~

5+Main.bar is not total as there are missing cases

6+

test/totality019/expected+12−2

@@ -1,2 +1,12 @@

1−totality019.idr:8:1-36:Main.testCov is not total as there are missing cases

2−totality019.idr:12:1-42:Main.testCov' is not total as there are missing cases

1+totality019.idr:8:1-36:

2+ |

3+8 | testCov False False = ?testCov_rhs_3

4+ | ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

5+Main.testCov is not total as there are missing cases

6+

7+totality019.idr:12:1-42:

8+ |

9+12 | testCov' (False ** False) = ?testCov_rhs_3

10+ | ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

11+Main.testCov' is not total as there are missing cases

12+

test/totality020/expected+12−2

@@ -1,2 +1,12 @@

1−totality020.idr:4:14-23:bug _ _ Refl is a valid case

2−totality020.idr:7:14-23:foo a b Refl is a valid case

1+totality020.idr:4:14-23:

2+ |

3+4 | bug _ _ Refl impossible

4+ | ~~~~~~~~~~

5+bug _ _ Refl is a valid case

6+

7+totality020.idr:7:14-23:

8+ |

9+7 | foo a b Refl impossible

10+ | ~~~~~~~~~~

11+foo a b Refl is a valid case

12+

test/totality021/expected+20

@@ -1,10 +1,30 @@

11totality021.idr:8:1-67:

2+ |

3+8 | sLevelNotSLevel' (SL (Delay level)) p = sLevelNotSLevel' level Refl

4+ | ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

25Main.sLevelNotSLevel' is possibly not total due to recursive path Main.sLevelNotSLevel' --> Main.sLevelNotSLevel'

6+

37totality021.idr:12:1-66:

8+ |

9+12 | sLevelNotSLevel (SL (Delay level)) p = sLevelNotSLevel' level Refl

10+ | ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

411Main.sLevelNotSLevel is possibly not total due to: Main.sLevelNotSLevel'

12+

513totality021.idr:18:1-26:

14+ |

15+18 | v = sLevelNotSLevel l Refl

16+ | ~~~~~~~~~~~~~~~~~~~~~~~~~~

617Main.v is possibly not total due to: Main.sLevelNotSLevel

18+

719totality021a.idr:9:1-37:

20+ |

21+9 | noNonEmptyPointInt {n} Nil impossible

22+ | ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

823Main.noNonEmptyPointInt is not total as there are missing cases

24+

925totality021a.idr:12:1-31:

26+ |

27+12 | myVoid = noNonEmptyPointInt [2]

28+ | ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

1029Main.myVoid is possibly not total due to: Main.noNonEmptyPointInt

30+

test/totality022/expected+6−1

@@ -1 +1,6 @@

1−totality022.idr:7:20-29:f _ [] (RSnoc _ _) is a valid case

1+totality022.idr:7:20-29:

2+ |

3+7 | f _ [] (RSnoc _ _) impossible -- = ?wat

4+ | ~~~~~~~~~~

5+f _ [] (RSnoc _ _) is a valid case

6+

test/totality023/expected+4

@@ -1,2 +1,6 @@

11totality023.idr:9:1-10:27:

2+ |

3+9 | run (Do x f) = do r <- x

4+ | ~~~~~~~~~~~~~~~~~~~~~~~~ ...

25Main.run is possibly not total due to recursive path Main.run --> Main.run

6+

test/tutorial002/expected+12

@@ -1,6 +1,18 @@

11tutorial002.idr:41:25-29:

2+ |

3+41 | Main.natToBin_lemma_1 = proof

4+ | ~~~~~

25This style of tactic proof is deprecated. See %runElab for the replacement.

6+

37tutorial002.idr:48:18-22:

8+ |

9+48 | parity_lemma_1 = proof

10+ | ~~~~~

411This style of tactic proof is deprecated. See %runElab for the replacement.

12+

513tutorial002.idr:54:18-22:

14+ |

15+54 | parity_lemma_2 = proof {

16+ | ~~~~~

617This style of tactic proof is deprecated. See %runElab for the replacement.

18+

test/tutorial004/expected+8

@@ -1,4 +1,12 @@

11tutorial004.idr:46:14-18:

2+ |

3+46 | plusredZ_S = proof {

4+ | ~~~~~

25This style of tactic proof is deprecated. See %runElab for the replacement.

6+

37tutorial004.idr:53:14-18:

8+ |

9+53 | plusredZ_Z = proof {

10+ | ~~~~~

411This style of tactic proof is deprecated. See %runElab for the replacement.

12+

test/tutorial006/expected+9−1

@@ -1,4 +1,7 @@

11tutorial006a.idr:5:23-24:

2+ |

3+5 | vapp (x :: xs) ys = x :: vapp xs xs -- BROKEN

4+ | ~~

25When checking right hand side of vapp with expected type

36 Vect (S len + m) a

47

@@ -13,7 +16,11 @@ When checking argument xs to constructor Data.Vect.:::

1316 plus len len

1417 and

1518 plus len m

16−tutorial006b.idr:10:37-50:

19+

20+tutorial006b.idr:10:39-50:

21+ |

22+10 | parity (S (S (j + j))) | Even = Even {n=S j}

23+ | ~~~~~~~~~~~~

1724When checking right hand side of with block in Main.parity with expected type

1825 Parity (S (S (j + j)))

1926

@@ -27,3 +34,4 @@ Specifically:

2734 plus (S j) (S j)

2835 and

2936 S (S (plus j j))

37+

test/unique004/expected+58−9

@@ -1,26 +1,75 @@

1−unique001a.idr:35:14-43:50:Type mismatch between

1+unique001a.idr:35:16-43:50:

2+ |

3+35 | showStuff xs = do

4+ | ~~ ...

5+Type mismatch between

26 Int -> String

37and

48 UniqueType (Int -> String)

5−unique001a.idr:46:15-54:28:Type mismatch between

9+

10+unique001a.idr:46:17-54:28:

11+ |

12+46 | showStuff' xs = do

13+ | ~~ ...

14+Type mismatch between

615 Int -> String

716and

817 UniqueType (Int -> String)

9−unique001a.idr:57:15-62:33:Type mismatch between

18+

19+unique001a.idr:57:17-62:33:

20+ |

21+57 | showThings xs = do

22+ | ~~ ...

23+Type mismatch between

1024 UniqueType (Int -> String)

1125and

1226 Int -> String

13−unique001b.idr:18:17-42:Borrowed name xs must not be used on RHS

14−unique001c.idr:47:12-62:Unique name f is used more than once

15−unique001d.idr:4:16-18:Borrowed name x must not be used on RHS

27+

28+unique001b.idr:18:19-42:

29+ |

30+18 | showU (x :: xs) = show x ++ "," ++ free xs

31+ | ~~~~~~~~~~~~~~~~~~~~~~~~

32+Borrowed name xs must not be used on RHS

33+

34+unique001c.idr:47:14-62:

35+ |

36+47 | ndup {a} x = (\f : Int -> a => MkUPair (f 0) (f 1)) (uconst x)

37+ | ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

38+Unique name f is used more than once

39+

40+unique001d.idr:4:18:

41+ |

42+4 | steal (Read x) = x

43+ | ^

44+Borrowed name x must not be used on RHS

45+

1646unique001e.idr:4:12-40:

47+ |

48+4 | Nil : {a : UniqueType} -> BadList a

49+ | ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

1750Constructor Main.Nil has a UniqueType, but the data type does not

18−unique002.idr:17:8-20:19:Unique name xs is used more than once

19−unique002a.idr:17:8-20:19:Type mismatch between

51+

52+unique002.idr:17:10-20:19:

53+ |

54+17 | foo xs = do -- let f = \x : Int => showU xs

55+ | ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ ...

56+Unique name xs is used more than once

57+

58+unique002a.idr:17:10-20:19:

59+ |

60+17 | foo xs = do let f = \x : Int => showU xs

61+ | ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ ...

62+Type mismatch between

2063 Int -> String

2164and

2265 UniqueType (Int -> String)

23−unique003.idr:20:8-24:19:Type mismatch between

66+

67+unique003.idr:20:10-24:19:

68+ |

69+20 | foo xs = do let f = \x : Int => showU xs -- can't build this in unique context

70+ | ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ ...

71+Type mismatch between

2472 Int -> String

2573and

2674 UniqueType (Int -> String)

75+

test/universes001/expected+8−3

@@ -1,9 +1,14 @@

1−universes001.idr:7:5-21:Universe inconsistency.

1+universes001.idr:7:7-21:

2+ |

3+7 | foo = Const (Const 0)

4+ | ~~~~~~~~~~~~~~~

5+Universe inconsistency.

26 Working on: ./universes001.idr.x

37 Old domain: (5,5)

48 New domain: (5,4)

59 Involved constraints:

6− ConstraintFC {uconstraint = ./universes001.idr.x <= ./universes001.idr.z, ufc = universes001.idr:7:5-21}

10+ ConstraintFC {uconstraint = ./universes001.idr.x <= ./universes001.idr.z, ufc = universes001.idr:7:7-21}

711 ConstraintFC {uconstraint = ./universes001.idr.x < ./universes001.idr.y, ufc = universes001.idr:1:6-8}

812 ConstraintFC {uconstraint = ./universes001.idr.z < ./universes001.idr.x, ufc = universes001.idr:1:6-8}

9− ConstraintFC {uconstraint = ./universes001.idr.x <= ./universes001.idr.z, ufc = universes001.idr:7:5-21}

13+ ConstraintFC {uconstraint = ./universes001.idr.x <= ./universes001.idr.z, ufc = universes001.idr:7:7-21}

14+

test/universes002/expected+8−3

@@ -1,9 +1,14 @@

1−universes002.idr:45:9-48:Universe inconsistency.

1+universes002.idr:45:11-48:

2+ |

3+45 | russell = lemma (MkMPair (MkMPair R lemma) REFL)

4+ | ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

5+Universe inconsistency.

26 Working on: ./universes002.idr.b1

37 Old domain: (5,5)

48 New domain: (5,4)

59 Involved constraints:

6− ConstraintFC {uconstraint = ./universes002.idr.b1 <= ./universes002.idr.e7, ufc = universes002.idr:45:9-48}

10+ ConstraintFC {uconstraint = ./universes002.idr.b1 <= ./universes002.idr.e7, ufc = universes002.idr:45:11-48}

711 ConstraintFC {uconstraint = ./universes002.idr.b1 < ./universes002.idr.c1, ufc = universes002.idr:3:6-10}

8− ConstraintFC {uconstraint = ./universes002.idr.b1 <= ./universes002.idr.e7, ufc = universes002.idr:45:9-48}

12+ ConstraintFC {uconstraint = ./universes002.idr.b1 <= ./universes002.idr.e7, ufc = universes002.idr:45:11-48}

913 ConstraintFC {uconstraint = ./universes002.idr.d1 <= ./universes002.idr.b1, ufc = universes002.idr:3:6-10}

14+