@@ -175,8 +175,8 @@ elabClass info syn_in doc fc constraints tn ps pDocs fds ds
175175 let lhs = PApp fc (PRef fc cfn) [pconst capp]
176176 let rhs = PResolveTC (fileFC "HACK")
177177 let ty = PPi constraint cnm c con
178− iLOG (showTmImpls ty)
179− iLOG (showTmImpls lhs ++ " = " ++ showTmImpls rhs)
178+ logLvl 2 ("Dictionary constraint: " ++ showTmImpls ty)
179+ logLvl 2 (showTmImpls lhs ++ " = " ++ showTmImpls rhs)
180180 i <- getIState
181181 let conn = case con of
182182 PRef _ n -> n
@@ -193,16 +193,16 @@ elabClass info syn_in doc fc constraints tn ps pDocs fds ds
193193 -- Generate a top level function which looks up a method in a given
194194 -- dictionary (this is inlinable, always)
195195 tfun cn c syn all (m, (doc, o, ty))
196− = do let ty' = insertConstraint c ty
196+ = do let ty' = expandMethNS syn (insertConstraint c ty)
197197 let mnames = take (length all) $ map (\x -> sMN x "meth") [0..]
198198 let capp = PApp fc (PRef fc cn) (map (pexp . PRef fc) mnames)
199199 let margs = getMArgs ty
200200 let anames = map (\x -> sMN x "arg") [0..]
201201 let lhs = PApp fc (PRef fc m) (pconst capp : lhsArgs margs anames)
202202 let rhs = PApp fc (getMeth mnames all m) (rhsArgs margs anames)
203− iLOG (showTmImpls ty')
203+ logLvl 2 ("Top level type: " ++ showTmImpls ty')
204204 iLOG (show (m, ty', capp, margs))
205− iLOG (showTmImpls lhs ++ " = " ++ showTmImpls rhs)
205+ logLvl 2 ("Definition: " ++ showTmImpls lhs ++ " = " ++ showTmImpls rhs)
206206 return [PTy doc [] syn fc o m ty',
207207 PClauses fc [Inlinable] m [PClause fc m lhs [] rhs []]]
208208
@@ -236,6 +236,15 @@ elabClass info syn_in doc fc constraints tn ps pDocs fds ds
236236 toExp ns e (PPi p n ty sc) = PPi p n ty (toExp ns e sc)
237237 toExp ns e sc = sc
238238
239+-- In a top level type for a method, expand all the method names namespaces
240+-- so that we don't have to disambiguate later
241+expandMethNS :: SyntaxInfo
242+ -> PTerm -> PTerm
243+expandMethNS syn = mapPT expand
244+ where
245+ expand (PRef fc n) | n `elem` imp_methods syn = PRef fc $ expandNS syn n
246+ expand t = t
247+
239248findDets :: Name -> [Name] -> Idris [Int]
240249findDets n ns =
241250 do i <- getIState