More DAML LF type synonym validation tests (digital-asset#4181)

* more type synonym validation tests, including negative tests * check type synonym definitions are well formed changelog_begin changelog_end
axman6 · Jan 24, 2020 · 706464d · 706464d
1 parent 3a4d356
commit 706464d
Show file tree

Hide file tree

Showing 3 changed files with 66 additions and 2 deletions.
diff --git a/daml-lf/parser/src/main/scala/com/digitalasset/daml/lf/testing/parser/Implicits.scala b/daml-lf/parser/src/main/scala/com/digitalasset/daml/lf/testing/parser/Implicits.scala
@@ -5,7 +5,7 @@ package com.digitalasset.daml.lf.testing
 package parser
 
 import com.digitalasset.daml.lf.data.{Numeric, Ref}
-import com.digitalasset.daml.lf.language.Ast.{Expr, Kind, Package, Type}
+import com.digitalasset.daml.lf.language.Ast.{Expr, Kind, Module, Package, Type}
 
 object Implicits {
 
@@ -26,6 +26,9 @@ object Implicits {
     def p[P](args: Any*)(implicit parserParameters: ParserParameters[P]): Package =
       interpolate(new ModParser[P](parserParameters).pkg)(args)
 
+    def m[P](args: Any*)(implicit parserParameters: ParserParameters[P]): Module =
+      interpolate(new ModParser[P](parserParameters).mod)(args)
+
     @SuppressWarnings(Array("org.wartremover.warts.Any"))
     def n(args: Any*): Ref.Name =
       Ref.Name.assertFromString(sc.standardInterpolator(identity, args.map(prettyPrint)))

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
@@ -265,7 +265,11 @@ private[validation] object Typing {
         }
       case (dfnName, dfn: DValue) =>
         Env(mod.languageVersion, world, ContextDefValue(pkgId, mod.name, dfnName)).checkDValue(dfn)
-      case (_, _: DTypeSyn) => // TODO #3616: check type synonyms
+      case (dfnName, DTypeSyn(params, replacementTyp)) =>
+        val env =
+          Env(mod.languageVersion, world, ContextTemplate(pkgId, mod.name, dfnName), params.toMap)
+        checkUniq[TypeVarName](params.keys, EDuplicateTypeParam(env.ctx, _))
+        env.checkType(replacementTyp, KStar)
     }
 
   case class Env(

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
@@ -815,13 +815,68 @@ class TypingSpec extends WordSpec with TableDrivenPropertyChecks with Matchers {
         T"(( (forall (a:*) . a) → Unit ))",
       E"(( λ (e : forall (a:*) . |Mod:SynIdentity a|) → () )) " ->
         T"(( (forall (a:*) . a) → Unit ))",
+      E"(( λ (e : |Mod:SynHigh List|) → () )) " ->
+        T"(( List Int64 → Unit ))",
+      E"(( λ (e : |Mod:SynHigh2 GenMap Party|) → () )) " ->
+        T"(( (GenMap Party Party) → Unit ))",
     )
 
     forEvery(testCases) { (exp: Expr, expectedType: Type) =>
       env.typeOf(exp) shouldBe expectedType
     }
   }
 
+  "reject ill formed type synonym application" in {
+    val testCases = Table(
+      "badly formed type synonym application",
+      E"(( λ (e : |Mod:MissingSyn|) → () )) ",
+      E"(( λ (e : |Mod:SynInt Text|) → () )) ",
+      E"(( λ (e : |Mod:SynIdentity|) → () )) ",
+      E"(( λ (e : |Mod:SynIdentity Text Text|) → () )) ",
+      E"(( λ (e : |Mod:SynPair Text|) → () )) ",
+      E"(( λ (e : |Mod:SynPair Text Text Text|) → () )) ",
+      E"(( λ (e : |Mod:SynIdentity List|) → () )) ",
+      E"(( λ (e : |Mod:SynHigh Text|) → () )) ",
+      E"(( λ (e : |Mod:SynHigh GenMap|) → () )) ",
+      E"(( λ (e : |Mod:SynHigh2 List Party|) → () )) ",
+    )
+
+    forEvery(testCases) { exp =>
+      a[ValidationError] should be thrownBy env.typeOf(exp)
+    }
+  }
+
+  "reject ill formed type synonym definitions" in {
+    val testCases = Table(
+      "module"
+        -> "reject",
+      //Good
+      m"""module Mod { synonym S = Int64 ; }""" -> false,
+      m"""module Mod { synonym S a = a ; }""" -> false,
+      m"""module Mod { synonym S a b = a ; }""" -> false,
+      m"""module Mod { synonym S (f: *) = f ; }""" -> false,
+      m"""module Mod { synonym S (f: * -> *) = f Int64; }""" -> false,
+      //Bad
+      m"""module Mod { synonym S = a ; }""" -> true,
+      m"""module Mod { synonym S a = b ; }""" -> true,
+      m"""module Mod { synonym S a a = a ; }""" -> true,
+      m"""module Mod { synonym S = List ; }""" -> true,
+      m"""module Mod { synonym S (f: * -> *) = f ; }""" -> true,
+      m"""module Mod { synonym S (f: *) = f Int64; }""" -> true,
+    )
+
+    forEvery(testCases) { (mod: Module, rejected: Boolean) =>
+      val world = new World(Map())
+
+      if (rejected)
+        a[ValidationError] should be thrownBy
+          Typing.checkModule(world, defaultPackageId, mod)
+      else
+        Typing.checkModule(world, defaultPackageId, mod)
+      ()
+    }
+  }
+
   private val pkg =
     p"""
        module Mod {
@@ -838,6 +893,8 @@ class TypingSpec extends WordSpec with TableDrivenPropertyChecks with Matchers {
          synonym SynSelfFunc (a: *) = a -> a ;
          synonym SynFunc (a: *) (b: *) = a -> b ;
          synonym SynPair (a: *) (b: *) = <one: a, two: b>;
+         synonym SynHigh (f: * -> *) = f Int64 ;
+         synonym SynHigh2 (f: * -> * -> *) (a: *) = f a a ;
 
          record T = {person: Party, name: Text };
          template (this : T) =  {