Add partial ContractId-in-template-key check (#13541)

* Add Keyability check in DA.Daml.LF.TypeChecker

* Update expected errors in daml-test-files/ContractIdInContractKey.daml

* Update no-contract-ids-in-keys daml-lf scenario test to circumvent new check

changelog_begin
[Daml Compiler] Implemented compile-time check disallowing ContractId types in contract key types. This check looks for potential problems with the contract key type only within the template's module.
changelog_end

Co-authored-by: Sofia Faro <sofia.faro@digitalasset.com>

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

@@ -15,6 +15,7 @@ import           DA.Daml.LF.Ast
 import qualified DA.Daml.LF.TypeChecker.Check      as Check
 import           DA.Daml.LF.TypeChecker.Env
 import           DA.Daml.LF.TypeChecker.Error
+import qualified DA.Daml.LF.TypeChecker.Keyability as Keyability
 import qualified DA.Daml.LF.TypeChecker.Recursion as Recursion
 import qualified DA.Daml.LF.TypeChecker.Serializability as Serializability
 import qualified DA.Daml.LF.TypeChecker.NameCollision as NameCollision
@@ -50,6 +51,7 @@ checkModuleInWorld world version m =
         Recursion.checkModule m
         Check.checkModule m
         Serializability.checkModule m
+        Keyability.checkModule m
 
 -- | Check whether the whole package satisfies the name collision condition.
 nameCheckPackage :: Package -> [Diagnostic]

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

@@ -106,6 +106,7 @@ data Error
   | EExpectedUpdateType    !Type
   | EExpectedScenarioType  !Type
   | EExpectedSerializableType !SerializabilityRequirement !Type !UnserializabilityReason
+  | EExpectedKeyTypeWithoutContractId !Type
   | EExpectedAnyType !Type
   | EExpectedExceptionType !Type
   | EExpectedExceptionTypeHasNoParams !ModuleName !TypeConName
@@ -341,6 +342,11 @@ instance Pretty Error where
       , "* problem:"
       , nest 4 (pretty info)
       ]
+    EExpectedKeyTypeWithoutContractId foundType ->
+      vcat
+      [ "contract key type should not contain ContractId:"
+      , "* found:" <-> pretty foundType
+      ]
     EExpectedAnyType foundType ->
       "expected a type containing neither type variables nor quantifiers, but found: " <> pretty foundType
     EExpectedExceptionType foundType ->

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

@@ -0,0 +1,121 @@
+-- Copyright (c) 2022 Digital Asset (Switzerland) GmbH and/or its affiliates. All rights reserved.
+-- SPDX-License-Identifier: Apache-2.0
+
+-- | This module performs a partial check ensuring that the types used as
+-- template keys do not contain 'ContractId's. The check is partial in that
+-- it will only check the key type expression and any types mentioned in it
+-- which are defined in the same module. For lack of a better name, we refer
+-- to this as the "keyability" of a type.
+-- Note that this check is performed after the serializability checks, so we
+-- do not have to worry about unserializable types being reported as keyable by
+-- this check.
+module DA.Daml.LF.TypeChecker.Keyability
+  ( checkModule
+  ) where
+
+import Control.Lens (matching, toListOf)
+import Control.Monad.Extra
+import Data.Foldable (for_)
+import Data.Semigroup.FixedPoint (leastFixedPointBy)
+import qualified Data.HashSet as HS
+import qualified Data.NameMap as NM
+import qualified Data.HashMap.Strict as HMS
+
+import DA.Daml.LF.Ast
+import DA.Daml.LF.Ast.Optics (_PRSelfModule, dataConsType)
+import DA.Daml.LF.TypeChecker.Env
+import DA.Daml.LF.TypeChecker.Error
+
+newtype CurrentModule = CurrentModule  ModuleName
+newtype UnkeyableTyConSet = UnkeyableTyConSet (HS.HashSet TypeConName)
+
+-- | Check whether a module satisfies all "keyability" constraints.
+checkModule :: MonadGamma m => Module -> m ()
+checkModule mod0 = do
+  let
+    currentModule = CurrentModule (moduleName mod0)
+    dataTypes = moduleDataTypes mod0
+    unkeyableTyCons = findUnkeyableTyConsInModule currentModule dataTypes
+
+  for_ (moduleTemplates mod0) $ \tpl ->
+    for_ (tplKey tpl) $ \key ->
+      withContext (ContextTemplate mod0 tpl TPKey) $ do
+        checkKeyType currentModule unkeyableTyCons (tplKeyType key)
+
+findUnkeyableTyConsInModule ::
+     CurrentModule
+  -> NM.NameMap DefDataType
+  -> UnkeyableTyConSet
+findUnkeyableTyConsInModule currentModule dataTypes = do
+  let eqs =
+        [ (dataTypeCon dataType, keyable, deps)
+        | dataType <- NM.toList dataTypes
+        , let (keyable, deps) =
+                case keyabilityConditionsDataType currentModule dataType of
+                  Nothing -> (False, [])
+                  Just deps0 -> (True, HS.toList deps0)
+        ]
+  case leastFixedPointBy (&&) eqs of
+    Left name -> error ("Reference to unknown data type: " ++ show name)
+    Right keyabilities ->
+      UnkeyableTyConSet $ HMS.keysSet $ HMS.filter not keyabilities
+
+-- | Determine whether a data type preserves "keyability".
+keyabilityConditionsDataType ::
+     CurrentModule
+  -> DefDataType
+  -> Maybe (HS.HashSet TypeConName)
+keyabilityConditionsDataType currentModule (DefDataType _loc _ _ _ cons) =
+  mconcatMapM
+    (keyabilityConditionsType currentModule)
+    (toListOf dataConsType cons)
+
+-- | Determine whether a type is "keyable".
+--
+-- Type constructors from the current module are returned as "keyability"
+-- conditions, while type constructors from other modules are assumed to be "keyable"
+keyabilityConditionsType ::
+     CurrentModule
+  -> Type
+  -> Maybe (HS.HashSet TypeConName)
+keyabilityConditionsType (CurrentModule currentModuleName) = go
+  where
+    unkeyable = Nothing
+    noConditions = Just HS.empty
+    conditionallyOn = Just . HS.singleton
+
+    go = \case
+      TContractId{} -> unkeyable
+
+      TList typ -> go typ
+      TOptional typ -> go typ
+      TTextMap typ -> go typ
+      TGenMap t1 t2 -> HS.union <$> go t1 <*> go t2
+      TApp tfun targ -> HS.union <$> go tfun <*> go targ
+
+      TCon qtcon
+        | Right tconName <- matching (_PRSelfModule currentModuleName) qtcon ->
+            conditionallyOn tconName
+        | otherwise -> noConditions
+
+      TNumeric{} -> noConditions
+      TVar{} -> noConditions
+      TBuiltin{} -> noConditions
+
+      -- By this point, the only remaining type synonyms are the ones for constraints,
+      -- which are deemed unserializable by DA.Daml.LF.TypeChecker.Serializability, so
+      -- we don't need any special handling here.
+      TSynApp{} -> noConditions
+
+      -- These are also unserializable so no special handling is needed either.
+      TNat{} -> noConditions
+      TForall{} -> noConditions
+      TStruct{} -> noConditions
+
+-- | Check whether a type is "keyable".
+checkKeyType :: MonadGamma m => CurrentModule -> UnkeyableTyConSet -> Type -> m ()
+checkKeyType currentModule (UnkeyableTyConSet unkeyableTyCons) typ = do
+  case keyabilityConditionsType currentModule typ of
+    Just conds
+      | HS.null (HS.intersection conds unkeyableTyCons) -> pure ()
+    _ -> throwWithContext (EExpectedKeyTypeWithoutContractId typ)

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

@@ -1,7 +1,4 @@
--- @ERROR range=25:1-25:14; Contract IDs are not supported in contract key
--- @ERROR range=34:1-34:13; Contract IDs are not supported in contract key
--- @ERROR range=40:1-40:14; Contract IDs are not supported in contract key
--- @ERROR range=46:1-46:16; Contract IDs are not supported in contract key
+-- @ERROR range=1:1-2:1; contract key type should not contain ContractId
 module ContractIdInContractKey where
 
 template Contract with

daml-lf/tests/BUILD.bazel

@@ -120,7 +120,7 @@ daml_compile(
             "//daml-lf/repl",
             file,
             "%s/EXPECTED.ledger" % "/".join(file.split("/")[0:3]),
-        ],
+        ] + (["scenario/stable/no-contract-ids-in-keys/Simple.daml"] if "no-contract-ids-in-keys" in file else []),
         toolchains = [
             "@rules_sh//sh/posix:make_variables",
         ],

daml-lf/tests/scenario/stable/no-contract-ids-in-keys/Simple.daml

@@ -0,0 +1,16 @@
+-- Copyright (c) 2022 Digital Asset (Switzerland) GmbH and/or its affiliates. All rights reserved.
+-- SPDX-License-Identifier: Apache-2.0
+
+
+module Simple where
+
+-- Test that values of contract keys may not contain contract IDs
+
+template Simple
+  with
+    p: Party
+  where
+    signatory p
+
+newtype SimpleContractId = SimpleContractId (ContractId Simple)
+  deriving (Eq, Show)

daml-lf/tests/scenario/stable/no-contract-ids-in-keys/Test.daml

@@ -1,28 +1,23 @@
 -- Copyright (c) 2022 Digital Asset (Switzerland) GmbH and/or its affiliates. All rights reserved.
 -- SPDX-License-Identifier: Apache-2.0
 
-
 module Test where
 
--- Test that values of contract keys may not contain contract IDs
-
-template Simple
-  with
-    p: Party
-  where
-    signatory p
+-- The SimpleContractId newtype has to be defined in a separate module so
+-- this circumvents the partial compile-time check on template keys.
+import Simple
 
 template KeyWithContractId
   with
     p: Party
-    k: ContractId Simple
+    k: SimpleContractId
   where
     signatory p
-    key (p, k): (Party, ContractId Simple)
+    key (p, k): (Party, SimpleContractId)
     maintainer key._1
 
 run = scenario do
   alice <- getParty "alice"
   cid <- submit alice $ create Simple with p = alice
   -- This should fail
-  submit alice $ create KeyWithContractId with p = alice, k = cid
+  submit alice $ create KeyWithContractId with p = alice, k = SimpleContractId cid