Steel definition fails in dependency loading

[857b]

The following Steel definition is accepted in normal and in lax mode but not when loaded as a dependency:

module A
open Steel.Effect

noeq
type fsteel (pre : pre_t) (post : post_t unit) : Type =
  | FSteel : (f : (unit -> SteelT unit pre post)) -> fsteel pre post

let foo (f : unit -> SteelT unit emp (fun () -> emp))
  : fsteel emp (fun () -> emp)
  = FSteel (fun () -> f ()) (*Error here*)

module B
open A

When checking B.fst in the ide without a .checked file for A.fst, the following error is reported:

(Error 228) Error while computing or loading dependencies:
user tactic failed: ‘Could not make progress, no solvable goal found‘

The error is raised by Steel.Effect.Common.fsti(2220,2221) https://github.com/FStarLang/FStar/blob/808657bb7b9657b37be1aa14efd770da7f2cb065/ulib/experimental/Steel.Effect.Common.fsti#L2220

The workaround is to generate A.fst.checked

[R1kM]

Trying to debug this further, it seems that lax-checking A.fst from Emacs does indeed succeed, but running fstar.exe --lax A.fst from the command-line leads to the same error as when trying to load A. I'm not sure yet what the exact issue is, I'll keep poking at it