@@ -269,23 +269,27 @@ elabClass info syn_in doc fc constraints tn tnfc ps pDocs fds ds mcn cd
269 rhsArgs (CA : xs) ns = pconst (PResolveTC fc) : rhsArgs xs ns
269 rhsArgs (CA : xs) ns = pconst (PResolveTC fc) : rhsArgs xs ns
270 rhsArgs [] _ = []
270 rhsArgs [] _ = []
272+ -- Add the top level constraint. Put it first - elaboration will resolve
273+ -- the order of the implicits if there are dependencies.
274+ -- Also ensure the dictionary is used for lookup of any methods that
275+ -- are used in the type
272 insertConstraint :: PTerm -> [Name] -> PTerm -> PTerm
276 insertConstraint :: PTerm -> [Name] -> PTerm -> PTerm
273− insertConstraint c all (PPi p@(Imp _ _ _ _ _) n fc ty sc)
277+ insertConstraint c all sc
274− = PPi p n fc ty (insertConstraint c all sc)
275− insertConstraint c all sc = let dictN = sMN 0 "__class"
278+ = let dictN = sMN 0 "__class" in
276− in PPi (constraint { pstatic = Static })
279+ PPi (constraint { pstatic = Static })
277− dictN NoFC c
280+ dictN NoFC c
278− (constrainMeths (map basename all)
281+ (constrainMeths (map basename all)
279− dictN sc)
282+ dictN sc)
281− -- After we insert the constraint into the lookup, we need to
284+ -- After we insert the constraint into the lookup, we need to
282− -- ensure that the same dictionary is used to resolve lookups
285+ -- ensure that the same dictionary is used to resolve lookups
283− -- to the other methods in the class
286+ -- to the other methods in the class
284 constrainMeths :: [Name] -> Name -> PTerm -> PTerm
287 constrainMeths :: [Name] -> Name -> PTerm -> PTerm
285 constrainMeths allM dictN tm = transform (addC allM dictN) tm
288 constrainMeths allM dictN tm = transform (addC allM dictN) tm
286 addC allM dictN m@(PRef fc hls n)
290 addC allM dictN m@(PRef fc hls n)
287− | n `elem` allM = PApp NoFC m [pconst (PRef NoFC hls dictN)]
291+ | n `elem` allM = PApp NoFC m [pconst (PRef NoFC hls dictN)]
288− | otherwise = m
292+ | otherwise = m
289 addC _ _ tm = tm
293 addC _ _ tm = tm
291 -- make arguments explicit and don't bind class parameters
295 -- make arguments explicit and don't bind class parameters