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

libs/prelude/IO.idr+5

compare with master

unifiedsplit

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

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

37||| it.

38abstract

39+%error_reverse

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

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

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

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

41

42

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

171

172

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

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

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

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

175+ %error_reverse

174 FFI_C : FFI

176 FFI_C : FFI

175 FFI_C = MkFFI C_Types String String

177 FFI_C = MkFFI C_Types String String

176

178

179+%error_reverse

177IO : Type -> Type

180IO : Type -> Type

178IO = IO' FFI_C

181IO = IO' FFI_C

179

182

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

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

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

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

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

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

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

234+%error_reverse

231FFI_JS : FFI

235FFI_JS : FFI

232FFI_JS = MkFFI JS_Types String String

236FFI_JS = MkFFI JS_Types String String

233

237

238+%error_reverse

234JS_IO : Type -> Type

239JS_IO : Type -> Type

235JS_IO = IO' FFI_JS

240JS_IO = IO' FFI_JS

236

241

src/Idris/AbsSyntax.hs+1−1

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

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

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

1346 when (not (null badnames)) $

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

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

1348 (NoSuchVariable (head badnames))))

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

1350 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

145 put (At fc e) = do putWord8 27

146 put fc

147 put e

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

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

149− put str

149+ put str

150− put n

150+ put n

151+ put ty

151− put e

152+ put e

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

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

153 put n1

154 put n1

154 put n2

155 put n2

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

233 26 -> fmap NoRewriting get

234 26 -> fmap NoRewriting get

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

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

235 return $ At x y

236 return $ At x y

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

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

237− return $ Elaborating x y z

238+ return $ Elaborating w x y z

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

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

239 return $ ElaboratingArg w x y z

240 return $ ElaboratingArg w x y z

240 30 -> fmap ProviderError get

241 30 -> fmap ProviderError get

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

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

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

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

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

152− rnf (Elaborating x1 x2 x3)

152+ rnf (Elaborating x1 x2 x3 x4)

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

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

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

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

156 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

119 rewriteErr (ProofSearchFail e) = ProofSearchFail (rewriteErr e)

120 rewriteErr e = f e

121

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

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

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

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

124

125

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

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

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

878

879updateError [] err = err

880updateError 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)

882updateError ns (ElaboratingArg f a env e)

883 = ElaboratingArg f a env (updateError ns e)

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

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

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

287 | ProofSearchFail (Err' t)

288 | NoRewriting t

289 | At FC (Err' t)

290− | Elaborating String Name (Err' t)

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

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

292 | ProviderError String

293 | LoadingFailed String (Err' t)

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

360 size (IncompleteTerm trm) = size trm

361 size ProgramLineComment = 1

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

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

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

364 size (ElaboratingArg _ _ _ err) = size err

365 size (ProviderError msg) = length msg

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

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

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

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

383 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

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

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

386 show (InfiniteUnify _ _ _) = "InfiniteUnify"

390 show (InfiniteUnify _ _ _) = "InfiniteUnify"

387 show (UnifyScope _ _ _ _) = "UnifyScope"

391 show (UnifyScope _ _ _ _) = "UnifyScope"

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

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

40

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

42 unrec (At _ e) = unrec e

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

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

44 unrec (ElaboratingArg _ _ _ e) = unrec e

45 unrec _ = False

46

src/Idris/Coverage.hs+2−2

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

137 _ -> False

138validCoverageCase ctxt (CantConvert _ _ _) = False

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

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

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

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

142validCoverageCase ctxt _ = True

143

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

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

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

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

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

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

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

172recoverableCoverage _ _ = False

173

src/Idris/Delaborate.hs+8−3

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

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

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

439pprintErr' 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 <>

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

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

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

442+ pprintTy ty <$>

442− pprintErr' i e

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

443pprintErr' i (ElaboratingArg f x _ e)

448pprintErr' i (ElaboratingArg f x _ e)

444 | isInternal f = pprintErr' i e

449 | isInternal f = pprintErr' i e

445 | isUN x =

450 | 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

571

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

573 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

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

576 probs <- get_probs

577 inj <- get_inj

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

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

656 setNextName

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

658− errAt "right hand side of " fname

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

659 (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)

661 (erun fc $ psolve lhs_tm)

662 hs <- get_holes

663 mapM_ (elabCaseHole is) hs

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

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

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

679 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

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

682 addDeferred def''

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

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

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

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

819 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

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

822 setContext ctxt'

823 processTacticDecls info newDecls

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

842 mapM_ addPSname (allNamesIn lhs_in)

843 setNextName

844 -- 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

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

847 erun fc $ psolve lhs_tm

848 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)

78 UType UniqueType -> return True

79 UType _ -> return False

80 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")))

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

83 ttag <- getName

84 i <- getIState

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

255 where

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

257 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))))

259 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))))

261

262 mkLazy (PPi pl n nfc ty sc)

263 = let ty' = if getTyName ty

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

339 let eliminatorDef = PClauses emptyFC [TotalFn] elimDeclName eliminatorClauses

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

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

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

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

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

344 case eliminatorClauses of

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

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

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

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

348 where elimLog :: String -> EliminatorState ()

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

350

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

181 ctxt <- getContext

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

183 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)))

185 setContext ctxt'

186 processTacticDecls info newDecls

187 sendHighlighting highlights

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

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

171 ttConsTy <-

172 case lookupTyExact dconName (tt_ctxt i) of

173 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."))

175

176 -- The arguments to the constructor

177 let constructorArgs = getArgTys ttConsTy

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

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

309 forceErr orig env (InfiniteUnify _ t _)

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

311 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

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

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

315 forceErr orig env t = False

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

484 | otherwise = t

485

486 isAmbiguous (CantResolveAlts _) = delayok

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

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

488 isAmbiguous (ElaboratingArg _ _ _ e) = isAmbiguous e

489 isAmbiguous (At _ e) = isAmbiguous e

490 isAmbiguous _ = False

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

1662 cantsolve (CantSolveGoal _ _) = True

1663 cantsolve (InternalMsg _) = True

1664 cantsolve (At _ e) = cantsolve e

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

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

1666 cantsolve (ElaboratingArg _ _ _ e) = cantsolve e

1667 cantsolve _ = False

1668

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

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

2397 err' <- handle err

2398 return (At fc err')

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

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

2400− err' <- handle err

2400+ err' <- handle err

2401− return (Elaborating what n err')

2401+ return (Elaborating what n ty err')

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

2403 hs <- getFnHandlers f a

2404 err' <- if null hs

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

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

69

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

71 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)))

73 setContext ctxt'

74 processTacticDecls info newDecls

75 sendHighlighting highlights

src/Idris/IBC.hs+1−1

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

40import Codec.Archive.Zip

41

42ibcVersion :: Word16

43−ibcVersion = 124

43+ibcVersion = 125

44

45data IBCFile = IBCFile { ver :: Word16,

46 sourcefile :: FilePath,

src/Idris/ProofSearch.hs+1−1

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

178 cantsolve (CantSolveGoal _ _) = True

179 cantsolve (IncompleteTerm _) = True

180 cantsolve (At _ e) = cantsolve e

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

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

182 cantsolve (ElaboratingArg _ _ _ e) = cantsolve e

183 cantsolve err = False

184

test/basic006/expected+4−1

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

1+test020a.idr:16:18:

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

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

3+ List a

4+

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

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

3 Type mismatch between

6 Type mismatch between

4 Vect n a (Type of xs)

7 Vect n a (Type of xs)

test/basic009/expected+4−1

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

1MAIN-PASS

2+Faulty.idr:7:7:

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

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

4+ num = 0

5+

3Type mismatch between

6Type mismatch between

4 0 = 0 (Type of Refl)

7 0 = 0 (Type of Refl)

5and

8and

test/error003/expected+4−1

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

1+ErrorReflection.idr:68:5:

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

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

3+ Tm [] TUnit

4+

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

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

test/error004/expected+8−2

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

1+FunErrTest.idr:35:17:

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

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

3+ Int

4+

2When checking argument cons2 to function FunErrTest.cadr:

5When checking argument cons2 to function FunErrTest.cadr:

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

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

7+FunErrTest.idr:38:17:

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

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

9+ Int

10+

5When checking argument cons2 to function FunErrTest.cadr:

11When checking argument cons2 to function FunErrTest.cadr:

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

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

test/error005/expected+20−5

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

1+error005.idr:13:1:

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

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

3+ Fin 2

4+

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

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

3 When using 2 as a literal for a Fin 2

6 When using 2 as a literal for a Fin 2

4 2 is not strictly less than 2

7 2 is not strictly less than 2

8+error005.idr:16:1:

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

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

10+ Fin n

11+

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

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

7 When using 0 as a literal for a Fin n

13 When using 0 as a literal for a Fin n

8 0 is not strictly less than n

14 0 is not strictly less than n

15+error005.idr:22:1:

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

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

17+ Fin (plus 2 n)

18+

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

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

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

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

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

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

22+error005.idr:23:24:

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

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

24+ Fin 3

25+

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

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

15 When using n as a literal for a Fin 3

27 When using n as a literal for a Fin 3

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

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

17 variable instead of a constant Integer

29 variable instead of a constant Integer

30+error005.idr:28:1:

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

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

32+ Fin 4

33+

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

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

20 When using 5 as a literal for a Fin 4

35 When using 5 as a literal for a Fin 4

21 5 is not strictly less than 4

36 5 is not strictly less than 4

test/meta002/expected+6−2

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

1Tacs.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 [])

4+

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

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

4AgdaStyleReflection.idr:243:5:

6AgdaStyleReflection.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)

9+

6PROOF SEARCH FAILURE is not defined.

10PROOF 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.

5Reflect.idr:190:15-20:

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

7test030a.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+

9When checking an application of function Reflect.getJust:

11When checking an application of function Reflect.getJust:

10 Type mismatch between

12 Type mismatch between

11 IsJust (Just x1) (Type of ItIsJust)

13 IsJust (Just x1) (Type of ItIsJust)

test/proof007/expected+3−1

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

1DefaultArgUnknownName.idr:9:6:

2−When checking right hand side of test:

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

3+ ()

4+

3When checking argument arg to function DefaultArgUnknownName.funWithBadDefArg:

5When checking argument arg to function DefaultArgUnknownName.funWithBadDefArg:

4 No such variable sadgjhsag

6 No such variable sadgjhsag

test/quasiquote003/expected+4−1

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

1+NoInfer.idr:11:5:

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

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

3+ TT

4+

2No such variable k

5No such variable k

test/quasiquote004/expected+3−1

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

5Quasiquote004.idr:50:27-32:

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

7Quasiquote004.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+

9Not a Nat goal

11Not a Nat goal

test/quasiquote006/expected+9−3

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

1quasiquote006.idr:9:3:

2−When checking right hand side of b:

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

3+ TTName

4+

3Can't disambiguate name: ForeignEnv.Nil,

5Can't disambiguate name: ForeignEnv.Nil,

4 Prelude.List.Nil

6 Prelude.List.Nil

5quasiquote006.idr:12:3:

7quasiquote006.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+

7No such variable alsdkjflkj

11No such variable alsdkjflkj

8quasiquote006.idr:15:3:

12quasiquote006.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+

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

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

11 Prelude.List.::,

17 Prelude.List.::,

12 Prelude.Stream.::

18 Prelude.Stream.::

test/reg007/expected+4−1

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

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

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

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

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

4+ 0 = 1

5+

3Type mismatch between

6Type mismatch between

4 n = lala (Type of isSame)

7 n = lala (Type of isSame)

5and

8and

test/reg023/expected+4−1

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

1+reg023.idr:7:5:

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

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

3+ f Nat

4+

2Type mismatch between

5Type mismatch between

3 Nat (Type of 0)

6 Nat (Type of 0)

4and

7and

test/reg044/expected+4−1

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

1reg044.idr:4:6-11:

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

3+reg044.idr:4:4:

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

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

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

6+

4Type mismatch between

7Type mismatch between

5 b = b (Type of Refl)

8 b = b (Type of Refl)

6and

9and

test/reg049/expected+4−1

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

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

2Void is not Main.Foo

3+reg049.idr:5:6:

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

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

5+ Void

6+

4No such variable Bogus

7No such variable Bogus

test/syntax001/expected+8−2

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

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

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

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

3+ Nat

4+

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

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

3 Type mismatch between

6 Type mismatch between

4 String (Type of "argh")

7 String (Type of "argh")

5 and

8 and

6 Nat (Expected type)

9 Nat (Expected type)

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

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

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

12+ Nat

13+

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

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

9 Type mismatch between

15 Type mismatch between

10 String (Type of "argh")

16 String (Type of "argh")

test/tutorial006/expected+7−2

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

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

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

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

3+ Vect (S k + m) a

4+

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

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

3 Type mismatch between

6 Type mismatch between

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

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

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

11 and

14 and

12 plus k m

15 plus k m

13tutorial006b.idr:10:10:

16tutorial006b.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+

15Type mismatch between

20Type mismatch between

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

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

17and

22and