Use full type declaration names in Boogie generation (#5030)

### Description

Use full type declaration names in Boogie generation. Failing to do this
was leading to spurious warnings about proofs due to contradictory
assumptions.

Fixes #5029

### How has this been tested?

`Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/github-issue-5029.dfy`

By submitting this pull request, I confirm that my contribution is made
under the terms of the MIT license.

Source/DafnyCore/AST/Members/ICodeContext.cs

@@ -163,6 +163,8 @@ public NoContext(ModuleDefinition module) {
 public interface RedirectingTypeDecl : ICallable {
   string Name { get; }
 
+  string FullDafnyName { get; }
+
   IToken tok { get; }
   Attributes Attributes { get; }
   ModuleDefinition Module { get; }

Source/DafnyCore/Verifier/BoogieGenerator.Types.cs

@@ -1379,7 +1379,7 @@ void AddWellformednessCheck(RedirectingTypeDecl decl) {
     Contract.Requires(currentModule == null && codeContext == null && isAllocContext == null);
     Contract.Ensures(currentModule == null && codeContext == null && isAllocContext == null);
 
-    proofDependencies.SetCurrentDefinition(MethodVerboseName(decl.Name, MethodTranslationKind.SpecWellformedness));
+    proofDependencies.SetCurrentDefinition(MethodVerboseName(decl.FullDafnyName, MethodTranslationKind.SpecWellformedness));
 
     if (!InVerificationScope(decl)) {
       // Checked in other file
@@ -1417,7 +1417,7 @@ void AddWellformednessCheck(RedirectingTypeDecl decl) {
     var proc = new Bpl.Procedure(decl.tok, name, new List<Bpl.TypeVariable>(),
       inParams, new List<Variable>(),
       false, req, mod, new List<Bpl.Ensures>(), etran.TrAttributes(decl.Attributes, null));
-    AddVerboseNameAttribute(proc, decl.Name, MethodTranslationKind.SpecWellformedness);
+    AddVerboseNameAttribute(proc, decl.FullDafnyName, MethodTranslationKind.SpecWellformedness);
     sink.AddTopLevelDeclaration(proc);
 
     // TODO: Can a checksum be inserted here?

Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/github-issue-5029.dfy

@@ -0,0 +1,11 @@
+// RUN: %verify "%s" --warn-contradictory-assumptions
+abstract module Digit {
+  function BASE(): nat
+    ensures BASE() > 1
+
+  type digit = i: nat | 0 <= i < BASE()
+}
+
+module M refines Digit {
+    function BASE(): nat { 32 }
+}

Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/github-issue-5029.dfy.expect

@@ -0,0 +1 @@
+Dafny program verifier finished with 4 verified, 0 errors