Forbid shadowing in more places

packages/coln-compiler/src/Coln/Frontend/Diagnostics.hs

@@ -16,6 +16,8 @@ data ParserCode
   | UnknownCommand
   | UnknownModifiers
   | UnknownMode
+  | DuplicateDefinition
+  | DuplicateField
   | ExpectedErrorNotReached
   deriving (Eq, Ord)
 
@@ -30,5 +32,7 @@ parserCodeTable =
     , (UnknownCommand, CodeMeta 5 SError Nothing)
     , (UnknownModifiers, CodeMeta 6 SError Nothing)
     , (UnknownMode, CodeMeta 7 SError Nothing)
-    , (ExpectedErrorNotReached, CodeMeta 8 SError Nothing)
+    , (DuplicateDefinition, CodeMeta 8 SError Nothing)
+    , (DuplicateField, CodeMeta 9 SError Nothing)
+    , (ExpectedErrorNotReached, CodeMeta 10 SError Nothing)
     ]

packages/coln-compiler/src/Coln/Frontend/Parser/Expr.hs

@@ -5,6 +5,7 @@
 
 module Coln.Frontend.Parser.Expr where
 
+import Control.Monad (when)
 import Data.List.NonEmpty (NonEmpty (..))
 import FNotation (Ntn)
 import FNotation qualified as N
@@ -85,6 +86,20 @@ fieldSetting e (N.Infix (N.Ident x sp) (N.Keyword ":=" _) body) =
   Record.FieldSetting x <$> chk e body <*> pure sp
 fieldSetting e n = unexpectedNotation e n "field setting of the form `<fieldname> := <expr>`"
 
+recordFields :: ParserEnv -> (Ntn -> IO a) -> [Ntn] -> IO [a]
+recordFields e parseField = go []
+ where
+  go _ [] = pure []
+  go seen (n : rest) = do
+    field <- parseField n
+    seen' <- case n of
+      N.Infix (N.Ident x sp) _ _ -> do
+        when (x `elem` seen) $
+          failWith e sp DuplicateField ("duplicate record field" <+> dpretty x)
+        pure (x : seen)
+      _ -> pure seen
+    (field :) <$> go seen' rest
+
 ident :: ParserEnv -> Ntn -> IO Name
 ident _ (N.Ident x _) = pure x
 ident e n = unexpectedNotation e n "identifier"
@@ -152,10 +167,10 @@ expr e n = case n of
               <*> syn e "term in equality" rhs
           )
   N.Block "sig" Nothing ns _ -> do
-    t <- Record.formation <$> traverse (fieldDecl e) ns
+    t <- Record.formation <$> recordFields e (fieldDecl e) ns
     fromTypD e (N.span n) t
-  N.Block "struct" Nothing ns s ->
-    FromChk "struct expression" <$> (Record.intro s <$> traverse (fieldSetting e) ns)
+  N.Block "struct" Nothing ns s -> do
+    FromChk "struct expression" <$> Record.intro s <$> recordFields e (fieldSetting e) ns
   N.Int i _ -> pure $ fromSynN $ Builtin.intro $ LitInt i
   N.String s _ -> pure $ fromSynN $ Builtin.intro $ LitString s
   n -> unexpectedNotation e n "expression"

packages/coln-compiler/src/Coln/Frontend/Parser/Top.hs

@@ -5,6 +5,7 @@
 module Coln.Frontend.Parser.Top where
 
 import Control.Exception (try)
+import Control.Monad (when)
 import Data.Foldable (foldlM, forM_)
 import Data.Functor.Contravariant (contramap)
 import Data.List.NonEmpty (NonEmpty (..))
@@ -42,11 +43,11 @@ argBindings e n@(N.Infix n0 (N.Keyword ":" _) n1) = do
   pure (N.span n, m, xs, a)
 argBindings e n = unexpectedNotation e n "argument binding of the form `<names> : <type>`"
 
-unpackArgs :: ParserEnv -> Ntn -> IO (Name, [(Span, Mode, [AbsEntry], Typ N)])
+unpackArgs :: ParserEnv -> Ntn -> IO (Name, Span, [(Span, Mode, [AbsEntry], Typ N)])
 unpackArgs e (N.Group (xN :| argsN)) = do
   x <- ident e xN
   args <- mapM (argBindings e) argsN
-  pure (x, args)
+  pure (x, N.span xN, args)
 
 withArgs :: (V.HasEvaluation c) => [(Span, Mode, [AbsEntry], Typ N)] -> (Typ N, Chk c) -> (Typ N, Chk c)
 withArgs args base = foldr go base args
@@ -61,23 +62,23 @@ withArgs args base = foldr go base args
   introArg sp (Named name) = Function.intro sp name
   introArg sp Anonymous = Function.intro sp "_"
 
-theory :: ParserEnv -> Ntn -> IO (Name, Typ N, Chk D)
+theory :: ParserEnv -> Ntn -> IO (Name, Span, Typ N, Chk D)
 theory e n = do
   (pat_n, body_n) <- definition e n
-  (name, args) <- unpackArgs e pat_n
+  (name, nameSpan, args) <- unpackArgs e pat_n
   body <- chk e body_n
   let (ty, tm) = withArgs args (Typ $ \_ -> pure $ M.univ TheoryU, body)
-  pure $ (name, ty, tm)
+  pure (name, nameSpan, ty, tm)
 
-def :: ParserEnv -> Ntn -> IO (Name, Typ N, Chk D)
+def :: ParserEnv -> Ntn -> IO (Name, Span, Typ N, Chk D)
 def e n = do
   (head_n, body_n) <- definition e n
   (pat_n, ty_n) <- annot e head_n
-  (name, args) <- unpackArgs e pat_n
+  (name, nameSpan, args) <- unpackArgs e pat_n
   returnTyp <- typ e ty_n
   body <- chk e body_n
   let (ty, tm) = withArgs args (returnTyp, body)
-  pure (name, ty, tm)
+  pure (name, nameSpan, ty, tm)
 
 elabDefinition :: DiagnosticEnv ElaboratorCode -> Globals -> Mode -> (Name, Typ N, Chk D) -> IO (Definition Global)
 elabDefinition e g m (x, ty, tm) = do
@@ -102,36 +103,44 @@ attr e sp ntn = do
   let msg = "invalid attr" <+> dpretty ntn
   failWith e sp UnexpectedNotation msg
 
+checkDuplicateIn :: DiagnosticEnv ColnCode -> OMap Name a -> Name -> Span -> IO ()
+checkDuplicateIn e entries x sp =
+  when (x `OMap.member` entries) $
+    failWith (contramap ParserCode e) sp DuplicateDefinition ("duplicate definition of" <+> dpretty x)
+
 decl :: DiagnosticEnv ColnCode -> Globals -> Ntn -> IO Globals
 decl e g (N.MDecl ms "theory" n sp) = do
   m <- mode (contramap ParserCode e) sp ms
-  (x, t, c) <- theory (contramap ParserCode e) n
+  (x, xsp, t, c) <- theory (contramap ParserCode e) n
+  checkDuplicateIn e g.definitions x xsp
   ge <- elabDefinition (contramap ElaboratorCode e) g m (x, t, c)
   pure $ addDefinition x ge g
 decl e g (N.MDecl ms "def" n sp) = do
   m <- mode (contramap ParserCode e) sp ms
-  (x, t, c) <- def (contramap ParserCode e) n
+  (x, xsp, t, c) <- def (contramap ParserCode e) n
+  checkDuplicateIn e g.definitions x xsp
   ge <- elabDefinition (contramap ElaboratorCode e) g m (x, t, c)
   pure $ addDefinition x ge g
 decl e g (N.Block "realm" (Just head) body _) = do
-  (x, r) <- realm e g head body
+  (x, xsp, r) <- realm e g head body
+  checkDuplicateIn e g.realms x xsp
   pure $ addRealm x r g
 decl e g (N.MDecl ms "attr" n sp) = do
   x <- attr (contramap ParserCode e) sp n
   pure $ pushAttr x g
 decl e _ n = unexpectedNotation (contramap ParserCode e) n "top-level declaration"
 
-realmHead :: ParserEnv -> Ntn -> IO (Name, Ntn)
-realmHead _ (N.Infix (N.Ident x _) (N.Keyword "@" _) n) = pure (x, n)
+realmHead :: ParserEnv -> Ntn -> IO (Name, Span, Ntn)
+realmHead _ (N.Infix (N.Ident x sp) (N.Keyword "@" _) n) = pure (x, sp, n)
 realmHead e n = unexpectedNotation e n "realm head"
 
-realm :: DiagnosticEnv ColnCode -> Globals -> Ntn -> [Ntn] -> IO (Name, Realm)
+realm :: DiagnosticEnv ColnCode -> Globals -> Ntn -> [Ntn] -> IO (Name, Span, Realm)
 realm e g head def_ns = do
-  (x, theory_n) <- realmHead (contramap ParserCode e) head
+  (x, xsp, theory_n) <- realmHead (contramap ParserCode e) head
   theory_typ <- typ (contramap ParserCode e) theory_n
   theory <- theory_typ.elab (emptyElabEnv (contramap ElaboratorCode e) g Inductive)
   defs <- realmDecls e g theory.val def_ns
-  pure (x, Realm theory defs)
+  pure (x, xsp, Realm theory defs)
 
 elabRealmDefinition :: ElabEnv N -> Mode -> (Typ N, Chk D) -> IO (Definition Local)
 elabRealmDefinition e m (ty, tm) = do
@@ -146,7 +155,9 @@ elabRealmDefinition e m (ty, tm) = do
 realmDecl :: DiagnosticEnv ColnCode -> ElabEnv N -> Ntn -> IO (Name, Definition Local)
 realmDecl de e (N.MDecl ms "def" n sp) = do
   m <- mode (contramap ParserCode de) sp ms
-  (x, t, c) <- def (contramap ParserCode de) n
+  (x, xsp, t, c) <- def (contramap ParserCode de) n
+  when (x `elem` e.scope.names) $
+    failWith (contramap ParserCode de) xsp DuplicateDefinition ("duplicate definition of" <+> dpretty x)
   d <- elabRealmDefinition e m (t, c)
   pure (x, d)
 realmDecl de _ n = unexpectedNotation (contramap ParserCode de) n "realm declaration"

packages/coln-compiler/test/golden/multi-pi.coln

@@ -77,8 +77,6 @@ def eq-dep-tail-backward (F : Int -> Set) (f : (^c x : Int) -> (^c y : Int) -> (
 
 ## Bad cases:
 
-def eq-multi-2 : (x y : Int) -> Int := x => y => 19
-
 attr expected-error "E0300"
 def eq-too-few : (x : Int) -> Int := eq-multi-2
 

packages/coln-compiler/test/golden/multi-pi.output

@@ -57,6 +57,10 @@ global entry named eq-multi-2-eq
 in mode: Conjunctive
 type: (x y : Int) -> Int
 value: eq-single-2
+global entry named eq-multi-2
+in mode: Conjunctive
+type: (x y : Int) -> Int
+value: x => y => 19
 global entry named eq-single-2-eq
 in mode: Conjunctive
 type: (x : Int) -> (y : Int) -> Int
@@ -127,19 +131,15 @@ global entry named eq-dep-tail-backward
 in mode: Conjunctive
 type: (F : Int -> Set) -> (f : (x : Int) -> (y : Int) -> (z : F y) -> F x) -> (x y : Int) -> (z : F y) -> F x
 value: F => f => f
-global entry named eq-multi-2
-in mode: Conjunctive
-type: (x y : Int) -> Int
-value: x => y => 19
 
 -- messages
 
 expected error[E0300]: expected type (x : Int) -> Int, but got type (x y : Int) -> Int
-83 | def eq-too-few : (x : Int) -> Int := eq-multi-2
-83 |                                      ^^^^^^^^^^
+81 | def eq-too-few : (x : Int) -> Int := eq-multi-2
+81 |                                      ^^^^^^^^^^
 types Int and (y : Int) -> Int are not equal 
 
 expected error[E0300]: expected type (x y z : Int) -> Int, but got type (x y : Int) -> Int
-86 | def eq-too-many : (x y z : Int) -> Int := eq-multi-2
-86 |                                           ^^^^^^^^^^
+84 | def eq-too-many : (x y z : Int) -> Int := eq-multi-2
+84 |                                           ^^^^^^^^^^
 types (z : Int) -> Int and Int are not equal 

packages/coln-compiler/test/golden/shadowing.coln

@@ -0,0 +1,83 @@
+def parameter_shadowing (x : Int) (x : Int) : Int := x
+
+def lambda_shadowing (x : Int) : (^c y : Int) -> Int := x => x
+
+theory PiShadowing := (x : Int) -> (x : Int) -> Set
+
+theory FieldArgumentShadowing (x : Int) := sig
+  x : Int
+end
+
+def top : Int := 19
+
+def param_top_shadowing (top : Int) : Int := 34
+
+theory ParamTopTheory (top : Int) := sig
+end
+
+def Pair : Set := sig
+  x : Int
+  y : Int
+end
+
+realm PairRealm @ Pair
+  def root_arg (root : Int) : Int := 41
+
+  def realm_def : Int := 38
+  def def_arg (realm_def : Int) : Int := 23
+end
+
+theory Nasty := sig
+  B : Set
+  E : B -> Set
+  n : (b : B) -> (b : E b) -> Int
+end
+
+theory NastyParam (b : Int) := sig
+  E : Int -> Set
+  b : E b
+end
+
+## Forbidden examples
+
+attr expected-error "E0208"
+def Pair : Set := sig
+  x : String
+  y : String
+end
+
+attr expected-error "E0209"
+def ShadowField : Set := sig
+  x : Int
+  # TODO: the expected-error should go here
+  x : String
+end
+
+# Banish him to the
+realm ShadowRealm @ Pair
+end
+
+attr expected-error "E0208"
+realm ShadowRealm @ Pair
+end
+
+attr expected-error "E0208"
+realm ShadowRoot @ Pair
+  def root : Pair := struct
+    x := 1
+    y := 2
+  end
+end
+
+attr expected-error "E0208"
+realm ShadowRealmDefinition @ Pair
+  def thing : Pair := struct
+    x := 1
+    y := 2
+  end
+
+  def thing : Pair := struct
+    x := 3
+    y := 4
+  end
+end