fix: missing test at has_trivial_structure

see #1074

src/library/compiler/util.cpp

@@ -448,7 +448,7 @@ optional<unsigned> has_trivial_structure(environment const & env, name const & I
     inductive_val I_val = env.get(I_name).to_inductive_val();
     if (I_val.is_unsafe())
         return optional<unsigned>();
-    if (I_val.get_ncnstrs() != 1)
+    if (I_val.get_ncnstrs() != 1 || I_val.is_rec())
         return optional<unsigned>();
     buffer<bool> rel_fields;
     get_constructor_relevant_fields(env, head(I_val.get_cnstrs()), rel_fields);

tests/lean/1074b.lean

@@ -0,0 +1,12 @@
+inductive Term
+| id: Term -> Term
+
+inductive Brx: Term -> Prop
+| id: Brx z -> Brx (Term.id n)
+
+def Brx.interp {a} (H: Brx a): Nat :=
+  match a with
+  | Term.id n => by
+    have ⟨Hn, Hz⟩: True ∧ Brx z
+      := by cases H <;> exact ⟨by simp, by assumption⟩;
+    exact Hz.interp

tests/lean/1074b.lean.expected.out

@@ -0,0 +1,13 @@
+1074b.lean:10:30-10:31: error: unknown identifier 'z'
+1074b.lean:11:43-11:53: error: tactic 'assumption' failed
+a : Term
+H : Brx a
+n : Term
+⊢ Brx (sorryAx Term)
+1074b.lean:11:9-11:55: error: unsolved goals
+case id
+a : Term
+H : Brx a
+n z✝ : Term
+a✝ : Brx z✝
+⊢ True ∧ Brx (sorryAx Term)