git.iko.soy/Idris-dev
on master help sign in
Propagation of explicit arguments in typeclasses

Given that we know what they're going to be, and this gives resolution a better chance with dependent classes in particular

commit22d1ae6b4c07b118c88c56c30326e25f30f1e616 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateFri 20 Mar 2015, 11:46 (12 years ago) parentb5052eb
2 files changed+6−5
compare with master
unifiedsplit
src/Idris/AbsSyntax.hs+3−3 src/Idris/Elab/Class.hs+3−2
src/Idris/AbsSyntax.hs+3−3
@@ -1685,9 +1685,9 @@ aiFn inpat expat qq imp_meths ist fc f ds as
16851685 case find n imps [] of
16861686 Just (tm, imps') ->
16871687 PImp p False l n tm : insImpAcc (M.insert n tm pnas) ps given imps'
1688− Nothing ->
1689− PImp p True l n Placeholder :
1690− insImpAcc (M.insert n Placeholder pnas) ps given imps
1688+ Nothing -> let ph = if f `elem` imp_meths then PRef fc n else Placeholder in
1689+ PImp p True l n ph :
1690+ insImpAcc (M.insert n ph pnas) ps given imps
16911691 insImpAcc pnas (PTacImplicit p l n sc' ty : ps) given imps =
16921692 let sc = addImpl imp_meths ist (substMatches (M.toList pnas) sc') in
16931693 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
9494 mapM_ (rec_elabDecl info EAll info) (concat cfns)
9595
9696 -- for each method, build a top level function
97− fns <- mapM (tfun cn constraint syn (map fst imethods)) imethods
97+ fns <- mapM (tfun cn constraint (syn { imp_methods = mnames })
98+ (map fst imethods)) imethods
9899 logLvl 5 $ "Functions " ++ show fns
99100 -- Elaborate the the top level methods
100101 mapM_ (rec_elabDecl info EAll info) (concat fns)
@@ -199,7 +200,7 @@ elabClass info syn_in doc fc constraints tn ps pDocs fds ds
199200 let anames = map (\x -> sMN x "arg") [0..]
200201 let lhs = PApp fc (PRef fc m) (pconst capp : lhsArgs margs anames)
201202 let rhs = PApp fc (getMeth mnames all m) (rhsArgs margs anames)
202− iLOG (showTmImpls ty)
203+ iLOG (showTmImpls ty')
203204 iLOG (show (m, ty', capp, margs))
204205 iLOG (showTmImpls lhs ++ " = " ++ showTmImpls rhs)
205206 return [PTy doc [] syn fc o m ty',