@@ -181,6 +181,9 @@ elabData info syn doc fc opts (PDatadecl n t_in dcons)
181 (errAt "data declaration " n (erun fc (build i info False n t)))
181 (errAt "data declaration " n (erun fc (build i info False n t)))
182 def' <- checkDef fc defer
182 def' <- checkDef fc defer
183 let def'' = map (\(n, (i, top, t)) -> (n, (i, top, t, True))) def'
183 let def'' = map (\(n, (i, top, t)) -> (n, (i, top, t, True))) def'
184+ -- if n is defined already, make sure it is just a type declaration
185+ -- with the same type we've just elaborated
186+ checkDefinedAs fc n t' (tt_ctxt i)
184 addDeferredTyCon def''
187 addDeferredTyCon def''
185 mapM_ (elabCaseBlock info []) is
188 mapM_ (elabCaseBlock info []) is
186 (cty, _) <- recheckC fc [] t'
189 (cty, _) <- recheckC fc [] t'
@@ -205,6 +208,14 @@ elabData info syn doc fc opts (PDatadecl n t_in dcons)
205 if DefaultEliminator `elem` opts then evalStateT (elabEliminator params n t dcons info) Map.empty
208 if DefaultEliminator `elem` opts then evalStateT (elabEliminator params n t dcons info) Map.empty
206 else return ()
209 else return ()
211+ checkDefinedAs fc n t ctxt
212+ = case lookupDef n ctxt of
215+ case converts ctxt [] t ty of
217+ _ -> tclift $ tfail (At fc (AlreadyDefined n))
218+ _ -> tclift $ tfail (At fc (AlreadyDefined n))
208 -- parameters are names which are unchanged across the structure,
219 -- parameters are names which are unchanged across the structure,
209 -- which appear exactly once in the return type of a constructor
220 -- which appear exactly once in the return type of a constructor