@@ -78,6 +78,12 @@ elabClass info syn_in doc fc constraints tn tnfc ps pDocs fds ds mcn cd
78 let idecls = filter instdecl ds -- default superclass instance declarations
78 let idecls = filter instdecl ds -- default superclass instance declarations
79 mapM_ checkDefaultSuperclassInstance idecls
79 mapM_ checkDefaultSuperclassInstance idecls
80 let mnames = map getMName mdecls
80 let mnames = map getMName mdecls
82+ let constraintNames = nub $
83+ concatMap (namesIn [] ist) (map snd constraints)
85+ mapM_ (checkConstraintName (map (\(x, _, _) -> x) ps)) constraintNames
81 logElab 1 $ "Building methods " ++ show mnames
87 logElab 1 $ "Building methods " ++ show mnames
82 ims <- mapM (tdecl mnames) mdecls
88 ims <- mapM (tdecl mnames) mdecls
83 defs <- mapM (defdecl (map (\ (x,y,z) -> z) ims) constraint)
89 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
148 $ tfail (At fc (Msg $ "Default instances must be for a superclass constraint on the containing class."))
154 $ tfail (At fc (Msg $ "Default instances must be for a superclass constraint on the containing class."))
149 return ()
155 return ()
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 ()
151 impbind :: [(Name, PTerm)] -> PTerm -> PTerm
165 impbind :: [(Name, PTerm)] -> PTerm -> PTerm
152 impbind [] x = x
166 impbind [] x = x
153 impbind ((n, ty): ns) x = PPi impl n NoFC ty (impbind ns x)
167 impbind ((n, ty): ns) x = PPi impl n NoFC ty (impbind ns x)