Merge pull request #39 from mlabs-haskell/compiler/multiple-declaration-error

Compiler: multiple declaration error

Author: cstml

lambda-buffers-compiler/src/LambdaBuffers/Compiler/KindCheck.hs

@@ -1,3 +1,5 @@
+{-# OPTIONS_GHC -Wno-redundant-constraints #-}
+
 module LambdaBuffers.Compiler.KindCheck (
   -- * Kindchecking functions.
   check,
@@ -11,9 +13,10 @@ module LambdaBuffers.Compiler.KindCheck (
 
 import Control.Lens (view, (&), (.~), (^.))
 import Control.Monad (void)
-import Control.Monad.Freer (Eff, Members, reinterpret, run)
+import Control.Monad.Freer (Eff, Member, Members, interpret, reinterpret, run)
 import Control.Monad.Freer.Error (Error, runError, throwError)
 import Control.Monad.Freer.Reader (Reader, ask, runReader)
+import Control.Monad.Freer.State (State, evalState, get, modify)
 import Control.Monad.Freer.TH (makeEffect)
 import Data.Foldable (traverse_)
 import Data.List.NonEmpty (NonEmpty ((:|)), uncons, (<|))
@@ -36,51 +39,12 @@ import LambdaBuffers.Compiler.KindCheck.Inference qualified as I
 import LambdaBuffers.Compiler.KindCheck.Type (Type (App))
 import LambdaBuffers.Compiler.KindCheck.Variable (Variable (ForeignRef, LocalRef))
 import LambdaBuffers.Compiler.ProtoCompat (kind2ProtoKind)
-import LambdaBuffers.Compiler.ProtoCompat.Types qualified as P (
-  ClassDef,
-  CompilerError (..),
-  CompilerInput,
-  Constructor,
-  Field,
-  ForeignRef,
-  InstanceClause,
-  Kind,
-  KindCheckError (
-    InconsistentTypeError,
-    IncorrectApplicationError,
-    RecursiveKindError,
-    UnboundTermError
-  ),
-  KindRefType (KType),
-  KindType (KindArrow, KindRef),
-  LocalRef,
-  Module,
-  ModuleName,
-  Product (..),
-  Record,
-  SourceInfo (SourceInfo),
-  SourcePosition (SourcePosition),
-  Sum,
-  Tuple,
-  Ty (..),
-  TyAbs,
-  TyApp,
-  TyArg,
-  TyBody (..),
-  TyDef (TyDef),
-  TyName,
-  TyRef (..),
-  TyVar,
-  VarName (VarName),
- )
+import LambdaBuffers.Compiler.ProtoCompat.Types qualified as P
 import LambdaBuffers.Compiler.ProtoCompat.Types qualified as PT
 
 --------------------------------------------------------------------------------
 -- Types
 
--- FIXME(cstml) - We should add the following tests:
--- - double declaration of a type
-
 -- | Kind Check failure types.
 type CompilerErr = P.CompilerError
 
@@ -121,20 +85,27 @@ makeEffect ''KindCheck
 
 --------------------------------------------------------------------------------
 
-runCheck :: Eff (Check ': '[]) a -> Either CompilerErr a
+-- | The Check effect runner.
+runCheck :: Eff '[Check, Err] a -> Either CompilerErr a
 runCheck = run . runError . runKindCheck . localStrategy . moduleStrategy . globalStrategy
 
--- | Run the check - return the validated context or the failure.
+{- | Run the check - return the validated context or the failure. The main API
+ function of the library.
+-}
 check :: P.CompilerInput -> PT.CompilerOutput
 check = fmap (const PT.CompilerResult) . runCheck . kCheck
 
--- | Run the check - drop the result if it succeeds.
+-- | Run the check - drop the result if it succeeds - useful for testing.
 check_ :: P.CompilerInput -> Either CompilerErr ()
 check_ = void . runCheck . kCheck
 
 --------------------------------------------------------------------------------
 
-type Transform x y = forall effs {a}. Eff (x ': effs) a -> Eff (y ': effs) a
+{- | A transformation (in the context of the Kind Checker) is a mapping from one
+ Effect to another. All effects can fial via the `Err` effect - which is
+ essentially the Kind Check failure.
+-}
+type Transform x y = forall effs {a}. Member Err effs => Eff (x ': effs) a -> Eff (y ': effs) a
 
 -- Transformation strategies
 globalStrategy :: Transform Check GlobalCheck
@@ -146,7 +117,7 @@ globalStrategy = reinterpret $ \case
 
 moduleStrategy :: Transform GlobalCheck ModuleCheck
 moduleStrategy = reinterpret $ \case
-  CreateContext ci -> resolveCreateContext ci
+  CreateContext ci -> evalState (mempty @(M.Map Variable P.TyDef)) . resolveCreateContext $ ci
   ValidateModule cx md -> do
     traverse_ (kCTypeDefinition (module2ModuleName md) cx) (md ^. #typeDefs)
     traverse_ (kCClassInstance cx) (md ^. #instances)
@@ -159,14 +130,14 @@ localStrategy = reinterpret $ \case
   KCClassInstance _ctx _instClause -> pure () -- "FIXME(cstml)"
   KCClass _ctx _classDef -> pure () --  "FIXME(cstml)"
 
-runKindCheck :: Eff '[KindCheck] a -> Eff '[Err] a
-runKindCheck = reinterpret $ \case
+runKindCheck :: forall effs {a}. Member Err effs => Eff (KindCheck ': effs) a -> Eff effs a
+runKindCheck = interpret $ \case
   KindFromTyDef moduleName tydef -> runReader moduleName (tyDef2Type tydef)
   -- TyDefToTypes moduleName tydef -> runReader moduleName (tyDef2Types tydef)
   InferTypeKind _modName tyDef ctx ty -> either (handleErr tyDef) pure $ infer ctx ty
   CheckKindConsistency mname def ctx k -> runReader mname $ resolveKindConsistency def ctx k
   where
-    handleErr :: forall a. P.TyDef -> InferErr -> Eff '[Err] a
+    handleErr :: forall {b}. P.TyDef -> InferErr -> Eff effs b
     handleErr td = \case
       InferUnboundTermErr uA ->
         throwError . P.CompKindCheckError $ P.UnboundTermError (tyDef2TyName td) (var2VarName uA)
@@ -208,15 +179,65 @@ resolveKindConsistency tydef _ctx inferredKind = do
           throwError . P.CompKindCheckError $
             P.InconsistentTypeError n (kind2ProtoKind i) (kind2ProtoKind d)
 
-resolveCreateContext :: forall effs. P.CompilerInput -> Eff effs Context
-resolveCreateContext ci = mconcat <$> traverse module2Context (ci ^. #modules)
-
 tyDef2TyName :: P.TyDef -> P.TyName
 tyDef2TyName (P.TyDef n _ _) = n
 
-module2Context :: forall effs. P.Module -> Eff effs Context
-module2Context m = mconcat <$> traverse (tyDef2Context (moduleName2ModName (m ^. #moduleName))) (m ^. #typeDefs)
+--------------------------------------------------------------------------------
+-- Context Creation
 
+{- | Resolver function for the context creation - it fails if two identical
+ declarations are found.
+-}
+resolveCreateContext ::
+  forall effs.
+  Member (State (M.Map Variable P.TyDef)) effs =>
+  Member Err effs =>
+  P.CompilerInput ->
+  Eff effs Context
+resolveCreateContext ci = do
+  ctxs <- traverse module2Context (ci ^. #modules)
+  pure $ mconcat ctxs
+
+module2Context ::
+  forall effs.
+  Member (State (M.Map Variable P.TyDef)) effs =>
+  Member Err effs =>
+  P.Module ->
+  Eff effs Context
+module2Context m = do
+  let typeDefinitions = m ^. #typeDefs
+  ctxs <- runReader (m ^. #moduleName) $ do
+    traverse (tyDef2Context (moduleName2ModName (m ^. #moduleName))) typeDefinitions
+  pure $ mconcat ctxs
+
+-- | Creates a Context entry from one type definition.
+tyDef2Context ::
+  forall effs.
+  Member (Reader P.ModuleName) effs =>
+  Member (State (M.Map Variable P.TyDef)) effs =>
+  Member Err effs =>
+  ModName ->
+  P.TyDef ->
+  Eff effs Context
+tyDef2Context curModName tyDef = do
+  r@(v, _) <- tyDef2NameAndKind curModName tyDef
+  associateName v tyDef
+  pure $ mempty & context .~ uncurry M.singleton r
+  where
+    -- Ads the name to our map - we can use its SourceLocation in the case of a
+    -- double use. If it's already in our map - that means we've double declared it.
+    associateName :: Variable -> P.TyDef -> Eff effs ()
+    associateName v curTyDef = do
+      modName <- ask
+      maps <- get @(M.Map Variable P.TyDef)
+      case maps M.!? v of
+        Just otherTyDef ->
+          throwError . PT.CompKindCheckError $ PT.MultipleTyDefError modName [otherTyDef, curTyDef]
+        Nothing -> modify (M.insert v curTyDef)
+
+{- | Converts the Proto Module name to a local modname - dropping the
+ information.
+-}
 moduleName2ModName :: P.ModuleName -> ModName
 moduleName2ModName mName = (\p -> p ^. #name) <$> mName ^. #parts
 
@@ -227,11 +248,6 @@ tyDef2NameAndKind curModName tyDef = do
   let k = tyAbsLHS2Kind (tyDef ^. #tyAbs)
   pure (name, k)
 
-tyDef2Context :: forall effs. ModName -> P.TyDef -> Eff effs Context
-tyDef2Context curModName tyDef = do
-  r <- tyDef2NameAndKind curModName tyDef
-  pure $ mempty & context .~ uncurry M.singleton r
-
 tyAbsLHS2Kind :: P.TyAbs -> Kind
 tyAbsLHS2Kind tyAbs = foldWithArrow $ pKind2Type . (\x -> x ^. #argKind) <$> (tyAbs ^. #tyArgs)
 

lambda-buffers-compiler/src/LambdaBuffers/Compiler/ProtoCompat.hs

@@ -566,6 +566,10 @@ instance IsMessage P.KindCheckError KindCheckError where
             <$> fromProto (err ^. P.tyName)
             <*> fromProto (err ^. P.inferredKind)
             <*> fromProto (err ^. P.definedKind)
+        P.KindCheckError'MultipleTydefError err ->
+          MultipleTyDefError
+            <$> fromProto (err ^. P.moduleName)
+            <*> traverse fromProto (err ^. P.tyDefs)
       Nothing -> throwProtoError EmptyField
 
   toProto = \case
@@ -586,6 +590,10 @@ instance IsMessage P.KindCheckError KindCheckError where
         & (P.inconsistentTypeError . P.tyName) .~ toProto name
         & (P.inconsistentTypeError . P.inferredKind) .~ toProto ki
         & (P.inconsistentTypeError . P.definedKind) .~ toProto kd
+    MultipleTyDefError m ds ->
+      defMessage
+        & (P.multipleTydefError . P.moduleName) .~ toProto m
+        & (P.multipleTydefError . P.tyDefs) .~ (toProto <$> ds)
 
 instance IsMessage P.CompilerError CompilerError where
   fromProto cErr = case cErr ^. P.maybe'compilerError of

lambda-buffers-compiler/src/LambdaBuffers/Compiler/ProtoCompat/Types.hs

@@ -1,7 +1,9 @@
 {-# LANGUAGE DuplicateRecordFields #-}
 {-# OPTIONS_GHC -Wno-orphans #-}
 {-# OPTIONS_GHC -Wno-redundant-constraints #-}
-{-# OPTIONS_GHC -Wno-unused-imports #-}
+--  this is needed so the deriving via can generate Arbitrary instances for data
+--  definitions with more than 4 constructors
+{-# OPTIONS_GHC -fconstraint-solver-iterations=0 #-}
 
 module LambdaBuffers.Compiler.ProtoCompat.Types (
   ClassDef (..),
@@ -50,7 +52,7 @@ module LambdaBuffers.Compiler.ProtoCompat.Types (
 
 -- for NonEmpty
 import Control.Exception (Exception)
-import Data.List.NonEmpty (NonEmpty ((:|)))
+import Data.List.NonEmpty (NonEmpty)
 import Data.Text (Text)
 import GHC.Generics (Generic)
 import LambdaBuffers.Compiler.KindCheck.Variable as VARS (Atom, Variable)
@@ -303,18 +305,16 @@ instance Arbitrary CompilerInput where
       fn n = CompilerInput <$> resize n arbitrary
 
 data KindCheckError
-  = -- | The following term is unbound in the following type definition.
-    UnboundTermError TyName VarName
-  | -- | Failed unifying TyRef with TyRef in TyName. This is the TyDef.
-    IncorrectApplicationError TyName Kind Kind
-  | -- | Kind recurses forever - not permitted.
-    RecursiveKindError TyName
-  | -- | The following type has the wrong.
-    InconsistentTypeError TyName Kind Kind
+  = UnboundTermError TyName VarName
+  | IncorrectApplicationError TyName Kind Kind
+  | RecursiveKindError TyName
+  | InconsistentTypeError TyName Kind Kind
+  | MultipleTyDefError ModuleName [TyDef]
   deriving stock (Show, Eq, Ord, Generic)
   deriving (Arbitrary) via GenericArbitrary KindCheckError
 instance Exception KindCheckError
 
+-- | All the compiler errors.
 data CompilerError
   = CompKindCheckError KindCheckError
   | InternalError Text

lambda-buffers-compiler/test/Test/KindCheck.hs

@@ -12,9 +12,8 @@ import LambdaBuffers.Compiler.KindCheck.Type (Type (App, Var))
 import LambdaBuffers.Compiler.KindCheck.Variable (
   Variable (LocalRef),
  )
-import LambdaBuffers.Compiler.ProtoCompat.Types qualified as P (
-  CompilerInput (CompilerInput),
- )
+import LambdaBuffers.Compiler.ProtoCompat.Types qualified as P
+
 import Test.QuickCheck (
   Arbitrary (arbitrary, shrink),
   Property,
@@ -28,15 +27,38 @@ import Test.Tasty (TestTree, testGroup)
 import Test.Tasty.HUnit (assertBool, testCase, (@?=))
 import Test.Tasty.QuickCheck (testProperty)
 import Test.Utils.CompilerInput (
+  compilerInput'doubleDeclaration,
+  compilerInput'doubleDeclarationDiffMod,
   compilerInput'incoherent,
   compilerInput'maybe,
  )
+import Test.Utils.Constructors (_ModuleName)
+import Test.Utils.TyDef (tyDef'maybe)
 
 --------------------------------------------------------------------------------
 -- Top Level tests
 
 test :: TestTree
-test = testGroup "Compiler tests" [testCheck, testFolds, testRefl]
+test = testGroup "Compiler tests" [testCheck, testFolds, testRefl, testMultipleDec]
+
+--------------------------------------------------------------------------------
+-- Multiple declaration test
+
+testMultipleDec :: TestTree
+testMultipleDec = testGroup "Multiple declaration tests." [doubleDeclaration, passingDoubleDeclaration]
+
+doubleDeclaration :: TestTree
+doubleDeclaration =
+  testCase "Two declarations of Maybe within the same module are caught." $
+    check_ compilerInput'doubleDeclaration
+      @?= Left (P.CompKindCheckError (P.MultipleTyDefError moduleName [tyDef'maybe, tyDef'maybe]))
+  where
+    moduleName = _ModuleName ["Module"]
+
+passingDoubleDeclaration :: TestTree
+passingDoubleDeclaration =
+  testCase "Two declarations of Maybe within different modules are fine." $
+    check_ compilerInput'doubleDeclarationDiffMod @?= Right ()
 
 --------------------------------------------------------------------------------
 -- Module tests
@@ -78,8 +100,8 @@ kcTestOrdering =
       shuffledMods <- shuffle mods
       pure (P.CompilerInput mods, P.CompilerInput shuffledMods)
 
-    eitherFailOrPass :: forall {a} {c}. Either a c -> Either () ()
-    eitherFailOrPass = bimap (const ()) (const ())
+eitherFailOrPass :: forall {a} {c}. Either a c -> Either () ()
+eitherFailOrPass = bimap (const ()) (const ())
 
 --------------------------------------------------------------------------------
 -- Fold tests

lambda-buffers-compiler/test/Test/Utils/CompilerInput.hs

@@ -1,13 +1,29 @@
-module Test.Utils.CompilerInput (compilerInput'incoherent, compilerInput'maybe) where
+module Test.Utils.CompilerInput (compilerInput'incoherent, compilerInput'maybe, compilerInput'doubleDeclarationDiffMod, compilerInput'doubleDeclaration) where
 
-import Control.Lens ((&), (.~))
+import Control.Lens ((%~), (&), (.~))
 import LambdaBuffers.Compiler.ProtoCompat qualified as P
 import Test.Utils.Module (module'incoherent, module'maybe)
+import Test.Utils.SourceInfo (sourceInfo'empty)
+
+_CompilerInput :: [P.Module] -> P.CompilerInput
+_CompilerInput x = P.CompilerInput {P.modules = x}
 
 -- | Compiler Input containing 1 module with 1 definition - Maybe.
 compilerInput'maybe :: P.CompilerInput
-compilerInput'maybe = P.CompilerInput {P.modules = [module'maybe]}
+compilerInput'maybe = _CompilerInput [module'maybe]
 
 -- | Contains 2 definitions - 1 wrong one.
 compilerInput'incoherent :: P.CompilerInput
 compilerInput'incoherent = compilerInput'maybe & #modules .~ [module'incoherent]
+
+-- | Declares maybe twice.
+compilerInput'doubleDeclaration :: P.CompilerInput
+compilerInput'doubleDeclaration = compilerInput'maybe <> compilerInput'maybe
+
+-- | Declares maybe twice - in different modules
+compilerInput'doubleDeclarationDiffMod :: P.CompilerInput
+compilerInput'doubleDeclarationDiffMod =
+  compilerInput'maybe
+    <> _CompilerInput
+      [ module'maybe & #moduleName . #parts %~ (P.ModuleNamePart "Module" sourceInfo'empty :)
+      ]