interfaces: Prevent circular and non-closed requirements. (#12073)

* interfaces: Prevent circular and non-closed reqs

Updates the haskell side to be more strict about requirements:
- requirements must be transitively closed, so if A requires B, and B requires C,
  then A requires C.
- no circular requirements allowed

The logic for circular requirements is a bit duplicated to get a better
error message.

Part of https://github.com/digital-asset/daml/issues/11978

changelog_begin
changelog_end

* Update compiler/daml-lf-tools/src/DA/Daml/LF/TypeChecker/Check.hs

Co-authored-by: Moritz Kiefer <moritz.kiefer@purelyfunctional.org>

* take a list in NotClosed error

Co-authored-by: Moritz Kiefer <moritz.kiefer@purelyfunctional.org>

compiler/daml-lf-tools/src/DA/Daml/LF/TypeChecker/Check.hs

@@ -43,6 +43,7 @@ import           Data.List.Extended
 import Data.Generics.Uniplate.Data (para)
 import qualified Data.Set as S
 import qualified Data.HashSet as HS
+import           Data.Maybe (listToMaybe)
 import qualified Data.Map.Strict as Map
 import qualified Data.NameMap as NM
 import qualified Data.IntSet as IntSet
@@ -828,18 +829,32 @@ checkDefTypeSyn DefTypeSyn{synParams,synType} = do
   where
     base = checkType synType KStar
 
+
 -- | Check that an interface definition is well defined.
 checkIface :: MonadGamma m => Module -> DefInterface -> m ()
-checkIface m DefInterface{..} = do
-  checkUnique (EDuplicateInterfaceChoiceName intName) $ NM.names intFixedChoices
-  checkUnique (EDuplicateInterfaceMethodName intName) $ NM.names intMethods
-  forM_ intRequires (inWorld . lookupInterface) -- verify that required interface exists
-  forM_ intMethods checkIfaceMethod
+checkIface m iface = do
+  let tcon = Qualified PRSelf (moduleName m) (intName iface)
 
-  let tcon = Qualified PRSelf (moduleName m) intName
-  introExprVar intParam (TCon tcon) $ do
-    forM_ intFixedChoices (checkTemplateChoice tcon)
-    checkExpr intPrecondition TBool
+  -- check requires
+  when (tcon `S.member` intRequires iface) $
+    throwWithContext (ECircularInterfaceRequires (intName iface) Nothing)
+  forM_ (intRequires iface) $ \requiredIfaceId -> do
+    requiredIface <- inWorld (lookupInterface requiredIfaceId)
+    when (tcon `S.member` intRequires requiredIface) $
+      throwWithContext (ECircularInterfaceRequires (intName iface) (Just requiredIfaceId))
+    let missing = intRequires requiredIface `S.difference` intRequires iface
+    unless (S.null missing) $ throwWithContext $
+      ENotClosedInterfaceRequires (intName iface) requiredIfaceId (S.toList missing)
+
+  -- check methods
+  checkUnique (EDuplicateInterfaceMethodName (intName iface)) $ NM.names (intMethods iface)
+  forM_ (intMethods iface) checkIfaceMethod
+
+  -- check choices
+  checkUnique (EDuplicateInterfaceChoiceName (intName iface)) $ NM.names (intFixedChoices iface)
+  introExprVar (intParam iface) (TCon tcon) $ do
+    forM_ (intFixedChoices iface) (checkTemplateChoice tcon)
+    checkExpr (intPrecondition iface) TBool
 
 checkIfaceMethod :: MonadGamma m => InterfaceMethod -> m ()
 checkIfaceMethod InterfaceMethod{ifmType} = do
@@ -910,9 +925,7 @@ checkIfaceImplementation Template{tplImplements} tplTcon TemplateImplements{..}
 
   -- check requires
   let missingRequires = S.difference intRequires (S.fromList (NM.names tplImplements))
-  case S.toList missingRequires of
-    [] -> pure ()
-    (missingInterface:_) ->
+  whenJust (listToMaybe (S.toList missingRequires)) $ \missingInterface ->
     throwWithContext (EMissingRequiredInterface tplName tpiInterface missingInterface)
 
   -- check fixed choices
@@ -922,9 +935,8 @@ checkIfaceImplementation Template{tplImplements} tplTcon TemplateImplements{..}
 
   -- check methods
   let missingMethods = HS.difference (NM.namesSet intMethods) (NM.namesSet tpiMethods)
-  case HS.toList missingMethods of
-    [] -> pure ()
-    (methodName:_) -> throwWithContext (EMissingInterfaceMethod tplName tpiInterface methodName)
+  whenJust (listToMaybe (HS.toList missingMethods)) $ \methodName ->
+    throwWithContext (EMissingInterfaceMethod tplName tpiInterface methodName)
   forM_ tpiMethods $ \TemplateImplementsMethod{tpiMethodName, tpiMethodExpr} -> do
     case NM.lookup tpiMethodName intMethods of
       Nothing -> throwWithContext (EUnknownInterfaceMethod tplName tpiInterface tpiMethodName)
@@ -952,9 +964,8 @@ checkDefException m DefException{..} = do
     unless (null tyParams) $ throwWithContext (EExpectedExceptionTypeHasNoParams modName exnName)
     checkExpr exnMessage (TCon tcon :-> TText)
     _ <- match _DataRecord (EExpectedExceptionTypeIsRecord modName exnName) dataCons
-    case NM.lookup exnName (moduleTemplates m) of
-        Nothing -> pure ()
-        Just _ -> throwWithContext (EExpectedExceptionTypeIsNotTemplate modName exnName)
+    whenJust (NM.lookup exnName (moduleTemplates m)) $ \_ ->
+      throwWithContext (EExpectedExceptionTypeIsNotTemplate modName exnName)
 
 -- NOTE(MH): It is important that the data type definitions are checked first.
 -- The type checker for expressions relies on the fact that data type

compiler/daml-lf-tools/src/DA/Daml/LF/TypeChecker/Error.hs

@@ -134,6 +134,8 @@ data Error
   | EDuplicateInterfaceChoiceName !TypeConName !ChoiceName
   | EDuplicateInterfaceMethodName !TypeConName !MethodName
   | EUnknownInterface !TypeConName
+  | ECircularInterfaceRequires !TypeConName !(Maybe (Qualified TypeConName))
+  | ENotClosedInterfaceRequires !TypeConName !(Qualified TypeConName) ![Qualified TypeConName]
   | EMissingRequiredInterface { emriTemplate :: !TypeConName, emriRequiringInterface :: !(Qualified TypeConName), emriRequiredInterface :: !(Qualified TypeConName) }
   | EBadInheritedChoices { ebicInterface :: !(Qualified TypeConName), ebicExpected :: ![ChoiceName], ebicGot :: ![ChoiceName] }
   | EMissingInterfaceChoice !ChoiceName
@@ -380,6 +382,17 @@ instance Pretty Error where
     EDuplicateInterfaceMethodName iface method ->
       "Duplicate method name '" <> pretty method <> "' in interface definition for " <> pretty iface
     EUnknownInterface tcon -> "Unknown interface: " <> pretty tcon
+    ECircularInterfaceRequires iface Nothing ->
+      "Circular interface requirement is not allowed: interface " <> pretty iface <> " requires itself."
+    ECircularInterfaceRequires iface (Just otherIface) ->
+      "Circular interface requirement is not allowed: interface "
+        <> pretty iface <> " requires "
+        <> pretty otherIface <> " requires "
+        <> pretty iface
+    ENotClosedInterfaceRequires iface ifaceRequired ifaceMissing ->
+      "Interface " <> pretty iface
+        <> " is missing requirement " <> pretty ifaceMissing
+        <> " required by " <> pretty ifaceRequired
     EMissingRequiredInterface {..} ->
       "Template " <> pretty emriTemplate <>
       " is missing an implementation of interface " <> pretty emriRequiredInterface <>

compiler/damlc/tests/daml-test-files/InterfaceRequiresCircular.daml

@@ -0,0 +1,15 @@
+-- Copyright (c) 2021 Digital Asset (Switzerland) GmbH and/or its affiliates. All rights reserved.
+-- SPDX-License-Identifier: Apache-2.0
+
+-- @SINCE-LF-FEATURE DAML_INTERFACE
+-- @ERROR Circular interface requirement is not allowed: interface A requires itself.
+
+-- | Check that an interface cannot require itself.
+module InterfaceRequiresCircular where
+
+interface A where
+
+-- TODO https://github.com/digital-asset/daml/issues/11978
+--   Implement "requires" syntax.
+_requires_A_A : DA.Internal.Desugar.RequiresT A A
+_requires_A_A = DA.Internal.Desugar.RequiresT

compiler/damlc/tests/daml-test-files/InterfaceRequiresCircularIndirect.daml

@@ -0,0 +1,20 @@
+-- Copyright (c) 2021 Digital Asset (Switzerland) GmbH and/or its affiliates. All rights reserved.
+-- SPDX-License-Identifier: Apache-2.0
+
+-- @SINCE-LF-FEATURE DAML_INTERFACE
+-- @ERROR Circular interface requirement is not allowed: interface A requires InterfaceRequiresCircularIndirect:B requires A
+
+-- | Check that an interface cannot require itself indirectly.
+module InterfaceRequiresCircularIndirect where
+
+interface A where
+
+interface B where
+
+-- TODO https://github.com/digital-asset/daml/issues/11978
+--   Implement "requires" syntax.
+_requires_A_B : DA.Internal.Desugar.RequiresT A B
+_requires_A_B = DA.Internal.Desugar.RequiresT
+
+_requires_B_A : DA.Internal.Desugar.RequiresT B A
+_requires_B_A = DA.Internal.Desugar.RequiresT

compiler/damlc/tests/daml-test-files/InterfaceRequiresNotClosed.daml

@@ -0,0 +1,22 @@
+-- Copyright (c) 2021 Digital Asset (Switzerland) GmbH and/or its affiliates. All rights reserved.
+-- SPDX-License-Identifier: Apache-2.0
+
+-- @SINCE-LF-FEATURE DAML_INTERFACE
+-- @ERROR Interface C is missing requirement [InterfaceRequiresNotClosed:A] required by InterfaceRequiresNotClosed:B
+
+-- | Check that interface requirements are transitively closed.
+module InterfaceRequiresNotClosed where
+
+interface A where
+
+interface B where
+
+interface C where
+
+-- TODO https://github.com/digital-asset/daml/issues/11978
+--   Implement "requires" syntax.
+_requires_B_A : DA.Internal.Desugar.RequiresT B A
+_requires_B_A = DA.Internal.Desugar.RequiresT
+
+_requires_C_B : DA.Internal.Desugar.RequiresT C B
+_requires_C_B = DA.Internal.Desugar.RequiresT