From 50291ed61bb2933821018e0e2acb8c450ef55838 Mon Sep 17 00:00:00 2001 From: Robin Krom Date: Thu, 16 Sep 2021 22:37:33 +0200 Subject: [PATCH] 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 --- .../src/DA/Daml/LF/TypeChecker/Check.hs | 30 +++--- .../src/DA/Daml/LF/TypeChecker/Error.hs | 2 - .../daml/lf/language/Interface.scala | 28 ++++++ .../daml/lf/language/LookupError.scala | 4 + .../daml/lf/validation/Collision.scala | 7 +- .../daml/lf/validation/NamedEntity.scala | 15 +++ .../daml/lf/validation/Typing.scala | 98 +++++++++++++++++-- .../daml/lf/validation/ValidationError.scala | 48 +++++++++ .../daml/lf/validation/CollisionSpec.scala | 1 + .../daml/lf/validation/TypingSpec.scala | 3 + 10 files changed, 203 insertions(+), 33 deletions(-) diff --git a/compiler/daml-lf-tools/src/DA/Daml/LF/TypeChecker/Check.hs b/compiler/daml-lf-tools/src/DA/Daml/LF/TypeChecker/Check.hs index f990bd540d..a0f4780667 100644 --- 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 diff --git a/compiler/daml-lf-tools/src/DA/Daml/LF/TypeChecker/Error.hs b/compiler/daml-lf-tools/src/DA/Daml/LF/TypeChecker/Error.hs index 1bc86ab661..993e4d2cf9 100644 --- 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" diff --git 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 index 4092f5edc5..1e38dfc245 100644 --- 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, diff --git 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 index 83905222d7..5ed407cac8 100644 --- 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." } diff --git 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 index 790517d34a..60c3c709a3 100644 --- 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 diff --git 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 index 37dc0c9f6e..aeb7eaee00 100644 --- 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" + } } diff --git 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 index 112807288d..5f914796ba 100644 --- 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) => diff --git 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 index 2b60614702..2d9359e652 100644 --- 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" +} diff --git 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 index 915fdc60a3..c5a4110057 100644 --- 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 { diff --git 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 index 0387f8bd36..dbe9a31941 100644 --- 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 =