update: change Context to be Infoless - to get the right sort of equality

Author: cstml

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

@@ -14,14 +14,15 @@ import Control.Monad (void)
 import Control.Monad.Freer (Eff, Member, Members, interpret, reinterpret, run)
 import Control.Monad.Freer.Error (Error, runError, throwError)
 import Control.Monad.Freer.Reader (Reader, ask, runReader)
-import Control.Monad.Freer.State (State, evalState)
 import Control.Monad.Freer.TH (makeEffect)
+import Data.Default (Default (def))
 import Data.Foldable (Foldable (toList), traverse_)
 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, TyVar))
+import LambdaBuffers.Compiler.ProtoCompat.InfoLess (InfoLess, mkInfoLess)
 import LambdaBuffers.Compiler.ProtoCompat.Types qualified as PC
 
 --------------------------------------------------------------------------------
@@ -102,7 +103,7 @@ globalStrategy = reinterpret $ \case
 
 moduleStrategy :: Transform GlobalCheck ModuleCheck
 moduleStrategy = reinterpret $ \case
-  CreateContext ci -> evalState (mempty @(M.Map Variable PC.TyDef)) . resolveCreateContext $ ci
+  CreateContext ci -> resolveCreateContext ci
   ValidateModule cx md -> do
     traverse_ (kCTypeDefinition (md ^. #moduleName) cx) (md ^. #typeDefs)
 
@@ -117,9 +118,9 @@ runKindCheck :: forall effs {a}. Member Err effs => Eff (KindCheck ': 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 modName
-  CheckKindConsistency modName def ctx k -> runReader modName $ resolveKindConsistency def ctx k
+  CheckKindConsistency modName tydef ctx k -> runReader modName $ resolveKindConsistency tydef ctx k
   GetSpecifiedKind modName tyDef -> do
-    (_, k) <- tyDef2NameAndKind modName tyDef
+    (_, k) <- runReader modName $ tyDef2NameAndKind tyDef
     pure k
   where
     handleErr :: forall {b}. PC.ModuleName -> PC.TyDef -> I.InferErr -> Eff effs b
@@ -150,7 +151,7 @@ resolveKindConsistency ::
   Eff effs Kind
 resolveKindConsistency tydef _ctx inferredKind = do
   modname <- ask @PC.ModuleName
-  (_, k) <- tyDef2NameAndKind modname tydef
+  (_, k) <- tyDef2NameAndKind tydef
   guard tydef k inferredKind modname
   pure inferredKind
   where
@@ -165,64 +166,38 @@ resolveKindConsistency tydef _ctx inferredKind = do
 --------------------------------------------------------------------------------
 -- Context Creation
 
-{- | Resolver function for the context creation - it fails if two identical
- declarations are found.
--}
-resolveCreateContext ::
-  forall effs.
-  Member (State (M.Map Variable PC.TyDef)) effs =>
-  Member Err effs =>
-  PC.CompilerInput ->
-  Eff effs Context
+-- | Resolver function for the context creation. There is a guarantee from ProtoCompat that the input is sanitised.
+resolveCreateContext :: forall effs. PC.CompilerInput -> Eff effs Context
 resolveCreateContext ci =
   mconcat <$> traverse module2Context (toList $ ci ^. #modules)
 
-module2Context ::
-  forall effs.
-  Member (State (M.Map Variable PC.TyDef)) effs =>
-  Member Err effs =>
-  PC.Module ->
-  Eff effs Context
+module2Context :: forall effs. PC.Module -> 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.
 tyDef2Context ::
   forall effs.
   Member (Reader PC.ModuleName) effs =>
-  Member Err effs =>
   PC.TyDef ->
   Eff effs Context
 tyDef2Context tyDef = do
-  curModName <- ask @PC.ModuleName
-  r <- tyDef2NameAndKind curModName tyDef
+  r <- tyDef2NameAndKind tyDef
   pure $ mempty & context .~ uncurry M.singleton r
 
-{-
-{- | Gets the kind of the variables from the definition and adds them to the
- context.
--}
-tyDefArgs2Context :: PC.TyDef -> Eff effs (M.Map Variable Kind)
-tyDefArgs2Context tydef = do
-  let ds = g <$> M.elems (tydef ^. #tyAbs . #tyArgs)
-  pure $ M.fromList ds
-  where
-    g :: PC.TyArg -> (Variable, Kind)
-    g tyarg = (v, k)
-      where
-        v = TyVar (tyarg ^. #argName)
-        k = pKind2Kind (tyarg ^. #argKind)
--}
-
-tyDef2NameAndKind :: forall effs. PC.ModuleName -> PC.TyDef -> Eff effs (Variable, Kind)
-tyDef2NameAndKind curModName tyDef = do
-  let name = ForeignRef $ view (PC.localRef2ForeignRef curModName) $ PC.LocalRef (tyDef ^. #tyName) (tyDef ^. #sourceInfo)
+tyDef2NameAndKind ::
+  forall effs.
+  Member (Reader PC.ModuleName) effs =>
+  PC.TyDef ->
+  Eff effs (InfoLess Variable, Kind)
+tyDef2NameAndKind tyDef = do
+  curModName <- ask
+  let tyname = tyDef ^. #tyName
+  let name = ForeignRef $ view (PC.localRef2ForeignRef curModName) $ PC.LocalRef tyname def
   let k = tyAbsLHS2Kind (tyDef ^. #tyAbs)
-  pure (name, k)
+  pure (mkInfoLess name, k)
 
 tyAbsLHS2Kind :: PC.TyAbs -> Kind
 tyAbsLHS2Kind tyAbs = foldWithArrowToType $ pKind2Kind . (\x -> x ^. #argKind) <$> toList (tyAbs ^. #tyArgs)

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

@@ -4,6 +4,7 @@ import Control.Lens (makeLenses, (^.))
 import Data.Map qualified as M
 import LambdaBuffers.Compiler.KindCheck.Kind (Kind)
 import LambdaBuffers.Compiler.KindCheck.Variable (Variable)
+import LambdaBuffers.Compiler.ProtoCompat (InfoLess)
 import Prettyprinter (
   Doc,
   Pretty (pretty),
@@ -15,8 +16,8 @@ import Prettyprinter (
  )
 
 data Context = Context
-  { _context :: M.Map Variable Kind
-  , _addContext :: M.Map Variable Kind
+  { _context :: M.Map (InfoLess Variable) Kind
+  , _addContext :: M.Map (InfoLess Variable) Kind
   }
   deriving stock (Show, Eq)
 
@@ -27,7 +28,7 @@ instance Pretty Context where
     [] -> "Γ"
     ctx -> "Γ" <+> "∪" <+> braces (setPretty ctx)
     where
-      setPretty :: [(Variable, Kind)] -> Doc ann
+      setPretty :: [(InfoLess Variable, Kind)] -> Doc ann
       setPretty = hsep . punctuate comma . fmap (\(v, t) -> pretty v <> ":" <+> pretty t)
 
 instance Semigroup Context where
@@ -37,5 +38,5 @@ instance Monoid Context where
   mempty = Context mempty mempty
 
 -- | Utility to unify the two.
-getAllContext :: Context -> M.Map Variable Kind
+getAllContext :: Context -> M.Map (InfoLess Variable) Kind
 getAllContext c = c ^. context <> c ^. addContext

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

@@ -31,13 +31,14 @@ import Control.Monad.Freer.Error (Error, runError, throwError)
 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)
+import LambdaBuffers.Compiler.ProtoCompat.InfoLess (mkInfoLess)
 
 import LambdaBuffers.Compiler.ProtoCompat qualified as PC
 
 import Data.String (fromString)
 import Data.Text qualified as T
 
-import Control.Lens ((%~), (&), (.~), (^.))
+import Control.Lens (view, (%~), (&), (.~), (^.))
 import Data.Map qualified as M
 
 import LambdaBuffers.Compiler.ProtoCompat (localRef2ForeignRef)
@@ -144,7 +145,7 @@ derive x = deriveTyAbs x
           freshT <- KVar <$> fresh
           ctx <- ask
 
-          let newContext = ctx & addContext %~ (<> M.singleton (TyVar n) vK)
+          let newContext = ctx & addContext %~ (<> M.singleton (mkInfoLess (TyVar n)) vK)
           let newAbs = tyabs & #tyArgs .~ uncurry M.singleton a
           let restAbs = tyabs & #tyArgs .~ M.fromList as
 
@@ -206,7 +207,7 @@ derive x = deriveTyAbs x
     deriveTyRef = \case
       PC.LocalI r -> do
         localModule <- ask
-        let ty = ForeignRef $ r ^. localRef2ForeignRef localModule
+        let ty = ForeignRef . view (localRef2ForeignRef localModule) $ r
         v <- getBinding ty
         c <- ask
         pure . Axiom . Judgement $ (c, Var ty, v)
@@ -273,7 +274,7 @@ derive x = deriveTyAbs x
 getBinding :: Variable -> Derive Kind
 getBinding t = do
   ctx <- asks getAllContext
-  case ctx M.!? t of
+  case ctx M.!? mkInfoLess t of
     Just x -> pure x
     Nothing -> throwError $ InferUnboundTermErr t
 

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

@@ -2,7 +2,9 @@ module LambdaBuffers.Compiler.KindCheck.Variable (Variable (ForeignRef, TyVar),
 
 import Data.Text (Text)
 import GHC.Generics (Generic)
+import Generics.SOP qualified as SOP
 import LambdaBuffers.Compiler.ProtoCompat qualified as PC
+import LambdaBuffers.Compiler.ProtoCompat.InfoLess (InfoLess, InfoLessC, withInfoLess)
 import Prettyprinter (Pretty (pretty), viaShow)
 import Test.QuickCheck (Arbitrary)
 import Test.QuickCheck.Arbitrary.Generic (GenericArbitrary (GenericArbitrary))
@@ -17,9 +19,15 @@ data Variable
   | TyVar PC.VarName
   deriving stock (Eq, Ord, Show, Generic)
   deriving (Arbitrary) via GenericArbitrary Variable
+  deriving anyclass (SOP.Generic)
 
 instance Pretty Variable where
   pretty = viaShow
 
+instance InfoLessC Variable
+
+instance Pretty (InfoLess Variable) where
+  pretty x = withInfoLess x pretty
+
 -- LocalRef a -> pretty a
 -- ForeignRef ms a -> concatWith (\x y -> x <> "." <> y) (pretty <$> (ms <> [a]))

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

@@ -7,6 +7,7 @@ module LambdaBuffers.Compiler.ProtoCompat.InfoLess (
   withInfoLess,
   withInfoLessF,
   mkInfoLess,
+  InfoLessC,
 ) where
 
 import Data.Bifunctor (Bifunctor (bimap))
@@ -67,7 +68,7 @@ newtype InfoLess a = InfoLess {unsafeInfoLess :: a}
   deriving stock (Functor, Traversable, Foldable)
 
 {- | SourceInfo Less ID.
- A TypeClass that provides id for types with SourceInfo - where SI is defaulted - therefore ignored. Not exported for obvious unsafe reasons.
+ A TypeClass that provides id for types with SourceInfo - where SI is defaulted - therefore ignored. Can only be derived.
 -}
 class Eq a => InfoLessC a where
   silId :: a -> a