diff --git a/Source/DafnyCore/Resolver.cs b/Source/DafnyCore/Resolver.cs index 22359c50d24..7991bb580cb 100644 --- a/Source/DafnyCore/Resolver.cs +++ b/Source/DafnyCore/Resolver.cs @@ -2750,7 +2750,11 @@ public void ResolveTopLevelDecls_Core(List/*!*/ declarations, if (field.Rhs != null) { var ec = reporter.Count(ErrorLevel.Error); scope.PushMarker(); - scope.AllowInstance = currentClass is ClassDecl cd && !cd.IsDefaultClass; + if ((currentClass is ClassDecl cd && !cd.IsDefaultClass) || currentClass is DatatypeDecl || + currentClass is OpaqueTypeDecl) { + } else { + scope.AllowInstance = false; + } ResolveExpression(field.Rhs, resolutionContext); scope.PopMarker(); if (reporter.Count(ErrorLevel.Error) == ec) {