interfaces: scala typechecker implementation (#10867)

* interfaces: scala typechecker implementation This is the scala side of the lf typechecker for interfaces. CHANGELOG_BEGIN CHANGELOG_END * added collision check * added exercise/fetch typechecking * review suggestions * added todos for collision/typing scala tests
2024-09-20 01:07:18 +03:00 · 2021-09-16 22:37:33 +02:00 · 2021-09-16 22:37:33 +02:00 · 50291ed61b
commit 50291ed61b
parent cac8391d4c
10 changed files with 203 additions and 33 deletions
--- a/compiler/daml-lf-tools/src/DA/Daml/LF/TypeChecker/Check.hs
+++ b/compiler/daml-lf-tools/src/DA/Daml/LF/TypeChecker/Check.hs
@ -842,26 +842,22 @@ checkTemplate m t@(Template _loc tpl param precond signatories observers text ch
    withPart TPAgreement $ checkExpr text TText
    for_ choices $ \c -> withPart (TPChoice c) $ checkTemplateChoice tcon c
  whenJust mbKey $ checkTemplateKey param tcon
-  forM_ implements $ checkIfaceImplementation (moduleName m) tcon
+  forM_ implements $ checkIfaceImplementation tcon
  where
    withPart p = withContext (ContextTemplate m t p)

-checkIfaceImplementation ::
-     MonadGamma m
-  => ModuleName
-  -> Qualified TypeConName
-  -> Qualified TypeConName
-  -> m ()
-checkIfaceImplementation modName tplTcon ifTcon
-  | Qualified PRSelf m _tconName <- ifTcon
-  , m == modName = do
-    DefInterface {intChoices} <- inWorld $ lookupInterface ifTcon
-    forM_ intChoices $ \InterfaceChoice {ifcName, ifcConsuming, ifcArgType, ifcRetType} -> do
-      TemplateChoice {chcConsuming, chcArgBinder, chcReturnType} <- inWorld $ lookupChoice (tplTcon, ifcName)
-      unless (chcConsuming == ifcConsuming) $ throwWithContext $ EBadInterfaceChoiceImplConsuming ifcName ifcConsuming chcConsuming
-      unless (alphaType (snd chcArgBinder) ifcArgType) $ throwWithContext $ EBadInterfaceChoiceImplArgType ifcName ifcArgType (snd chcArgBinder)
-      unless (alphaType chcReturnType ifcRetType) $ throwWithContext $ EBadInterfaceChoiceImplRetType ifcName ifcRetType chcReturnType
-  | otherwise = throwWithContext $ EForeignInterfaceImplementation ifTcon
+checkIfaceImplementation :: MonadGamma m => Qualified TypeConName -> Qualified TypeConName -> m ()
+checkIfaceImplementation tplTcon ifTcon = do
+  DefInterface {intChoices} <- inWorld $ lookupInterface ifTcon
+  forM_ intChoices $ \InterfaceChoice {ifcName, ifcConsuming, ifcArgType, ifcRetType} -> do
+    TemplateChoice {chcConsuming, chcArgBinder, chcReturnType} <-
+      inWorld $ lookupChoice (tplTcon, ifcName)
+    unless (chcConsuming == ifcConsuming) $
+      throwWithContext $ EBadInterfaceChoiceImplConsuming ifcName ifcConsuming chcConsuming
+    unless (alphaType (snd chcArgBinder) ifcArgType) $
+      throwWithContext $ EBadInterfaceChoiceImplArgType ifcName ifcArgType (snd chcArgBinder)
+    unless (alphaType chcReturnType ifcRetType) $
+      throwWithContext $ EBadInterfaceChoiceImplRetType ifcName ifcRetType chcReturnType

 _checkFeature :: MonadGamma m => Feature -> m ()
 _checkFeature feature = do
--- a/compiler/daml-lf-tools/src/DA/Daml/LF/TypeChecker/Error.hs
+++ b/compiler/daml-lf-tools/src/DA/Daml/LF/TypeChecker/Error.hs
@ -137,7 +137,6 @@ data Error
  | EBadInterfaceChoiceImplConsuming !ChoiceName !Bool !Bool
  | EBadInterfaceChoiceImplArgType !ChoiceName !Type !Type
  | EBadInterfaceChoiceImplRetType !ChoiceName !Type !Type
-  | EForeignInterfaceImplementation !(Qualified TypeConName)

 contextLocation :: Context -> Maybe SourceLoc
 contextLocation = \case
@ -400,7 +399,6 @@ instance Pretty Error where
      , "Expected: " <> pretty ifaceRetType
      , "But got: " <> pretty tplRetType
      ]
-    EForeignInterfaceImplementation tcon -> "The definition and implementation for the interface " <> pretty tcon <> " need to be in the same module."

 prettyConsuming :: Bool -> Doc ann
 prettyConsuming consuming = if consuming then "consuming" else "non-consuming"
--- a/daml-lf/language/src/main/scala/com/digitalasset/daml/lf/language/Interface.scala
+++ b/daml-lf/language/src/main/scala/com/digitalasset/daml/lf/language/Interface.scala
@ -179,6 +179,19 @@ private[lf] class Interface(signatures: PartialFunction[PackageId, PackageSignat
  def lookupTemplate(name: TypeConName): Either[LookupError, TemplateSignature] =
    lookupTemplate(name, Reference.Template(name))

+  private[this] def lookupInterface(
+      name: TypeConName,
+      context: => Reference,
+  ): Either[LookupError, DefInterface] =
+    lookupModule(name.packageId, name.qualifiedName.module, context).flatMap(
+      _.interfaces
+        .get(name.qualifiedName.name)
+        .toRight(LookupError(Reference.Interface(name), context))
+    )
+
+  def lookupInterface(name: TypeConName): Either[LookupError, DefInterface] =
+    lookupInterface(name, Reference.Interface(name))
+
  private[this] def lookupChoice(
      tmpName: TypeConName,
      chName: ChoiceName,
@ -194,6 +207,21 @@ private[lf] class Interface(signatures: PartialFunction[PackageId, PackageSignat
  ): Either[LookupError, TemplateChoiceSignature] =
    lookupChoice(tmpName, chName, Reference.Choice(tmpName, chName))

+  private[this] def lookupInterfaceChoice(
+      tmpName: TypeConName,
+      chName: ChoiceName,
+      context: => Reference,
+  ): Either[LookupError, InterfaceChoice] =
+    lookupInterface(tmpName, context).flatMap(
+      _.choices.get(chName).toRight(LookupError(Reference.Choice(tmpName, chName), context))
+    )
+
+  def lookupInterfaceChoice(
+      tmpName: TypeConName,
+      chName: ChoiceName,
+  ): Either[LookupError, InterfaceChoice] =
+    lookupInterfaceChoice(tmpName, chName, Reference.Choice(tmpName, chName))
+
  private[this] def lookupTemplateKey(
      name: TypeConName,
      context: => Reference,
--- a/daml-lf/language/src/main/scala/com/digitalasset/daml/lf/language/LookupError.scala
+++ b/daml-lf/language/src/main/scala/com/digitalasset/daml/lf/language/LookupError.scala
@ -95,6 +95,10 @@ object Reference {
    override def pretty: String = s"template $tyCon"
  }

+  final case class Interface(tyCon: TypeConName) extends Reference {
+    override def pretty: String = s"interface $tyCon"
+  }
+
  final case class TemplateKey(tyCon: TypeConName) extends Reference {
    override def pretty: String = s"template without contract key $tyCon."
  }
--- a/daml-lf/validation/src/main/scala/com/digitalasset/daml/lf/validation/Collision.scala
+++ b/daml-lf/validation/src/main/scala/com/digitalasset/daml/lf/validation/Collision.scala
@ -63,10 +63,9 @@ private[validation] object Collision {
      case dDef @ Ast.DDataType(_, _, Ast.DataEnum(values)) =>
        val enumDef = NEnumDef(module, defName, dDef)
        enumDef :: values.toList.map(NEnumCon(enumDef, _))
-      case Ast.DDataType(_, _, Ast.DataInterface) =>
-        // TODO https://github.com/digital-asset/daml/issues/10810
-        //  handle interfaces
-        List.empty
+      case iDef @ Ast.DDataType(_, _, Ast.DataInterface) =>
+        val interfaceDef = NInterface(module, defName, iDef)
+        interfaceDef :: List.empty
      case _: Ast.DValue =>
        // ignore values
        List.empty
--- a/daml-lf/validation/src/main/scala/com/digitalasset/daml/lf/validation/NamedEntity.scala
+++ b/daml-lf/validation/src/main/scala/com/digitalasset/daml/lf/validation/NamedEntity.scala
@ -143,4 +143,19 @@ object NamedEntity {
    def pretty: String = s"variant constructor $modName:${dfn.name}:$name"
  }

+  final case class NInterface(
+      module: NModDef,
+      name: DottedName,
+      dfn: Ast.DDataType,
+  ) extends NamedEntity {
+
+    def modName: ModuleName = module.name
+
+    val fullyResolvedName: DottedName =
+      module.fullyResolvedName ++ name.toUpperCase
+
+    override def toString: String = s"NInterface($modName:$name)"
+
+    def pretty: String = s"interface $modName:$name"
+  }
 }
--- a/daml-lf/validation/src/main/scala/com/digitalasset/daml/lf/validation/Typing.scala
+++ b/daml-lf/validation/src/main/scala/com/digitalasset/daml/lf/validation/Typing.scala
@ -273,7 +273,7 @@ private[validation] object Typing {
          case DataEnum(values) =>
            env.checkEnumType(tyConName, params, values)
          case DataInterface =>
-            ()
+            env.checkInterfaceType(tyConName, params)
        }
      case (dfnName, dfn: DValue) =>
        Env(langVersion, interface, ContextDefValue(pkgId, mod.name, dfnName)).checkDValue(dfn)
@ -304,6 +304,12 @@ private[validation] object Typing {
          throw EExpectedExceptionableType(env.ctx, tyConName)
      }
    }
+    mod.interfaces.foreach { case (ifaceName, defInterface) =>
+      // uniquess of choice names is already checked on construction of the choice map.
+      val tyConName = TypeConName(pkgId, QualifiedName(mod.name, ifaceName))
+      val env = Env(langVersion, interface, ContextDefInterface(tyConName), Map.empty)
+      defInterface.choices.values.foreach { env.checkIfaceChoice(_) }
+    }
  }

  case class Env(
@ -369,6 +375,14 @@ private[validation] object Typing {
      checkUniq[Name](values.iterator, EDuplicateEnumCon(ctx, _))
    }

+    def checkInterfaceType[X](
+        tyConName: => TypeConName,
+        params: ImmArray[X],
+    ): Unit = {
+      if (params.nonEmpty) throw EIllegalHigherInterfaceType(ctx, tyConName)
+      val _ = handleLookup(ctx, interface.lookupInterface(tyConName))
+    }
+
    def checkDValue(dfn: DValue): Unit = dfn match {
      case DValue(typ, _, body, isTest) =>
        checkType(typ, KStar)
@ -417,7 +431,16 @@ private[validation] object Typing {
      }

    def checkTemplate(tplName: TypeConName, template: Template): Unit = {
-      val Template(param, precond, signatories, agreementText, choices, observers, mbKey, _) =
+      val Template(
+        param,
+        precond,
+        signatories,
+        agreementText,
+        choices,
+        observers,
+        mbKey,
+        implementations,
+      ) =
        template
      val env = introExprVar(param, TTyCon(tplName))
      env.checkExpr(precond, TBool)
@ -431,6 +454,46 @@ private[validation] object Typing {
        checkExpr(key.maintainers, TFun(key.typ, TParties))
        ()
      }
+      implementations.foreach(env.checkIfaceImplementation(tplName, _))
+    }
+
+    def checkIfaceChoice(choice: InterfaceChoice): Unit = {
+      checkType(choice.argType, KStar)
+      checkType(choice.returnType, KStar)
+    }
+
+    def checkIfaceImplementation(tplTcon: TypeConName, ifaceTcon: TypeConName): Unit = {
+      val DefInterface(choices) = handleLookup(ctx, interface.lookupInterface(ifaceTcon))
+      choices.values.foreach { case InterfaceChoice(name, consuming, argType, returnType) =>
+        val tplChoice = handleLookup(ctx, interface.lookupChoice(tplTcon, name))
+        if (tplChoice.consuming != consuming)
+          throw EBadInterfaceChoiceImplConsuming(
+            ctx,
+            ifaceTcon,
+            tplTcon,
+            name,
+            consuming,
+            tplChoice.consuming,
+          )
+        if (!alphaEquiv(tplChoice.argBinder._2, argType))
+          throw EBadInterfaceChoiceImplArgType(
+            ctx,
+            ifaceTcon,
+            tplTcon,
+            name,
+            argType,
+            tplChoice.argBinder._2,
+          )
+        if (!alphaEquiv(tplChoice.returnType, returnType))
+          throw EBadInterfaceChoiceImplRetType(
+            ctx,
+            ifaceTcon,
+            tplTcon,
+            name,
+            returnType,
+            tplChoice.returnType,
+          )
+      }
    }

    def checkDefException(excepName: TypeConName, defException: DefException): Unit = {
@ -736,8 +799,7 @@ private[validation] object Typing {
                    introPatternEnum(scrutTCon, cons),
                  )
                case DataInterface =>
-                  // TODO https://github.com/digital-asset/daml/issues/10810
-                  sys.error("Interface not supported")
+                  (defaultExpectedPatterns, introOnlyPatternDefault(scrutType))
              }
          }
        case TUnit =>
@ -833,6 +895,18 @@ private[validation] object Typing {
      TUpdate(choice.returnType)
    }

+    private def typeOfExerciseInterface(
+        tpl: TypeConName,
+        chName: ChoiceName,
+        cid: Expr,
+        arg: Expr,
+    ): Type = {
+      val choice = handleLookup(ctx, interface.lookupInterfaceChoice(tpl, chName))
+      checkExpr(cid, TContractId(TTyCon(tpl)))
+      checkExpr(arg, choice.argType)
+      TUpdate(choice.returnType)
+    }
+
    private def typeOfExerciseByKey(
        tmplId: TypeConName,
        chName: ChoiceName,
@ -851,6 +925,12 @@ private[validation] object Typing {
      TUpdate(TTyCon(tpl))
    }

+    private def typeOfFetchInterface(tpl: TypeConName, cid: Expr): Type = {
+      handleLookup(ctx, interface.lookupInterface(tpl))
+      checkExpr(cid, TContractId(TTyCon(tpl)))
+      TUpdate(TTyCon(tpl))
+    }
+
    private def checkByKey(tmplId: TypeConName, key: Expr): Unit = {
      val tmplKey = handleLookup(ctx, interface.lookupTemplateKey(tmplId))
      checkExpr(key, tmplKey.typ)
@ -867,16 +947,14 @@ private[validation] object Typing {
        typeOfCreate(tpl, arg)
      case UpdateExercise(tpl, choice, cid, arg) =>
        typeOfExercise(tpl, choice, cid, arg)
-      case UpdateExerciseInterface(_, _, _, _) =>
-        // TODO https://github.com/digital-asset/daml/issues/10810
-        sys.error("Interface not supported")
+      case UpdateExerciseInterface(tpl, choice, cid, arg) =>
+        typeOfExerciseInterface(tpl, choice, cid, arg)
      case UpdateExerciseByKey(tpl, choice, key, arg) =>
        typeOfExerciseByKey(tpl, choice, key, arg)
      case UpdateFetch(tpl, cid) =>
        typeOfFetch(tpl, cid)
-      case UpdateFetchInterface(_, _) =>
-        // TODO https://github.com/digital-asset/daml/issues/10810
-        sys.error("Interface not supported")
+      case UpdateFetchInterface(tpl, cid) =>
+        typeOfFetchInterface(tpl, cid)
      case UpdateGetTime =>
        TUpdate(TTimestamp)
      case UpdateEmbedExpr(typ, exp) =>
--- a/daml-lf/validation/src/main/scala/com/digitalasset/daml/lf/validation/ValidationError.scala
+++ b/daml-lf/validation/src/main/scala/com/digitalasset/daml/lf/validation/ValidationError.scala
@ -27,6 +27,9 @@ final case class ContextTemplate(tycon: TypeConName) extends Context {
 final case class ContextDefException(tycon: TypeConName) extends Context {
  def pretty: String = s"exception definition ${tycon.qualifiedName}"
 }
+final case class ContextDefInterface(tycon: TypeConName) extends Context {
+  def pretty: String = s"interface definition ${tycon.qualifiedName}"
+}
 final case class ContextDefValue(ref: ValueRef) extends Context {
  def pretty: String = s"value definition ${ref.qualifiedName}"
 }
@ -366,6 +369,10 @@ final case class EIllegalHigherEnumType(context: Context, defn: TypeConName)
    extends ValidationError {
  protected def prettyInternal: String = s"illegal higher order enum type"
 }
+final case class EIllegalHigherInterfaceType(context: Context, defn: TypeConName)
+    extends ValidationError {
+  protected def prettyInternal: String = s"illegal higher interface type"
+}
 final case class EIllegalEnumArgument(context: Context, typ: Type) extends ValidationError {
  protected def prettyInternal: String = s"illegal non Unit enum argument"
 }
@ -409,3 +416,44 @@ final case class EModuleVersionDependencies(

  override def context: Context = NoContext
 }
+
+final case class EBadInterfaceChoiceImplConsuming(
+    context: Context,
+    iface: TypeConName,
+    template: TypeConName,
+    choice: ChoiceName,
+    ifaceConsuming: Boolean,
+    tplConsuming: Boolean,
+) extends ValidationError {
+
+  def prettyConsuming(consuming: Boolean): String = if (consuming) "consuming" else "non-consuming"
+
+  override protected def prettyInternal: String =
+    s"The implementation of the choice $choice of interface $iface in template $template differs from the interface definition in the consuming/non-consuming behaviour.\nExpected: ${prettyConsuming(ifaceConsuming)}\n But got: ${prettyConsuming(tplConsuming)}"
+}
+
+final case class EBadInterfaceChoiceImplArgType(
+    context: Context,
+    iface: TypeConName,
+    template: TypeConName,
+    choice: ChoiceName,
+    ifaceArgType: Type,
+    tplArgType: Type,
+) extends ValidationError {
+
+  override protected def prettyInternal: String =
+    s"The implementation of the choice $choice of interface $iface in template $template differs from the interface definition in the argument type.\nExpected: $ifaceArgType\n But got: $tplArgType"
+}
+
+final case class EBadInterfaceChoiceImplRetType(
+    context: Context,
+    iface: TypeConName,
+    template: TypeConName,
+    choice: ChoiceName,
+    ifaceRetType: Type,
+    tplRetType: Type,
+) extends ValidationError {
+
+  override protected def prettyInternal: String =
+    s"The implementation of the choice $choice of interface $iface in template $template differs from the interface definition in the return type.\nExpected: $ifaceRetType\n But got: $tplRetType"
+}
--- a/daml-lf/validation/src/test/scala/com/digitalasset/daml/lf/validation/CollisionSpec.scala
+++ b/daml-lf/validation/src/test/scala/com/digitalasset/daml/lf/validation/CollisionSpec.scala
@ -15,6 +15,7 @@ class CollisionSpec extends AnyWordSpec with Matchers with TableDrivenPropertyCh
  def check(pkg: Package): Unit =
    Collision.checkPackage(defaultPackageId, pkg)

+  // TODO add check for collision of interface names.
  "Collision validation" should {

    "detect collisions of record fields" in {
--- a/daml-lf/validation/src/test/scala/com/digitalasset/daml/lf/validation/TypingSpec.scala
+++ b/daml-lf/validation/src/test/scala/com/digitalasset/daml/lf/validation/TypingSpec.scala
@ -322,6 +322,7 @@ 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" ->
@ -799,6 +800,8 @@ class TypingSpec extends AnyWordSpec with TableDrivenPropertyChecks with Matcher
      }
    }

+    //TODO add check for interface definitions.
+    //TODO add check for interface implementations.
    "reject ill formed template definition" in {

      val pkg =