@@ -66,7 +66,7 @@ elabInstance info syn what fc cs n ps t expn ds = do
6666 cs -> tclift $ tfail $ At fc
6767 (CantResolveAlts (map fst cs))
6868 let constraint = PApp fc (PRef fc n) (map pexp ps)
69− let iname = mkiname n ps expn
69+ let iname = mkiname n (namespace info) ps expn
7070 let emptyclass = null (class_methods ci)
7171 when (what /= EDefns || (null ds && not emptyclass)) $ do
7272 nty <- elabType' True info syn emptyDocstring [] fc [] iname t
@@ -140,9 +140,11 @@ elabInstance info syn what fc cs n ps t expn ds = do
140140 [PConstant (AType (ATInt ITNative))] -> True
141141 _ -> False
142142
143− mkiname n' ps' expn' =
143+ mkiname n' ns ps' expn' =
144144 case expn' of
145− Nothing -> SN (sInstanceN n' (map show ps'))
145+ Nothing -> case ns of
146+ Nothing -> SN (sInstanceN n' (map show ps'))
147+ Just m -> sNS (SN (sInstanceN n' (map show ps'))) m
146148 Just nm -> nm
147149
148150 substInstance ips pnames (PInstance syn _ cs n ps t expn ds)
@@ -150,7 +152,7 @@ elabInstance info syn what fc cs n ps t expn ds = do
150152
151153 isOverlapping i (PInstance syn _ _ n ps t expn _)
152154 = case lookupCtxtName n (idris_classes i) of
153− [(n, ci)] -> let iname = (mkiname n ps expn) in
155+ [(n, ci)] -> let iname = (mkiname n (namespace info) ps expn) in
154156 case lookupTy iname (tt_ctxt i) of
155157 [] -> elabFindOverlapping i ci iname syn t
156158 (_:_) -> return True