92a4d84 · Idris-dev · git.iko.soy

CHANGELOG+2

@@ -84,6 +84,8 @@ Minor language changes

8484* Dependent pairs now can be specified using a telescope-style syntax, without

8585 requirement of nesting, e.g. it is possible to now write the following:

8686 (a : Type ** n : Nat ** Vect n a)

87+* Idris will give a warning if an implicit is bound automatically, but would

88+ otherwise be a valid expressio if the name was used as a global

8789

8890External Dependencies

8991---------------------

idris.cabal+3

@@ -378,6 +378,9 @@ Extra-source-files:

378378 test/basic017/run

379379 test/basic017/*.idr

380380 test/basic017/expected

381+ test/basic018/run

382+ test/basic018/*.idr

383+ test/basic018/expected

381384

382385 test/bignum001/run

383386 test/bignum001/*.idr

src/Idris/AbsSyntax.hs+7−7

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

14711471 -- if all of args in ns, then add it

14721472 doAdd (UImplicit n ty : cs) ns t

14731473 | elem n ns

1474− = PPi (Imp [] Dynamic False Nothing) n NoFC ty (doAdd cs ns t)

1474+ = PPi (Imp [] Dynamic False Nothing False) n NoFC ty (doAdd cs ns t)

14751475 | otherwise = doAdd cs ns t

14761476

14771477 -- bind the free names which weren't in the using block

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

14791479 bindFree (n:ns) tm

14801480 | elem n (map iname uimpls) = bindFree ns tm

14811481 | otherwise

1482− = PPi (Imp [InaccessibleArg] Dynamic False Nothing) n NoFC Placeholder (bindFree ns tm)

1482+ = PPi (Imp [InaccessibleArg] Dynamic False Nothing False) n NoFC Placeholder (bindFree ns tm)

14831483

14841484 getArgnames (PPi _ n _ c sc)

14851485 = n : getArgnames sc

@@ -1502,9 +1502,9 @@ getUnboundImplicits i t tm = getImps t (collectImps tm)

15021502 getImps (Bind n (Pi _ t _) sc) imps

15031503 | Just (p, t') <- lookup n imps = argInfo n p t' : getImps sc imps

15041504 where

1505− argInfo n (Imp opt _ _ _) Placeholder

1505+ argInfo n (Imp opt _ _ _ _) Placeholder

15061506 = (True, PImp 0 True opt n Placeholder)

1507− argInfo n (Imp opt _ _ _) t'

1507+ argInfo n (Imp opt _ _ _ _) t'

15081508 = (False, PImp (getPriority i t') True opt n t')

15091509 argInfo n (Exp opt _ _) t'

15101510 = (InaccessibleArg `elem` opt,

@@ -1598,7 +1598,7 @@ implicitise auto syn ignore ist tm = -- trace ("INCOMING " ++ showImp True tm) $

15981598 = do (decls, ns) <- get

15991599 let isn = nub (implNamesIn uvars ty)

16001600 put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))

1601− imps top env (PPi (Imp l _ _ _) n _ ty sc)

1601+ imps top env (PPi (Imp l _ _ _ _) n _ ty sc)

16021602 = do let isn = nub (implNamesIn uvars ty) `dropAll` [n]

16031603 (decls , ns) <- get

16041604 put (PImp (getPriority ist ty) True l n Placeholder : decls,

@@ -1664,9 +1664,9 @@ implicitise auto syn ignore ist tm = -- trace ("INCOMING " ++ showImp True tm) $

16641664 pibind using [] sc = sc

16651665 pibind using (n:ns) sc

16661666 = case lookup n using of

1667− Just ty -> PPi (Imp [] Dynamic False (Just (Impl False True)))

1667+ Just ty -> PPi (Imp [] Dynamic False (Just (Impl False True)) False)

16681668 n NoFC ty (pibind using ns sc)

1669− Nothing -> PPi (Imp [InaccessibleArg] Dynamic False (Just (Impl False True)))

1669+ Nothing -> PPi (Imp [InaccessibleArg] Dynamic False (Just (Impl False True)) False)

16701670 n NoFC Placeholder (pibind using ns sc)

16711671

16721672-- Add implicit arguments in function calls

src/Idris/AbsSyntaxTree.hs+11−8

@@ -615,7 +615,8 @@ deriving instance NFData Static

615615data Plicity = Imp { pargopts :: [ArgOpt],

616616 pstatic :: Static,

617617 pparam :: Bool,

618− pscoped :: Maybe ImplicitInfo -- Nothing, if top level

618+ pscoped :: Maybe ImplicitInfo, -- Nothing, if top level

619+ pinsource :: Bool -- Explicitly written in source

619620 }

620621 | Exp { pargopts :: [ArgOpt],

621622 pstatic :: Static,

@@ -633,13 +634,13 @@ deriving instance NFData Plicity

633634!-}

634635

635636is_scoped :: Plicity -> Maybe ImplicitInfo

636−is_scoped (Imp _ _ _ s) = s

637+is_scoped (Imp _ _ _ s _) = s

637638is_scoped _ = Nothing

638639

639−impl = Imp [] Dynamic False (Just (Impl False True))

640+impl = Imp [] Dynamic False (Just (Impl False True)) False

640641

641−forall_imp = Imp [] Dynamic False (Just (Impl False False))

642−forall_constraint = Imp [] Dynamic False (Just (Impl True False))

642+forall_imp = Imp [] Dynamic False (Just (Impl False False)) False

643+forall_constraint = Imp [] Dynamic False (Just (Impl True False)) False

643644

644645expl = Exp [] Dynamic False

645646expl_param = Exp [] Dynamic True

@@ -784,11 +785,13 @@ data EState = EState {

784785 case_decls :: [(Name, PDecl)],

785786 delayed_elab :: [(Int, Elab' EState ())],

786787 new_tyDecls :: [RDeclInstructions],

787− highlighting :: [(FC, OutputAnnotation)]

788+ highlighting :: [(FC, OutputAnnotation)],

789+ auto_binds :: [Name], -- names bound as auto implicits

790+ implicit_warnings :: [(FC, Name)] -- Implicit warnings to report (location and global name)

788791 }

789792

790793initEState :: EState

791−initEState = EState [] [] [] []

794+initEState = EState [] [] [] [] [] []

792795

793796type ElabD a = Elab' EState a

794797

@@ -1754,7 +1757,7 @@ pprintPTerm ppo bnd docArgs infixes = prettySe (ppopt_depth ppo) startPrec bnd

17541757 case s of

17551758 Static -> text "%static" <> space

17561759 _ -> empty

1757− prettySe d p bnd (PPi (Imp l s _ fa) n _ ty sc)

1760+ prettySe d p bnd (PPi (Imp l s _ fa _) n _ ty sc)

17581761 | ppopt_impl ppo =

17591762 depth d . bracket p startPrec $

17601763 lbrace <> prettyBindingOf n True <+> colon <+> prettySe (decD d) startPrec bnd ty <> rbrace <+>

src/Idris/Core/Elaborate.hs+14−8

@@ -123,15 +123,21 @@ errAt :: String -> Name -> Maybe Type -> Elab' aux a -> Elab' aux a

123123errAt thing n ty = transformErr (Elaborating thing n ty)

124124

125125

126+erunAux :: FC -> Elab' aux a -> Elab' aux (a, aux)

127+erunAux f elab

128+ = do s <- get

129+ case runStateT elab s of

130+ OK (a, s') -> do put s'

131+ aux <- getAux

132+ return $! (a, aux)

133+ Error (ProofSearchFail (At f e))

134+ -> lift $ Error (ProofSearchFail (At f e))

135+ Error (At f e) -> lift $ Error (At f e)

136+ Error e -> lift $ Error (At f e)

137+

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

127−erun f elab = do s <- get

128− case runStateT elab s of

129− OK (a, s') -> do put s'

130− return $! a

131− Error (ProofSearchFail (At f e))

132− -> lift $ Error (ProofSearchFail (At f e))

133− Error (At f e) -> lift $ Error (At f e)

134− Error e -> lift $ Error (At f e)

139+erun f e = do (x, _) <- erunAux f e

140+ return x

135141

136142runElab :: aux -> Elab' aux a -> ProofState -> TC (a, ElabState aux)

137143runElab a e ps = runStateT e (ES (ps, a) "" Nothing)

src/Idris/DeepSeq.hs+2−2

@@ -388,8 +388,8 @@ instance NFData ArgOpt where

388388 rnf _ = ()

389389

390390instance NFData Plicity where

391− rnf (Imp x1 x2 x3 x4)

392− = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` ()

391+ rnf (Imp x1 x2 x3 x4 x5)

392+ = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` rnf x5 `seq` ()

393393 rnf (Exp x1 x2 x3)

394394 = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()

395395 rnf (Constraint x1 x2)

src/Idris/Delaborate.hs+3−3

@@ -112,14 +112,14 @@ delabTy' ist imps tm fullname mvs = de [] imps tm

112112 = PLam un n NoFC (de env [] ty) (de ((n,n):env) [] sc)

113113 de env (_ : is) (Bind n (Pi (Just impl) ty _) sc)

114114 | toplevel_imp impl -- information in 'imps' repeated

115− = PPi (Imp [] Dynamic False (Just impl)) n NoFC (de env [] ty) (de ((n,n):env) is sc)

115+ = PPi (Imp [] Dynamic False (Just impl) False) n NoFC (de env [] ty) (de ((n,n):env) is sc)

116116 de env is (Bind n (Pi (Just impl) ty _) sc)

117117 | tcinstance impl

118118 = PPi constraint n NoFC (de env [] ty) (de ((n,n):env) is sc)

119119 | otherwise

120− = PPi (Imp [] Dynamic False (Just impl)) n NoFC (de env [] ty) (de ((n,n):env) is sc)

120+ = PPi (Imp [] Dynamic False (Just impl) False) n NoFC (de env [] ty) (de ((n,n):env) is sc)

121121 de env ((PImp { argopts = opts }):is) (Bind n (Pi _ ty _) sc)

122− = PPi (Imp opts Dynamic False Nothing) n NoFC (de env [] ty) (de ((n,n):env) is sc)

122+ = PPi (Imp opts Dynamic False Nothing False) n NoFC (de env [] ty) (de ((n,n):env) is sc)

123123 de env (PConstraint _ _ _ _:is) (Bind n (Pi _ ty _) sc)

124124 = PPi constraint n NoFC (de env [] ty) (de ((n,n):env) is sc)

125125 de env (PTacImplicit _ _ _ tac _:is) (Bind n (Pi _ ty _) sc)

src/Idris/Elab/Class.hs+4−4

@@ -176,7 +176,7 @@ elabClass info syn_in doc fc constraints tn tnfc ps pDocs fds ds mcn cd

176176 logElab 2 $ "Method " ++ show n ++ " : " ++ showTmImpls t'

177177 return ( (n, (toExp (map (\(pn, _, _) -> pn) ps) Exp t')),

178178 (n, (nfc, doc, o, (toExp (map (\(pn, _, _) -> pn) ps)

179− (\ l s p -> Imp l s p Nothing) t'))),

179+ (\ l s p -> Imp l s p Nothing True) t'))),

180180 (n, (nfc, syn, o, t) ) )

181181 tdecl _ _ = ifail "Not allowed in a class declaration"

182182

@@ -250,7 +250,7 @@ elabClass info syn_in doc fc constraints tn tnfc ps pDocs fds ds mcn cd

250250 return [PTy doc [] syn fc o m mfc ty',

251251 PClauses fc [Inlinable] m [PClause fc m lhs [] rhs []]]

252252

253− getMArgs (PPi (Imp _ _ _ _) n _ ty sc) = IA n : getMArgs sc

253+ getMArgs (PPi (Imp _ _ _ _ _) n _ ty sc) = IA n : getMArgs sc

254254 getMArgs (PPi (Exp _ _ _) n _ ty sc) = EA n : getMArgs sc

255255 getMArgs (PPi (Constraint _ _) n _ ty sc) = CA : getMArgs sc

256256 getMArgs _ = []

@@ -270,7 +270,7 @@ elabClass info syn_in doc fc constraints tn tnfc ps pDocs fds ds mcn cd

270270 rhsArgs [] _ = []

271271

272272 insertConstraint :: PTerm -> [Name] -> PTerm -> PTerm

273− insertConstraint c all (PPi p@(Imp _ _ _ _) n fc ty sc)

273+ insertConstraint c all (PPi p@(Imp _ _ _ _ _) n fc ty sc)

274274 = PPi p n fc ty (insertConstraint c all sc)

275275 insertConstraint c all sc = let dictN = sMN 0 "__class"

276276 in PPi (constraint { pstatic = Static })

@@ -289,7 +289,7 @@ elabClass info syn_in doc fc constraints tn tnfc ps pDocs fds ds mcn cd

289289 addC _ _ tm = tm

290290

291291 -- make arguments explicit and don't bind class parameters

292− toExp ns e (PPi (Imp l s p _) n fc ty sc)

292+ toExp ns e (PPi (Imp l s p _ _) n fc ty sc)

293293 | n `elem` ns = toExp ns e sc

294294 | otherwise = PPi (e l s p) n fc ty (toExp ns e sc)

295295 toExp ns e (PPi p n fc ty sc) = PPi p n fc ty (toExp ns e sc)

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

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

233233 lamBind i (PPi _ n _ ty sc) sc'

234234 = PLam fc (sMN i "meth") NoFC Placeholder (lamBind (i+1) sc sc')

235235 lamBind i _ sc = sc

236− methArgs i (PPi (Imp _ _ _ _) n _ ty sc)

236+ methArgs i (PPi (Imp _ _ _ _ _) n _ ty sc)

237237 = PImp 0 True [] n (PRef fc [] (sMN i "meth")) : methArgs (i+1) sc

238238 methArgs i (PPi (Exp _ _ _) n _ ty sc)

239239 = PExp 0 [] (sMN 0 "marg") (PRef fc [] (sMN i "meth")) : methArgs (i+1) sc

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

266266 conbind [] x = x

267267

268268 coninsert :: [(Name, PTerm)] -> PTerm -> PTerm

269− coninsert cs (PPi p@(Imp _ _ _ _) n fc t sc) = PPi p n fc t (coninsert cs sc)

269+ coninsert cs (PPi p@(Imp _ _ _ _ _) n fc t sc) = PPi p n fc t (coninsert cs sc)

270270 coninsert cs sc = conbind cs sc

271271

272272 -- Reorder declarations to be in the same order as defined in the

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

@@ -441,7 +441,7 @@ in_name n = n

441441

442442-- | Creates a PArg with a given plicity, name, and term.

443443asArg :: Plicity -> Name -> PTerm -> PArg

444−asArg (Imp os _ _ _) n t = PImp 0 False os n t

444+asArg (Imp os _ _ _ _) n t = PImp 0 False os n t

445445asArg (Exp os _ _) n t = PExp 0 os n t

446446asArg (Constraint os _) n t = PConstraint 0 os n t

447447asArg (TacImp os _ s) n t = PTacImplicit 0 os n s t

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

@@ -36,7 +36,7 @@ elabRunElab info fc script' ns =

3636 tclift $ elaborate ctxt (idris_datatypes ist) (idris_name ist) (sMN 0 "toplLevelElab") elabScriptTy initEState

3737 (transformErr RunningElabScript

3838 (erun fc (do tm <- runElabAction ist fc [] script ns

39− EState is _ impls highlights <- getAux

39+ EState is _ impls highlights _ _ <- getAux

4040 ctxt <- get_context

4141 let ds = [] -- todo

4242 log <- getLog

src/Idris/Elab/Term.hs+35−16

@@ -120,7 +120,7 @@ build ist info emode opts fn tm

120120 when tydecl (do mkPat

121121 update_term liftPats

122122 update_term orderPats)

123− EState is _ impls highlights <- getAux

123+ EState is _ impls highlights _ _ <- getAux

124124 tt <- get_term

125125 ctxt <- get_context

126126 let (tm, ds) = runState (collectDeferred (Just fn) (map fst is) ctxt tt) []

@@ -165,7 +165,7 @@ buildTC ist info emode opts fn ns tm

165165 -- unification

166166 when (not (null dots)) $

167167 lift (Error (CantMatch (getInferTerm tm)))

168− EState is _ impls highlights <- getAux

168+ EState is _ impls highlights _ _ <- getAux

169169 tt <- get_term

170170 ctxt <- get_context

171171 let (tm, ds) = runState (collectDeferred (Just fn) (map fst is) ctxt tt) []

@@ -412,16 +412,6 @@ elab ist info emode opts fn tm

412412 [pimp (sUN "A") Placeholder False,

413413 pimp (sUN "B") Placeholder False,

414414 pexp l, pexp r])

415−-- _ -> try' (elab' ina (Just fc) (PApp fc (PRef fc pairCon)

416−-- [pimp (sUN "A") Placeholder False,

417−-- pimp (sUN "B") Placeholder False,

418−-- pexp l, pexp r]))

419−-- (elab' ina (Just fc) (PApp fc (PRef fc upairCon)

420−-- [pimp (sUN "A") Placeholder False,

421−-- pimp (sUN "B") Placeholder False,

422−-- pexp l, pexp r]))

423−-- True

424−

425415 elab' ina _ (PDPair fc hls p l@(PRef nfc hl n) t r)

426416 = case t of

427417 Placeholder ->

@@ -589,7 +579,9 @@ elab ist info emode opts fn tm

589579 | pattern && not reflection && not (e_qq ec) && e_nomatching ec

590580 = lift $ tfail $ Msg ("Attempting concrete match on polymorphic argument: " ++ show tm)

591581 | (pattern || intransform || (bindfree && bindable n)) && not (inparamBlock n) && not (e_qq ec)

592− = do let ina = e_inarg ec

582+ = do ty <- goal

583+ testImplicitWarning fc n ty

584+ let ina = e_inarg ec

593585 guarded = e_guarded ec

594586 inty = e_intype ec

595587 ctxt <- get_context

@@ -676,6 +668,7 @@ elab ist info emode opts fn tm

676668 highlightSource nfc (AnnBoundName n False)

677669 elab' ina fc (PPi p n nfc Placeholder sc)

678670 = do attack; arg n (is_scoped p) (sMN 0 "ty")

671+ addAutoBind p n

679672 addPSname n -- okay for proof search

680673 elabE (ina { e_inarg = True, e_intype = True }) fc sc

681674 solve

@@ -687,6 +680,7 @@ elab ist info emode opts fn tm

687680 MN _ _ -> unique_hole n

688681 _ -> return n

689682 forall n' (is_scoped p) (Var tyn)

683+ addAutoBind p n'

690684 addPSname n' -- okay for proof search

691685 focus tyn

692686 let ec' = ina { e_inarg = True, e_intype = True }

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

12071201 -- We now have an elaborated term. Reflect it and solve the

12081202 -- original goal in the original proof state, preserving highlighting

12091203 env <- get_env

1210− EState _ _ _ hs <- getAux

1204+ EState _ _ _ hs _ _ <- getAux

12111205 loadState

12121206 updateAux (\aux -> aux { highlighting = hs })

12131207

@@ -1403,8 +1397,8 @@ elab ist info emode opts fn tm

14031397 -- case block functions that don't yet exist)

14041398 fullyElaborated :: Term -> ElabD ()

14051399 fullyElaborated (P _ n _) =

1406− do EState cases _ _ _ <- getAux

1407− case lookup n cases of

1400+ do estate <- getAux

1401+ case lookup n (case_decls estate) of

14081402 Nothing -> return ()

14091403 Just _ -> lift . tfail $ ElabScriptStaging n

14101404 fullyElaborated (Bind n b body) = fullyElaborated body >> for_ b fullyElaborated

@@ -1549,6 +1543,31 @@ elab ist info emode opts fn tm

15491543 elabArgs _ _ _ _ _ _ (((arg, hole), _) : _) _ [] =

15501544 fail $ "Can't elaborate these args: " ++ show arg ++ " " ++ show hole

15511545

1546+ addAutoBind :: Plicity -> Name -> ElabD ()

1547+ addAutoBind (Imp _ _ _ _ False) n

1548+ = updateAux (\est -> est { auto_binds = n : auto_binds est })

1549+ addAutoBind _ _ = return ()

1550+

1551+ testImplicitWarning :: FC -> Name -> Type -> ElabD ()

1552+ testImplicitWarning fc n goal

1553+ | implicitable n && emode == ETyDecl

1554+ = do env <- get_env

1555+ est <- getAux

1556+ when (n `elem` auto_binds est) $

1557+ tryUnify env (lookupTyName n (tt_ctxt ist))

1558+ | otherwise = return ()

1559+ where

1560+ tryUnify env [] = return ()

1561+ tryUnify env ((nm, ty) : ts)

1562+ = do inj <- get_inj

1563+ hs <- get_holes

1564+ case unify (tt_ctxt ist) env (ty, Nothing) (goal, Nothing)

1565+ inj hs [] [] of

1566+ OK _ ->

1567+ updateAux (\est -> est { implicit_warnings =

1568+ (fc, nm) : implicit_warnings est })

1569+ _ -> tryUnify env ts

1570+

15521571-- For every alternative, look at the function at the head. Automatically resolve

15531572-- any nested alternatives where that function is also at the head

15541573

src/Idris/Elab/Type.hs+5−2

@@ -67,9 +67,12 @@ buildType info syn fc opts n ty' = do

6767 logElab 5 $ "with methods " ++ show (imp_methods syn)

6868 logElab 2 $ show n ++ " type " ++ show (using syn) ++ "\n" ++ showTmImpls ty

6969

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

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

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

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

72+ (errAt "type of " n Nothing

73+ (erunAux fc (build i info ETyDecl [] n ty)))

74+

75+ displayWarnings est

7376 setContext ctxt'

7477 processTacticDecls info newDecls

7578 sendHighlighting highlights

src/Idris/Elab/Utils.hs+9

@@ -395,3 +395,12 @@ setDetaggable n = do

395395 case lookupCtxt n opt of

396396 [oi] -> putIState ist { idris_optimisation = addDef n oi { detaggable = True } opt }

397397 _ -> putIState ist { idris_optimisation = addDef n (Optimise [] True) opt }

398+

399+displayWarnings :: EState -> Idris ()

400+displayWarnings est

401+ = mapM_ displayImpWarning (implicit_warnings est)

402+ where

403+ displayImpWarning :: (FC, Name) -> Idris ()

404+ displayImpWarning (fc, n) =

405+ iputStrLn $ show fc ++ ":WARNING: " ++ show (nsroot n) ++ " is bound as an implicit\n"

406+ ++ "\tDid you mean to refer to " ++ show n ++ "?"

src/Idris/IBC.hs+2−2

@@ -1154,7 +1154,7 @@ instance Binary Static where

11541154instance Binary Plicity where

11551155 put x

11561156 = case x of

1157− Imp x1 x2 x3 x4 ->

1157+ Imp x1 x2 x3 x4 _ ->

11581158 do putWord8 0

11591159 put x1

11601160 put x2

@@ -1181,7 +1181,7 @@ instance Binary Plicity where

11811181 x2 <- get

11821182 x3 <- get

11831183 x4 <- get

1184− return (Imp x1 x2 x3 x4)

1184+ return (Imp x1 x2 x3 x4 False)

11851185 1 -> do x1 <- get

11861186 x2 <- get

11871187 x3 <- get

src/Idris/Parser/Expr.hs+3−3

@@ -1079,10 +1079,10 @@ normalImplicit opts st syn = do

10791079 sc <- expr syn

10801080 let (im,cl)

10811081 = if implicitAllowed syn

1082− then (Imp opts st False (Just (Impl False True)),

1082+ then (Imp opts st False (Just (Impl False True)) True,

10831083 constraint)

1084− else (Imp opts st False (Just (Impl False False)),

1085− Imp opts st False (Just (Impl True False)))

1084+ else (Imp opts st False (Just (Impl False False)) True,

1085+ Imp opts st False (Just (Impl True False)) True)

10861086 return (bindList (PPi im) xt

10871087 (bindList (PPi cl) cs sc))

10881088

test/basic009/expected+2

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

11MAIN-PASS

2+Faulty.idr:6:9-12:WARNING: num is bound as an implicit

3+ Did you mean to refer to A.num?

24Faulty.idr:7:7:

35When checking right hand side of fault with expected type

46 num = 0

test/basic018/basic018.idrnew file+14

@@ -0,0 +1,14 @@

1+import Data.Vect

2+

3+thing : Nat

4+thing = 42

5+

6+foo : -- (thing : Nat) ->

7+ Vect thing elem

8+

9+bar : {thing : Nat} ->

10+ Vect thing elem

11+

12+test : thing = S 41

13+test = Refl

14+

test/basic018/expectednew file+18

@@ -0,0 +1,18 @@

1+basic018.idr:7:12-17:WARNING: thing is bound as an implicit

2+ Did you mean to refer to Main.thing?

3+basic018.idr:12:8-13:WARNING: thing is bound as an implicit

4+ Did you mean to refer to Main.thing?

5+basic018.idr:13:6:

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

7+ thing = S 41

8+

9+Type mismatch between

10+ 42 = 42 (Type of Refl)

11+and

12+ thing = 42 (Expected type)

13+

14+Specifically:

15+ Type mismatch between

16+ 42

17+ and

18+ thing

test/basic018/runnew file+3

@@ -0,0 +1,3 @@

1+#!/usr/bin/env bash

2+${IDRIS:-idris} $@ basic018.idr --check --nocolor

3+rm -f *.ibc

test/disambig002/disambig002.idr+1−1

@@ -75,7 +75,7 @@ sigmaUniqueLemma1 : {A : Type} ->

7575 (a : A) ->

7676 (p : P a) ->

7777 (ss : Vect n (DPair A P)) ->

78− Elem a (map fst ss) ->

78+ Elem a (map DPair.fst ss) ->

7979 Elem (a ** p) ss

8080

8181toVectComplete : {A : Type} ->

test/proofsearch002/Process.idr+2−2

@@ -123,10 +123,10 @@ mutual

123123 ((x : a) -> Process b iface (hs' x) hs'' (p' x) p'') ->

124124 Process b iface hs hs'' p p''

125125

126− Fork : Process () serveri [] (const []) (runningServer 1) (const doneServer) ->

126+ Fork : Process () serveri [] (const []) (runningServer 1) (const Process.doneServer) ->

127127 Process (ProcID serveri) iface hs (const hs) p (\res => (newServer res p))

128128 Work : (worker : (pid : ProcID iface) -> Worker [pid] ()) ->

129− (waiter : Process t iface hs (const hs) (runningServer 1) (const doneServer)) ->

129+ (waiter : Process t iface hs (const hs) (runningServer 1) (const Process.doneServer)) ->

130130 Process t iface hs (const hs) p (const p)

131131

132132 Request : (r : ProcID serveri) -> (x : serveri ty) ->

test/reg056/reg056.idr+1−1

@@ -6,7 +6,7 @@ postulate trap : Z = Z

66dodgy : (a, b : ()) -> a = b -> Void

77dodgy n m Refl impossible

88

9−nonk : (trap = Refl {x = Z}) -> Void

9+nonk : (Main.trap = Refl {x = Z}) -> Void

1010nonk Refl impossible

1111

1212false : Void

test/reg068/expected+2

@@ -3,5 +3,7 @@ Main.nat has a name which may be implicitly bound.

33This is likely to lead to problems!

44reg068.idr:2:6:Main.ze has a name which may be implicitly bound.

55This is likely to lead to problems!

6+reg068.idr:2:8-11:WARNING: nat is bound as an implicit

7+ Did you mean to refer to Main.nat?

68reg068.idr:2:6:When checking constructor Main.ze:

79Type level variable nat is not Main.nat