git.iko.soy/Idris-dev
on master help sign in
Propagation of explicit arguments in typeclasses
22d1ae6Edwin Brady
src/Idris/AbsSyntax.hs+3−3
compare with master
unifiedsplit
@@ -1685,9 +1685,9 @@ aiFn inpat expat qq imp_meths ist fc f ds as
1685 case find n imps [] of
1685 case find n imps [] of
1686 Just (tm, imps') ->
1686 Just (tm, imps') ->
1687 PImp p False l n tm : insImpAcc (M.insert n tm pnas) ps given imps'
1687 PImp p False l n tm : insImpAcc (M.insert n tm pnas) ps given imps'
1688− Nothing ->
1688+ Nothing -> let ph = if f `elem` imp_meths then PRef fc n else Placeholder in
1689− PImp p True l n Placeholder :
1689+ PImp p True l n ph :
1690− insImpAcc (M.insert n Placeholder pnas) ps given imps
1690+ insImpAcc (M.insert n ph pnas) ps given imps
1691 insImpAcc pnas (PTacImplicit p l n sc' ty : ps) given imps =
1691 insImpAcc pnas (PTacImplicit p l n sc' ty : ps) given imps =
1692 let sc = addImpl imp_meths ist (substMatches (M.toList pnas) sc') in
1692 let sc = addImpl imp_meths ist (substMatches (M.toList pnas) sc') in
1693 case find n imps [] of
1693 case find n imps [] of
src/Idris/Elab/Class.hs+3−2
@@ -94,7 +94,8 @@ elabClass info syn_in doc fc constraints tn ps pDocs fds ds
94 mapM_ (rec_elabDecl info EAll info) (concat cfns)
94 mapM_ (rec_elabDecl info EAll info) (concat cfns)
95
95
96 -- for each method, build a top level function
96 -- for each method, build a top level function
97+ fns <- mapM (tfun cn constraint (syn { imp_methods = mnames })
97− fns <- mapM (tfun cn constraint syn (map fst imethods)) imethods
98+ (map fst imethods)) imethods
98 logLvl 5 $ "Functions " ++ show fns
99 logLvl 5 $ "Functions " ++ show fns
99 -- Elaborate the the top level methods
100 -- Elaborate the the top level methods
100 mapM_ (rec_elabDecl info EAll info) (concat fns)
101 mapM_ (rec_elabDecl info EAll info) (concat fns)
@@ -199,7 +200,7 @@ elabClass info syn_in doc fc constraints tn ps pDocs fds ds
199 let anames = map (\x -> sMN x "arg") [0..]
200 let anames = map (\x -> sMN x "arg") [0..]
200 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)
201 let rhs = PApp fc (getMeth mnames all m) (rhsArgs margs anames)
202 let rhs = PApp fc (getMeth mnames all m) (rhsArgs margs anames)
202− iLOG (showTmImpls ty)
203+ iLOG (showTmImpls ty')
203 iLOG (show (m, ty', capp, margs))
204 iLOG (show (m, ty', capp, margs))
204 iLOG (showTmImpls lhs ++ " = " ++ showTmImpls rhs)
205 iLOG (showTmImpls lhs ++ " = " ++ showTmImpls rhs)
205 return [PTy doc [] syn fc o m ty',
206 return [PTy doc [] syn fc o m ty',