NullReferenceException when using :- with the type-system-refresh option

[amaurremi]

Dafny version

4.3.0

Code to produce this issue

datatype Option<T> = Some(val: T) | None {
    predicate  IsFailure() {
       None?
    }
    
    function  PropagateFailure<V>(): Option<V>
      requires None?
    {
      None
    }

    function Extract(): T
      requires Some?
    {
      val
    }
}

function foo(): Option<bool> {
  var x: Option<bool> :- None;
  None
}

Command to run and resulting output

dafny /typeSystemRefresh:1 Test.dfy

Resulting in

Unhandled exception. System.AggregateException: One or more errors occurred. (One or more errors occurred. (One or more errors occurred. (Object reference not set to an instance of an object.)))
 ---> System.AggregateException: One or more errors occurred. (One or more errors occurred. (Object reference not set to an instance of an object.))
 ---> System.AggregateException: One or more errors occurred. (Object reference not set to an instance of an object.)
 ---> System.NullReferenceException: Object reference not set to an instance of an object.
   at Microsoft.Dafny.PreTypeResolver.<>c__DisplayClass58_7.<ResolveExpression>b__6()
   at Microsoft.Dafny.PreTypeConstraints.ApplyGuardedConstraints()
   at Microsoft.Dafny.PreTypeConstraints.PartiallySolveTypeConstraints(String printableContext, Boolean makeDecisions)
   at Microsoft.Dafny.PreTypeConstraints.SolveAllTypeConstraints(String printableContext)
   at Microsoft.Dafny.PreTypeResolver.ResolveFunction(Function f)
   at Microsoft.Dafny.PreTypeResolver.ResolveMember(MemberDecl member)
   at Microsoft.Dafny.PreTypeResolver.ResolveDeclarationBody(Declaration d)
   at Microsoft.Dafny.PreTypeResolver.ResolveDeclarations(List`1 declarations, ModuleResolver resolver, Boolean firstPhaseOnly)
   at Microsoft.Dafny.ModuleResolver.ResolveTopLevelDecls_Core(List`1 declarations, Graph`1 datatypeDependencies, Graph`1 codatatypeDependencies, String moduleName, Boolean isAnExport)
   at Microsoft.Dafny.ModuleDefinition.Resolve(ModuleSignature sig, ModuleResolver resolver, Boolean isAnExport)
   at Microsoft.Dafny.LiteralModuleDecl.Resolve(ModuleResolver resolver, CompilationData compilation)
   at Microsoft.Dafny.ModuleResolver.ResolveModuleDeclaration(CompilationData compilation, ModuleDecl decl)
   at Microsoft.Dafny.ProgramResolver.ResolveModuleDeclaration(CompilationData compilation, ModuleDecl decl)
   at Microsoft.Dafny.ProgramResolver.Resolve(CancellationToken cancellationToken)
   at Microsoft.Dafny.DafnyMain.<>c__DisplayClass5_0.<Resolve>b__0()
   at System.Threading.Tasks.Task.InnerInvoke()
   at System.Threading.Tasks.Task.<>c.<.cctor>b__272_0(Object obj)
   at System.Threading.ExecutionContext.RunInternal(ExecutionContext executionContext, ContextCallback callback, Object state)

### What happened?

It appears that using a failure-with-update statement with the `typeSystemRefresh` option results in a null-reference exception. 

The error appears to originate from [referencing](https://github.com/dafny-lang/dafny/blob/master/Source/DafnyCore/Resolver/PreType/PreTypeResolve.Expressions.cs#L616) a field on the type of the right-hand side of the update statement, which is set to null.


### What type of operating system are you experiencing the problem on?

Mac