@@ -66,7 +66,7 @@ elabInstance info syn what fc cs n ps t expn ds = do
66 cs -> tclift $ tfail $ At fc
66 cs -> tclift $ tfail $ At fc
67 (CantResolveAlts (map fst cs))
67 (CantResolveAlts (map fst cs))
68 let constraint = PApp fc (PRef fc n) (map pexp ps)
68 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
70 let emptyclass = null (class_methods ci)
70 let emptyclass = null (class_methods ci)
71 when (what /= EDefns || (null ds && not emptyclass)) $ do
71 when (what /= EDefns || (null ds && not emptyclass)) $ do
72 nty <- elabType' True info syn emptyDocstring [] fc [] iname t
72 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
140 [PConstant (AType (ATInt ITNative))] -> True
140 [PConstant (AType (ATInt ITNative))] -> True
141 _ -> False
141 _ -> False
143− mkiname n' ps' expn' =
143+ mkiname n' ns ps' expn' =
144 case expn' of
144 case expn' of
145+ Nothing -> case ns of
146+ Nothing -> SN (sInstanceN n' (map show ps'))
145− Nothing -> SN (sInstanceN n' (map show ps'))
147+ Just m -> sNS (SN (sInstanceN n' (map show ps'))) m
146 Just nm -> nm
148 Just nm -> nm
148 substInstance ips pnames (PInstance syn _ cs n ps t expn ds)
150 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
151 isOverlapping i (PInstance syn _ _ n ps t expn _)
153 isOverlapping i (PInstance syn _ _ n ps t expn _)
152 = case lookupCtxtName n (idris_classes i) of
154 = 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
154 case lookupTy iname (tt_ctxt i) of
156 case lookupTy iname (tt_ctxt i) of
155 [] -> elabFindOverlapping i ci iname syn t
157 [] -> elabFindOverlapping i ci iname syn t
156 (_:_) -> return True
158 (_:_) -> return True