LF: Test scala interface type checking (#11833)

CHANGELOG_BEGIN
CHANGELOG_END

daml-lf/parser/src/main/scala/com/digitalasset/daml/lf/testing/parser/ExprParser.scala

@@ -340,7 +340,7 @@ private[parser] class ExprParser[P](parserParameters: ParserParameters[P]) {
   )
 
   private lazy val eCallInterface: Parser[ECallInterface] =
-    `icall` ~! `@` ~> fullIdentifier ~ id ~ expr0 ^^ { case ifaceId ~ name ~ body =>
+    `call_method` ~! `@` ~> fullIdentifier ~ id ~ expr0 ^^ { case ifaceId ~ name ~ body =>
       ECallInterface(interfaceId = ifaceId, methodName = name, value = body)
     }
 

daml-lf/parser/src/main/scala/com/digitalasset/daml/lf/testing/parser/Lexer.scala

@@ -45,7 +45,7 @@ private[parser] object Lexer extends RegexParsers {
     "catch" -> `catch`,
     "to_interface" -> `to_interface`,
     "from_interface" -> `from_interface`,
-    "icall" -> `icall`,
+    "call_method" -> `call_method`,
   )
 
   val token: Parser[Token] =

daml-lf/parser/src/main/scala/com/digitalasset/daml/lf/testing/parser/Token.scala

@@ -53,7 +53,7 @@ private[parser] object Token {
   case object `catch` extends Token
   case object `to_interface` extends Token
   case object `from_interface` extends Token
-  case object `icall` extends Token
+  case object `call_method` extends Token
 
   final case class Id(s: String) extends Token
   final case class ContractId(s: String) extends Token

daml-lf/parser/src/test/scala/com/digitalasset/daml/lf/testing/parser/ParsersSpec.scala

@@ -332,9 +332,9 @@ class ParsersSpec extends AnyWordSpec with ScalaCheckPropertyChecks with Matcher
           EFromAnyException(E, e"anyException"),
         "throw @Unit @Mod:E exception" ->
           EThrow(TUnit, E, e"exception"),
-        "icall @Mod:I method body" ->
+        "call_method @Mod:I method body" ->
           ECallInterface(I.tycon, n"method", e"body"),
-        "icall @'-pkgId-':Mod:I method body" ->
+        "call_method @'-pkgId-':Mod:I method body" ->
           ECallInterface(I.tycon, n"method", e"body"),
         "to_interface @Mod:T @Mod:I body" ->
           EToInterface(T.tycon, I.tycon, e"body"),
@@ -762,10 +762,10 @@ class ParsersSpec extends AnyWordSpec with ScalaCheckPropertyChecks with Matcher
             method asParty: Party;
             method getName: Text;
             choice Sleep (self) (u:Unit) : ContractId Mod:Person
-              , controllers Cons @Party [icall @Mod:Person asParty this] (Nil @Party)
+              , controllers Cons @Party [call_method @Mod:Person asParty this] (Nil @Party)
               to upure @(ContractId Mod:Person) self;
             choice @nonConsuming Nap (self) (i : Int64): Int64
-              , controllers Cons @Party [icall @Mod:Person asParty this] (Nil @Party)
+              , controllers Cons @Party [call_method @Mod:Person asParty this] (Nil @Party)
               , observers Nil @Party
               to upure @Int64 i;
           } ;
@@ -785,7 +785,7 @@ class ParsersSpec extends AnyWordSpec with ScalaCheckPropertyChecks with Matcher
             n"Sleep" -> TemplateChoice(
               name = n"Sleep",
               consuming = true,
-              controllers = e"Cons @Party [icall @Mod:Person asParty this] (Nil @Party)",
+              controllers = e"Cons @Party [call_method @Mod:Person asParty this] (Nil @Party)",
               choiceObservers = None,
               selfBinder = n"self",
               argBinder = n"u" -> TUnit,
@@ -795,7 +795,7 @@ class ParsersSpec extends AnyWordSpec with ScalaCheckPropertyChecks with Matcher
             n"Nap" -> TemplateChoice(
               name = n"Nap",
               consuming = false,
-              controllers = e"Cons @Party [icall @Mod:Person asParty this] (Nil @Party)",
+              controllers = e"Cons @Party [call_method @Mod:Person asParty this] (Nil @Party)",
               choiceObservers = Some(e"Nil @Party"),
               selfBinder = n"self",
               argBinder = n"i" -> TInt64,

daml-lf/validation/src/main/scala/com/digitalasset/daml/lf/validation/Typing.scala

@@ -456,12 +456,10 @@ private[validation] object Typing {
     def checkDefIface(ifaceName: TypeConName, iface: DefInterface): Unit =
       iface match {
         case DefInterface(param, fixedChoices, methods, precond) =>
-          fixedChoices.values.foreach(
-            introExprVar(param, TTyCon(ifaceName)).checkChoice(ifaceName, _)
-          )
-          methods.values.foreach(checkIfaceMethod)
           val env = introExprVar(param, TTyCon(ifaceName))
           env.checkExpr(precond, TBool)
+          methods.values.foreach(checkIfaceMethod)
+          fixedChoices.values.foreach(env.checkChoice(ifaceName, _))
       }
 
     def checkIfaceMethod(method: InterfaceMethod): Unit = {

daml-lf/validation/src/test/scala/com/digitalasset/daml/lf/validation/TypingSpec.scala

@@ -5,7 +5,7 @@ package com.daml.lf.validation
 
 import com.daml.lf.data.Ref.DottedName
 import com.daml.lf.language.Ast._
-import com.daml.lf.language.{PackageInterface, LookupError, Reference, LanguageVersion => LV}
+import com.daml.lf.language.{LookupError, PackageInterface, Reference, LanguageVersion => LV}
 import com.daml.lf.testing.parser.Implicits._
 import com.daml.lf.testing.parser.{defaultLanguageVersion, defaultPackageId}
 import com.daml.lf.validation.SpecUtil._
@@ -15,7 +15,7 @@ import org.scalatest.wordspec.AnyWordSpec
 
 class TypingSpec extends AnyWordSpec with TableDrivenPropertyChecks with Matchers {
 
-  "Checker.checkKind" should {
+  "checkKind" should {
     // TEST_EVIDENCE: Input Validation: ill-formed kinds are rejected
     "reject invalid kinds" in {
 
@@ -42,7 +42,7 @@ class TypingSpec extends AnyWordSpec with TableDrivenPropertyChecks with Matcher
     }
   }
 
-  "Checker.kindOf" should {
+  "kindOf" should {
 
     // TEST_EVIDENCE: Input Validation: ensure builtin operators have the correct type
     "infers the proper kind for builtin types (but ContractId)" in {
@@ -102,7 +102,7 @@ class TypingSpec extends AnyWordSpec with TableDrivenPropertyChecks with Matcher
     }
   }
 
-  "Checker.typeOf" should {
+  "typeOf" should {
 
     // TEST_EVIDENCE: Input Validation: ensure expression forms have the correct type
 
@@ -258,6 +258,15 @@ class TypingSpec extends AnyWordSpec with TableDrivenPropertyChecks with Matcher
         // Forall shadowing
         E"(Λ (τ : ⋆) (τ : ⋆). λ (e₁ : τ)  → 0) @Int64 @Text" ->
           T"Text -> Int64",
+        // EToInterface
+        E"λ (t: Mod:Ti) → (( to_interface @Mod:I @Mod:Ti t ))" ->
+          T"Mod:Ti → Mod:I",
+        // EFromInterface
+        E"λ (i: Mod:I) → (( from_interface @Mod:I @Mod:Ti i ))" ->
+          T"Mod:I → Option Mod:Ti",
+        // ECallInterface
+        E"λ (i: Mod:I) → (( call_method @Mod:I getParties i ))" ->
+          T"Mod:I → List Party",
       )
 
       forEvery(testCases) { (exp: Expr, expectedType: Type) =>
@@ -330,7 +339,6 @@ class TypingSpec extends AnyWordSpec with TableDrivenPropertyChecks with Matcher
       }
     }
 
-    //TODO add a check for exerciseInterface/checkInterface.
     "infers proper type for Update" in {
       val testCases = Table(
         "expression" ->
@@ -342,12 +350,18 @@ class TypingSpec extends AnyWordSpec with TableDrivenPropertyChecks with Matcher
           T"∀ (τ : ⋆) (τ₂ : ⋆) (τ₁ : ⋆). Update τ₁ → Update τ₂ → (τ₁ → τ₂ → Update τ) → (( Update τ ))",
         E"λ (e: Mod:T) → (( create @Mod:T e))" ->
           T"Mod:T → (( Update (ContractId Mod:T) ))",
+        E"λ (e: Mod:I) → (( create_by_interface @Mod:I e))" ->
+          T"Mod:I → (( Update (ContractId Mod:I) ))",
         E"λ (e₁: ContractId Mod:T) (e₂: Int64) → (( exercise @Mod:T Ch e₁ e₂ ))" ->
           T"ContractId Mod:T → Int64 → (( Update Decimal ))",
+        E"λ (e₁: ContractId Mod:I) (e₂: Int64) → (( exercise_by_interface @Mod:I ChIface e₁ e₂ ))" ->
+          T"ContractId Mod:I → Int64 → (( Update Decimal ))",
         E"λ (e₁: Party) (e₂: Int64) → (( exercise_by_key @Mod:T Ch e₁ e₂ ))" ->
           T"Party → Int64 → (( Update Decimal ))",
         E"λ (e: ContractId Mod:T) → (( fetch @Mod:T e ))" ->
           T"ContractId Mod:T → (( Update Mod:T ))",
+        E"λ (e: ContractId Mod:I) → (( fetch_by_interface @Mod:I e ))" ->
+          T"ContractId Mod:I → (( Update Mod:I ))",
         E"λ (e: Party) → (( fetch_by_key @Mod:T e ))" ->
           T"Party → (( Update (⟨ contract: Mod:T, contractId: ContractId Mod:T ⟩) ))",
         E"λ (e: Party) →  (( lookup_by_key @Mod:T 'Bob' ))" ->
@@ -744,30 +758,102 @@ class TypingSpec extends AnyWordSpec with TableDrivenPropertyChecks with Matcher
           },
         E"Λ (σ : ⋆). λ (e: σ) → ⸨ create @Mod:T e ⸩" -> //
           { case _: ETypeMismatch => },
+        // UpdCreateInterface
+        E"λ (e: Mod:U) → ⸨ create_by_interface @Mod:U nothing ⸩" -> //
+          {
+            case EUnknownDefinition(
+                  _,
+                  LookupError(Reference.Interface(_), Reference.Interface(_)),
+                ) =>
+          },
+        E"Λ (σ : ⋆). λ (e: σ) → ⸨ create_by_interface @Mod:I e ⸩" -> //
+          { case _: ETypeMismatch => },
         // UpdExercise
-        E"λ (e₂: List Party) (e₃: Int64) → ⸨ exercise @Mod:U Ch nothing e₂ e₃ ⸩" -> //
+        E"λ (e₁: ContractId Mod:U) (e₂: Int64) → ⸨ exercise @Mod:U Ch e₁ e₂ ⸩" -> //
           {
             case EUnknownDefinition(
                   _,
                   LookupError(Reference.Template(_), Reference.TemplateChoice(_, _)),
                 ) =>
           },
-        E"λ (e₁: ContractId Mod:T) (e₂: List Party) (e₃: Int64) → ⸨ exercise @Mod:T Not e₁ e₂ e₃ ⸩" -> //
+        E"λ (e₁: ContractId Mod:T) (e₂: Int64) → ⸨ exercise @Mod:T ChTmpl e₁ e₂⸩" -> //
           {
             case EUnknownDefinition(
                   _,
                   LookupError(Reference.TemplateChoice(_, _), Reference.TemplateChoice(_, _)),
                 ) =>
           },
-        E"Λ (σ : ⋆).λ (e₁: ContractId Mod:T) (e₂: List Party) (e₃: σ) → ⸨ exercise @Mod:T Ch e₁ e₂ e₃ ⸩" -> //
+        E"Λ (σ : ⋆).λ (e₁: ContractId Mod:T) (e₂: σ) → ⸨ exercise @Mod:T Ch e₁ e₂ ⸩" -> //
           { case _: ETypeMismatch => },
-        E"Λ (σ : ⋆).λ (e₁: ContractId Mod:T) (e₂: List σ) (e₃: Int64) → ⸨ exercise @Mod:T Ch e₁ e₂ e₃ ⸩" -> //
+        E"Λ (σ : ⋆).λ (e₁: ContractId σ) (e₂: Int64) → ⸨ exercise @Mod:T Ch e₁ e₂ ⸩" -> //
           { case _: ETypeMismatch => },
-        E"Λ (σ : ⋆).λ (e₁: ContractId Mod:T) (e₂: σ) (e₃: Int64) → ⸨ exercise @Mod:T Ch e₁ e₂ e₃ ⸩" -> //
+        // This verifies that template choice cannot be exercised by interface
+        E"λ (e₁: ContractId Mod:I) (e₂: List Party) (e₃: Int64) → ⸨ exercise @Mod:I ChTmpl e₁ e₂ ⸩" -> {
+          case EUnknownDefinition(
+                _,
+                LookupError(Reference.Template(_), Reference.TemplateChoice(_, _)),
+              ) =>
+            // We double check that Ti implements I and Ti has a choice ChTmpl
+            val TTyCon(conI) = t"Mod:I"
+            val TTyCon(conTi) = t"Mod:Ti"
+            assert(env.interface.lookupTemplateImplements(conI, conTi).isRight)
+            assert(env.interface.lookupTemplateChoice(conTi, n"ChTmpl").isRight)
+        },
+        // UpdExerciseInterface
+        E"λ (e₁: ContractId Mod:U) (e₂: Int64) → ⸨ exercise_by_interface @Mod:U ChIface e₁ e₂ ⸩" -> //
+          {
+            case EUnknownDefinition(
+                  _,
+                  LookupError(Reference.Interface(_), Reference.InterfaceChoice(_, _)),
+                ) =>
+          },
+        E"λ (e₁: ContractId Mod:I) (e₂: Int64) → ⸨ exercise_by_interface @Mod:I Not e₁ e₂ ⸩" -> //
+          {
+            case EUnknownDefinition(
+                  _,
+                  LookupError(Reference.TemplateChoice(_, _), Reference.InterfaceChoice(_, _)),
+                ) =>
+          },
+        E"Λ (σ : ⋆).λ (e₁: ContractId Mod:I) (e₂: σ) → ⸨ exercise_by_interface @Mod:T ChIface e₁ e₂ ⸩" -> //
           { case _: ETypeMismatch => },
-        E"Λ (σ : ⋆).λ (e₁: ContractId σ) (e₂: List Party) (e₃: Int64) → ⸨ exercise @Mod:T Ch e₁ e₂ e₃ ⸩" -> //
+        E"Λ (σ : ⋆).λ (e₁: ContractId Mod:I) (e₂: Int64) → ⸨ exercise_by_interface @Mod:T ChIface e₁ e₂ ⸩" -> //
           { case _: ETypeMismatch => },
-        // FecthByKey & lookupByKey
+        E"Λ (σ : ⋆).λ (e₁: ContractId σ) (e₂: Int64) → ⸨ exercise_by_interface @Mod:T ChIface e₁ e₂ ⸩" -> //
+          { case _: ETypeMismatch => },
+        // This verifies that interface choice cannot be exercise by template
+        E"""λ (e₁: ContractId Mod:Ti) (e: Mod:Ti) (e₂: Int64) → ⸨ exercise_by_interface @Mod:Ti ChIface e₁ e₂ ⸩""" -> //
+          {
+            case EUnknownDefinition(
+                  _,
+                  LookupError(Reference.Interface(_), Reference.InterfaceChoice(_, _)),
+                ) =>
+              // We double check that Ti implements I and Ti has a choice ChTmpl
+              val TTyCon(conI) = t"Mod:I"
+              val TTyCon(conTi) = t"Mod:Ti"
+              assert(env.interface.lookupTemplateImplements(conI, conTi).isRight)
+              assert(env.interface.lookupInterfaceChoice(conI, n"ChIface").isRight)
+          },
+        // UpdFetch
+        E"λ (e: ContractId Mod:U) → ⸨ fetch @Mod:U e ⸩" -> //
+          {
+            case EUnknownDefinition(
+                  _,
+                  LookupError(Reference.Template(_), Reference.Template(_)),
+                ) =>
+          },
+        E"Λ (σ : ⋆). λ (e: σ) → ⸨ fetch @Mod:T e ⸩" -> //
+          { case _: ETypeMismatch => },
+        // UpdFetchInterface
+        E"λ (e: ContractId Mod:U) → ⸨ fetch_by_interface @Mod:U e ⸩" -> //
+          {
+            case EUnknownDefinition(
+                  _,
+                  LookupError(Reference.Interface(_), Reference.Interface(_)),
+                ) =>
+          },
+        E"Λ (σ : ⋆). λ (e: σ) → ⸨ fetch_by_interface @Mod:I e ⸩" -> //
+          { case _: ETypeMismatch => },
+        // UpFecthByKey & lookupByKey
         E"""⸨ fetch_by_key @Mod:U "Bob" ⸩""" -> //
           {
             case EUnknownDefinition(
@@ -779,19 +865,51 @@ class TypingSpec extends AnyWordSpec with TableDrivenPropertyChecks with Matcher
           { case _: ETypeMismatch => },
         E"""⸨ lookup_by_key @Mod:T "Bob" ⸩""" -> //
           { case _: ETypeMismatch => },
-        // UpdFetch
+        // ScenarioEmbedExpr
-        E"Λ (σ: ⋆). λ (e: ContractId Mod:U) → ⸨ fetch @Mod:U e ⸩" -> //
+        E"Λ (τ : ⋆) (σ : ⋆). λ (e : σ) → ⸨ uembed_expr @τ e ⸩" -> //
+          { case _: ETypeMismatch => },
+        // EToInterface
+        E"""λ (t: Mod:Ti) → ⸨ to_interface @Mod:T @Mod:Ti t  ⸩""" -> //
+          {
+            case EUnknownDefinition(
+                  _,
+                  LookupError(Reference.Interface(_), Reference.Interface(_)),
+                ) =>
+          },
+        E"""λ (t: Mod:Ti) → ⸨ to_interface @Mod:I @Mod:T t  ⸩""" -> //
+          { case ETemplateDoesNotImplementInterface(_, _, _) => },
+        E"""λ (t: Mod:T) → ⸨ to_interface @Mod:I @Mod:Ti t  ⸩""" -> //
+          { case _: ETypeMismatch => },
+        // EFromInterface
+        E"""λ (i: Mod:I) → ⸨ from_interface @Mod:I @Mod:I i ⸩""" -> //
           {
             case EUnknownDefinition(
                   _,
                   LookupError(Reference.Template(_), Reference.Template(_)),
                 ) =>
           },
-        E"Λ (σ : ⋆). λ (e: σ) → ⸨ fetch @Mod:T e ⸩" -> //
+        E"λ (i: Mod:I) → ⸨ from_interface @Mod:I @Mod:T i ⸩" -> //
+          { case ETemplateDoesNotImplementInterface(_, _, _) => },
+        E"λ (i: Mod:J) → ⸨ from_interface @Mod:I @Mod:Ti i ⸩" -> //
           { case _: ETypeMismatch => },
-        // ScenarioEmbedExpr
+        // ECallInterface
-        E"Λ (τ : ⋆) (σ : ⋆). λ (e : σ) → ⸨ uembed_expr @τ e ⸩" -> //
+        E"λ (i: Mod:U) → ⸨  call_method @Mod:U getParties i ⸩" -> //
+          {
+            case EUnknownDefinition(
+                  _,
+                  LookupError(Reference.Interface(_), Reference.Method(_, _)),
+                ) =>
+          },
+        E"λ (i: Mod:I) → ⸨  call_method @Mod:I getParty i ⸩" -> //
+          {
+            case EUnknownDefinition(
+                  _,
+                  LookupError(Reference.Method(_, _), Reference.Method(_, _)),
+                ) =>
+          },
+        E"Λ (σ : ⋆). λ (e: σ) → ⸨ call_method @Mod:I getParties e ⸩" -> //
           { case _: ETypeMismatch => },
+        //
       )
 
       val ELocation(expectedLocation, EVar("something")) = E"⸨ something ⸩"
@@ -809,9 +927,6 @@ class TypingSpec extends AnyWordSpec with TableDrivenPropertyChecks with Matcher
       }
     }
 
-    //TODO add check for interface definitions.
-    //TODO add check for interface implementations.
-
     // TEST_EVIDENCE: Input Validation: ill-formed templates are rejected
     "reject ill formed template definition" in {
 
@@ -819,13 +934,16 @@ class TypingSpec extends AnyWordSpec with TableDrivenPropertyChecks with Matcher
         p"""
 
           module Mod {
-            record @serializable U = {};
+            record @serializable Key = {person: Text, party: Party};
-            record @serializable Box (a :*) = { value: a };
+
+            interface (this: I) = {
+              precondition True;
+              method getParties: List Party;
+            };
           }
 
           module NegativeTestCase {
             record @serializable T = {person: Party, name: Text};
-            record @serializable TBis = {person: Text, party: Party};
 
             template (this : T) =  {
               precondition True;
@@ -843,13 +961,62 @@ class TypingSpec extends AnyWordSpec with TableDrivenPropertyChecks with Matcher
                   , controllers Cons @Party ['Alice'] (Nil @Party)
                   , observers Cons @Party ['Alice'] (Nil @Party)
                   to upure @Unit ();
-              key @NegativeTestCase:TBis
+              implements Mod:I {
-                  (NegativeTestCase:TBis { person = (NegativeTestCase:T {name} this), party = (NegativeTestCase:T {person} this) })
+                method getParties = \(self: NegativeTestCase:T) -> Cons @Party [NegativeTestCase:T {person} self] (Nil @Party);
-                  (\ (key: NegativeTestCase:TBis) -> Cons @Party [(NegativeTestCase:TBis {party} key), 'Alice'] (Nil @Party)  );
+              };
+              key @Mod:Key
+                  (Mod:Key { person = (NegativeTestCase:T {name} this), party = (NegativeTestCase:T {person} this) })
+                  (\ (key: Mod:Key) -> Cons @Party [(Mod:Key {party} key), 'Alice'] (Nil @Party)  );
             } ;
           }
 
-          module PositiveTestCase1 {
+
+          module PositiveTestCase_TemplateTypeShouldBeStar {
+            record @serializable T (a: *) = {x: a};
+
+            // in the next line, T should be of type *.
+            template (this : T) =  {
+              precondition True;
+              signatories Cons @Party ['Bob'] (Nil @Party);
+              observers Cons @Party ['Alice'] (Nil @Party);
+              agreement "Agreement";
+            };
+          }
+
+          module PositiveTestCase_TemplateTypeShouldBeRecord {
+            variant @serializable V = P : Party;
+
+            // in the next line, V should be of record.
+            template (this : V) =  {
+              precondition True;
+              signatories Cons @Party ['Bob'] (Nil @Party);
+              observers Cons @Party ['Alice'] (Nil @Party);
+              agreement "Agreement";
+            };
+          }
+
+           module PositiveTestCase_TemplateTypeShouldExists{
+             // template without data type
+             template (this : T) =  {
+              precondition True;
+              signatories Cons @Party ['Bob'] (Nil @Party);
+              observers Cons @Party ['Alice'] (Nil @Party);
+              agreement "Agreement";
+            } ;
+          }
+
+          module PositiveTestCase_PreconditionShouldBeBoolean{
+             record @serializable T = {person: Party, name: Text};
+              
+             template (this : T) =  {
+              precondition ();                               // precondition should be a boolean
+              signatories Cons @Party ['Bob'] (Nil @Party);
+              observers Cons @Party ['Alice'] (Nil @Party);
+              agreement "Agreement";
+            } ;
+          }
+
+          module PositiveTestCase_SignatoriesShouldBeListParty {
             record @serializable T = {};
 
             template (this : T) =  {
@@ -861,7 +1028,7 @@ class TypingSpec extends AnyWordSpec with TableDrivenPropertyChecks with Matcher
             } ;
           }
 
-          module PositiveTestCase2 {
+          module PositiveTestCase_ObserversShouldBeListParty {
             record @serializable T = {};
 
             template (this : T) =  {
@@ -902,7 +1069,7 @@ class TypingSpec extends AnyWordSpec with TableDrivenPropertyChecks with Matcher
             } ;
           }
 
-          module PositiveTestCase3 {
+          module PositiveTestCase_AgreementShouldBeText {
             record @serializable T = {};
 
             template (this : T) =  {
@@ -940,9 +1107,9 @@ class TypingSpec extends AnyWordSpec with TableDrivenPropertyChecks with Matcher
             } ;
           }
 
-      module PositiveTestCase6 {
+          module PositiveTestCase_KeyBodyShouldBeProperType {
             record @serializable T = {person: Party, name: Text};
-        record @serializable TBis = {person: Text, party: Party};
+            record @serializable Key = {person: Text, party: Party};
          
             template (this : T) =  {
               precondition True;
@@ -950,15 +1117,59 @@ class TypingSpec extends AnyWordSpec with TableDrivenPropertyChecks with Matcher
               observers Cons @Party ['Alice'] (Nil @Party);
               agreement "Agreement";
               choice Ch (self) (i : Unit) : Unit, controllers Cons @Party ['Alice'] (Nil @Party) to upure @Unit ();
-          key @PositiveTestCase6:TBis
+              key @Mod:Key
                 // In the next line, the declared type do not match body
-            (NegativeTestCase:TBis { person = (PositiveTestCase6:T {name} this), party = (PositiveTestCase6:T {person} this) })
+                (PositiveTestCase_KeyBodyShouldBeProperType:Key { 
-            (\ (key: PositiveTestCase6:TBis) -> Cons @Party [(PositiveTestCase6:TBis {party} key), 'Alice'] (Nil @Party)  );
+                  person = (PositiveTestCase_KeyBodyShouldBeProperType:T {name} this), 
+                  party = (PositiveTestCase_KeyBodyShouldBeProperType:T {person} this) 
+                })
+                (\ (key: Mod:Key) -> Cons @Party [(Mod:Key {party} key), 'Alice'] (Nil @Party)  );
               } ;
           }
          
          
-      module PositiveTestCase7 {
+           module PositiveTestCase_MaintainersShouldBeProperType {
+            record @serializable T = {person: Party, name: Text};
+            record @serializable Key = {person: Text, party: Party};
+         
+            template (this : T) =  {
+              precondition True;
+              signatories Cons @Party ['Bob'] (Nil @Party);
+              observers Cons @Party ['Alice'] (Nil @Party);
+              agreement "Agreement";
+              choice Ch (self) (i : Unit) : Unit, controllers Cons @Party ['Alice'] (Nil @Party) to upure @Unit ();
+              key @Mod:Key
+                // In the next line, the declared type do not match body
+                (Mod:Key { 
+                  person = (PositiveTestCase_MaintainersShouldBeProperType:T {name} this), 
+                  party = (PositiveTestCase_MaintainersShouldBeProperType:T {person} this) 
+                })
+                (\ (key: PositiveTestCase_MaintainersShouldBeProperType:Key) -> 
+                  Cons @Party [(PositiveTestCase_MaintainersShouldBeProperType:Key {party} key), 'Alice'] (Nil @Party)  );
+              } ;
+          }
+         
+           module PositiveTestCase_MaintainersShouldBeListParty {
+            record @serializable T = {person: Party, name: Text};
+            record @serializable Key = {person: Text, party: Party};
+         
+            template (this : T) =  {
+              precondition True;
+              signatories Cons @Party ['Bob'] (Nil @Party);
+              observers Cons @Party ['Alice'] (Nil @Party);
+              agreement "Agreement";
+              choice Ch (self) (i : Unit) : Unit, controllers Cons @Party ['Alice'] (Nil @Party) to upure @Unit ();
+              key @Mod:Key
+                // In the next line, the declared type do not match body
+                (Mod:Key { 
+                  person = (PositiveTestCase_MaintainersShouldBeListParty:T {name} this), 
+                  party = (PositiveTestCase_MaintainersShouldBeListParty:T {person} this) 
+                })
+                (\ (key: Mod:Key) -> ()  );
+              } ;
+          }
+         
+          module PositiveTestCase_MaintainersShouldNotUseThis {
             record @serializable T = {person: Party, name: Text};
             record @serializable TBis = {person: Text, party: Party};
          
@@ -968,61 +1179,89 @@ class TypingSpec extends AnyWordSpec with TableDrivenPropertyChecks with Matcher
               observers Cons @Party ['Alice'] (Nil @Party);
               agreement "Agreement";
               choice Ch (self) (i : Unit) : Unit, controllers Cons @Party ['Alice'] (Nil @Party) to upure @Unit ();
-          key @PositiveTestCase7:TBis
+              key @PositiveTestCase_MaintainersShouldNotUseThis:TBis
-            (PositiveTestCase7:TBis { person = (PositiveTestCase7:T {name} this), party = (PositiveTestCase7:T {person} this) })
+                (PositiveTestCase_MaintainersShouldNotUseThis:TBis { 
-            // in the next line, expect PositiveTestCase7:TBis -> List Party
+                  person = (PositiveTestCase_MaintainersShouldNotUseThis:T {name} this), 
-            (\ (key: NegativeTestCase:TBis) -> Cons @Party [(PositiveTestCase7:TBis {party} key), 'Alice'] (Nil @Party)  );
+                  party = (PositiveTestCase_MaintainersShouldNotUseThis:T {person} this) 
-        } ;
+                })
-      }
-
-      module PositiveTestCase8 {
-        record @serializable T = {person: Party, name: Text};
-        record @serializable TBis = {person: Text, party: Party};
-
-        template (this : T) =  {
-          precondition True;
-          signatories Cons @Party ['Bob'] (Nil @Party);
-          observers Cons @Party ['Alice'] (Nil @Party);
-          agreement "Agreement";
-          choice Ch (self) (i : Unit) : Unit, controllers Cons @Party ['Alice'] (Nil @Party) to upure @Unit ();
-          key @PositiveTestCase8:TBis
-            (PositiveTestCase8:TBis { person = (PositiveTestCase8:T {name} this), party = (PositiveTestCase8:T {person} this) })
                 // In the next line, cannot use `this`
-            (\ (key: PositiveTestCase8:TBis) -> Cons @Party [(PositiveTestCase8:T {person} this), 'Alice'] (Nil @Party)  );
+                (\ (key: PositiveTestCase_MaintainersShouldNotUseThis:TBis) -> 
+                  Cons @Party [(PositiveTestCase_MaintainersShouldNotUseThis:T {person} this), 'Alice'] (Nil @Party)  );
             };
           }
      
-      module PositiveTestCase9 {
+          module PositiveCase_InterfaceMethodShouldBeProperType {
-        record @serializable T (a: *) = {x: a};
+            record @serializable T = {person: Party, name: Text};
 
-        // in the next line, T must have kind *.
             template (this : T) =  {
               precondition True;
               signatories Cons @Party ['Bob'] (Nil @Party);
               observers Cons @Party ['Alice'] (Nil @Party);
               agreement "Agreement";
+              choice Ch (self) (i : Unit) : Unit
+                  , controllers Cons @Party ['Alice'] (Nil @Party)
+                  to upure @Unit ();
+              implements Mod:I {
+                method getParties = \(self: PositiveCase_InterfaceMethodShouldBeProperType:T) -> (); // should Be of type 
+              };
             };
           }
         
-      module PositiveTestCase10{
+          module PositiveCase_ImplementsShouldOverrideAllMethods {
-         // template without data type
+            record @serializable T = {person: Party, name: Text};
+
             template (this : T) =  {
               precondition True;
               signatories Cons @Party ['Bob'] (Nil @Party);
               observers Cons @Party ['Alice'] (Nil @Party);
               agreement "Agreement";
+              choice Ch (self) (i : Unit) : Unit
+                  , controllers Cons @Party ['Alice'] (Nil @Party)
+                  to upure @Unit ();
+              implements Mod:I {
+              };
+            };
+          }
+          
+          module PositiveCase_ImplementsShouldOverrideOnlyMethods {
+            record @serializable T = {person: Party, name: Text};
+
+            template (this : T) =  {
+              precondition True;
+              signatories Cons @Party ['Bob'] (Nil @Party);
+              observers Cons @Party ['Alice'] (Nil @Party);
+              agreement "Agreement";
+              choice Ch (self) (i : Unit) : Unit
+                  , controllers Cons @Party ['Alice'] (Nil @Party)
+                  to upure @Unit ();
+              implements Mod:I {
+                method getParties = \(self: PositiveCase_ImplementsShouldOverrideOnlyMethods:T) -> 
+                  Cons @Party [(PositiveCase_ImplementsShouldOverrideOnlyMethods:T {person} this), 'Alice'] (Nil @Party);
+                method getName = \(self: PositiveCase_ImplementsShouldOverrideOnlyMethods:T) -> 
+                  PositiveCase_ImplementsShouldOverrideOnlyMethods:T {name} this;   
+              };
             };
           }
       """
+
+      val nonTemplateTypeCases = Table(
+        "moduleName",
+        "PositiveTestCase_TemplateTypeShouldBeStar",
+        "PositiveTestCase_TemplateTypeShouldBeRecord",
+      )
+
       val typeMismatchCases = Table(
         "moduleName",
-        "PositiveTestCase1",
+        "PositiveTestCase_PreconditionShouldBeBoolean",
-        "PositiveTestCase2",
+        "PositiveTestCase_SignatoriesShouldBeListParty",
+        "PositiveTestCase_ObserversShouldBeListParty",
         "PositiveTestCase_ControllersMustBeListParty",
         "PositiveTestCase_ChoiceObserversMustBeListParty",
-        "PositiveTestCase3",
+        "PositiveTestCase_AgreementShouldBeText",
-        "PositiveTestCase6",
+        "PositiveTestCase_KeyBodyShouldBeProperType",
-        "PositiveTestCase7",
+        "PositiveTestCase_MaintainersShouldBeProperType",
+        "PositiveTestCase_MaintainersShouldBeListParty",
+        "PositiveCase_InterfaceMethodShouldBeProperType",
       )
 
       val kindMismatchCases = Table(
@@ -1031,26 +1270,142 @@ class TypingSpec extends AnyWordSpec with TableDrivenPropertyChecks with Matcher
         "PositiveTestCase5",
       )
 
-      def checkModule(pkg: Package, modName: String) = Typing.checkModule(
+      val pkgIface = PackageInterface(Map(defaultPackageId -> pkg))
-        PackageInterface(Map(defaultPackageId -> pkg)),
+
+      def checkModule(modName: String): Unit = Typing.checkModule(
+        pkgIface,
+        defaultPackageId,
+        pkg.modules(DottedName.assertFromString(modName)),
+      )
+
+      checkModule("NegativeTestCase") shouldBe ()
+      forEvery(nonTemplateTypeCases)(mod =>
+        an[EExpectedTemplatableType] shouldBe thrownBy(checkModule(mod))
+      )
+      an[EUnknownDefinition] shouldBe thrownBy(
+        checkModule("PositiveTestCase_TemplateTypeShouldExists")
+      )
+      forEvery(typeMismatchCases)(mod => an[ETypeMismatch] shouldBe thrownBy(checkModule(mod)))
+      forEvery(kindMismatchCases)(mod => an[EKindMismatch] shouldBe thrownBy(checkModule(mod)))
+      an[EUnknownExprVar] shouldBe thrownBy(
+        checkModule("PositiveTestCase_MaintainersShouldNotUseThis")
+      )
+
+      an[EMissingInterfaceMethod] shouldBe thrownBy(
+        checkModule("PositiveCase_ImplementsShouldOverrideAllMethods")
+      )
+      an[EUnknownInterfaceMethod] shouldBe thrownBy(
+        checkModule("PositiveCase_ImplementsShouldOverrideOnlyMethods")
+      )
+    }
+
+    // TEST_EVIDENCE: Input Validation: ill-formed interfaces are rejected
+    "reject ill formed interface definition" in {
+
+      val pkg =
+        p"""
+          module NegativeTestCase {
+            interface (this : I) =  {
+              precondition True;
+              method getParties: List Party;
+              choice Ch1 (self) (i : Unit) : Unit,
+                  controllers Cons @Party ['Alice'] (Nil @Party)
+                to upure @Unit ();
+              choice Ch2 (self) (i : Unit) : Unit,
+                 controllers call_method @NegativeTestCase:I getParties this,
+                 observers Nil @Party
+               to upure @Unit ();
+              choice Ch3 (self) (i : Unit) : Unit,
+                  controllers call_method @NegativeTestCase:I getParties this,
+                  observers call_method @NegativeTestCase:I getParties this
+                to upure @Unit ();
+            } ;
+          }
+
+          module PositiveTestCase_PreconditionShouldBeBoolean {
+            interface (this : I) =  {
+              precondition (); // Precondition should be a boolean              
+            } ;
+          }
+
+          module PositiveTestCase_ControllersShouldBeListParty {
+            interface (this : I) =  {
+              precondition True;
+              choice Ch (self) (i : Unit) : Unit,
+                  controllers ()                                  // should be of type (List Party)
+                to upure @Unit ();             
+            } ;
+          }
+
+          module PositiveTestCase_ChoiceObserversShouldBeListParty {
+             interface (this : I) =  {
+              precondition True;
+              method getParties: List Party;
+              choice Ch (self) (i : Unit) : Unit,
+                  controllers (call_method @NegativeTestCase:I getParties this),
+                  observers ()                                  // should be of type (List Party)
+                to upure @Unit ();
+            } ;
+          }
+
+          module PositiveTestCase_ChoiceArgumentTypeShouldBeStar {
+             interface (this : I) =  {
+              precondition True;
+              method getParties: List Party;
+              choice Ch (self) (i : List) : Unit,   // the type of i (here List) should be of kind * (here it is * -> *)
+                  controllers (call_method @NegativeTestCase:I getParties this)
+                to upure @Unit ();
+            } ;
+          }
+
+          module PositiveTestCase_ChoiceResultTypeShouldBeStar {
+             interface (this : I) =  {
+              precondition True;
+              method getParties: List Party;
+              choice Ch (self) (i : Unit) : List,   // the return type (here List) should be of kind * (here it is * -> *)
+                  controllers (call_method @NegativeTestCase:I getParties this)
+                to upure @(List) (/\ (tau : *). Nil @tau);
+            } ;
+          }
+      """
+
+      val typeMismatchCases = Table(
+        "moduleName",
+        "PositiveTestCase_PreconditionShouldBeBoolean",
+        "PositiveTestCase_ControllersShouldBeListParty",
+        "PositiveTestCase_ChoiceObserversShouldBeListParty",
+      )
+
+      val kindMismatchCases = Table(
+        "moduleName",
+        "PositiveTestCase_ChoiceArgumentTypeShouldBeStar",
+        "PositiveTestCase_ChoiceResultTypeShouldBeStar",
+      )
+
+      val pkgInterface = PackageInterface(Map(defaultPackageId -> pkg))
+
+      def checkModule(pkg: Package, modName: String) =
+        Typing.checkModule(
+          pkgInterface,
           defaultPackageId,
           pkg.modules(DottedName.assertFromString(modName)),
         )
 
       checkModule(pkg, "NegativeTestCase")
-      forAll(typeMismatchCases)(module =>
+      "NegativeTestCase" shouldBe "NegativeTestCase"
+      forEvery(typeMismatchCases)(module =>
         an[ETypeMismatch] shouldBe thrownBy(checkModule(pkg, module))
-      ) // and
+      )
-      forAll(kindMismatchCases)(module =>
+      forEvery(kindMismatchCases)(module =>
         an[EKindMismatch] shouldBe thrownBy(checkModule(pkg, module))
       )
-      an[EUnknownExprVar] shouldBe thrownBy(checkModule(pkg, "PositiveTestCase8"))
+
-      an[EExpectedTemplatableType] shouldBe thrownBy(checkModule(pkg, "PositiveTestCase9"))
-      an[EUnknownDefinition] shouldBe thrownBy(checkModule(pkg, "PositiveTestCase10"))
     }
 
   }
 
+  "checkModule" should {
+
     // TEST_EVIDENCE: Input Validation: ill-formed exception definitions are rejected
     "reject ill formed exception definitions" in {
 
@@ -1272,7 +1627,10 @@ class TypingSpec extends AnyWordSpec with TableDrivenPropertyChecks with Matcher
       forEvery(positiveTestCases)(mod => a[ValidationError] should be thrownBy checkModule(mod))
     }
 
-  private val pkg =
+  }
+
+  private[this] val env = {
+    val pkg =
       p"""
        module Mod {
          record R (a: *) = { f1: Int64, f2: List a } ;
@@ -1303,6 +1661,30 @@ class TypingSpec extends AnyWordSpec with TableDrivenPropertyChecks with Matcher
            key @Party (Mod:Person {person} this) (\ (p: Party) -> Cons @Party ['Alice', p] (Nil @Party));
          };
 
+         interface (this : I) = {
+              precondition True;
+              method getParties: List Party;
+              choice ChIface (self) (x: Int64) : Decimal,
+                  controllers 'Bob' 
+                to upure @INT64 (DECIMAL_TO_INT64 x);
+         };
+         
+          interface (this : J) = {
+              precondition True;
+         };
+         
+         record @serializable Ti = { person: Party, name: Text };
+         template (this: Ti) = {
+           precondition True;
+           signatories Cons @Party ['Bob'] Nil @Party;
+           observers Cons @Party ['Alice'] (Nil @Party);
+           agreement "Agreement";
+           choice ChTmpl (self) (x: Int64) : Decimal, controllers 'Bob' to upure @INT64 (DECIMAL_TO_INT64 x);
+           implements Mod:I {
+              method getParties = Cons @Party [(Mod:Ti {person} this)] (Nil @Party);
+           };
+         };
+
          record @serializable U = { person: Party, name: Text };
 
          val f : Int64 -> Bool = ERROR @(Bool -> Int64) "not implemented";
@@ -1312,8 +1694,7 @@ class TypingSpec extends AnyWordSpec with TableDrivenPropertyChecks with Matcher
 
        }
      """
-
-  private val env =
     Typing.Env(LV.default, PackageInterface(Map(defaultPackageId -> pkg)), NoContext)
+  }
 
 }

security-evidence.md

@@ -44,20 +44,21 @@
 - ensure expression forms have the correct type: [TypingSpec.scala](daml-lf/validation/src/test/scala/com/digitalasset/daml/lf/validation/TypingSpec.scala#L107)
 - ill-formed create command is rejected: [CommandPreprocessorSpec.scala](daml-lf/engine/src/test/scala/com/digitalasset/daml/lf/engine/CommandPreprocessorSpec.scala#L133)
 - ill-formed create-and-exercise command is rejected: [CommandPreprocessorSpec.scala](daml-lf/engine/src/test/scala/com/digitalasset/daml/lf/engine/CommandPreprocessorSpec.scala#L154)
-- ill-formed exception definitions are rejected: [TypingSpec.scala](daml-lf/validation/src/test/scala/com/digitalasset/daml/lf/validation/TypingSpec.scala#L1054)
+- ill-formed exception definitions are rejected: [TypingSpec.scala](daml-lf/validation/src/test/scala/com/digitalasset/daml/lf/validation/TypingSpec.scala#L1409)
 - ill-formed exercise command is rejected: [CommandPreprocessorSpec.scala](daml-lf/engine/src/test/scala/com/digitalasset/daml/lf/engine/CommandPreprocessorSpec.scala#L138)
 - ill-formed exercise-by-key command is rejected: [CommandPreprocessorSpec.scala](daml-lf/engine/src/test/scala/com/digitalasset/daml/lf/engine/CommandPreprocessorSpec.scala#L145)
-- ill-formed expressions are rejected: [TypingSpec.scala](daml-lf/validation/src/test/scala/com/digitalasset/daml/lf/validation/TypingSpec.scala#L408)
+- ill-formed expressions are rejected: [TypingSpec.scala](daml-lf/validation/src/test/scala/com/digitalasset/daml/lf/validation/TypingSpec.scala#L422)
 - ill-formed fetch command is rejected: [CommandPreprocessorSpec.scala](daml-lf/engine/src/test/scala/com/digitalasset/daml/lf/engine/CommandPreprocessorSpec.scala#L167)
 - ill-formed fetch-by-key command is rejected: [CommandPreprocessorSpec.scala](daml-lf/engine/src/test/scala/com/digitalasset/daml/lf/engine/CommandPreprocessorSpec.scala#L170)
+- ill-formed interfaces are rejected: [TypingSpec.scala](daml-lf/validation/src/test/scala/com/digitalasset/daml/lf/validation/TypingSpec.scala#L1302)
 - ill-formed kinds are rejected: [TypingSpec.scala](daml-lf/validation/src/test/scala/com/digitalasset/daml/lf/validation/TypingSpec.scala#L19)
 - ill-formed lookup command is rejected: [CommandPreprocessorSpec.scala](daml-lf/engine/src/test/scala/com/digitalasset/daml/lf/engine/CommandPreprocessorSpec.scala#L175)
-- ill-formed records are rejected: [TypingSpec.scala](daml-lf/validation/src/test/scala/com/digitalasset/daml/lf/validation/TypingSpec.scala#L1196)
+- ill-formed records are rejected: [TypingSpec.scala](daml-lf/validation/src/test/scala/com/digitalasset/daml/lf/validation/TypingSpec.scala#L1551)
-- ill-formed templates are rejected: [TypingSpec.scala](daml-lf/validation/src/test/scala/com/digitalasset/daml/lf/validation/TypingSpec.scala#L815)
+- ill-formed templates are rejected: [TypingSpec.scala](daml-lf/validation/src/test/scala/com/digitalasset/daml/lf/validation/TypingSpec.scala#L930)
-- ill-formed type synonyms applications are rejected: [TypingSpec.scala](daml-lf/validation/src/test/scala/com/digitalasset/daml/lf/validation/TypingSpec.scala#L1175)
+- ill-formed type synonyms applications are rejected: [TypingSpec.scala](daml-lf/validation/src/test/scala/com/digitalasset/daml/lf/validation/TypingSpec.scala#L1530)
-- ill-formed type synonyms definitions are rejected: [TypingSpec.scala](daml-lf/validation/src/test/scala/com/digitalasset/daml/lf/validation/TypingSpec.scala#L1242)
+- ill-formed type synonyms definitions are rejected: [TypingSpec.scala](daml-lf/validation/src/test/scala/com/digitalasset/daml/lf/validation/TypingSpec.scala#L1597)
 - ill-formed types are rejected: [TypingSpec.scala](daml-lf/validation/src/test/scala/com/digitalasset/daml/lf/validation/TypingSpec.scala#L99)
-- ill-formed variants are rejected: [TypingSpec.scala](daml-lf/validation/src/test/scala/com/digitalasset/daml/lf/validation/TypingSpec.scala#L1219)
+- ill-formed variants are rejected: [TypingSpec.scala](daml-lf/validation/src/test/scala/com/digitalasset/daml/lf/validation/TypingSpec.scala#L1574)
 - well formed create command is accepted: [CommandPreprocessorSpec.scala](daml-lf/engine/src/test/scala/com/digitalasset/daml/lf/engine/CommandPreprocessorSpec.scala#L79)
 - well formed create-and-exercise command is accepted: [CommandPreprocessorSpec.scala](daml-lf/engine/src/test/scala/com/digitalasset/daml/lf/engine/CommandPreprocessorSpec.scala#L98)
 - well formed exercise command is accepted: [CommandPreprocessorSpec.scala](daml-lf/engine/src/test/scala/com/digitalasset/daml/lf/engine/CommandPreprocessorSpec.scala#L84)