Solving type constructors implicits before data constructor implicits

src/typechecker/FStar.TypeChecker.TcInductive.fst

@@ -749,6 +749,8 @@ let check_inductive_well_typedness (env:env_t) (ses:list sigelt) (quals:list qua
     env, (tc, tc_u)::all_tcs, Env.conj_guard g (Env.conj_guard guard g')
   ) tys (env, [], Env.trivial_guard)
   in
+  (* Try to solve some implicits. See issue #3130. *)
+  let g = Rel.resolve_implicits env g in
 
   (* Check each datacon *)
   let datas, g = List.fold_right (fun se (datas, g) ->

tests/typeclasses/Bug3130.fst

@@ -0,0 +1,34 @@
+module Bug3130
+
+class typeclass1 (a:Type0) = {
+  x: unit;
+}
+
+class typeclass2 (bytes:Type0) {|typeclass1 bytes|} (a:Type) = {
+  y:unit;
+}
+
+assume val bytes: Type0
+assume val bytes_typeclass1: typeclass1 bytes
+instance bytes_typeclass1_ = bytes_typeclass1
+assume val t: Type0 -> Type0
+assume val t_inst: t bytes
+
+assume val truc:
+  #bytes:Type0 -> {|typeclass1 bytes|} ->
+  #a:Type -> {|typeclass2 bytes a|} ->
+  t bytes -> a ->
+  Type0
+
+open FStar.Tactics.Typeclasses
+
+#set-options "--debug_level Low"
+
+noeq
+type machin (a:Type) (d : typeclass2 bytes #solve a) (content:a) = {
+  lemma:
+   unit ->
+    Lemma
+    (ensures truc #bytes #bytes_typeclass1_ #a #solve t_inst content) // error here on `truc`
+  ;
+}

tests/typeclasses/Bug3130b.fst

@@ -0,0 +1,23 @@
+module Bug3130b
+
+(* This never actually regressed, but it's a decent test anyway *)
+
+open FStar.Tactics
+
+assume val it : int -> Type0
+assume val mk5 : (#[exact (`5)] x:int) -> it x
+assume val mk6 : (#[exact (`6)] x:int) -> it x
+
+let test0 = mk5
+let test1 = mk6
+
+let test2 (y : it 6) = let p : Type0 = mk5 == y in ()
+let test3 (y : it 6) = let p : Type0 = y == mk5 in ()
+let test4 (y : it 6) = let p : Type0 = mk6 == y in ()
+let test5 (y : it 6) = let p : Type0 = y == mk6 in ()
+
+let test6 () = let p : Type0 = mk5 == mk6 in ()
+let test7 () = let p : Type0 = mk6 == mk5 in ()
+
+let test8 (x:_) = let p : Type0 = mk5 == x /\ x == mk6 in ()
+let test9 (x:_) = let p : Type0 = mk6 == x /\ x == mk5 in ()

ulib/FStar.Tactics.Typeclasses.fst

@@ -100,11 +100,16 @@ let rec tcresolve' (seen : list term) (glb : list fv) (fuel : int) : Tac unit =
     let g = cur_goal () in
 
     (* Try to detect loops *)
-    if L.existsb (Reflection.V2.TermEq.term_eq g) seen then
-      raise NoInst;
+    if L.existsb (Reflection.V2.TermEq.term_eq g) seen then (
+      debug (fun () -> "loop");
+      raise NoInst
+    );
 
     match head_of g with
-    | None -> fail ("goal does not look like a typeclass")
+    | None ->
+      debug (fun () -> "goal does not look like a typeclass");
+      raise NoInst
+
     | Some head_fv ->
       (* ^ Maybe should check is this really is a class too? *)
       let seen = g :: seen in
@@ -125,15 +130,22 @@ and global (head_fv : fv) (seen : list term) (glb : list fv) (fuel : int) () : T
           glb
 
 and trywith (head_fv : fv) (seen:list term) (glb : list fv) (fuel:int) (t typ : term) : Tac unit =
+    debug (fun () -> "trywith " ^ term_to_string t);
     match head_of (res_typ typ) with
-    | None -> raise NoInst
+    | None ->
+      debug (fun () -> "no head for typ of this? " ^ term_to_string t ^ "    typ=" ^ term_to_string typ);
+      raise NoInst
     | Some fv' ->
       if fv_eq fv' head_fv
       then (
         debug (fun () -> "Trying to apply hypothesis/instance: " ^ term_to_string t);
-        (fun () -> apply_noinst t) `seq` (fun () -> tcresolve' seen glb (fuel-1))
-      ) else
+        (fun () -> apply_noinst t) `seq` (fun () ->
+          debug (fun () -> dump "next"; "apply seems to have worked");
+          tcresolve' seen glb (fuel-1))
+      ) else (
+        debug (fun () -> "different class");
         raise NoInst
+      )
 
 private
 let rec maybe_intros () : Tac unit =