@@ -269,23 +269,27 @@ elabClass info syn_in doc fc constraints tn tnfc ps pDocs fds ds mcn cd
269269 rhsArgs (CA : xs) ns = pconst (PResolveTC fc) : rhsArgs xs ns
270270 rhsArgs [] _ = []
271271
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
272276 insertConstraint :: PTerm -> [Name] -> PTerm -> PTerm
273− insertConstraint c all (PPi p@(Imp _ _ _ _ _) n fc ty sc)
274− = PPi p n fc ty (insertConstraint c all sc)
275− insertConstraint c all sc = let dictN = sMN 0 "__class"
276− in PPi (constraint { pstatic = Static })
277− dictN NoFC c
278− (constrainMeths (map basename all)
279− dictN sc)
280− where
281− -- After we insert the constraint into the lookup, we need to
282− -- ensure that the same dictionary is used to resolve lookups
283− -- to the other methods in the class
277+ insertConstraint c all sc
278+ = let dictN = sMN 0 "__class" in
279+ PPi (constraint { pstatic = Static })
280+ dictN NoFC c
281+ (constrainMeths (map basename all)
282+ dictN sc)
283+ where
284+ -- After we insert the constraint into the lookup, we need to
285+ -- ensure that the same dictionary is used to resolve lookups
286+ -- to the other methods in the class
284287 constrainMeths :: [Name] -> Name -> PTerm -> PTerm
285288 constrainMeths allM dictN tm = transform (addC allM dictN) tm
289+
286290 addC allM dictN m@(PRef fc hls n)
287− | n `elem` allM = PApp NoFC m [pconst (PRef NoFC hls dictN)]
288− | otherwise = m
291+ | n `elem` allM = PApp NoFC m [pconst (PRef NoFC hls dictN)]
292+ | otherwise = m
289293 addC _ _ tm = tm
290294
291295 -- make arguments explicit and don't bind class parameters