@@ -66,9 +66,10 @@ elabData info syn doc argDocs fc opts (PDatadecl n t_in dcons)
66 undef <- isUndefined fc n
66 undef <- isUndefined fc n
67 (cty, _, t, inacc) <- buildType info syn fc [] n t_in
67 (cty, _, t, inacc) <- buildType info syn fc [] n t_in
68 -- if n is defined already, make sure it is just a type declaration
68 -- if n is defined already, make sure it is just a type declaration
69− -- with the same type we've just elaborated
69+ -- with the same type we've just elaborated, and no constructors
70 i <- getIState
71 i <- getIState
71− checkDefinedAs fc n cty (tt_ctxt i)
72+ checkDefinedAs fc n cty i
72 -- temporary, to check cons
73 -- temporary, to check cons
73 when undef $ updateContext (addTyDecl n (TCon 0 0) cty)
74 when undef $ updateContext (addTyDecl n (TCon 0 0) cty)
74 let cnameinfo = cinfo info (map cname dcons)
75 let cnameinfo = cinfo info (map cname dcons)
@@ -124,14 +125,18 @@ elabData info syn doc argDocs fc opts (PDatadecl n t_in dcons)
124 [oi] -> putIState ist{ idris_optimisation = addDef n oi{ detaggable = True } opt }
125 [oi] -> putIState ist{ idris_optimisation = addDef n oi{ detaggable = True } opt }
125 _ -> putIState ist{ idris_optimisation = addDef n (Optimise [] True) opt }
126 _ -> putIState ist{ idris_optimisation = addDef n (Optimise [] True) opt }
127− checkDefinedAs fc n t ctxt
128+ checkDefinedAs fc n t i
129+ = let defined = tclift $ tfail (At fc (AlreadyDefined n))
128− = case lookupDef n ctxt of
131+ case lookupDef n ctxt of
129 [] -> return ()
132 [] -> return ()
130 [TyDecl _ ty] ->
133 [TyDecl _ ty] ->
131 case converts ctxt [] t ty of
134 case converts ctxt [] t ty of
135+ OK () -> case lookupCtxtExact n (idris_datatypes i) of
132− OK () -> return ()
136+ Nothing -> return ()
133− _ -> tclift $ tfail (At fc (AlreadyDefined n))
137+ _ -> defined
134− _ -> tclift $ tfail (At fc (AlreadyDefined n))
138+ _ -> defined
135 -- parameters are names which are unchanged across the structure,
140 -- parameters are names which are unchanged across the structure,
136 -- which appear exactly once in the return type of a constructor
141 -- which appear exactly once in the return type of a constructor