@@ -78,6 +78,12 @@ elabClass info syn_in doc fc constraints tn tnfc ps pDocs fds ds mcn cd
7878 let idecls = filter instdecl ds -- default superclass instance declarations
7979 mapM_ checkDefaultSuperclassInstance idecls
8080 let mnames = map getMName mdecls
81+ ist <- getIState
82+ let constraintNames = nub $
83+ concatMap (namesIn [] ist) (map snd constraints)
84+
85+ mapM_ (checkConstraintName (map (\(x, _, _) -> x) ps)) constraintNames
86+
8187 logElab 1 $ "Building methods " ++ show mnames
8288 ims <- mapM (tdecl mnames) mdecls
8389 defs <- mapM (defdecl (map (\ (x,y,z) -> z) ims) constraint)
@@ -148,6 +154,14 @@ elabClass info syn_in doc fc constraints tn tnfc ps pDocs fds ds mcn cd
148154 $ tfail (At fc (Msg $ "Default instances must be for a superclass constraint on the containing class."))
149155 return ()
150156
157+ checkConstraintName :: [Name] -> Name -> Idris ()
158+ checkConstraintName bound cname
159+ | cname `notElem` bound
160+ = tclift $ tfail (At fc (Msg $ "Name " ++ show cname ++
161+ " is not bound in interface " ++ show tn
162+ ++ " " ++ showSep " " (map show bound)))
163+ | otherwise = return ()
164+
151165 impbind :: [(Name, PTerm)] -> PTerm -> PTerm
152166 impbind [] x = x
153167 impbind ((n, ty): ns) x = PPi impl n NoFC ty (impbind ns x)