fix: all refs are qualified

Author: cstml

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

@@ -9,7 +9,7 @@ module LambdaBuffers.Compiler.KindCheck (
   foldWithArrowToType,
 ) where
 
-import Control.Lens ((&), (.~), (^.))
+import Control.Lens (view, (&), (.~), (^.))
 import Control.Monad (void)
 import Control.Monad.Freer (Eff, Member, Members, interpret, reinterpret, run)
 import Control.Monad.Freer.Error (Error, runError, throwError)
@@ -21,7 +21,7 @@ import Data.Map qualified as M
 import LambdaBuffers.Compiler.KindCheck.Context (Context, context)
 import LambdaBuffers.Compiler.KindCheck.Inference qualified as I
 import LambdaBuffers.Compiler.KindCheck.Kind (Kind (KType, (:->:)), kind2ProtoKind)
-import LambdaBuffers.Compiler.KindCheck.Variable (Variable (ForeignRef, LocalRef, TyVar))
+import LambdaBuffers.Compiler.KindCheck.Variable (Variable (ForeignRef, TyVar))
 import LambdaBuffers.Compiler.ProtoCompat.Types qualified as PC
 
 --------------------------------------------------------------------------------
@@ -110,7 +110,7 @@ localStrategy = reinterpret $ \case
 runKindCheck :: forall effs {a}. Member Err effs => Eff (KindCheck ': effs) a -> Eff effs a
 runKindCheck = interpret $ \case
   -- TypesFromTyDef modName tydef -> runReader modName (tyDef2Types tydef)
-  InferTypeKind modName tyDef ctx k -> either (handleErr modName tyDef) pure $ I.infer ctx tyDef k
+  InferTypeKind modName tyDef ctx k -> either (handleErr modName tyDef) pure $ I.infer ctx tyDef k modName
   CheckKindConsistency modName def ctx k -> runReader modName $ resolveKindConsistency def ctx k
   GetSpecifiedKind modName tyDef -> do
     (_, k) <- tyDef2NameAndKind modName tyDef
@@ -120,11 +120,15 @@ runKindCheck = interpret $ \case
     handleErr modName td = \case
       I.InferUnboundTermErr uA -> do
         case uA of
-          LocalRef lr -> throwError . PC.CompKindCheckError $ PC.UnboundTyRefError td (PC.LocalI lr) modName
-          ForeignRef fr -> throwError . PC.CompKindCheckError $ PC.UnboundTyRefError td (PC.ForeignI fr) modName
+          ForeignRef fr ->
+            if (fr ^. #moduleName) == modName
+              then -- We're looking at the local module.
+                throwError . PC.CompKindCheckError $ PC.UnboundTyRefError td (PC.LocalI $ fr ^. PC.foreignRef2LocalRef) modName
+              else -- We're looking at a foreign module.
+                throwError . PC.CompKindCheckError $ PC.UnboundTyRefError td (PC.ForeignI fr) modName
           TyVar tv -> throwError . PC.CompKindCheckError $ PC.UnboundTyVarError td (PC.TyVar tv) modName
       I.InferUnifyTermErr (I.Constraint (k1, k2)) ->
-        throwError . PC.CompKindCheckError $ {-- error $ show k1 <>" <-> " <> show k2 --} PC.IncorrectApplicationError td (kind2ProtoKind k1) (kind2ProtoKind k2) modName
+        throwError . PC.CompKindCheckError $ PC.IncorrectApplicationError td (kind2ProtoKind k1) (kind2ProtoKind k2) modName
       I.InferRecursiveSubstitutionErr _ ->
         throwError . PC.CompKindCheckError $ PC.RecursiveKindError td modName
       I.InferImpossibleErr t ->
@@ -207,9 +211,8 @@ tyDefArgs2Context tydef = do
         k = pKind2Kind (tyarg ^. #argKind)
 
 tyDef2NameAndKind :: forall effs. PC.ModuleName -> PC.TyDef -> Eff effs (Variable, Kind)
-tyDef2NameAndKind _curModName tyDef = do
-  -- Names are local.
-  let name = LocalRef $ PC.LocalRef (tyDef ^. #tyName) (tyDef ^. #sourceInfo)
+tyDef2NameAndKind curModName tyDef = do
+  let name = ForeignRef $ view (PC.localRef2ForeignRef curModName) $ PC.LocalRef (tyDef ^. #tyName) (tyDef ^. #sourceInfo)
   let k = tyAbsLHS2Kind (tyDef ^. #tyAbs)
   pure (name, k)
 

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

@@ -24,7 +24,7 @@ import LambdaBuffers.Compiler.KindCheck.Derivation (Derivation (Abstraction, App
 import LambdaBuffers.Compiler.KindCheck.Judgement (Judgement (Judgement))
 import LambdaBuffers.Compiler.KindCheck.Kind (Kind (KType, KVar, (:->:)))
 import LambdaBuffers.Compiler.KindCheck.Type (Type (Abs, App, Constructor, Opaque, Product, Sum, Var, VoidT))
-import LambdaBuffers.Compiler.KindCheck.Variable (Atom, Variable (ForeignRef, LocalRef, TyVar))
+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)
@@ -40,6 +40,7 @@ import Data.Text qualified as T
 import Control.Lens ((&), (.~), (^.))
 import Data.Map qualified as M
 
+import LambdaBuffers.Compiler.ProtoCompat (localRef2ForeignRef)
 import Prettyprinter (
   Pretty (pretty),
   (<+>),
@@ -76,6 +77,7 @@ type Derive a =
   Members
     '[ Reader Context
      , Reader Kind
+     , Reader PC.ModuleName
      , State DerivationContext
      , Writer [Constraint]
      , Error InferErr
@@ -87,12 +89,30 @@ type Derive a =
 -- Runners
 
 -- | Run derivation builder - not unified yet.
-runDerive :: Context -> PC.TyAbs -> Kind -> Either InferErr (Derivation, [Constraint])
-runDerive ctx t k = run $ runError $ runWriter $ evalState (DC atoms) $ runReader ctx $ runReader k (derive t)
-
-infer :: Context -> PC.TyDef -> Kind -> Either InferErr Kind
-infer ctx t k = do
-  (d, c) <- runDerive (defContext <> ctx) (t ^. #tyAbs) k
+runDerive ::
+  Context ->
+  PC.TyAbs ->
+  Kind ->
+  PC.ModuleName ->
+  Either InferErr (Derivation, [Constraint])
+runDerive ctx t k localMod =
+  run $
+    runError $
+      runWriter $
+        evalState (DC atoms) $
+          runReader ctx $
+            runReader k $
+              runReader localMod $
+                derive t
+
+infer ::
+  Context ->
+  PC.TyDef ->
+  Kind ->
+  PC.ModuleName ->
+  Either InferErr Kind
+infer ctx t k localMod = do
+  (d, c) <- runDerive (defContext <> ctx) (t ^. #tyAbs) k localMod
   s <- runUnify' c
   let res = foldl (flip substitute) d s
   pure $ res ^. dTopKind
@@ -178,7 +198,8 @@ derive x = deriveTyAbs x
     deriveTyRef :: PC.TyRef -> Derive Derivation
     deriveTyRef = \case
       PC.LocalI r -> do
-        let ty = LocalRef r
+        localModule <- ask
+        let ty = ForeignRef $ r ^. localRef2ForeignRef localModule
         v <- getBinding ty
         c <- ask
         pure . Axiom . Judgement $ (c, Var ty, v)

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

@@ -1,4 +1,4 @@
-module LambdaBuffers.Compiler.KindCheck.Variable (Variable (LocalRef, ForeignRef, TyVar), Atom) where
+module LambdaBuffers.Compiler.KindCheck.Variable (Variable (ForeignRef, TyVar), Atom) where
 
 import Data.Text (Text)
 import GHC.Generics (Generic)
@@ -11,8 +11,9 @@ import Test.QuickCheck.Instances.Text ()
 type Atom = Text
 
 data Variable
-  = LocalRef PC.LocalRef
-  | ForeignRef PC.ForeignRef
+  = -- | Notionally all Refs. are fully qualified. The context determines if
+    -- they're local or not.
+    ForeignRef PC.ForeignRef
   | TyVar PC.VarName
   deriving stock (Eq, Ord, Show, Generic)
   deriving (Arbitrary) via GenericArbitrary Variable

lambda-buffers-compiler/src/LambdaBuffers/Compiler/ProtoCompat/Types.hs

@@ -6,6 +6,8 @@
 {-# OPTIONS_GHC -fconstraint-solver-iterations=0 #-}
 
 module LambdaBuffers.Compiler.ProtoCompat.Types (
+  foreignRef2LocalRef,
+  localRef2ForeignRef,
   ClassDef (..),
   ClassName (..),
   CompilerError (..),
@@ -53,6 +55,8 @@ module LambdaBuffers.Compiler.ProtoCompat.Types (
 ) where
 
 import Control.Exception (Exception)
+import Control.Lens (Getter, to, (^.))
+import Data.Generics.Labels ()
 import Data.Map (Map)
 import Data.Set (Set)
 import Data.Text (Text)
@@ -173,11 +177,32 @@ data ForeignRef = ForeignRef {tyName :: TyName, moduleName :: ModuleName, source
   deriving (Arbitrary) via GenericArbitrary ForeignRef
   deriving anyclass (SOP.Generic)
 
+foreignRef2LocalRef :: Getter ForeignRef LocalRef
+foreignRef2LocalRef =
+  to
+    ( \fr ->
+        LocalRef
+          { tyName = fr ^. #tyName
+          , sourceInfo = fr ^. #sourceInfo
+          }
+    )
+
 data LocalRef = LocalRef {tyName :: TyName, sourceInfo :: SourceInfo}
   deriving stock (Show, Eq, Ord, Generic)
   deriving (Arbitrary) via GenericArbitrary LocalRef
   deriving anyclass (SOP.Generic)
 
+localRef2ForeignRef :: ModuleName -> Getter LocalRef ForeignRef
+localRef2ForeignRef modName =
+  to
+    ( \lr ->
+        ForeignRef
+          { tyName = lr ^. #tyName
+          , sourceInfo = lr ^. #sourceInfo
+          , moduleName = modName
+          }
+    )
+
 data TyRef = LocalI LocalRef | ForeignI ForeignRef
   deriving stock (Show, Eq, Ord, Generic)
   deriving (Arbitrary) via GenericArbitrary TyRef