Import and use a class without open in Lean

.project

+ *.lean
- flycheck*.lean
- .#*.lean

export_class.lean

namespace imported

structure is_unit [class] {A : Type} (R : A → unit) := (u : unit)

end imported

use_class.lean

import export_class
-- This is required, though it feels like it shouldn't be:
-- open [class] imported

definition using_imported {A : Type} {R : A → unit} [imported.is_unit R] : unit := imported.is_unit.u R
-- Error on the above line:
-- don't know how to synthesize placeholder
--  A : Type,
--  R : A → unit,
--  _inst_1 : imported.is_unit R
--  ⊢ imported.is_unit R (lean-checker)

See the mailing list discussion.