@@ -301,6 +301,9 @@ elabClass info syn fc constraints tn ps ds
301301 let usyn = syn { using = ps ++ using syn }
302302 fns <- mapM (tfun cn constraint usyn (map fst imethods)) imethods
303303 mapM_ (elabDecl info) (concat fns)
304+ -- for each constraint, bui;d a top level function to chase it
305+ fns <- mapM (cfun cn constraint usyn (map fst imethods)) constraints
306+ mapM_ (elabDecl info) (concat fns)
304307 i <- get
305308 put (i { idris_classes = addDef tn (CI cn imethods (map fst ps))
306309 (idris_classes i) })
@@ -318,6 +321,18 @@ elabClass info syn fc constraints tn ps ds
318321 tdecl (PClauses _ _ _ _) = fail "No default definitions allowed yet"
319322 tdecl _ = fail "Not allowed in a class declaration"
320323
324+ cfun cn c syn all con
325+ = do let cfn = UN ('@':show cn ++ "#" ++ show con)
326+ let mnames = take (length all) $ map (\x -> MN x "meth") [0..]
327+ let capp = PApp fc (PRef fc cn) (map (pexp . PRef fc) mnames)
328+ let lhs = PApp fc (PRef fc cfn) [pconst capp]
329+ let rhs = PResolveTC (FC "HACK" 0)
330+ let ty = PPi constraint (MN 0 "pc") c con
331+ iLOG (showImp True ty)
332+ iLOG (showImp True lhs ++ " = " ++ showImp True rhs)
333+ return [PTy syn fc cfn ty,
334+ PClauses fc True cfn [PClause cfn lhs [] rhs []]]
335+
321336 tfun cn c syn all (m, ty)
322337 = do let ty' = insertConstraint c ty
323338 let mnames = take (length all) $ map (\x -> MN x "meth") [0..]
@@ -513,6 +528,8 @@ elab ist info pattern tm
513528 elab' (PTrue fc) = try (elab' (PRef fc unitCon))
514529 (elab' (PRef fc unitTy))
515530 elab' (PFalse fc) = elab' (PRef fc falseTy)
531+ elab' (PResolveTC (FC "HACK" _))
532+ = resolveTC 10 ist
516533 elab' (PResolveTC fc) = do c <- unique_hole (MN 0 "c")
517534 instanceArg c
518535 elab' (PRefl fc) = elab' (PApp fc (PRef fc eqCon) [pimp (MN 0 "a") Placeholder,