Merge remote-tracking branch 'origin/bladyjoker/proto-compat-rework' into bladyjoker/frontend

Author: bladyjoker

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

@@ -36,7 +36,7 @@ import LambdaBuffers.Compiler.KindCheck.Inference (
  )
 import LambdaBuffers.Compiler.KindCheck.Inference qualified as I
 import LambdaBuffers.Compiler.KindCheck.Kind (kind2ProtoKind)
-import LambdaBuffers.Compiler.KindCheck.Type (Type (App), tyProd, tySum, tyUnit, tyVoid)
+import LambdaBuffers.Compiler.KindCheck.Type (Type (App), tyOpaque, tyProd, tySum, tyUnit, tyVoid)
 import LambdaBuffers.Compiler.KindCheck.Variable (Variable (ForeignRef, LocalRef))
 import LambdaBuffers.Compiler.ProtoCompat ()
 import LambdaBuffers.Compiler.ProtoCompat.Types qualified as PC
@@ -459,7 +459,7 @@ tyBody2Types ::
   PC.TyBody ->
   Eff eff [Type]
 tyBody2Types = \case
-  PC.OpaqueI _ -> pure [Var $ LocalRef "Opaque"]
+  PC.OpaqueI _ -> pure [Var tyOpaque]
   PC.SumI s -> sum2Types s
 
 sum2Types ::

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

@@ -21,7 +21,7 @@ import LambdaBuffers.Compiler.KindCheck.Context (Context (Context), addContext,
 import LambdaBuffers.Compiler.KindCheck.Derivation (Derivation (Abstraction, Application, Axiom))
 import LambdaBuffers.Compiler.KindCheck.Judgement (Judgement (Judgement))
 import LambdaBuffers.Compiler.KindCheck.Kind (Kind (KVar, Type, (:->:)))
-import LambdaBuffers.Compiler.KindCheck.Type (Type (Abs, App, Var), tyProd, tySum, tyUnit, tyVoid)
+import LambdaBuffers.Compiler.KindCheck.Type (Type (Abs, App, Var), tyOpaque, tyProd, tySum, tyUnit, tyVoid)
 import LambdaBuffers.Compiler.KindCheck.Variable (Atom, Variable)
 
 import Control.Monad.Freer (Eff, Member, Members, run)
@@ -87,20 +87,23 @@ runDerive ctx t = run $ runError $ runWriter $ evalState (DC atoms) $ runReader
 
 infer :: Context -> Type -> Either InferErr Kind
 infer ctx t = do
-  (d, c) <- runDerive (defTerms <> ctx) t
+  (d, c) <- runDerive (defContext <> ctx) t
   s <- runUnify' c
   let res = foldl (flip substitute) d s
   pure $ res ^. topKind
-  where
-    defTerms =
-      mempty
-        & context
-          .~ M.fromList
-            [ (tySum, Type :->: Type :->: Type)
-            , (tyProd, Type :->: Type :->: Type)
-            , (tyUnit, Type)
-            , (tyVoid, Type)
-            ]
+
+-- | Default KC Context.
+defContext :: Context
+defContext =
+  mempty
+    & context
+      .~ M.fromList
+        [ (tySum, Type :->: Type :->: Type)
+        , (tyProd, Type :->: Type :->: Type)
+        , (tyUnit, Type)
+        , (tyVoid, Type)
+        , (tyOpaque, Type)
+        ]
 
 --------------------------------------------------------------------------------
 -- Implementation