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

CHANGELOG+2

compare with master

unifiedsplit

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

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

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

86 (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

87

89

88External Dependencies

90External Dependencies

89---------------------

91---------------------

idris.cabal+3

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

378 test/basic017/run

379 test/basic017/*.idr

380 test/basic017/expected

381+ test/basic018/run

382+ test/basic018/*.idr

383+ test/basic018/expected

381

384

382 test/bignum001/run

385 test/bignum001/run

383 test/bignum001/*.idr

386 test/bignum001/*.idr

src/Idris/AbsSyntax.hs+7−7

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

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

1472 doAdd (UImplicit n ty : cs) ns t

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

1475 | otherwise = doAdd cs ns t

1476

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

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

1479 bindFree (n:ns) tm

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

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

1483

1484 getArgnames (PPi _ n _ c sc)

1485 = n : getArgnames sc

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

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

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

1504 where

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

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

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

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

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

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

1509 argInfo n (Exp opt _ _) t'

1510 = (InaccessibleArg `elem` opt,

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

1598 = do (decls, ns) <- get

1599 let isn = nub (implNamesIn uvars ty)

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

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

1603 (decls , ns) <- get

1604 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) $

1664 pibind using [] sc = sc

1665 pibind using (n:ns) sc

1666 = 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)

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

1670 n NoFC Placeholder (pibind using ns sc)

1671

1672-- Add implicit arguments in function calls

src/Idris/AbsSyntaxTree.hs+11−8

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

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

616 pstatic :: Static,

617 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

619 }

620 }

620 | Exp { pargopts :: [ArgOpt],

621 | Exp { pargopts :: [ArgOpt],

621 pstatic :: Static,

622 pstatic :: Static,

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

633!-}

634!-}

634

635

635is_scoped :: Plicity -> Maybe ImplicitInfo

636is_scoped :: Plicity -> Maybe ImplicitInfo

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

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

637is_scoped _ = Nothing

638is_scoped _ = Nothing

638

639

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

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

640

641

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

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

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

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

643

644

644expl = Exp [] Dynamic False

645expl = Exp [] Dynamic False

645expl_param = Exp [] Dynamic True

646expl_param = Exp [] Dynamic True

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

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

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

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

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

786 new_tyDecls :: [RDeclInstructions],

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

788 }

791 }

789

792

790initEState :: EState

793initEState :: EState

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

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

792

795

793type ElabD a = Elab' EState a

796type ElabD a = Elab' EState a

794

797

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

1754 case s of

1757 case s of

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

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

1756 _ -> empty

1759 _ -> 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)

1758 | ppopt_impl ppo =

1761 | ppopt_impl ppo =

1759 depth d . bracket p startPrec $

1762 depth d . bracket p startPrec $

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

1763 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

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

124

125

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+

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

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

127−erun f elab = do s <- get

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

128− case runStateT elab s of

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

130− return $! a

140+ return x

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)

135

141

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

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

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

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

src/Idris/DeepSeq.hs+2−2

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

388 rnf _ = ()

389

390instance NFData Plicity where

391− rnf (Imp x1 x2 x3 x4)

391+ rnf (Imp x1 x2 x3 x4 x5)

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

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

393 rnf (Exp x1 x2 x3)

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

395 rnf (Constraint x1 x2)

src/Idris/Delaborate.hs+3−3

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

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

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

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

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

117 | tcinstance impl

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

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

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

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

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

125 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

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

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

178 (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'))),

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

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

182

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

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

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

252

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

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

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

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

256 getMArgs _ = []

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

270 rhsArgs [] _ = []

271

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

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

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

276 in PPi (constraint { pstatic = Static })

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

289 addC _ _ tm = tm

290

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

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

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

295 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

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

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

235 lamBind i _ sc = sc

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

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

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

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

239 = 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

266 conbind [] x = x

267

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

270 coninsert cs sc = conbind cs sc

271

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

441

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

443asArg :: 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

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

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

447asArg (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 =

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

37 (transformErr RunningElabScript

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

39− EState is _ impls highlights <- getAux

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

40 ctxt <- get_context

41 let ds = [] -- todo

42 log <- getLog

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

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

120 when tydecl (do mkPat

121 update_term liftPats

122 update_term orderPats)

123− EState is _ impls highlights <- getAux

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

124 tt <- get_term

125 ctxt <- get_context

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

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

165 -- unification

166 when (not (null dots)) $

167 lift (Error (CantMatch (getInferTerm tm)))

168− EState is _ impls highlights <- getAux

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

169 tt <- get_term

170 ctxt <- get_context

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

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

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

413 pimp (sUN "B") Placeholder False,

414 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−

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

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

426 = case t of

416 = case t of

427 Placeholder ->

417 Placeholder ->

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

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

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

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

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

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

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

582+ = do ty <- goal

583+ testImplicitWarning fc n ty

592− = do let ina = e_inarg ec

584+ let ina = e_inarg ec

593 guarded = e_guarded ec

585 guarded = e_guarded ec

594 inty = e_intype ec

586 inty = e_intype ec

595 ctxt <- get_context

587 ctxt <- get_context

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

676 highlightSource nfc (AnnBoundName n False)

668 highlightSource nfc (AnnBoundName n False)

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

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

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

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

671+ addAutoBind p n

679 addPSname n -- okay for proof search

672 addPSname n -- okay for proof search

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

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

681 solve

674 solve

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

687 MN _ _ -> unique_hole n

680 MN _ _ -> unique_hole n

688 _ -> return n

681 _ -> return n

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

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

683+ addAutoBind p n'

690 addPSname n' -- okay for proof search

684 addPSname n' -- okay for proof search

691 focus tyn

685 focus tyn

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

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

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

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

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

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

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

1209 env <- get_env

1203 env <- get_env

1210− EState _ _ _ hs <- getAux

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

1211 loadState

1205 loadState

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

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

1213

1207

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

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

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

1404 fullyElaborated :: Term -> ElabD ()

1398 fullyElaborated :: Term -> ElabD ()

1405 fullyElaborated (P _ n _) =

1399 fullyElaborated (P _ n _) =

1406− do EState cases _ _ _ <- getAux

1400+ do estate <- getAux

1407− case lookup n cases of

1401+ case lookup n (case_decls estate) of

1408 Nothing -> return ()

1402 Nothing -> return ()

1409 Just _ -> lift . tfail $ ElabScriptStaging n

1403 Just _ -> lift . tfail $ ElabScriptStaging n

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

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

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

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

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

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

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

1551

1545

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+

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

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

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

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

1554

1573

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

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

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

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

69

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

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

71 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

73 setContext ctxt'

76 setContext ctxt'

74 processTacticDecls info newDecls

77 processTacticDecls info newDecls

75 sendHighlighting highlights

78 sendHighlighting highlights

src/Idris/Elab/Utils.hs+9

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

395 case lookupCtxt n opt of

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

397 _ -> 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

1154instance Binary Plicity where

1155 put x

1156 = case x of

1157− Imp x1 x2 x3 x4 ->

1157+ Imp x1 x2 x3 x4 _ ->

1158 do putWord8 0

1159 put x1

1160 put x2

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

1181 x2 <- get

1182 x3 <- get

1183 x4 <- get

1184− return (Imp x1 x2 x3 x4)

1184+ return (Imp x1 x2 x3 x4 False)

1185 1 -> do x1 <- get

1186 x2 <- get

1187 x3 <- get

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

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

1079 sc <- expr syn

1080 let (im,cl)

1081 = if implicitAllowed syn

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

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

1083 constraint)

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

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

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

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

1086 return (bindList (PPi im) xt

1087 (bindList (PPi cl) cs sc))

1088

test/basic009/expected+2

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

1MAIN-PASS

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

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

2Faulty.idr:7:7:

4Faulty.idr:7:7:

3When checking right hand side of fault with expected type

5When checking right hand side of fault with expected type

4 num = 0

6 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} ->

75 (a : A) ->

76 (p : P a) ->

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

78− Elem a (map fst ss) ->

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

79 Elem (a ** p) ss

80

81toVectComplete : {A : Type} ->

test/proofsearch002/Process.idr+2−2

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

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

124 Process b iface hs hs'' p p''

125

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

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

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

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

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

131

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

test/reg056/reg056.idr+1−1

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

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

7dodgy n m Refl impossible

8

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

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

10nonk Refl impossible

11

12false : Void

test/reg068/expected+2

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

3This is likely to lead to problems!

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

5This 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?

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

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

7Type level variable nat is not Main.nat

9Type level variable nat is not Main.nat