syntax sugar for self types on ADTs

the following syntax:

data[] Bool { #True:Bool #False:Bool }: Bool

will desugar to:

$(s: Bool) data[] Bool { #True:Bool #False:Bool }

the extra self type is useful for equality, for the reasons below:
https://gist.github.com/VictorTaelin/3f748a46e95071e29462b1ac93c294c5

src/Kind/Parse.hs

@@ -248,7 +248,14 @@ parseDat = withSrc $ do
     tele <- parseTele
     return $ Ctr nm tele
   char_end '}'
-  return $ Dat scp cts
+  ann <- P.optionMaybe $ P.try $ do
+    skip
+    char_skp ':'
+    parseTerm
+  let dat = Dat scp cts
+  return $ case ann of
+    Just a  -> Slf "" a (\x -> dat)
+    Nothing -> dat
 
 parseTele :: Parser Tele
 parseTele = do