@@ -101,6 +101,7 @@ elabInterface info syn_in doc fc constraints tn tnfc ps pDocs fds ds mcn cd
101101 let idecls = filter impldecl ds -- default super interface implementation declarations
102102 mapM_ checkDefaultSuperInterfaceImplementation idecls
103103 let mnames = map getMName mdecls
104+ let fullmnames = map getFullMName mdecls
104105 ist <- getIState
105106 let constraintNames = nub $
106107 concatMap (namesIn [] ist) (map snd constraints)
@@ -113,7 +114,7 @@ elabInterface info syn_in doc fc constraints tn tnfc ps pDocs fds ds mcn cd
113114 imp_methods = mnames }) doc pDocs fc [] pre_ddecl
114115 dets <- findDets tn (map fst fds)
115116
116− logElab 2 $ "Building methods " ++ show mnames
117+ logElab 3 $ "Building methods " ++ show fullmnames
117118 ims <- mapM (tdecl impps mnames) mdecls
118119 defs <- mapM (defdecl (map (\ (x,y,z) -> z) ims) constraint)
119120 (filter clause ds)
@@ -134,28 +135,43 @@ elabInterface info syn_in doc fc constraints tn tnfc ps pDocs fds ds mcn cd
134135 let (cfnTyDecls, cfnDefs) = unzip cfns
135136 mapM_ (rec_elabDecl info EAll info) cfnTyDecls
136137
138+ -- for each method, build a top level function
139+ -- 'tfun' builds appropriate implicits for the constructor
140+ -- declaration
141+ fns <- mapM (tfun cn constraint (syn { imp_methods = mnames }) -- mnames })
142+ (map fst imethods)) imethods
143+ let (fnTyDecls, fnDefs) = unzip fns
144+ mapM_ (rec_elabDecl info EAll info) fnTyDecls
145+
146+ elabMethTys <- mapM getElabMethTy fullmnames
147+ logElab 3 $ "Method types:\n" ++ showSep "\n" (map showTmImpls elabMethTys)
148+
149+ let cpos = map (\ (n, ty) -> (n, findConstraint ty))
150+ (zip fullmnames elabMethTys)
151+ logElab 5 $ "Constraint pos: " ++ show cpos
152+
137153 -- build implementation constructor type
138− let cty = impbind [(pn, pt) | (pn, _, pt) <- impps ++ ps] $ conbind constraints
154+ let cty = impbind [(pn, pt) | (pn, _, pt) <- impps ++ ps] $
155+ conbind constraints $
156+ pibind (map (mkMethTy cpos) (zip fullmnames elabMethTys))
157+ constraint
158+ let ctyOld = impbind [(pn, pt) | (pn, _, pt) <- impps ++ ps] $ conbind constraints
139159 $ pibind (map (\ (n, ty) -> (nsroot n, ty)) methods)
140160 constraint
161+
162+ logElab 3 $ "Constraint constructor type: " ++ showTmImpls cty
163+
141164
142165 let cons = [(cd, pDocs ++ mapMaybe memberDocs ds, cn, NoFC, cty, fc, [])]
143166 let ddecl = PDatadecl tn NoFC tty cons
144167
145− logElab 5 $ "Interface " ++ show (showDImp verbosePPOption ddecl)
168+ logElab 10 $ "Interface " ++ show (showDImp verbosePPOption ddecl)
146169
147− -- for each method, build a top level function
148− -- 'tfun' builds appropriate implicits for the constructor
149− -- declaration
150− fns <- mapM (tfun cn constraint (syn { imp_methods = mnames }) -- mnames })
151− (map fst imethods)) imethods
152− let (fnTyDecls, fnDefs) = unzip fns
153170
154171 -- Elaborate the data declaration
155172 elabData info (syn { no_imp = no_imp syn ++ mnames,
156− imp_methods = mnames }) doc pDocs fc [] ddecl
173+ imp_methods = [] }) doc pDocs fc [] ddecl
157174
158− mapM_ (rec_elabDecl info EAll info) fnTyDecls
159175
160176 logElab 5 $ "Function types " ++ show fnTyDecls
161177 logElab 5 $ "Method types now: " ++ show imethods
@@ -182,6 +198,48 @@ elabInterface info syn_in doc fc constraints tn tnfc ps pDocs fds ds mcn cd
182198 maybe [] (\(conN, conNFC) -> [(conNFC, AnnName conN Nothing Nothing Nothing)]) mcn
183199
184200 where
201+ getElabMethTy :: Name -> Idris PTerm
202+ getElabMethTy n = do ist <- getIState
203+ case lookupTyExact n (tt_ctxt ist) of
204+ Just ty -> return (delabDirect ist ty)
205+ Nothing -> tclift $ tfail (At fc (InternalMsg "Can't happen, elabMethTy"))
206+
207+ -- Find the argument position of the current interface in a method type
208+ -- (we'll use this to update the elaborated top level method types before
209+ -- building a data declaration
210+ findConstraint :: PTerm -> Int
211+ findConstraint = findPos 0
212+ where
213+ findPos i (PPi _ _ _ (PRef _ _ n) sc)
214+ | n == tn = i
215+ findPos i (PPi _ _ _ (PApp _ (PRef _ _ n) _) sc)
216+ | n == tn = i
217+ findPos i (PPi _ _ _ ty sc) = findPos (i + 1) sc
218+ findPos i _ = -1 -- Can't happen!
219+
220+ -- Make the method component of the constructor type by taking the
221+ -- elaborated top level method and removing the implicits/constraint
222+ mkMethTy :: [(Name, Int)] -> (Name, PTerm) -> (Name, PTerm)
223+ mkMethTy cpos (n, tm) = (nsroot n, dropPis num (mapPT dropImp tm))
224+ where
225+ num = case lookup n cpos of
226+ Just i -> i + 1
227+ Nothing -> 0
228+
229+ dropPis n (PPi _ _ _ _ sc) | n > 0 = dropPis (n - 1) sc
230+ dropPis _ tm = tm
231+
232+ dropImp (PApp fc (PRef fcr fcs n) args)
233+ | Just pos <- lookup n cpos
234+ = PApp fc (PRef fcr fcs (nsroot n))
235+ (filter notConstr (drop (pos + 1) args))
236+ dropImp (PApp fc f args)
237+ = PApp fc f (filter notConstr args)
238+ dropImp tm = tm
239+
240+ notConstr (PConstraint {}) = False
241+ notConstr _ = True
242+
185243 nodoc (n, (inj, _, _, o, t)) = (n, (inj, o, t))
186244
187245 pibind [] x = x
@@ -224,6 +282,9 @@ elabInterface info syn_in doc fc constraints tn tnfc ps pDocs fds ds mcn cd
224282
225283 getMName (PTy _ _ _ _ _ n nfc _) = nsroot n
226284 getMName (PData _ _ _ _ _ (PLaterdecl n nfc _)) = nsroot n
285+
286+ getFullMName (PTy _ _ _ _ _ n nfc _) = n
287+ getFullMName (PData _ _ _ _ _ (PLaterdecl n nfc _)) = n
227288
228289 tdecl impps allmeths (PTy doc _ syn _ o n nfc t)
229290 = do t' <- implicit' info syn (map (\(n, _, _) -> n) (impps ++ ps) ++ allmeths) n t