git.iko.soy/Idris-dev
on master help sign in
Fix warning for implicitable names
commit69921ee9a8251f6d80e9c842643bb8b185e0e7f4 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateSat 13 Feb 2016, 13:27 (11 years ago) parentebed396
7 files changed+30−7
compare with master
unifiedsplit
docs/tutorial/typesfuns.rst+3−2 idris.cabal+3 src/Idris/Elab/Data.hs+9−4 test/mktest.pl+1−1 test/reg068/expected+7 test/reg068/reg068.idr+4 test/reg068/run+3
docs/tutorial/typesfuns.rst+3−2
@@ -137,8 +137,9 @@ Unlike Haskell, there is no restriction on whether types and function
137137names must begin with a capital letter or not. Function names
138138(``plus`` and ``mult`` above), data constructors (``Z``, ``S``,
139139``Nil`` and ``::``) and type constructors (``Nat`` and ``List``) are
140−all part of the same namespace. We can test these functions at the
141−Idris prompt:
140+all part of the same namespace. By convention, however,
141+data types and constructor names typically begin with a capital letter.
142+We can test these functions at the Idris prompt:
142143
143144::
144145
idris.cabal+3
@@ -314,6 +314,9 @@ Extra-source-files:
314314 test/reg067/run
315315 test/reg067/*.idr
316316 test/reg067/expected
317+ test/reg068/run
318+ test/reg068/*.idr
319+ test/reg068/expected
317320
318321 test/basic001/run
319322 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)
6060 = do let codata = Codata `elem` opts
6161 logElab 1 (show (fc, doc))
6262 checkUndefined fc n
63− when (implicitable n) $ warnLC fc n
63+ when (implicitable (nsroot n)) $ warnLC fc n
6464 (cty, _, t, inacc) <- buildType info syn fc [] n t_in
6565
6666 addIBC (IBCDef n)
@@ -71,7 +71,7 @@ elabData info syn doc argDocs fc opts (PDatadecl n nfc t_in dcons)
7171 = do let codata = Codata `elem` opts
7272 logElab 1 (show fc)
7373 undef <- isUndefined fc n
74− when (implicitable n) $ warnLC fc n
74+ when (implicitable (nsroot n)) $ warnLC fc n
7575 (cty, ckind, t, inacc) <- buildType info syn fc [] n t_in
7676 -- if n is defined already, make sure it is just a type declaration
7777 -- with the same type we've just elaborated, and no constructors
@@ -231,7 +231,7 @@ elabCon :: ElabInfo -> SyntaxInfo -> Name -> Bool ->
231231 Idris (Name, Type)
232232elabCon info syn tn codata expkind dkind (doc, argDocs, n, nfc, t_in, fc, forcenames)
233233 = do checkUndefined fc n
234− when (implicitable n) $ warnLC fc n
234+ when (implicitable (nsroot n)) $ warnLC fc n
235235 logElab 2 $ show fc ++ ":Constructor " ++ show n ++ " : " ++ show t_in
236236 (cty, ckind, t, inacc) <- buildType info syn fc [Constructor] n (if codata then mkLazy t_in else t_in)
237237 ctxt <- getContext
@@ -261,7 +261,12 @@ elabCon info syn tn codata expkind dkind (doc, argDocs, n, nfc, t_in, fc, forcen
261261 addIBC (IBCOpt n)
262262 return (n, cty')
263263 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 ()
265270 tyIs con t | (P _ n' _, _) <- unApply t
266271 = if n' /= tn then tclift $ tfail (At fc (Elaborating "constructor " con Nothing (Msg (show n' ++ " is not " ++ show tn))))
267272 else return ()
test/mktest.pl+1−1
@@ -13,7 +13,7 @@ chdir($test);
1313open(FOO,">run");
1414
1515print 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";
1717print FOO "./$test\n";print FOO "rm -f $test *.ibc\n";
1818
1919close(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