Simplified strict validation

cedar-dafny/difftest/main.dfy

@@ -30,7 +30,7 @@ module difftest.main {
   import opened def.ext.fun
   import opened restrictedExpr
   import opened validation.types
-  import opened validation.strict
+  import opened validation.typechecker
   import opened validation.validator
   import opened helpers
 
@@ -582,23 +582,17 @@ module difftest.main {
       case UnknownEntities(_) => "UnknownEntities"
       case ExtensionErr(_) => "ExtensionErr"
       case EmptyLUB => "EmptyLUB"
-    }
-  }
-
-  function strictTypeErrorToString(e: StrictTypeError): string {
-    match e {
-      case TypeError(e1) => typeErrorToString(e1)
-      case TypesMustMatch => "TypesMustMatch"
       case EmptySetForbidden => "EmptySetForbidden"
       case NonLitExtConstructor => "NonLitExtConstructor"
       case NonSingletonLub => "NonSingletonLub"
+      case HierarchyNotRespected => "HierarchyNotRespected"
     }
   }
 
   function validationErrorToString(e: ValidationError): string {
     match e {
       case AllFalse => "AllFalse"
-      case StrictTypeError(e1) => strictTypeErrorToString(e1)
+      case TypeError(e1) => typeErrorToString(e1)
     }
   }
 

cedar-dafny/validation/all.dfy

@@ -14,7 +14,6 @@
  * limitations under the License.
  */
 
-include "strict.dfy"
 include "subtyping.dfy"
 include "typechecker.dfy"
 include "types.dfy"