Fix reveal statement inside witness bug (#5887)

Fixes #5882

### How has this been tested?
CLI test added

<small>By submitting this pull request, I confirm that my contribution
is made under the terms of the [MIT
license](https://github.com/dafny-lang/dafny/blob/master/LICENSE.txt).</small>

Source/DafnyCore/AST/TypeDeclarations/TypeSynonymDeclBase.cs

@@ -77,10 +77,7 @@ bool RedirectingTypeDecl.ConstraintIsCompilable {
   Expression RedirectingTypeDecl.Witness { get { return null; } }
   VerificationIdGenerator RedirectingTypeDecl.IdGenerator { get { return IdGenerator; } }
 
-  public bool ContainsHide {
-    get => throw new NotSupportedException();
-    set => throw new NotSupportedException();
-  }
+  public bool ContainsHide { get; set; }
 
   bool ICodeContext.IsGhost => throw new NotSupportedException(); // if .IsGhost is needed, the object should always be wrapped in an CodeContextWrapper
   List<TypeParameter> ICodeContext.TypeArgs => TypeArgs;

Source/IntegrationTests/TestFiles/LitTests/LitTest/ast/reveal/revealInBlock.dfy

@@ -99,4 +99,8 @@ method hide()
   decreases *
 {
   hide();  
-}
+}
+
+opaque function f(): int { 0 }
+
+type T = x: int | true witness (reveal f(); 0)

Source/IntegrationTests/TestFiles/LitTests/LitTest/ast/reveal/revealInBlock.dfy.expect

@@ -9,4 +9,4 @@ revealInBlock.dfy(81,10): Error: assertion might not hold
 revealInBlock.dfy(91,14): Error: assertion might not hold
 revealInBlock.dfy(94,10): Error: assertion might not hold
 
-Dafny program verifier finished with 19 verified, 10 errors
+Dafny program verifier finished with 20 verified, 10 errors

Source/IntegrationTests/TestFiles/LitTests/LitTest/ast/reveal/revealInExpression.dfy

@@ -1,6 +1,5 @@
-// RUN: echo 'turned off for the moment'
-// NOOP: ! %verify --type-system-refresh --allow-axioms --isolate-assertions %s > %t
-// NOOP: %diff "%s.expect" "%t"
+// RUN: ! %verify --type-system-refresh --allow-axioms --isolate-assertions %s > %t
+// RUN: %diff "%s.expect" "%t"
 
 function P(x: int): bool {
   true
@@ -15,15 +14,15 @@ method RevealExpressionScope()
 {
   hide *;
   var a := (reveal P; assert P(0); true);
-  assert P(1); // error
+  assert P(1); // no error, expression leaks.
   var b := (var x := (reveal P; assert P(2); true); 
-            assert P(3); x); // error
+            assert P(3); x); // no error, expression leaks.
   var c := (var x: bool :| (reveal P; assert P(4); x); 
-            assert P(5); x); // error
+            assert P(5); x); // no error, expression leaks.
   var d := (forall x: int :: reveal P; assert P(x); Q(x)) || 
-           (assert P(7); true); // error
+           (assert P(7); true); // no error, expression leaks.
   var e := ((x: bool) => reveal P; assert P(7); x)(true) || 
-           (assert P(8); true); // error
+           (assert P(8); true); // no error, expression leaks.
 }
 
 function MatchExpressionScope(x: int): int {
@@ -34,6 +33,6 @@ function MatchExpressionScope(x: int): int {
     case _ =>
       assert P(0); 2 // error
   };
-  assert P(1); // error
+  assert P(1); // no error, expression leaks.
   x
 }

Source/IntegrationTests/TestFiles/LitTests/LitTest/ast/reveal/revealInExpression.dfy.expect

@@ -1,8 +1,3 @@
-revealInExpression.dfy(18,10): Error: assertion might not hold
-revealInExpression.dfy(20,20): Error: assertion might not hold
-revealInExpression.dfy(22,20): Error: assertion might not hold
-revealInExpression.dfy(24,20): Error: assertion might not hold
-revealInExpression.dfy(35,14): Error: assertion might not hold
-revealInExpression.dfy(37,10): Error: assertion might not hold
+revealInExpression.dfy(34,14): Error: assertion might not hold
 
-Dafny program verifier finished with 12 verified, 6 errors
+Dafny program verifier finished with 15 verified, 1 error

docs/dev/news/5882.fix

@@ -0,0 +1 @@
+Enable using reveal statement expression inside witness expressions