Set grounding-ctor-type-parameters and test compilation

Source/DafnyCore/AST/TypeDeclarations/IndDatatypeDecl.cs

@@ -1,17 +1,33 @@
 using System.Collections.Generic;
 using System.Diagnostics.Contracts;
+using System.Linq;
 
 namespace Microsoft.Dafny;
 
 public class IndDatatypeDecl : DatatypeDecl {
  public override string WhatKind { get { return "datatype"; } }
- public DatatypeCtor GroundingCtor;  // set during resolution
+ [FilledInDuringResolution] public DatatypeCtor GroundingCtor; // set during resolution (possibly to null)
 
  public override DatatypeCtor GetGroundingCtor() {
- return GroundingCtor;
+ return GroundingCtor ?? Ctors.FirstOrDefault(ctor => ctor.IsGhost, Ctors[0]);;
  }
 
- public bool[] TypeParametersUsedInConstructionByGroundingCtor; // set during resolution; has same length as the number of type arguments
+ private bool[] typeParametersUsedInConstructionByGroundingCtor = null;
+
+ public bool[] TypeParametersUsedInConstructionByGroundingCtor {
+ get {
+ if (typeParametersUsedInConstructionByGroundingCtor == null) {
+ typeParametersUsedInConstructionByGroundingCtor = new bool[TypeArgs.Count];
+ for (var i = 0; i < typeParametersUsedInConstructionByGroundingCtor.Length; i++) {
+ typeParametersUsedInConstructionByGroundingCtor[i] = true;
+ }
+ }
+ return typeParametersUsedInConstructionByGroundingCtor;
+ }
+ set {
+ typeParametersUsedInConstructionByGroundingCtor = value;
+ }
+ }
 
  public enum ES { NotYetComputed, Never, ConsultTypeArguments }
  public ES EqualitySupport = ES.NotYetComputed;

Source/DafnyCore/Resolver/ModuleResolver.cs

@@ -2941,7 +2941,7 @@ public ReportOtherAdditionalInformation_Visitor(ModuleResolver resolver)
  }
 
  /// <summary>
- /// Check that the datatype has some constructor all whose argument types can be constructed.
+ /// Check if the datatype has some constructor all whose argument types can be constructed.
  /// Returns 'true' and sets dt.GroundingCtor if that is the case.
  /// </summary>
  bool ComputeGroundingCtor(IndDatatypeDecl dt) {

Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-4939c.dfy

@@ -0,0 +1,16 @@
+// RUN: %testDafnyForEachCompiler "%s" -- --general-traits=datatype
+
+module NoAutoInit {
+ trait GeneralTrait { }
+ trait ReferenceTrait extends object { }
+
+ datatype A = A(g: GeneralTrait)
+ datatype B = B(h: ReferenceTrait)
+
+ method Main() {
+ // Test that code generation succeeds, even thought "a" and "b" are never defined or used
+ var a: A := *;
+ var b: B := *;
+ print "done\n";
+ }
+}

Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-4939c.dfy.expect

@@ -0,0 +1 @@
+done