@@ -260,9 +260,12 @@ makeLemma fn updatefile l n
260260 _ -> return (-1)
261261
262262 if (not isProv) then do
263− let skip = guessImps (tt_ctxt i) mty
263+ let skip = guessImps i (tt_ctxt i) mty
264+ let classes = guessClasses i (tt_ctxt i) mty
264265
265− let lem = show n ++ " : " ++ show (stripMNBind skip (delab i mty))
266+ let lem = show n ++ " : " ++
267+ constraints i classes mty ++
268+ show (stripMNBind skip (delab i mty))
266269 let lem_app = show n ++ appArgs skip margs mty
267270
268271 if updatefile then
@@ -312,15 +315,52 @@ makeLemma fn updatefile l n
312315 stripMNBind skip (PPi b _ _ ty sc) = stripMNBind skip sc
313316 stripMNBind skip t = t
314317
318+ constraints :: IState -> [Name] -> Type -> String
319+ constraints i [] ty = ""
320+ constraints i [n] ty = showSep ", " (showConstraints i [n] ty) ++ " => "
321+ constraints i ns ty = "(" ++ showSep ", " (showConstraints i ns ty) ++ ") => "
322+
323+ showConstraints i ns (Bind n (Pi _ ty _) sc)
324+ | n `elem` ns = show (delab i ty) :
325+ showConstraints i ns (substV (P Bound n Erased) sc)
326+ | otherwise = showConstraints i ns (substV (P Bound n Erased) sc)
327+ showConstraints _ _ _ = []
328+
315329 -- Guess which binders should be implicits in the generated lemma.
316330 -- Make them implicit if they appear guarded by a top level constructor,
317331 -- or at the top level themselves.
318− guessImps :: Context -> Term -> [Name]
319− guessImps ctxt (Bind n (Pi _ _ _) sc)
332+ -- Also, make type class instances implicit
333+ guessImps :: IState -> Context -> Term -> [Name]
334+ guessImps ist ctxt (Bind n (Pi _ ty _) sc)
320335 | guarded ctxt n (substV (P Bound n Erased) sc)
321− = n : guessImps ctxt sc
322− | otherwise = guessImps ctxt sc
323− guessImps ctxt _ = []
336+ = n : guessImps ist ctxt sc
337+ | isClass ist ty
338+ = n : guessImps ist ctxt sc
339+ | otherwise = guessImps ist ctxt sc
340+ guessImps ist ctxt _ = []
341+
342+ guessClasses :: IState -> Context -> Term -> [Name]
343+ guessClasses ist ctxt (Bind n (Pi _ ty _) sc)
344+ | isParamClass ist ty
345+ = n : guessClasses ist ctxt sc
346+ | otherwise = guessClasses ist ctxt sc
347+ guessClasses ist ctxt _ = []
348+
349+ isClass ist t
350+ | (P _ n _, args) <- unApply t
351+ = case lookupCtxtExact n (idris_classes ist) of
352+ Just _ -> True
353+ _ -> False
354+ | otherwise = False
355+
356+ isParamClass ist t
357+ | (P _ n _, args) <- unApply t
358+ = case lookupCtxtExact n (idris_classes ist) of
359+ Just _ -> any isV args
360+ _ -> False
361+ | otherwise = False
362+ where isV (V _) = True
363+ isV _ = False
324364
325365 guarded ctxt n (P _ n' _) | n == n' = True
326366 guarded ctxt n ap@(App _ _ _)