@@ -74,9 +74,11 @@ elabData info syn doc argDocs fc opts (PDatadecl n nfc t_in dcons)
74 -- temporary, to check cons
74 -- temporary, to check cons
75 when undef $ updateContext (addTyDecl n (TCon 0 0) cty)
75 when undef $ updateContext (addTyDecl n (TCon 0 0) cty)
76 let cnameinfo = cinfo info (map cname dcons)
76 let cnameinfo = cinfo info (map cname dcons)
77− let unique = case getRetTy cty of
77+ unique <- case getRetTy (normalise (tt_ctxt i) [] cty) of
78− UType UniqueType -> True
78+ UType UniqueType -> return True
79+ UType _ -> return False
79− _ -> False
80+ TType _ -> return False
81+ rt -> tclift $ tfail (At fc (Elaborating "type constructor " n (Msg "Not a valid type constructor")))
80 cons <- mapM (elabCon cnameinfo syn n codata (getRetTy cty) ckind) dcons
82 cons <- mapM (elabCon cnameinfo syn n codata (getRetTy cty) ckind) dcons
81 ttag <- getName
83 ttag <- getName
82 i <- getIState
84 i <- getIState