I was trying to understand bidirectional typechecking so I tried a similar approach in Coq of specifying inference rules and wellformed rules separately. No idea if this works as a type system but it seems to handle non-strictly positive recursion much better.

somethinglikebidi.v

Section s1.
Variable v : Set.

Inductive term : Set :=
| var : v -> term -> term
| typ : term
| set : term
| app : term -> term -> term
| all_ : term -> (v -> term) -> term
| lam_ : term -> (v -> term) -> term
.

Definition all a f := all_ a (fun x => f (var x a)).
Definition lam a f := lam_ a (fun x => f (var x a)).

Declare Custom Entry coc.
Notation "<{ e }>" := e (e custom coc at level 99).
Notation "x" := x (in custom coc at level 0, x constr at level 0).
Notation "f x" := (app f x) (in custom coc at level 1, left associativity).
Notation "'fun' ( x : A ) => y" :=
  (lam A (fun x => y)) (in custom coc at level 90,
                     x constr at level 99,
                     A custom coc at level 99,
                     y custom coc at level 99,
                     left associativity).
                    
Notation "'forall' ( x : A ) , B" := (all A (fun x => B)) (x constr at level 99,
 in custom coc at level 50, right associativity).

Section s2.
Variable u : v.

Fixpoint infer x : term :=
match x with
| var _ t => t
| set => typ
| app f x => match infer f with
   | all_ a b => app (lam_ a b) x
   | _ => var u typ
   end
| lam_ a f => all_ a (fun x => infer (f x))
| all_ a f => infer (f u)
| _ => var u typ
end.

Inductive wf : term -> Prop :=
| var_wf : forall v t, wf (var v t)
| typ_wf : wf typ
| set_wf : wf set
| app_wf : forall f x a b, <{ forall (x : a) , (b x) }> = infer f -> a = infer x -> wf f -> wf x -> wf <{ f x }>
| all_wf_ : forall a f, wf a -> (forall x, wf (f (var x a))) -> wf <{ forall (x : a) , (f x) }>
| lam_wf_ : forall a f, wf a -> (forall x, wf (f (var x a))) -> wf <{ fun (x : a) => (f x) }>
.

Definition lam_wf a f (awf : wf a) (fwf : forall x, wf (var x a) -> wf (f (var x a))) := lam_wf_ a f awf (fun x => fwf x (var_wf x a)).
Definition all_wf a f (awf : wf a) (fwf : forall x, wf (var x a) -> wf (f (var x a))) := all_wf_ a f awf (fun x => fwf x (var_wf x a)).

Declare Custom Entry typ.
Notation "<[ e ]>" := e (e custom typ at level 99).
Notation "x" := x (in custom typ at level 0, x constr at level 0).
Notation "f x" := (app_wf _ _ _ _ _ _ f x) (in custom typ at level 1, left associativity).
Notation "'fun' ( x : A ) => y" :=
  (lam_wf _ _ A (fun _ x => y)) (in custom typ at level 90,
                     x constr at level 99,
                     A custom typ at level 99,
                     y custom typ at level 99,
                     left associativity).
                    
Notation "'forall' ( x : A ) , B" := (all_wf _ _ A (fun _ x => B)) (x constr at level 99,
 in custom typ at level 50, right associativity).

Inductive oftype t : Set :=
| isoftype : forall (x : term), t = infer x -> wf x -> oftype t.


Definition identity : oftype <{ forall (a : set) , forall (x : a) , a }>
 := isoftype <{ forall (a : set) , forall (x : a) , a }> <{ fun (a : set) => fun (x : a) => x }> _ <[ fun (a : set_wf) => fun (x : a) => x ]>.
split.
eapply <[ fun (a : set_wf)  => fun (x : a) => x ]>.
simpl.
symmetry.
simpl.


Definition identity : wf <{ fun (a : set) => fun (x : a) => x }> := <[ fun (a : set_wf)  => fun (x : a) => x ]>.
Print identity.
 

Definition identity : oftype <{ forall (a : typ) , forall (_ : a) , a }>.
eapply (exist (fun x => wf x /\ <{ forall (a : typ) , forall (_ : a) , a }> = infer x) <{ fun (a : typ) => fun (x : a) => x }>).
split.
eapply lam_wf.
apply typ_wf.
intro.
eapply lam_wf.
apply var_wf.
intro.
apply var_wf.
auto.
Qed.


End s2.