DAML-LF: LF type checkers reject repeated variables in pattern (digit…

…al-asset#5894) CHANGELOG_BEGIN CHANGELOG_END
kgeonw · May 7, 2020 · 560525b · 560525b
1 parent 1115b39
commit 560525b
Show file tree

Hide file tree

Showing 6 changed files with 17 additions and 8 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
@@ -413,11 +413,12 @@ introCasePattern scrutType patn cont = case patn of
   CPNil -> do
     _ :: Type <- match _TList (EExpectedListType scrutType) scrutType
     cont
-  CPCons headVar tailVar -> do
-    elemType <- match _TList (EExpectedListType scrutType) scrutType
-    -- NOTE(MH): The second 'introExprVar' will catch the bad case @headVar ==
-    -- tailVar@.
-    introExprVar headVar elemType $ introExprVar tailVar (TList elemType) cont
+  CPCons headVar tailVar
+    | headVar == tailVar ->
+        throwWithContext (EClashingPatternVariables headVar)
+    | otherwise -> do
+        elemType <- match _TList (EExpectedListType scrutType) scrutType
+        introExprVar headVar elemType $ introExprVar tailVar (TList elemType) cont
   CPDefault -> cont
   CPSome bodyVar -> do
     bodyType <- match _TOptional (EExpectedOptionalType scrutType) scrutType

diff --git a/compiler/daml-lf-tools/src/DA/Daml/LF/TypeChecker/Env.hs b/compiler/daml-lf-tools/src/DA/Daml/LF/TypeChecker/Env.hs
@@ -74,8 +74,7 @@ emptyGamma :: World -> Version -> Gamma
 emptyGamma = Gamma ContextNone mempty mempty
 
 -- | Run a computation in the current environment extended by a new type
--- variable. Fails if the type variable would shadow some existing type
--- variable.
+-- variable/kind binding. Does not fail on shadowing.
 introTypeVar :: MonadGamma m => TypeVarName -> Kind -> m a -> m a
 introTypeVar v k = local (tvars . at v ?~ k)
 

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
@@ -102,6 +102,7 @@ data Error
   | EExpectedListType      !Type
   | EExpectedOptionalType  !Type
   | EEmptyCase
+  | EClashingPatternVariables !ExprVarName
   | EExpectedTemplatableType !TypeConName
   | EImportCycle           ![ModuleName] -- TODO: implement check for this error
   | ETypeSynCycle          ![TypeSynName]
@@ -260,6 +261,8 @@ instance Pretty Error where
     EExpectedListType foundType ->
       "expected list type, but found: " <> pretty foundType
     EEmptyCase -> "empty case"
+    EClashingPatternVariables varName ->
+      "the variable " <> pretty varName <> " is used more than once in the pattern"
     EExpectedTemplatableType tpl ->
       "expected monomorphic record type in template definition, but found:"
       <-> pretty tpl

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
@@ -611,6 +611,8 @@ private[validation] object Typing {
         }
 
       case CPCons(headVar, tailVar) =>
+        if (headVar == tailVar)
+          throw EClashingPatternVariables(ctx, headVar)
         scrutType match {
           case TList(elemType) =>
             introExprVar(headVar, elemType).introExprVar(tailVar, TList(elemType))

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
@@ -308,11 +308,14 @@ final case class EExpectedOptionType(context: Context, typ: Type) extends Valida
 final case class EEmptyCase(context: Context) extends ValidationError {
   protected def prettyInternal: String = "empty case"
 }
+final case class EClashingPatternVariables(context: Context, varName: ExprVarName)
+    extends ValidationError {
+  protected def prettyInternal: String = s"$varName is used more than one in pattern"
+}
 final case class EExpectedTemplatableType(context: Context, conName: TypeConName)
     extends ValidationError {
   protected def prettyInternal: String =
     s"expected monomorphic record type in template definition, but found: ${conName.qualifiedName}"
-
 }
 final case class EImportCycle(context: Context, modName: List[ModuleName]) extends ValidationError {
   protected def prettyInternal: String = s"cycle in module dependency ${modName.mkString(" -> ")}"

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
@@ -359,6 +359,7 @@ class TypingSpec extends WordSpec with TableDrivenPropertyChecks with Matchers {
         E"Λ (τ : ⋆). λ (e : τ) → (( case e of Nil → () ))",
         // ExpCaseCons
         E"Λ (τ : ⋆). λ (e : τ) → (( case e of Cons x y → () ))",
+        E"Λ (τ : ⋆). λ (e: List τ) → (( case e of Cons x x → () ))",
         // ExpCaseFalse & ExpCaseTrue
         E"Λ (τ : ⋆). λ (e : τ) → (( case e of True → () ))",
         E"Λ (τ : ⋆). λ (e : τ) → (( case e of False → () ))",