https://code.google.com/p/agda/issues/detail?id=886&q=Display in Coq

886.v

Module Bug.
  Axiom A : Set.
  Axiom I : Set.

  Module Type IWrapper.
    Axiom i : I.
  End IWrapper.

  Module R (i : IWrapper).
    Axiom f : A.
  End R.

  Axiom r : I.
  Axiom X : I -> I.
  Axiom Q : A -> Set.

  Module Qualified.
    Module K : IWrapper.
      Definition i := X r.
    End K.

    Module RK := R K.

    (* open in agda is Import in Coq, I think *)
    Import RK.


    Definition foo : Q f.
      (**                                                                                                                                   
1 subgoals, subgoal 1 (ID 8)                                                                                                                
                                                                                                                                            
  ============================                                                                                                              
   Q f                                                                                                                                      
(dependent evars:)                                                                                                                          
*)
    Admitted.
  End Qualified.