Fix warning for implicitable names

docs/tutorial/typesfuns.rst

@@ -137,8 +137,9 @@ Unlike Haskell, there is no restriction on whether types and function
 names must begin with a capital letter or not. Function names
 (``plus`` and ``mult`` above), data constructors (``Z``, ``S``,
 ``Nil`` and ``::``) and type constructors (``Nat`` and ``List``) are
-all part of the same namespace. We can test these functions at the
-Idris prompt:
+all part of the same namespace. By convention, however, 
+data types and constructor names typically begin with a capital letter.
+We can test these functions at the Idris prompt:
 
 ::
 

idris.cabal

@@ -314,6 +314,9 @@ Extra-source-files:
                        test/reg067/run
                        test/reg067/*.idr
                        test/reg067/expected
+                       test/reg068/run
+                       test/reg068/*.idr
+                       test/reg068/expected
 
                        test/basic001/run
                        test/basic001/*.idr

src/Idris/Elab/Data.hs

@@ -60,7 +60,7 @@ elabData info syn doc argDocs fc opts (PLaterdecl n nfc t_in)
     = do let codata = Codata `elem` opts
          logElab 1 (show (fc, doc))
          checkUndefined fc n
-         when (implicitable n) $ warnLC fc n
+         when (implicitable (nsroot n)) $ warnLC fc n
          (cty, _, t, inacc) <- buildType info syn fc [] n t_in
 
          addIBC (IBCDef n)
@@ -71,7 +71,7 @@ elabData info syn doc argDocs fc opts (PDatadecl n nfc t_in dcons)
     = do let codata = Codata `elem` opts
          logElab 1 (show fc)
          undef <- isUndefined fc n
-         when (implicitable n) $ warnLC fc n
+         when (implicitable (nsroot n)) $ warnLC fc n
          (cty, ckind, t, inacc) <- buildType info syn fc [] n t_in
          -- if n is defined already, make sure it is just a type declaration
          -- with the same type we've just elaborated, and no constructors
@@ -231,7 +231,7 @@ elabCon :: ElabInfo -> SyntaxInfo -> Name -> Bool ->
            Idris (Name, Type)
 elabCon info syn tn codata expkind dkind (doc, argDocs, n, nfc, t_in, fc, forcenames)
     = do checkUndefined fc n
-         when (implicitable n) $ warnLC fc n
+         when (implicitable (nsroot n)) $ warnLC fc n
          logElab 2 $ show fc ++ ":Constructor " ++ show n ++ " : " ++ show t_in
          (cty, ckind, t, inacc) <- buildType info syn fc [Constructor] n (if codata then mkLazy t_in else t_in)
          ctxt <- getContext
@@ -261,7 +261,12 @@ elabCon info syn tn codata expkind dkind (doc, argDocs, n, nfc, t_in, fc, forcen
          addIBC (IBCOpt n)
          return (n, cty')
   where
-    tyIs con (Bind n b sc) = tyIs con sc
+    tyIs con (Bind n b sc) = tyIs con (substV (P Bound n Erased) sc)
+    tyIs con t | (P Bound n' _, _) <- unApply t
+        = if n' /= tn then 
+               tclift $ tfail (At fc (Elaborating "constructor " con Nothing 
+                         (Msg ("Type level variable " ++ show n' ++ " is not " ++ show tn))))
+             else return ()
     tyIs con t | (P _ n' _, _) <- unApply t
         = if n' /= tn then tclift $ tfail (At fc (Elaborating "constructor " con Nothing (Msg (show n' ++ " is not " ++ show tn))))
              else return ()

test/mktest.pl

@@ -13,7 +13,7 @@ chdir($test);
 open(FOO,">run");
 
 print FOO "#!/usr/bin/env bash\n";
-print FOO "${IDRIS:-idris} \$@ $test.idr -o $test\n";
+print FOO "\${IDRIS:-idris} \$@ $test.idr -o $test\n";
 print FOO "./$test\n";print FOO "rm -f $test *.ibc\n";
 
 close(FOO);

test/reg068/expected

@@ -0,0 +1,7 @@
+reg068.idr:1:6:
+Main.nat has a name which may be implicitly bound.
+This is likely to lead to problems!
+reg068.idr:2:6:Main.ze has a name which may be implicitly bound.
+This is likely to lead to problems!
+reg068.idr:2:6:When checking constructor Main.ze:
+Type level variable nat is not Main.nat

test/reg068/reg068.idr

@@ -0,0 +1,4 @@
+data nat : Type where --error
+  ze : nat --hello.idr:10:6:When checking constructor Main.ze: !!V 0!! is not Main.nat
+  su : nat -> nat
+

test/reg068/run

@@ -0,0 +1,3 @@
+#!/usr/bin/env bash
+${IDRIS:-idris} $@ reg068.idr --check
+rm -f *.ibc