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