@@ -181,6 +181,9 @@ elabData info syn doc fc opts (PDatadecl n t_in dcons)
181181 (errAt "data declaration " n (erun fc (build i info False n t)))
182182 def' <- checkDef fc defer
183183 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)
184187 addDeferredTyCon def''
185188 mapM_ (elabCaseBlock info []) is
186189 (cty, _) <- recheckC fc [] t'
@@ -205,6 +208,14 @@ elabData info syn doc fc opts (PDatadecl n t_in dcons)
205208 if DefaultEliminator `elem` opts then evalStateT (elabEliminator params n t dcons info) Map.empty
206209 else return ()
207210 where
211+ checkDefinedAs fc n t ctxt
212+ = case lookupDef n ctxt of
213+ [] -> return ()
214+ [TyDecl _ ty] ->
215+ case converts ctxt [] t ty of
216+ OK () -> return ()
217+ _ -> tclift $ tfail (At fc (AlreadyDefined n))
218+ _ -> tclift $ tfail (At fc (AlreadyDefined n))
208219 -- parameters are names which are unchanged across the structure,
209220 -- which appear exactly once in the return type of a constructor
210221