add IDs to kinds

we take advantage of this to output proper universally-unique IDs in `viewTreeKind`

Signed-off-by: George Thomas <georgefsthomas@gmail.com>

primer-api/src/Primer/API.hs

@@ -96,7 +96,7 @@ import Control.Monad.Trans (MonadTrans)
 import Control.Monad.Writer (MonadWriter)
 import Control.Monad.Zip (MonadZip)
 import Data.Map qualified as Map
-import Data.Tuple.Extra (curry3)
+import Data.Tuple.Extra (curry3, (&&&))
 import Optics (ifoldr, over, preview, to, traverseOf, view, (%), (^.), _Just)
 import Primer.API.NodeFlavor qualified as Flavor
 import Primer.API.RecordPair (RecordPair (RecordPair))
@@ -154,7 +154,9 @@ import Primer.Core (
   GlobalName (..),
   HasID (..),
   ID,
-  Kind (..),
+  Kind,
+  Kind' (..),
+  KindMeta,
   LVarName,
   ModuleName,
   PrimCon (..),
@@ -172,6 +174,7 @@ import Primer.Core (
   unsafeMkLocalName,
   _bindMeta,
   _exprMetaLens,
+  _kindMeta,
   _type,
   _typeMeta,
   _typeMetaLens,
@@ -398,8 +401,8 @@ data APILog
   | GetProgram' (ReqResp SessionId Prog)
   | GetProgram (ReqResp SessionId App.Prog)
   | Edit (ReqResp (SessionId, MutationRequest) (Either ProgError App.Prog))
-  | VariablesInScope (ReqResp (SessionId, (GVarName, ID)) (Either ProgError (([(TyVarName, Kind)], [(LVarName, Type' ())]), [(GVarName, Type' ())])))
-  | GenerateNames (ReqResp (SessionId, ((GVarName, ID), Either (Maybe (Type' ())) (Maybe Kind))) (Either ProgError [Name.Name]))
+  | VariablesInScope (ReqResp (SessionId, (GVarName, ID)) (Either ProgError (([(TyVarName, Kind' ())], [(LVarName, Type' ())]), [(GVarName, Type' ())])))
+  | GenerateNames (ReqResp (SessionId, ((GVarName, ID), Either (Maybe (Type' ())) (Maybe (Kind' ())))) (Either ProgError [Name.Name]))
   | EvalStep (ReqResp (SessionId, EvalReq) (Either ProgError EvalResp))
   | EvalFull (ReqResp (SessionId, EvalFullReq) (Either ProgError App.EvalFullResp))
   | EvalFull' (ReqResp (SessionId, Maybe TerminationBound, GVarName) EvalFullResp)
@@ -996,7 +999,7 @@ viewTreeType' t0 = case t0 of
       -- for now we expect all kinds in student programs to be `KType`
       -- but we show something for other kinds, in order to keep rendering injective
       withKindAnn = case k of
-        KType -> identity
+        KType _ -> identity
         _ -> (<> (" :: " <> show k))
   TLet _ n t b ->
     Tree
@@ -1008,41 +1011,34 @@ viewTreeType' t0 = case t0 of
   where
     nodeId = t0 ^. _typeMetaLens
 
--- | Like 'viewTreeType', but for kinds. This generates ids
+-- | Like 'viewTreeType', but for kinds.
 viewTreeKind :: Kind -> Tree
-viewTreeKind = flip evalState (0 :: Integer) . go
-  where
-    go k = do
-      id' <- get
-      let nodeId = "kind" <> show id'
-      modify succ
-      case k of
-        KType ->
-          pure $
-            Tree
-              { nodeId
-              , body = NoBody Flavor.KType
-              , childTrees = []
-              , rightChild = Nothing
-              }
-        KHole ->
-          pure $
-            Tree
-              { nodeId
-              , body = NoBody Flavor.KHole
-              , childTrees = []
-              , rightChild = Nothing
-              }
-        KFun k1 k2 -> do
-          k1tree <- go k1
-          k2tree <- go k2
-          pure $
-            Tree
-              { nodeId
-              , body = NoBody Flavor.KFun
-              , childTrees = [k1tree, k2tree]
-              , rightChild = Nothing
-              }
+viewTreeKind = viewTreeKind' . over _kindMeta (show . view _id)
+
+-- | Like 'viewTreeType'', but for kinds.
+viewTreeKind' :: Kind' Text -> Tree
+viewTreeKind' = \case
+  KType nodeId ->
+    Tree
+      { nodeId
+      , body = NoBody Flavor.KType
+      , childTrees = []
+      , rightChild = Nothing
+      }
+  KHole nodeId ->
+    Tree
+      { nodeId
+      , body = NoBody Flavor.KHole
+      , childTrees = []
+      , rightChild = Nothing
+      }
+  KFun nodeId k1 k2 ->
+    Tree
+      { nodeId
+      , body = NoBody Flavor.KFun
+      , childTrees = [viewTreeKind' k1, viewTreeKind' k2]
+      , rightChild = Nothing
+      }
 
 globalName :: GlobalName k -> Name
 globalName n = Name{qualifiedModule = Just $ Core.qualifiedModule n, baseName = Core.baseName n}
@@ -1061,14 +1057,14 @@ variablesInScope ::
   (MonadIO m, MonadThrow m, MonadAPILog l m) =>
   SessionId ->
   (GVarName, ID) ->
-  PrimerM m (Either ProgError (([(TyVarName, Kind)], [(LVarName, Type' ())]), [(GVarName, Type' ())]))
+  PrimerM m (Either ProgError (([(TyVarName, Kind' ())], [(LVarName, Type' ())]), [(GVarName, Type' ())]))
 variablesInScope = curry $ logAPI (leftResultError VariablesInScope) $ \(sid, (defname, exprid)) ->
   liftQueryAppM (handleQuestion (App.VariablesInScope defname exprid)) sid
 
 generateNames ::
   (MonadIO m, MonadThrow m, MonadAPILog l m) =>
   SessionId ->
-  ((GVarName, ID), Either (Maybe (Type' ())) (Maybe Kind)) ->
+  ((GVarName, ID), Either (Maybe (Type' ())) (Maybe (Kind' ()))) ->
   PrimerM m (Either ProgError [Name.Name])
 generateNames = curry $ logAPI (leftResultError GenerateNames) $ \(sid, ((defname, exprid), tk)) ->
   liftQueryAppM (handleQuestion $ GenerateName defname exprid tk) sid
@@ -1220,13 +1216,13 @@ findASTDef allDefs def = case allDefs Map.!? def of
   Just (_, Def.DefPrim _) -> throwM $ UnexpectedPrimDef def
   Just (editable, Def.DefAST d) -> pure (editable, d)
 
-findASTTypeDef :: MonadThrow m => Map TyConName (Editable, TypeDef.TypeDef a) -> TyConName -> m (Editable, ASTTypeDef a)
+findASTTypeDef :: MonadThrow m => Map TyConName (Editable, TypeDef.TypeDef a b) -> TyConName -> m (Editable, ASTTypeDef a b)
 findASTTypeDef allTypeDefs def = case allTypeDefs Map.!? def of
   Nothing -> throwM $ UnknownTypeDef def
   Just (_, TypeDef.TypeDefPrim _) -> throwM $ UnexpectedPrimTypeDef def
   Just (editable, TypeDef.TypeDefAST d) -> pure (editable, d)
 
-findASTTypeOrTermDef :: MonadThrow f => App.Prog -> Selection -> f (Editable, Either (ASTTypeDef TypeMeta) ASTDef)
+findASTTypeOrTermDef :: MonadThrow f => App.Prog -> Selection -> f (Editable, Either (ASTTypeDef TypeMeta KindMeta) ASTDef)
 findASTTypeOrTermDef prog = \case
   App.SelectionTypeDef sel ->
     Left <<$>> findASTTypeDef (progAllTypeDefsMeta prog) sel.def
@@ -1334,7 +1330,7 @@ getSelectionTypeOrKind = curry $ logAPI (noError GetTypeOrKind) $ \(sid, sel0) -
       def <- snd <$> findASTTypeDef allTypeDefs sel.def
       case sel.node of
         -- type def itself selected - return its kind
-        Nothing -> pure $ Kind $ viewTreeKind $ typeDefKind $ TypeDef.TypeDefAST def
+        Nothing -> pure $ Kind $ viewTreeKindGenIDs $ typeDefKind $ forgetTypeDefMetadata $ TypeDef.TypeDefAST def
         -- param node selected - return its kind
         Just (TypeDefParamNodeSelection p) ->
           maybe (throw' $ ParamNotFound p) (pure . Kind . viewTreeKind . snd) $
@@ -1376,4 +1372,9 @@ getSelectionTypeOrKind = curry $ logAPI (noError GetTypeOrKind) $ \(sid, sel0) -
     viewTypeKind :: TypeMeta -> TypeOrKind
     viewTypeKind = Kind . fromMaybe trivialTree . viewTypeKind'
     viewTypeKind' :: TypeMeta -> Maybe Tree
-    viewTypeKind' = preview $ _type % _Just % to viewTreeKind
+    viewTypeKind' = preview $ _type % _Just % to viewTreeKindGenIDs
+    viewTreeKindGenIDs :: Kind' () -> Tree
+    viewTreeKindGenIDs =
+      viewTreeKind' . flip evalState (0 :: Integer) . traverseOf
+        _kindMeta
+        \() -> state $ show &&& succ

primer-api/test/Tests/API.hs

@@ -157,11 +157,11 @@ unit_viewTreeType_injective_var =
 
 unit_viewTreeType_injective_forall_param :: Assertion
 unit_viewTreeType_injective_forall_param =
-  distinctTreeType (tforall "a" KType tEmptyHole) (tforall "b" KType tEmptyHole)
+  distinctTreeType (tforall "a" (KType ()) tEmptyHole) (tforall "b" (KType ()) tEmptyHole)
 
 unit_viewTreeType_injective_forall_kind :: Assertion
 unit_viewTreeType_injective_forall_kind =
-  distinctTreeType (tforall "a" KType tEmptyHole) (tforall "a" KHole tEmptyHole)
+  distinctTreeType (tforall "a" (KType ()) tEmptyHole) (tforall "a" (KHole ()) tEmptyHole)
 
 distinctTreeExpr :: S Expr -> S Expr -> Assertion
 distinctTreeExpr e1 e2 =

primer-service/src/Primer/Client.hs

@@ -49,7 +49,7 @@ import Primer.App (
 import Primer.Core (
   GVarName,
   ID,
-  Kind,
+  Kind',
   LVarName,
   TyVarName,
   Type',
@@ -149,13 +149,13 @@ edit sid req = apiClient // API.sessionsAPI // API.sessionAPI /: sid // API.edit
 variablesInScope ::
   SessionId ->
   (GVarName, ID) ->
-  ClientM (Either ProgError (([(TyVarName, Kind)], [(LVarName, Type' ())]), [(GVarName, Type' ())]))
+  ClientM (Either ProgError (([(TyVarName, Kind' ())], [(LVarName, Type' ())]), [(GVarName, Type' ())]))
 variablesInScope sid ctx = apiClient // API.sessionsAPI // API.sessionAPI /: sid // API.questionAPI // API.variablesInScope /: ctx
 
 -- | As 'Primer.API.generateNames'.
 generateNames ::
   SessionId ->
-  ((GVarName, ID), Either (Maybe (Type' ())) (Maybe Kind)) ->
+  ((GVarName, ID), Either (Maybe (Type' ())) (Maybe (Kind' ()))) ->
   ClientM (Either ProgError [Name])
 generateNames sid ctx = apiClient // API.sessionsAPI // API.sessionAPI /: sid // API.questionAPI // API.generateNames /: ctx
 

primer-service/src/Primer/Servant/API.hs

@@ -23,7 +23,7 @@ import Primer.App (
 import Primer.Core (
   GVarName,
   ID,
-  Kind,
+  Kind',
   LVarName,
   TyVarName,
   Type',
@@ -67,25 +67,25 @@ data RootAPI mode = RootAPI
   , adminAPI ::
       mode
         :- "admin"
-          :> NamedRoutes AdminAPI
+        :> NamedRoutes AdminAPI
   , sessionsAPI ::
       mode
         :- "sessions"
-          :> NamedRoutes SessionsAPI
+        :> NamedRoutes SessionsAPI
   }
   deriving stock (Generic)
 
 newtype AdminAPI mode = AdminAPI
   { flushSessions ::
       mode
         :- "flush-sessions"
-          :> Summary "Flush the in-memory session database"
-          :> Description
-              "Flush the in-memory session database. Note that \
-              \all dirty state will be saved to the persistent \
-              \database before it's discarded from memory; i.e., \
-              \this is a non-destructive operation."
-          :> Put '[JSON] NoContent
+        :> Summary "Flush the in-memory session database"
+        :> Description
+            "Flush the in-memory session database. Note that \
+            \all dirty state will be saved to the persistent \
+            \database before it's discarded from memory; i.e., \
+            \this is a non-destructive operation."
+        :> Put '[JSON] NoContent
   }
   deriving stock (Generic)
 
@@ -96,21 +96,21 @@ data SessionsAPI mode = SessionsAPI
   , addSession ::
       mode
         :- "add-session"
-          :> Summary "Directly add a session to the database"
-          :> Description
-              "Given an existing app and a proposed session name, \
-              \create a new session and return its session ID. If the \
-              \given session name is invalid, it will be replaced with \
-              \a default session name. However, this is not reflected \
-              \in the returned status code. Query the returned session ID \
-              \to determine the actual session name that was assigned."
-          :> Capture' '[Description "The session's name"] "name" Text
-          :> ReqBody '[JSON] App
-          :> Post '[JSON] SessionId
+        :> Summary "Directly add a session to the database"
+        :> Description
+            "Given an existing app and a proposed session name, \
+            \create a new session and return its session ID. If the \
+            \given session name is invalid, it will be replaced with \
+            \a default session name. However, this is not reflected \
+            \in the returned status code. Query the returned session ID \
+            \to determine the actual session name that was assigned."
+        :> Capture' '[Description "The session's name"] "name" Text
+        :> ReqBody '[JSON] App
+        :> Post '[JSON] SessionId
   , sessionAPI ::
       mode
         :- Capture' '[Description "The session ID"] "sessionId" SessionId
-          :> NamedRoutes SessionAPI
+        :> NamedRoutes SessionAPI
   }
   deriving stock (Generic)
 
@@ -120,59 +120,59 @@ data SessionAPI mode = SessionAPI
   , getProgram ::
       mode
         :- "program"
-          :> Summary "Get the current program program state"
-          :> Get '[JSON] Prog
+        :> Summary "Get the current program program state"
+        :> Get '[JSON] Prog
   , getApp ::
       mode
         :- "app"
-          :> Summary "Get the current app"
-          :> Get '[JSON] App
+        :> Summary "Get the current app"
+        :> Get '[JSON] App
   , getSessionName :: GetSessionName mode
   , setSessionName :: SetSessionName mode
   , editSession ::
       mode
         :- "edit"
-          :> Summary "Edit the program"
-          :> Description "Submit an action, returning the updated program state."
-          :> ReqBody '[JSON] MutationRequest
-          :> Post '[JSON] (Either ProgError Prog)
+        :> Summary "Edit the program"
+        :> Description "Submit an action, returning the updated program state."
+        :> ReqBody '[JSON] MutationRequest
+        :> Post '[JSON] (Either ProgError Prog)
   , questionAPI ::
       mode
         :- "question"
-          :> NamedRoutes QuestionAPI
+        :> NamedRoutes QuestionAPI
   , evalStep ::
       mode
         :- "eval-step"
-          :> Summary "Perform one step of evaluation on the given expression"
-          :> ReqBody '[JSON] EvalReq
-          :> Post '[JSON] (Either ProgError EvalResp)
+        :> Summary "Perform one step of evaluation on the given expression"
+        :> ReqBody '[JSON] EvalReq
+        :> Post '[JSON] (Either ProgError EvalResp)
   , evalFull ::
       mode
         :- "eval"
-          :> Summary "Evaluate the given expression to normal form (or time out)"
-          :> ReqBody '[JSON] EvalFullReq
-          :> Post '[JSON] (Either ProgError EvalFullResp)
+        :> Summary "Evaluate the given expression to normal form (or time out)"
+        :> ReqBody '[JSON] EvalFullReq
+        :> Post '[JSON] (Either ProgError EvalFullResp)
   }
   deriving stock (Generic)
 
 data QuestionAPI mode = QuestionAPI
   { variablesInScope ::
       mode
         :- "variables-in-scope"
-          :> Summary "Ask what variables are in scope for the given node ID"
-          :> ReqBody '[JSON] (GVarName, ID)
-          :> Post '[JSON] (Either ProgError (([(TyVarName, Kind)], [(LVarName, Type' ())]), [(GVarName, Type' ())]))
+        :> Summary "Ask what variables are in scope for the given node ID"
+        :> ReqBody '[JSON] (GVarName, ID)
+        :> Post '[JSON] (Either ProgError (([(TyVarName, Kind' ())], [(LVarName, Type' ())]), [(GVarName, Type' ())]))
   , generateNames ::
       mode
         :- "generate-names"
-          :> Summary "Ask for a list of possible names at the given location"
-          :> Description
-              "Ask for a list of possible names for a binding \
-              \at the given location. This method would be GET \
-              \(since it doesn't modify any state) but we need \
-              \to provide a request body, which isn't well \
-              \supported for GET requests."
-          :> ReqBody '[JSON] ((GVarName, ID), Either (Maybe (Type' ())) (Maybe Kind))
-          :> Post '[JSON] (Either ProgError [Name])
+        :> Summary "Ask for a list of possible names at the given location"
+        :> Description
+            "Ask for a list of possible names for a binding \
+            \at the given location. This method would be GET \
+            \(since it doesn't modify any state) but we need \
+            \to provide a request body, which isn't well \
+            \supported for GET requests."
+        :> ReqBody '[JSON] ((GVarName, ID), Either (Maybe (Type' ())) (Maybe (Kind' ())))
+        :> Post '[JSON] (Either ProgError [Name])
   }
   deriving stock (Generic)

primer/gen/Primer/Gen/App.hs

@@ -26,7 +26,7 @@ import Primer.App (
   mkApp,
   tcWholeProgWithImports,
  )
-import Primer.Core (GlobalName (baseName), Kind (KType), ModuleName (ModuleName), qualifyName)
+import Primer.Core (GlobalName (baseName), Kind' (KType), ModuleName (ModuleName), qualifyName)
 import Primer.Core.Utils (forgetTypeMetadata, generateIDs, generateTypeIDs)
 import Primer.Def (ASTDef (ASTDef), Def (DefAST), defType)
 import Primer.Module (Module (Module, moduleDefs, moduleName, moduleTypes), moduleDefsQualified, moduleTypesQualified)
@@ -108,7 +108,7 @@ genProg sh initialImports = local (extendCxtByModules initialImports) $ do
 -- Generate a mutually-recursive group of term definitions
 genASTDefGroup :: ModuleName -> GenT WT (Map Name Def)
 genASTDefGroup mod = do
-  nts <- genList 5 $ (\n t -> (qualifyName mod n, t)) <$> freshNameForCxt <*> genWTType KType
+  nts <- genList 5 $ (\n t -> (qualifyName mod n, t)) <$> freshNameForCxt <*> genWTType (KType ())
   nTyTms <- local (extendGlobalCxt nts) $ for nts $ \(n, ty) -> (n,ty,) <$> genChk ty
   fmap M.fromList . for nTyTms $ \(n, ty, tm) -> do
     tm' <- generateIDs tm