69921ee · Idris-dev · git.iko.soy

docs/tutorial/typesfuns.rst+3−2

compare with master

unifiedsplit

@@ -137,8 +137,9 @@ Unlike Haskell, there is no restriction on whether types and function

137names must begin with a capital letter or not. Function names

138(``plus`` and ``mult`` above), data constructors (``Z``, ``S``,

139``Nil`` and ``::``) and type constructors (``Nat`` and ``List``) are

140+all part of the same namespace. By convention, however,

141+data types and constructor names typically begin with a capital letter.

140−all part of the same namespace. We can test these functions at the

142+We can test these functions at the Idris prompt:

141−Idris prompt:

142

143

143::

144::

144

145

idris.cabal+3

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

314 test/reg067/run

315 test/reg067/*.idr

316 test/reg067/expected

317+ test/reg068/run

318+ test/reg068/*.idr

319+ test/reg068/expected

317

320

318 test/basic001/run

321 test/basic001/run

319 test/basic001/*.idr

322 test/basic001/*.idr

src/Idris/Elab/Data.hs+9−4

@@ -60,7 +60,7 @@ elabData info syn doc argDocs fc opts (PLaterdecl n nfc t_in)

60 = do let codata = Codata `elem` opts

61 logElab 1 (show (fc, doc))

62 checkUndefined fc n

63− when (implicitable n) $ warnLC fc n

63+ when (implicitable (nsroot n)) $ warnLC fc n

64 (cty, _, t, inacc) <- buildType info syn fc [] n t_in

65

66 addIBC (IBCDef n)

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

71 = do let codata = Codata `elem` opts

72 logElab 1 (show fc)

73 undef <- isUndefined fc n

74− when (implicitable n) $ warnLC fc n

74+ when (implicitable (nsroot n)) $ warnLC fc n

75 (cty, ckind, t, inacc) <- buildType info syn fc [] n t_in

76 -- if n is defined already, make sure it is just a type declaration

77 -- with the same type we've just elaborated, and no constructors

@@ -231,7 +231,7 @@ elabCon :: ElabInfo -> SyntaxInfo -> Name -> Bool ->

231 Idris (Name, Type)

232elabCon info syn tn codata expkind dkind (doc, argDocs, n, nfc, t_in, fc, forcenames)

233 = do checkUndefined fc n

234− when (implicitable n) $ warnLC fc n

234+ when (implicitable (nsroot n)) $ warnLC fc n

235 logElab 2 $ show fc ++ ":Constructor " ++ show n ++ " : " ++ show t_in

236 (cty, ckind, t, inacc) <- buildType info syn fc [Constructor] n (if codata then mkLazy t_in else t_in)

237 ctxt <- getContext

@@ -261,7 +261,12 @@ elabCon info syn tn codata expkind dkind (doc, argDocs, n, nfc, t_in, fc, forcen

261 addIBC (IBCOpt n)

262 return (n, cty')

263 where

264− tyIs con (Bind n b sc) = tyIs con sc

264+ tyIs con (Bind n b sc) = tyIs con (substV (P Bound n Erased) sc)

265+ tyIs con t | (P Bound n' _, _) <- unApply t

266+ = if n' /= tn then

267+ tclift $ tfail (At fc (Elaborating "constructor " con Nothing

268+ (Msg ("Type level variable " ++ show n' ++ " is not " ++ show tn))))

269+ else return ()

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

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

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

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

267 else return ()

272 else return ()

test/mktest.pl+1−1

@@ -13,7 +13,7 @@ chdir($test);

13open(FOO,">run");

14

15print FOO "#!/usr/bin/env bash\n";

16−print FOO "${IDRIS:-idris} \$@ $test.idr -o $test\n";

16+print FOO "\${IDRIS:-idris} \$@ $test.idr -o $test\n";

17print FOO "./$test\n";print FOO "rm -f $test *.ibc\n";

18

19close(FOO);

test/reg068/expectednew file+7

@@ -0,0 +1,7 @@

1+reg068.idr:1:6:

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

3+This is likely to lead to problems!

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

5+This is likely to lead to problems!

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

7+Type level variable nat is not Main.nat

test/reg068/reg068.idrnew file+4

@@ -0,0 +1,4 @@

1+data nat : Type where --error

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

3+ su : nat -> nat

4+

test/reg068/runnew file+3

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

1+#!/usr/bin/env bash

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

3+rm -f *.ibc