@@ -589,7 +589,7 @@ elabClass info syn fc constraints tn ps ds
589589 clause _ = False
590590
591591 cfun cn c syn all con
592− = do let cfn = UN ('@':show cn ++ "#" ++ show con)
592+ = do let cfn = UN ('@':'@':show cn ++ "#" ++ show con)
593593 let mnames = take (length all) $ map (\x -> MN x "meth") [0..]
594594 let capp = PApp fc (PRef fc cn) (map (pexp . PRef fc) mnames)
595595 let lhs = PApp fc (PRef fc cfn) [pconst capp]
@@ -662,6 +662,9 @@ elabInstance info syn fc cs n ps t ds
662662 [c] -> return c
663663 _ -> fail $ show fc ++ ":" ++ show n ++ " is not a type class"
664664 let iname = UN ('@':show n ++ "$" ++ show ps)
665+ -- if the instance type matches any of the instances we have already,
666+ -- then it's overlapping, so report an error
667+ mapM_ (checkNotOverlapping i t) (class_instances ci)
665668 addInstance n iname
666669 elabType info syn fc [] iname t
667670 let ips = zip (class_params ci) ps
@@ -695,6 +698,23 @@ elabInstance info syn fc cs n ps t ds
695698 elabDecl info idecl
696699 addIBC (IBCInstance n iname)
697700 where
701+ checkNotOverlapping i t n
702+ | take 2 (show n) == "@@" = return ()
703+ | otherwise
704+ = case lookupTy Nothing n (tt_ctxt i) of
705+ [t'] -> let tret = getRetType t
706+ tret' = getRetType (delab i t') in
707+ case matchClause i tret' tret of
708+ Right _ -> overlapping tret tret'
709+ Left _ -> case matchClause i tret tret' of
710+ Right _ -> overlapping tret tret'
711+ Left _ -> return ()
712+ _ -> return ()
713+ overlapping t t' = tclift $ tfail (At fc (Msg $
714+ "Overlapping instance: " ++ show t' ++ " already defined"))
715+ getRetType (PPi _ _ _ sc) = getRetType sc
716+ getRetType t = t
717+
698718 mkMethApp (n, _, _, ty) = lamBind 0 ty (papp fc (PRef fc n) (methArgs 0 ty))
699719 lamBind i (PPi (Constraint _ _) _ _ sc) sc'
700720 = PLam (MN i "meth") Placeholder (lamBind (i+1) sc sc')