83f0af1 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Display expected type of RHS in error messages

Also added %error_reverse annotations on IO so that IO related messages are more readable. This improves the error in #2672.

commit83f0af13fba5498ed4ac7c3944ff36701b6e00b6 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateSat 17 Oct 2015, 14:30 (11 years ago) parentdb07875

35 files changed+157−70

compare with master

unifiedsplit

libs/prelude/IO.idr+5 src/Idris/AbsSyntax.hs+1−1 src/Idris/Core/Binary.hs+7−6 src/Idris/Core/DeepSeq.hs+2−2 src/Idris/Core/Elaborate.hs+2−2 src/Idris/Core/ProofState.hs+1−1 src/Idris/Core/TT.hs+7−3 src/Idris/Core/Unify.hs+1−1 src/Idris/Coverage.hs+2−2 src/Idris/Delaborate.hs+8−3 src/Idris/Elab/Clause.hs+6−6 src/Idris/Elab/Data.hs+5−5 src/Idris/Elab/Instance.hs+1−1 src/Idris/Elab/Record.hs+1−1 src/Idris/Elab/Term.hs+6−6 src/Idris/Elab/Type.hs+1−1 src/Idris/IBC.hs+1−1 src/Idris/ProofSearch.hs+1−1 test/basic006/expected+4−1 test/basic009/expected+4−1 test/error003/expected+4−1 test/error004/expected+8−2 test/error005/expected+20−5 test/meta002/expected+6−2 test/proof002/expected+3−1 test/proof007/expected+3−1 test/quasiquote003/expected+4−1 test/quasiquote004/expected+3−1 test/quasiquote006/expected+9−3 test/reg007/expected+4−1 test/reg023/expected+4−1 test/reg044/expected+4−1 test/reg049/expected+4−1 test/syntax001/expected+8−2 test/tutorial006/expected+7−2

libs/prelude/IO.idr+5

@@ -36,6 +36,7 @@ record FFI where

3636||| The IO type, parameterised over the FFI that is available within

3737||| it.

3838abstract

39+%error_reverse

3940data IO' : (lang : FFI) -> Type -> Type where

4041 MkIO : (World -> PrimIO (WorldRes a)) -> IO' lang a

4142

@@ -171,9 +172,11 @@ namespace FFI_C

171172

172173 ||| A descriptor for the C FFI. See the constructors of `C_Types`

173174 ||| and `C_IntTypes` for the concrete types that are available.

175+ %error_reverse

174176 FFI_C : FFI

175177 FFI_C = MkFFI C_Types String String

176178

179+%error_reverse

177180IO : Type -> Type

178181IO = IO' FFI_C

179182

@@ -228,9 +231,11 @@ mutual

228231||| The JavaScript FFI. The strings naming functions in this API are

229232||| JavaScript code snippets, into which the arguments are substituted

230233||| for the placeholders `%0`, `%1`, etc.

234+%error_reverse

231235FFI_JS : FFI

232236FFI_JS = MkFFI JS_Types String String

233237

238+%error_reverse

234239JS_IO : Type -> Type

235240JS_IO = IO' FFI_JS

236241

src/Idris/AbsSyntax.hs+1−1

@@ -1344,7 +1344,7 @@ addUsingImpls syn n fc t

13441344 let badnames = filter (\n -> not (implicitable n) &&

13451345 n `notElem` (map iname uimpls)) ns

13461346 when (not (null badnames)) $

1347− throwError (At fc (Elaborating "type of " n

1347+ throwError (At fc (Elaborating "type of " n Nothing

13481348 (NoSuchVariable (head badnames))))

13491349 let cs = getArgnames t -- get already bound names

13501350 let addimpls = filter (\n -> iname n `notElem` cs) uimpls

src/Idris/Core/Binary.hs+7−6

@@ -145,10 +145,11 @@ instance Binary a => Binary (Err' a) where

145145 put (At fc e) = do putWord8 27

146146 put fc

147147 put e

148− put (Elaborating str n e) = do putWord8 28

149− put str

150− put n

151− put e

148+ put (Elaborating str n ty e) = do putWord8 28

149+ put str

150+ put n

151+ put ty

152+ put e

152153 put (ElaboratingArg n1 n2 ns e) = do putWord8 29

153154 put n1

154155 put n2

@@ -233,8 +234,8 @@ instance Binary a => Binary (Err' a) where

233234 26 -> fmap NoRewriting get

234235 27 -> do x <- get ; y <- get

235236 return $ At x y

236− 28 -> do x <- get ; y <- get ; z <- get

237− return $ Elaborating x y z

237+ 28 -> do w <- get; x <- get ; y <- get ; z <- get

238+ return $ Elaborating w x y z

238239 29 -> do w <- get ; x <- get ; y <- get ; z <- get

239240 return $ ElaboratingArg w x y z

240241 30 -> fmap ProviderError get

src/Idris/Core/DeepSeq.hs+2−2

@@ -149,8 +149,8 @@ instance NFData Err where

149149 rnf (ProofSearchFail x1) = rnf x1 `seq` ()

150150 rnf (NoRewriting x1) = rnf x1 `seq` ()

151151 rnf (At x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

152− rnf (Elaborating x1 x2 x3)

153− = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()

152+ rnf (Elaborating x1 x2 x3 x4)

153+ = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` ()

154154 rnf (ProviderError x1) = rnf x1 `seq` ()

155155 rnf (LoadingFailed x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

156156 rnf (ElabScriptDebug x1 x2 x3) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()

src/Idris/Core/Elaborate.hs+2−2

@@ -119,8 +119,8 @@ transformErr f elab = do s <- get

119119 rewriteErr (ProofSearchFail e) = ProofSearchFail (rewriteErr e)

120120 rewriteErr e = f e

121121

122−errAt :: String -> Name -> Elab' aux a -> Elab' aux a

123−errAt thing n = transformErr (Elaborating thing n)

122+errAt :: String -> Name -> Maybe Type -> Elab' aux a -> Elab' aux a

123+errAt thing n ty = transformErr (Elaborating thing n ty)

124124

125125

126126erun :: FC -> Elab' aux a -> Elab' aux a

src/Idris/Core/ProofState.hs+1−1

@@ -878,7 +878,7 @@ updateProv ns p = p

878878

879879updateError [] err = err

880880updateError ns (At f e) = At f (updateError ns e)

881−updateError ns (Elaborating s n e) = Elaborating s n (updateError ns e)

881+updateError ns (Elaborating s n ty e) = Elaborating s n ty (updateError ns e)

882882updateError ns (ElaboratingArg f a env e)

883883 = ElaboratingArg f a env (updateError ns e)

884884updateError ns (CantUnify b (l,lp) (r,rp) e xs sc)

src/Idris/Core/TT.hs+7−3

@@ -287,7 +287,7 @@ data Err' t

287287 | ProofSearchFail (Err' t)

288288 | NoRewriting t

289289 | At FC (Err' t)

290− | Elaborating String Name (Err' t)

290+ | Elaborating String Name (Maybe t) (Err' t)

291291 | ElaboratingArg Name Name [(Name, Name)] (Err' t)

292292 | ProviderError String

293293 | LoadingFailed String (Err' t)

@@ -360,7 +360,7 @@ instance Sized Err where

360360 size (IncompleteTerm trm) = size trm

361361 size ProgramLineComment = 1

362362 size (At fc err) = size fc + size err

363− size (Elaborating _ n err) = size err

363+ size (Elaborating _ _ _ err) = size err

364364 size (ElaboratingArg _ _ _ err) = size err

365365 size (ProviderError msg) = length msg

366366 size (LoadingFailed fn e) = 1 + length fn + size e

@@ -381,7 +381,11 @@ instance Show Err where

381381 show (At f e) = show f ++ ":" ++ show e

382382 show (ElaboratingArg f x prev e) = "Elaborating " ++ show f ++ " arg " ++

383383 show x ++ ": " ++ show e

384− show (Elaborating what n e) = "Elaborating " ++ what ++ show n ++ ":" ++ show e

384+ show (Elaborating what n ty e) = "Elaborating " ++ what ++ show n ++

385+ showType ty ++ ":" ++ show e

386+ where

387+ showType Nothing = ""

388+ showType (Just ty) = " with expected type " ++ show ty

385389 show (ProofSearchFail e) = "Proof search fail: " ++ show e

386390 show (InfiniteUnify _ _ _) = "InfiniteUnify"

387391 show (UnifyScope _ _ _ _) = "UnifyScope"

src/Idris/Core/Unify.hs+1−1

@@ -40,7 +40,7 @@ unrecoverable = any bad

4040

4141 unrec (CantUnify r _ _ _ _ _) = not r

4242 unrec (At _ e) = unrec e

43− unrec (Elaborating _ _ e) = unrec e

43+ unrec (Elaborating _ _ _ e) = unrec e

4444 unrec (ElaboratingArg _ _ _ e) = unrec e

4545 unrec _ = False

4646

src/Idris/Coverage.hs+2−2

@@ -137,7 +137,7 @@ validCoverageCase ctxt (CantUnify _ (topx, _) (topy, _) e _ _)

137137 _ -> False

138138validCoverageCase ctxt (CantConvert _ _ _) = False

139139validCoverageCase ctxt (At _ e) = validCoverageCase ctxt e

140−validCoverageCase ctxt (Elaborating _ _ e) = validCoverageCase ctxt e

140+validCoverageCase ctxt (Elaborating _ _ _ e) = validCoverageCase ctxt e

141141validCoverageCase ctxt (ElaboratingArg _ _ _ e) = validCoverageCase ctxt e

142142validCoverageCase ctxt _ = True

143143

@@ -167,7 +167,7 @@ recoverableCoverage ctxt (CantUnify r (topx, _) (topy, _) e _ _)

167167 | (Bound, Bound) <- (x, y) = True

168168 | otherwise = False -- name is different, unrecoverable

169169recoverableCoverage ctxt (At _ e) = recoverableCoverage ctxt e

170−recoverableCoverage ctxt (Elaborating _ _ e) = recoverableCoverage ctxt e

170+recoverableCoverage ctxt (Elaborating _ _ _ e) = recoverableCoverage ctxt e

171171recoverableCoverage ctxt (ElaboratingArg _ _ _ e) = recoverableCoverage ctxt e

172172recoverableCoverage _ _ = False

173173

src/Idris/Delaborate.hs+8−3

@@ -437,9 +437,14 @@ pprintErr' i (AlreadyDefined n) = annName n<+>

437437pprintErr' i (ProofSearchFail e) = pprintErr' i e

438438pprintErr' i (NoRewriting tm) = text "rewrite did not change type" <+> annTm tm (pprintTerm i (delabSugared i tm))

439439pprintErr' i (At f e) = annotate (AnnFC f) (text (show f)) <> colon <> pprintErr' i e

440−pprintErr' i (Elaborating s n e) = text "When checking" <+> text s <>

441− annName' n (showqual i n) <> colon <$>

442− pprintErr' i e

440+pprintErr' i (Elaborating s n ty e) = text "When checking" <+> text s <>

441+ annName' n (showqual i n) <>

442+ pprintTy ty <$>

443+ pprintErr' i e

444+ where pprintTy Nothing = colon

445+ pprintTy (Just ty) = text " with expected type" <>

446+ indented (annTm ty (pprintTerm i (delabSugared i ty)))

447+ <> line

443448pprintErr' i (ElaboratingArg f x _ e)

444449 | isInternal f = pprintErr' i e

445450 | isUN x =

src/Idris/Elab/Clause.hs+6−6

@@ -571,7 +571,7 @@ elabClause info opts (cnum, PClause fc fname lhs_in_as withs rhs_in_as wherebloc

571571

572572 ((ElabResult lhs' dlhs [] ctxt' newDecls highlights, probs, inj), _) <-

573573 tclift $ elaborate ctxt (idris_datatypes i) (sMN 0 "patLHS") infP initEState

574− (do res <- errAt "left hand side of " fname

574+ (do res <- errAt "left hand side of " fname Nothing

575575 (erun fc (buildTC i info ELHS opts fname (infTerm lhs)))

576576 probs <- get_probs

577577 inj <- get_inj

@@ -655,9 +655,9 @@ elabClause info opts (cnum, PClause fc fname lhs_in_as withs rhs_in_as wherebloc

655655 mapM_ setinj (nub (tcparams ++ inj))

656656 setNextName

657657 (ElabResult _ _ is ctxt' newDecls highlights) <-

658− errAt "right hand side of " fname

658+ errAt "right hand side of " fname (Just clhsty)

659659 (erun fc (build i winfo ERHS opts fname rhs))

660− errAt "right hand side of " fname

660+ errAt "right hand side of " fname (Just clhsty)

661661 (erun fc $ psolve lhs_tm)

662662 hs <- get_holes

663663 mapM_ (elabCaseHole is) hs

@@ -677,7 +677,7 @@ elabClause info opts (cnum, PClause fc fname lhs_in_as withs rhs_in_as wherebloc

677677 logLvl 4 $ "---> " ++ show rhs'

678678 when (not (null defer)) $ logLvl 1 $ "DEFERRED " ++

679679 show (map (\ (n, (_,_,t,_)) -> (n, t)) defer)

680− def' <- checkDef fc (Elaborating "deferred type of ") defer

680+ def' <- checkDef fc (\n -> Elaborating "deferred type of " n Nothing) defer

681681 let def'' = map (\(n, (i, top, t, ns)) -> (n, (i, top, t, ns, False))) def'

682682 addDeferred def''

683683 mapM_ (\(n, _) -> addIBC (IBCDef n)) def''

@@ -817,7 +817,7 @@ elabClause info opts (_, PWith fc fname lhs_in withs wval_in pn_in withblock)

817817 logLvl 2 ("LHS: " ++ show lhs)

818818 (ElabResult lhs' dlhs [] ctxt' newDecls highlights, _) <-

819819 tclift $ elaborate ctxt (idris_datatypes i) (sMN 0 "patLHS") infP initEState

820− (errAt "left hand side of with in " fname

820+ (errAt "left hand side of with in " fname Nothing

821821 (erun fc (buildTC i info ELHS opts fname (infTerm lhs))) )

822822 setContext ctxt'

823823 processTacticDecls info newDecls

@@ -842,7 +842,7 @@ elabClause info opts (_, PWith fc fname lhs_in withs wval_in pn_in withblock)

842842 mapM_ addPSname (allNamesIn lhs_in)

843843 setNextName

844844 -- TODO: may want where here - see winfo abpve

845− (ElabResult _ d is ctxt' newDecls highlights) <- errAt "with value in " fname

845+ (ElabResult _ d is ctxt' newDecls highlights) <- errAt "with value in " fname Nothing

846846 (erun fc (build i info ERHS opts fname (infTerm wval)))

847847 erun fc $ psolve lhs_tm

848848 tt <- get_term

src/Idris/Elab/Data.hs+5−5

@@ -78,7 +78,7 @@ elabData info syn doc argDocs fc opts (PDatadecl n nfc t_in dcons)

7878 UType UniqueType -> return True

7979 UType _ -> return False

8080 TType _ -> return False

81− rt -> tclift $ tfail (At fc (Elaborating "type constructor " n (Msg "Not a valid type constructor")))

81+ rt -> tclift $ tfail (At fc (Elaborating "type constructor " n Nothing (Msg "Not a valid type constructor")))

8282 cons <- mapM (elabCon cnameinfo syn n codata (getRetTy cty) ckind) dcons

8383 ttag <- getName

8484 i <- getIState

@@ -255,9 +255,9 @@ elabCon info syn tn codata expkind dkind (doc, argDocs, n, nfc, t_in, fc, forcen

255255 where

256256 tyIs con (Bind n b sc) = tyIs con sc

257257 tyIs con t | (P _ n' _, _) <- unApply t

258− = if n' /= tn then tclift $ tfail (At fc (Elaborating "constructor " con (Msg (show n' ++ " is not " ++ show tn))))

258+ = if n' /= tn then tclift $ tfail (At fc (Elaborating "constructor " con Nothing (Msg (show n' ++ " is not " ++ show tn))))

259259 else return ()

260− tyIs con t = tclift $ tfail (At fc (Elaborating "constructor " con (Msg (show t ++ " is not " ++ show tn))))

260+ tyIs con t = tclift $ tfail (At fc (Elaborating "constructor " con Nothing (Msg (show t ++ " is not " ++ show tn))))

261261

262262 mkLazy (PPi pl n nfc ty sc)

263263 = let ty' = if getTyName ty

@@ -339,12 +339,12 @@ elabCaseFun ind paramPos n ty cons info = do

339339 let eliminatorDef = PClauses emptyFC [TotalFn] elimDeclName eliminatorClauses

340340 elimLog $ "-- case function definition: " ++ (show . showDeclImp verbosePPOption) eliminatorDef

341341 State.lift $ idrisCatch (rec_elabDecl info EAll info eliminatorTyDecl)

342− (ierror . Elaborating "type declaration of " elimDeclName)

342+ (ierror . Elaborating "type declaration of " elimDeclName Nothing)

343343 -- Do not elaborate clauses if there aren't any

344344 case eliminatorClauses of

345345 [] -> State.lift $ solveDeferred elimDeclName -- Remove meta-variable for type

346346 _ -> State.lift $ idrisCatch (rec_elabDecl info EAll info eliminatorDef)

347− (ierror . Elaborating "clauses of " elimDeclName)

347+ (ierror . Elaborating "clauses of " elimDeclName Nothing)

348348 where elimLog :: String -> EliminatorState ()

349349 elimLog s = State.lift (logLvl 2 s)

350350

src/Idris/Elab/Instance.hs+1−1

@@ -181,7 +181,7 @@ elabInstance info syn doc argDocs what fc cs n nfc ps t expn ds = do

181181 ctxt <- getContext

182182 (ElabResult tyT _ _ ctxt' newDecls highlights, _) <-

183183 tclift $ elaborate ctxt (idris_datatypes i) iname (TType (UVal 0)) initEState

184− (errAt "type of " iname (erun fc (build i info ERHS [] iname ty)))

184+ (errAt "type of " iname Nothing (erun fc (build i info ERHS [] iname ty)))

185185 setContext ctxt'

186186 processTacticDecls info newDecls

187187 sendHighlighting highlights

src/Idris/Elab/Record.hs+1−1

@@ -171,7 +171,7 @@ elabRecordFunctions info rsyn fc tyn params fields dconName target

171171 ttConsTy <-

172172 case lookupTyExact dconName (tt_ctxt i) of

173173 Just as -> return as

174− Nothing -> tclift $ tfail $ At fc (Elaborating "record " tyn (InternalMsg "It seems like the constructor for this record has disappeared. :( \n This is a bug. Please report."))

174+ Nothing -> tclift $ tfail $ At fc (Elaborating "record " tyn Nothing (InternalMsg "It seems like the constructor for this record has disappeared. :( \n This is a bug. Please report."))

175175

176176 -- The arguments to the constructor

177177 let constructorArgs = getArgTys ttConsTy

src/Idris/Elab/Term.hs+6−6

@@ -309,7 +309,7 @@ elab ist info emode opts fn tm

309309 forceErr orig env (InfiniteUnify _ t _)

310310 | (P _ (UN ht) _, _) <- unApply (normalise (tt_ctxt ist) env t),

311311 ht == txt "Lazy'" = notDelay orig

312− forceErr orig env (Elaborating _ _ t) = forceErr orig env t

312+ forceErr orig env (Elaborating _ _ _ t) = forceErr orig env t

313313 forceErr orig env (ElaboratingArg _ _ _ t) = forceErr orig env t

314314 forceErr orig env (At _ t) = forceErr orig env t

315315 forceErr orig env t = False

@@ -484,7 +484,7 @@ elab ist info emode opts fn tm

484484 | otherwise = t

485485

486486 isAmbiguous (CantResolveAlts _) = delayok

487− isAmbiguous (Elaborating _ _ e) = isAmbiguous e

487+ isAmbiguous (Elaborating _ _ _ e) = isAmbiguous e

488488 isAmbiguous (ElaboratingArg _ _ _ e) = isAmbiguous e

489489 isAmbiguous (At _ e) = isAmbiguous e

490490 isAmbiguous _ = False

@@ -1662,7 +1662,7 @@ solveAuto ist fn ambigok (n, failc)

16621662 cantsolve (CantSolveGoal _ _) = True

16631663 cantsolve (InternalMsg _) = True

16641664 cantsolve (At _ e) = cantsolve e

1665− cantsolve (Elaborating _ _ e) = cantsolve e

1665+ cantsolve (Elaborating _ _ _ e) = cantsolve e

16661666 cantsolve (ElaboratingArg _ _ _ e) = cantsolve e

16671667 cantsolve _ = False

16681668

@@ -2396,9 +2396,9 @@ withErrorReflection x = idrisCatch x (\ e -> handle e >>= ierror)

23962396 handle e@(At fc err) = do logLvl 3 "Reflecting body of At"

23972397 err' <- handle err

23982398 return (At fc err')

2399− handle e@(Elaborating what n err) = do logLvl 3 "Reflecting body of Elaborating"

2400− err' <- handle err

2401− return (Elaborating what n err')

2399+ handle e@(Elaborating what n ty err) = do logLvl 3 "Reflecting body of Elaborating"

2400+ err' <- handle err

2401+ return (Elaborating what n ty err')

24022402 handle e@(ElaboratingArg f a prev err) = do logLvl 3 "Reflecting body of ElaboratingArg"

24032403 hs <- getFnHandlers f a

24042404 err' <- if null hs

src/Idris/Elab/Type.hs+1−1

@@ -69,7 +69,7 @@ buildType info syn fc opts n ty' = do

6969

7070 (ElabResult tyT' defer is ctxt' newDecls highlights, log) <-

7171 tclift $ elaborate ctxt (idris_datatypes i) n (TType (UVal 0)) initEState

72− (errAt "type of " n (erun fc (build i info ETyDecl [] n ty)))

72+ (errAt "type of " n Nothing (erun fc (build i info ETyDecl [] n ty)))

7373 setContext ctxt'

7474 processTacticDecls info newDecls

7575 sendHighlighting highlights

src/Idris/IBC.hs+1−1

@@ -40,7 +40,7 @@ import System.Directory

4040import Codec.Archive.Zip

4141

4242ibcVersion :: Word16

43−ibcVersion = 124

43+ibcVersion = 125

4444

4545data IBCFile = IBCFile { ver :: Word16,

4646 sourcefile :: FilePath,

src/Idris/ProofSearch.hs+1−1

@@ -178,7 +178,7 @@ proofSearch rec fromProver ambigok deferonfail maxDepth elab fn nroot psnames hi

178178 cantsolve (CantSolveGoal _ _) = True

179179 cantsolve (IncompleteTerm _) = True

180180 cantsolve (At _ e) = cantsolve e

181− cantsolve (Elaborating _ _ e) = cantsolve e

181+ cantsolve (Elaborating _ _ _ e) = cantsolve e

182182 cantsolve (ElaboratingArg _ _ _ e) = cantsolve e

183183 cantsolve err = False

184184

test/basic006/expected+4−1

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

1−test020a.idr:16:18:When checking right hand side of foo:

1+test020a.idr:16:18:

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

3+ List a

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

36 Type mismatch between

47 Vect n a (Type of xs)

test/basic009/expected+4−1

@@ -1,5 +1,8 @@

11MAIN-PASS

2−Faulty.idr:7:7:When checking right hand side of fault:

2+Faulty.idr:7:7:

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

4+ num = 0

36Type mismatch between

47 0 = 0 (Type of Refl)

58and

test/error003/expected+4−1

@@ -1,2 +1,5 @@

1−ErrorReflection.idr:68:5:When checking right hand side of bad:

1+ErrorReflection.idr:68:5:

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

3+ Tm [] TUnit

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

test/error004/expected+8−2

@@ -1,6 +1,12 @@

1−FunErrTest.idr:35:17:When checking right hand side of badCadr1:

1+FunErrTest.idr:35:17:

2+When checking right hand side of badCadr1 with expected type

3+ Int

25When checking argument cons2 to function FunErrTest.cadr:

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

4−FunErrTest.idr:38:17:When checking right hand side of badCadr2:

7+FunErrTest.idr:38:17:

8+When checking right hand side of badCadr2 with expected type

9+ Int

10+

511When checking argument cons2 to function FunErrTest.cadr:

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

test/error005/expected+20−5

@@ -1,21 +1,36 @@

1−error005.idr:13:1:When checking right hand side of two:

1+error005.idr:13:1:

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

3+ Fin 2

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

36 When using 2 as a literal for a Fin 2

47 2 is not strictly less than 2

5−error005.idr:16:1:When checking right hand side of hahaha:

8+error005.idr:16:1:

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

10+ Fin n

11+

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

713 When using 0 as a literal for a Fin n

814 0 is not strictly less than n

9−error005.idr:22:1:When checking right hand side of notOk:

15+error005.idr:22:1:

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

17+ Fin (plus 2 n)

18+

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

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

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

13−error005.idr:23:24:When checking right hand side of b0rken:

22+error005.idr:23:24:

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

24+ Fin 3

25+

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

1527 When using n as a literal for a Fin 3

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

1729 variable instead of a constant Integer

18−error005.idr:28:1:When checking right hand side of x:

30+error005.idr:28:1:

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

32+ Fin 4

33+

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

2035 When using 5 as a literal for a Fin 4

2136 5 is not strictly less than 4

test/meta002/expected+6−2

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

11Tacs.idr:298:15:

2−When checking right hand side of testElab3:

2+When checking right hand side of testElab3 with expected type

3+ Sigma Ty (Tm [])

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

46AgdaStyleReflection.idr:243:5:

5−When checking right hand side of baz:

7+When checking right hand side of baz with expected type

8+ (Nat, Void)

610PROOF SEARCH FAILURE is not defined.

test/proof002/expected+3−1

@@ -5,7 +5,9 @@ This style of tactic proof is deprecated. See %runElab for the replacement.

55Reflect.idr:190:15-20:

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

77test030a.idr:12:26-14:1:

8−When checking right hand side of testReflect1:

8+When checking right hand side of testReflect1 with expected type

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

10+

911When checking an application of function Reflect.getJust:

1012 Type mismatch between

1113 IsJust (Just x1) (Type of ItIsJust)

test/proof007/expected+3−1

@@ -1,4 +1,6 @@

11DefaultArgUnknownName.idr:9:6:

2−When checking right hand side of test:

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

3+ ()

35When checking argument arg to function DefaultArgUnknownName.funWithBadDefArg:

46 No such variable sadgjhsag

test/quasiquote003/expected+4−1

@@ -1,2 +1,5 @@

1−NoInfer.idr:11:5:When checking right hand side of zzz:

1+NoInfer.idr:11:5:

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

3+ TT

25No such variable k

test/quasiquote004/expected+3−1

@@ -5,5 +5,7 @@ This style of tactic proof is deprecated. See %runElab for the replacement.

55Quasiquote004.idr:50:27-32:

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

77Quasiquote004.idr:50:25:

8−When checking right hand side of Quasiquote004.getMeNat':

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

9+ String

10+

911Not a Nat goal

test/quasiquote006/expected+9−3

@@ -1,12 +1,18 @@

11quasiquote006.idr:9:3:

2−When checking right hand side of b:

2+When checking right hand side of b with expected type

3+ TTName

35Can't disambiguate name: ForeignEnv.Nil,

46 Prelude.List.Nil

57quasiquote006.idr:12:3:

6−When checking right hand side of c:

8+When checking right hand side of c with expected type

9+ TTName

10+

711No such variable alsdkjflkj

812quasiquote006.idr:15:3:

9−When checking right hand side of d:

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

14+ TTName

15+

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

1117 Prelude.List.::,

1218 Prelude.Stream.::

test/reg007/expected+4−1

@@ -1,5 +1,8 @@

11reg007.lidr:8:1:A.n is already defined

2−reg007.lidr:12:11-17:When checking right hand side of hurrah:

2+reg007.lidr:12:11-17:

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

4+ 0 = 1

36Type mismatch between

47 n = lala (Type of isSame)

58and

test/reg023/expected+4−1

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

1−reg023.idr:7:5:When checking right hand side of bad:

1+reg023.idr:7:5:

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

3+ f Nat

25Type mismatch between

36 Nat (Type of 0)

47and

test/reg044/expected+4−1

@@ -1,6 +1,9 @@

11reg044.idr:4:6-11:

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

3−reg044.idr:4:4:When checking right hand side of Main.pf:

3+reg044.idr:4:4:

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

5+ (b : Nat) -> (a : Nat) -> (S a = S b) -> a = b

47Type mismatch between

58 b = b (Type of Refl)

69and

test/reg049/expected+4−1

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

11reg049.idr:2:9:When checking constructor Main.Bogus:

22Void is not Main.Foo

3−reg049.idr:5:6:When checking right hand side of uhOh:

3+reg049.idr:5:6:

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

5+ Void

47No such variable Bogus

test/syntax001/expected+8−2

@@ -1,10 +1,16 @@

1−Syntax.idr:6:7-9:1:When checking right hand side of foo:

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

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

3+ Nat

25When checking an application of function Prelude.Classes.+:

36 Type mismatch between

47 String (Type of "argh")

58 and

69 Nat (Expected type)

7−SyntaxTest.idr:5:7-6:1:When checking right hand side of foo:

10+SyntaxTest.idr:5:7-6:1:

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

12+ Nat

13+

814When checking an application of function Prelude.Classes.+:

915 Type mismatch between

1016 String (Type of "argh")

test/tutorial006/expected+7−2

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

1−tutorial006a.idr:5:23-25:When checking right hand side of vapp:

1+tutorial006a.idr:5:23-25:

2+When checking right hand side of vapp with expected type

3+ Vect (S k + m) a

25When checking argument xs to constructor Data.Vect.:::

36 Type mismatch between

47 Vect (k + k) a (Type of vapp xs xs)

@@ -11,7 +14,9 @@ When checking argument xs to constructor Data.Vect.:::

1114 and

1215 plus k m

1316tutorial006b.idr:10:10:

14−When checking right hand side of with block in Main.parity:

17+When checking right hand side of with block in Main.parity with expected type

18+ Parity (S (S (j + j)))

19+

1520Type mismatch between

1621 Parity (plus (S j) (S j)) (Type of even)

1722and