@@ -175,8 +175,8 @@ elabClass info syn_in doc fc constraints tn ps pDocs fds ds
175 let lhs = PApp fc (PRef fc cfn) [pconst capp]
175 let lhs = PApp fc (PRef fc cfn) [pconst capp]
176 let rhs = PResolveTC (fileFC "HACK")
176 let rhs = PResolveTC (fileFC "HACK")
177 let ty = PPi constraint cnm c con
177 let ty = PPi constraint cnm c con
178− iLOG (showTmImpls ty)
178+ logLvl 2 ("Dictionary constraint: " ++ showTmImpls ty)
179− iLOG (showTmImpls lhs ++ " = " ++ showTmImpls rhs)
179+ logLvl 2 (showTmImpls lhs ++ " = " ++ showTmImpls rhs)
180 i <- getIState
180 i <- getIState
181 let conn = case con of
181 let conn = case con of
182 PRef _ n -> n
182 PRef _ n -> n
@@ -193,16 +193,16 @@ elabClass info syn_in doc fc constraints tn ps pDocs fds ds
193 -- Generate a top level function which looks up a method in a given
193 -- Generate a top level function which looks up a method in a given
194 -- dictionary (this is inlinable, always)
194 -- dictionary (this is inlinable, always)
195 tfun cn c syn all (m, (doc, o, ty))
195 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)
197 let mnames = take (length all) $ map (\x -> sMN x "meth") [0..]
197 let mnames = take (length all) $ map (\x -> sMN x "meth") [0..]
198 let capp = PApp fc (PRef fc cn) (map (pexp . PRef fc) mnames)
198 let capp = PApp fc (PRef fc cn) (map (pexp . PRef fc) mnames)
199 let margs = getMArgs ty
199 let margs = getMArgs ty
200 let anames = map (\x -> sMN x "arg") [0..]
200 let anames = map (\x -> sMN x "arg") [0..]
201 let lhs = PApp fc (PRef fc m) (pconst capp : lhsArgs margs anames)
201 let lhs = PApp fc (PRef fc m) (pconst capp : lhsArgs margs anames)
202 let rhs = PApp fc (getMeth mnames all m) (rhsArgs margs anames)
202 let rhs = PApp fc (getMeth mnames all m) (rhsArgs margs anames)
203− iLOG (showTmImpls ty')
203+ logLvl 2 ("Top level type: " ++ showTmImpls ty')
204 iLOG (show (m, ty', capp, margs))
204 iLOG (show (m, ty', capp, margs))
205− iLOG (showTmImpls lhs ++ " = " ++ showTmImpls rhs)
205+ logLvl 2 ("Definition: " ++ showTmImpls lhs ++ " = " ++ showTmImpls rhs)
206 return [PTy doc [] syn fc o m ty',
206 return [PTy doc [] syn fc o m ty',
207 PClauses fc [Inlinable] m [PClause fc m lhs [] rhs []]]
207 PClauses fc [Inlinable] m [PClause fc m lhs [] rhs []]]
@@ -236,6 +236,15 @@ elabClass info syn_in doc fc constraints tn ps pDocs fds ds
236 toExp ns e (PPi p n ty sc) = PPi p n ty (toExp ns e sc)
236 toExp ns e (PPi p n ty sc) = PPi p n ty (toExp ns e sc)
237 toExp ns e sc = sc
237 toExp ns e sc = sc
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
243+expandMethNS syn = mapPT expand
245+ expand (PRef fc n) | n `elem` imp_methods syn = PRef fc $ expandNS syn n
239findDets :: Name -> [Name] -> Idris [Int]
248findDets :: Name -> [Name] -> Idris [Int]
240findDets n ns =
249findDets n ns =
241 do i <- getIState
250 do i <- getIState