update: change how variables find their kind

Author: cstml

lambda-buffers-compiler/src/LambdaBuffers/Compiler/KindCheck.hs

@@ -66,7 +66,13 @@ makeEffect ''KindCheck
 
 -- | The Check effect runner.
 runCheck :: Eff '[Check, Err] a -> Either CompilerErr a
-runCheck = run . runError . runKindCheck . localStrategy . moduleStrategy . globalStrategy
+runCheck =
+  run
+    . runError
+    . runKindCheck
+    . localStrategy
+    . moduleStrategy
+    . globalStrategy
 
 {- | Run the check - return the validated context or the failure. The main API
  function of the library.
@@ -168,9 +174,8 @@ resolveCreateContext ::
   Member Err effs =>
   PC.CompilerInput ->
   Eff effs Context
-resolveCreateContext ci = do
-  ctxs <- traverse module2Context (toList $ ci ^. #modules)
-  pure $ mconcat ctxs
+resolveCreateContext ci =
+  mconcat <$> traverse module2Context (toList $ ci ^. #modules)
 
 module2Context ::
   forall effs.
@@ -180,7 +185,9 @@ module2Context ::
   Eff effs Context
 module2Context m = do
   let typeDefinitions = toList $ m ^. #typeDefs
-  ctxs <- runReader (m ^. #moduleName) $ traverse tyDef2Context typeDefinitions
+  ctxs <-
+    runReader (m ^. #moduleName) $
+      traverse tyDef2Context typeDefinitions
   pure $ mconcat ctxs
 
 -- | Creates a Context entry from one type definition.
@@ -193,9 +200,9 @@ tyDef2Context ::
 tyDef2Context tyDef = do
   curModName <- ask @PC.ModuleName
   r <- tyDef2NameAndKind curModName tyDef
-  ctx2 <- tyDefArgs2Context tyDef
-  pure $ mempty & context .~ uncurry M.singleton r <> ctx2
+  pure $ mempty & context .~ uncurry M.singleton r
 
+{-
 {- | Gets the kind of the variables from the definition and adds them to the
  context.
 -}
@@ -209,6 +216,7 @@ tyDefArgs2Context tydef = do
       where
         v = TyVar (tyarg ^. #argName)
         k = pKind2Kind (tyarg ^. #argKind)
+-}
 
 tyDef2NameAndKind :: forall effs. PC.ModuleName -> PC.TyDef -> Eff effs (Variable, Kind)
 tyDef2NameAndKind curModName tyDef = do

lambda-buffers-compiler/src/LambdaBuffers/Compiler/KindCheck/Inference.hs

@@ -22,13 +22,13 @@ import Data.Foldable (foldrM)
 import LambdaBuffers.Compiler.KindCheck.Context (Context (Context), addContext, context, getAllContext)
 import LambdaBuffers.Compiler.KindCheck.Derivation (Derivation (Abstraction, Application, Axiom, Implication), dTopKind, dType)
 import LambdaBuffers.Compiler.KindCheck.Judgement (Judgement (Judgement))
-import LambdaBuffers.Compiler.KindCheck.Kind (Kind (KType, KVar, (:->:)))
+import LambdaBuffers.Compiler.KindCheck.Kind (Kind (KType, KVar, (:->:)), protoKind2Kind)
 import LambdaBuffers.Compiler.KindCheck.Type (Type (Abs, App, Constructor, Opaque, Product, Sum, Var, VoidT))
 import LambdaBuffers.Compiler.KindCheck.Variable (Atom, Variable (ForeignRef, TyVar))
 
 import Control.Monad.Freer (Eff, Member, Members, run)
 import Control.Monad.Freer.Error (Error, runError, throwError)
-import Control.Monad.Freer.Reader (Reader, ask, asks, runReader)
+import Control.Monad.Freer.Reader (Reader, ask, asks, local, runReader)
 import Control.Monad.Freer.State (State, evalState, get, put)
 import Control.Monad.Freer.Writer (Writer, runWriter, tell)
 
@@ -37,7 +37,7 @@ import LambdaBuffers.Compiler.ProtoCompat qualified as PC
 import Data.String (fromString)
 import Data.Text qualified as T
 
-import Control.Lens ((&), (.~), (^.))
+import Control.Lens ((%~), (&), (.~), (^.))
 import Data.Map qualified as M
 
 import LambdaBuffers.Compiler.ProtoCompat (localRef2ForeignRef)
@@ -140,16 +140,23 @@ derive x = deriveTyAbs x
       case M.toList (tyabs ^. #tyArgs) of
         [] -> deriveTyBody (x ^. #tyBody)
         a@(n, _) : as -> do
-          vK <- getBinding (TyVar n)
+          vK <- protoKind2Kind <$> getVarAnnotation tyabs n
           freshT <- KVar <$> fresh
+          ctx <- ask
+
+          let newContext = ctx & addContext %~ (<> M.singleton (TyVar n) vK)
           let newAbs = tyabs & #tyArgs .~ uncurry M.singleton a
           let restAbs = tyabs & #tyArgs .~ M.fromList as
-          restF <- deriveTyAbs restAbs
+
+          restF <- local (const newContext) $ deriveTyAbs restAbs
+
           let uK = restF ^. dTopKind
           tell [Constraint (freshT, uK)]
-          ctx <- ask
           pure $ Abstraction (Judgement (ctx, Abs newAbs, vK :->: freshT)) restF
 
+    getVarAnnotation :: PC.TyAbs -> PC.VarName -> Derive PC.Kind
+    getVarAnnotation tyabs varname = pure $ ((tyabs ^. #tyArgs) M.! varname) ^. #argKind
+
     deriveTyBody :: PC.TyBody -> Derive Derivation
     deriveTyBody = \case
       PC.OpaqueI si -> do