Compiler: Class Definition/Instance Kind Checking

lambda-buffers-compiler/lambda-buffers-compiler.cabal

@@ -172,12 +172,14 @@ test-suite tests
     Test.DeriveCheck
     Test.KindCheck
     Test.KindCheck.Errors
+    Test.KindCheck.TyClass
     Test.LambdaBuffers.Compiler
     Test.LambdaBuffers.Compiler.Coverage
     Test.LambdaBuffers.Compiler.Mutation
     Test.LambdaBuffers.Compiler.Utils
     Test.LambdaBuffers.Compiler.WellFormed
     Test.TypeClassCheck
+    Test.Utils.ClassDef
     Test.Utils.CompilerInput
     Test.Utils.Constructors
     Test.Utils.Module

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

@@ -9,7 +9,8 @@ module LambdaBuffers.Compiler.KindCheck (
   foldWithArrowToType,
 ) where
 
-import Control.Lens (Getter, to, view, (&), (.~), (^.))
+import Control.Lens (view, (&), (.~), (^.))
+import Control.Lens.Iso (withIso)
 import Control.Monad (void)
 import Control.Monad.Freer (Eff, Member, Members, interpret, reinterpret, run)
 import Control.Monad.Freer.Error (Error, runError, throwError)
@@ -18,11 +19,21 @@ 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.Derivation (Context, context)
+import LambdaBuffers.Compiler.KindCheck.Derivation (Context, classContext, context)
+import LambdaBuffers.Compiler.KindCheck.Inference (protoKind2Kind)
 import LambdaBuffers.Compiler.KindCheck.Inference qualified as I
-import LambdaBuffers.Compiler.KindCheck.Kind (Kind (KType, (:->:)), kind2ProtoKind)
-import LambdaBuffers.Compiler.KindCheck.Type (Variable (QualifiedTyRef, TyVar))
+import LambdaBuffers.Compiler.KindCheck.Kind (Kind (KConstraint, KType, KVar, (:->:)))
+import LambdaBuffers.Compiler.KindCheck.Type (
+  QualifiedTyClassRefName (QualifiedTyClassRefName),
+  Variable (QualifiedTyClassRef, QualifiedTyRef, TyVar),
+  fcrISOqtcr,
+  ftrISOqtr,
+  lcrISOqtcr,
+  ltrISOqtr,
+  qTyClass'moduleName,
+  qTyRef'moduleName,
+ )
+import LambdaBuffers.Compiler.ProtoCompat (KindCheckError)
 import LambdaBuffers.Compiler.ProtoCompat.InfoLess (InfoLess, mkInfoLess)
 import LambdaBuffers.Compiler.ProtoCompat.Types qualified as PC
 
@@ -50,18 +61,22 @@ makeEffect ''GlobalCheck
 -- | Interactions that happen at the level of the
 data ModuleCheck a where -- Module
   KCTypeDefinition :: PC.ModuleName -> Context -> PC.TyDef -> ModuleCheck Kind
+  KCClassDef :: PC.ModuleName -> Context -> PC.ClassDef -> ModuleCheck ()
+  KCClassInstance :: PC.ModuleName -> Context -> PC.InstanceClause -> ModuleCheck ()
 
--- NOTE(cstml & gnumonik): Lets reach consensus on these - Note(1).
---  KCClassInstance :: Context -> P.InstanceClause -> ModuleCheck ()
 --  KCClass :: Context -> P.ClassDef -> ModuleCheck ()
 
 makeEffect ''ModuleCheck
 
 data KindCheck a where
   GetSpecifiedKind :: PC.ModuleName -> PC.TyDef -> KindCheck Kind
   InferTypeKind :: PC.ModuleName -> PC.TyDef -> Context -> Kind -> KindCheck Kind
+  CheckClassDefinition :: PC.ModuleName -> PC.ClassDef -> Context -> KindCheck ()
+  CheckClassInstance :: PC.ModuleName -> PC.InstanceClause -> Context -> KindCheck ()
   CheckKindConsistency :: PC.ModuleName -> PC.TyDef -> Context -> Kind -> KindCheck Kind
 
+--  CheckClassInstance :: PC.ModuleName -> KindCheck Kind
+
 makeEffect ''KindCheck
 
 --------------------------------------------------------------------------------
@@ -104,66 +119,78 @@ moduleStrategy :: Transform GlobalCheck ModuleCheck
 moduleStrategy = reinterpret $ \case
   CreateContext ci ->
     resolveCreateContext ci
-  ValidateModule cx md ->
+  ValidateModule cx md -> do
     traverse_ (kCTypeDefinition (md ^. #moduleName) cx) (md ^. #typeDefs)
+    traverse_ (kCClassDef (md ^. #moduleName) cx) (md ^. #classDefs)
+    traverse_ (kCClassInstance (md ^. #moduleName) cx) (md ^. #instances)
 
 localStrategy :: Transform ModuleCheck KindCheck
 localStrategy = reinterpret $ \case
   KCTypeDefinition modName ctx tyDef -> do
     desiredK <- getSpecifiedKind modName tyDef
     k <- inferTypeKind modName tyDef ctx desiredK
     checkKindConsistency modName tyDef ctx k
+  KCClassDef modName ctx classDef ->
+    checkClassDefinition modName classDef ctx
+  KCClassInstance modName ctx inst ->
+    checkClassInstance modName inst ctx
 
 runKindCheck :: forall effs {a}. Member Err effs => Eff (KindCheck ': effs) a -> Eff effs a
 runKindCheck = interpret $ \case
-  InferTypeKind modName tyDef ctx k ->
-    either (handleErr modName tyDef) pure $ I.infer ctx tyDef k modName
+  InferTypeKind modName tyDef ctx _k ->
+    either (handleErrTyDef modName tyDef) pure $ I.infer ctx tyDef modName
   CheckKindConsistency modName tyDef ctx k ->
     runReader modName $ resolveKindConsistency tyDef ctx k
   GetSpecifiedKind modName tyDef ->
     fmap snd $ runReader modName $ tyDef2NameAndKind tyDef
+  CheckClassDefinition modName classDef ctx ->
+    either (handleErrClassDef modName classDef) pure $ I.runClassDefCheck ctx modName classDef
+  CheckClassInstance modName classInst ctx ->
+    either (handleErrClassInst modName classInst) pure $ I.runClassInstanceCheck ctx modName classInst
   where
-    handleErr :: forall {b}. PC.ModuleName -> PC.TyDef -> I.InferErr -> Eff effs b
-    handleErr modName td = \case
-      I.InferUnboundTermErr uA -> do
-        case uA of
-          QualifiedTyRef fr ->
-            if (fr ^. #moduleName) == modName
-              then -- We're looking at the local module.
-
-                throwError
-                  . PC.CompKindCheckError
-                  $ PC.UnboundTyRefError td (PC.LocalI $ fr ^. foreignRef2LocalRef) modName
-              else -- We're looking at a foreign module.
-
-                throwError
-                  . PC.CompKindCheckError
-                  $ PC.UnboundTyRefError td (PC.ForeignI fr) modName
+    handleErrClassInst :: forall {b}. PC.ModuleName -> PC.InstanceClause -> I.InferErr -> Eff effs b
+    handleErrClassInst = handleErr PC.CKC'ClassInstanceError
+
+    handleErrClassDef :: forall {b}. PC.ModuleName -> PC.ClassDef -> I.InferErr -> Eff effs b
+    handleErrClassDef = handleErr PC.CKC'ClassDefError
+
+    handleErrTyDef :: forall {b}. PC.ModuleName -> PC.TyDef -> I.InferErr -> Eff effs b
+    handleErrTyDef = handleErr PC.CKC'TyDefError
+
+    handleErr :: forall {loc} {b}. (KindCheckError loc -> CompilerErr) -> PC.ModuleName -> loc -> I.InferErr -> Eff effs b
+    handleErr constructor modName loc = \case
+      I.InferUnboundTermErr ut ->
+        case ut of
+          QualifiedTyRef qtr -> do
+            if qtr ^. qTyRef'moduleName == modName
+              then do
+                -- We're looking at the local module.
+                let localRef = PC.LocalI . fst . withIso ltrISOqtr (\_ f -> f) $ qtr
+                let err = PC.UnboundTyRefError loc localRef modName
+                throwError . constructor $ err
+              else do
+                -- We're looking at a foreign module.
+                let foreignRef = PC.ForeignI . withIso ftrISOqtr (\_ f -> f) $ qtr
+                throwError . constructor $ PC.UnboundTyRefError loc foreignRef modName
           TyVar tv ->
-            throwError
-              . PC.CompKindCheckError
-              $ PC.UnboundTyVarError td (PC.TyVar tv) modName
-      I.InferUnifyTermErr (I.Constraint (k1, k2)) ->
-        throwError
-          . PC.CompKindCheckError
-          $ PC.IncorrectApplicationError td (kind2ProtoKind k1) (kind2ProtoKind k2) modName
-      I.InferRecursiveSubstitutionErr _ ->
-        throwError
-          . PC.CompKindCheckError
-          $ PC.RecursiveKindError td modName
-      I.InferImpossibleErr t ->
-        throwError $
-          PC.InternalError t
-
-    foreignRef2LocalRef :: Getter PC.ForeignRef PC.LocalRef
-    foreignRef2LocalRef =
-      to
-        ( \fr ->
-            PC.LocalRef
-              { tyName = fr ^. #tyName
-              , sourceInfo = fr ^. #sourceInfo
-              }
-        )
+            throwError . constructor $ PC.UnboundTyVarError loc (PC.TyVar tv) modName
+          QualifiedTyClassRef qcr ->
+            if qcr ^. qTyClass'moduleName == modName
+              then do
+                -- We're looking at the local module.
+                let localClassRef = PC.LocalCI . fst . withIso lcrISOqtcr (\_ f -> f) $ qcr
+                let err = PC.UnboundTyClassRefError loc localClassRef modName
+                throwError . constructor $ err
+              else do
+                -- We're looking at a foreign module.
+                let foreignRef = PC.ForeignCI . withIso fcrISOqtcr (\_ f -> f) $ qcr
+                let err = PC.UnboundTyClassRefError loc foreignRef modName
+                throwError . constructor $ err
+      I.InferUnifyTermErr (I.Constraint (k1, k2)) -> do
+        err <- PC.IncorrectApplicationError loc <$> kind2ProtoKind k1 <*> kind2ProtoKind k2 <*> pure modName
+        throwError $ constructor err
+      I.InferRecursiveSubstitutionErr _ -> throwError . constructor $ PC.RecursiveKindError loc modName
+      I.InferImpossibleErr t -> throwError $ PC.C'InternalError t
 
 --------------------------------------------------------------------------------
 -- Resolvers
@@ -183,24 +210,28 @@ resolveKindConsistency tyDef _ctx inferredKind = do
     guard t i d
       | i == d = pure ()
       | otherwise = do
-          mn <- ask
-          throwError
-            . PC.CompKindCheckError
-            $ PC.InconsistentTypeError t (kind2ProtoKind i) (kind2ProtoKind d) mn
+          err <- PC.InconsistentTypeError t <$> kind2ProtoKind i <*> kind2ProtoKind d <*> ask
+          throwError $ PC.CKC'TyDefError err
 
 --------------------------------------------------------------------------------
 -- Context Creation
 
 -- | 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)
+resolveCreateContext = fmap mconcat . traverse module2Context . toList . view #modules
 
 module2Context :: forall effs. PC.Module -> Eff effs Context
 module2Context m = do
   let typeDefinitions = toList $ m ^. #typeDefs
-  ctxs <- runReader (m ^. #moduleName) $ traverse tyDef2Context typeDefinitions
-  pure $ mconcat ctxs
+  let classDefinitions = toList $ m ^. #classDefs
+  -- Context built from type definitions.
+  typeDefCtx <- fmap mconcat . runReader (m ^. #moduleName) $ traverse tyDef2Context typeDefinitions
+  -- Context built from class definitions.
+  classDefCtx <- fmap mconcat . runReader (m ^. #moduleName) $ traverse classDef2Context classDefinitions
+  return $ typeDefCtx <> classDefCtx
+
+--------------------------------------------------------------------------------
+-- Type Definition Based Context Building.
 
 -- | Creates a Context entry from one type definition.
 tyDef2Context ::
@@ -219,19 +250,47 @@ tyDef2NameAndKind ::
   Eff effs (InfoLess Variable, Kind)
 tyDef2NameAndKind tyDef = do
   curModName <- ask
-
-  -- InfoLess name - the SourceInfo doesn't matter therefore it is defaulted.
+  -- InfoLess Qualified name - the SourceInfo doesn't matter therefore it is defaulted.
   let name =
         QualifiedTyRef
-          . view (PC.localRef2ForeignRef curModName)
+          . withIso ltrISOqtr const
+          . (,curModName)
           $ PC.LocalRef (tyDef ^. #tyName) def
 
       k = tyAbsLHS2Kind (tyDef ^. #tyAbs)
 
   pure (mkInfoLess name, k)
 
 tyAbsLHS2Kind :: PC.TyAbs -> Kind
-tyAbsLHS2Kind tyAbs = foldWithArrowToType $ pKind2Kind . (\x -> x ^. #argKind) <$> toList (tyAbs ^. #tyArgs)
+tyAbsLHS2Kind tyAbs = foldWithArrowToType $ tyArg2Kind <$> toList (tyAbs ^. #tyArgs)
+
+tyArg2Kind :: PC.TyArg -> Kind
+tyArg2Kind = protoKind2Kind . view #argKind
+
+--------------------------------------------------------------------------------
+-- Class Definition Based Context Building.
+
+--- | Convert from internal Kind to Proto Kind.
+kind2ProtoKind :: forall effs. Member Err effs => Kind -> Eff effs PC.Kind
+kind2ProtoKind = \case
+  k1 :->: k2 -> fmap PC.Kind $ PC.KindArrow <$> kind2ProtoKind k1 <*> kind2ProtoKind k2
+  KType -> pure . PC.Kind . PC.KindRef $ PC.KType
+  KVar _ -> pure . PC.Kind . PC.KindRef $ PC.KUnspecified -- this shouldn't happen.
+  KConstraint -> pure . PC.Kind . PC.KindRef $ PC.KConstraint
+
+--------------------------------------------------------------------------------
+-- Class Definition Based Context Building.
+
+classDef2Context :: forall effs. Member (Reader PC.ModuleName) effs => PC.ClassDef -> Eff effs Context
+classDef2Context cDef = do
+  modName <- ask
+  let className = cDef ^. #className
+  let qtcn = mkInfoLess . QualifiedTyClassRef $ QualifiedTyClassRefName className modName def
+  let classArg = tyArg2Kind . view #classArgs $ cDef
+  pure $ mempty & classContext .~ M.singleton qtcn (classArg :->: KConstraint)
+
+--------------------------------------------------------------------------------
+-- utilities
 
 {- | Folds kinds and appends them to a Kind result type. In essence creates a
  curried function with a Type final kind.
@@ -250,13 +309,3 @@ foldWithArrowToType = foldWithArrowToKind KType
 
 foldWithArrowToKind :: Kind -> [Kind] -> Kind
 foldWithArrowToKind = foldr (:->:)
-
---------------------------------------------------------------------------------
--- To Kind Conversion functions
-
-pKind2Kind :: PC.Kind -> Kind
-pKind2Kind k =
-  case k ^. #kind of
-    PC.KindRef PC.KType -> KType
-    PC.KindArrow l r -> pKind2Kind l :->: pKind2Kind r
-    PC.KindRef PC.KUnspecified -> KType -- (for now) defaulting unspecified kinds to Type

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

@@ -1,5 +1,8 @@
+{-# OPTIONS_GHC -Wno-unused-imports #-}
+
 module LambdaBuffers.Compiler.KindCheck.Derivation (
   Derivation (Axiom, Abstraction, Application, Implication),
+  QClassName (QClassName),
   d'type,
   d'kind,
   Judgement (Judgement),
@@ -10,12 +13,14 @@ module LambdaBuffers.Compiler.KindCheck.Derivation (
   context,
   addContext,
   getAllContext,
+  classContext,
 ) where
 
 import Control.Lens (Lens', lens, makeLenses, (&), (.~), (^.))
+import Control.Lens.Operators ((%~))
 import Data.Map qualified as M
 import LambdaBuffers.Compiler.KindCheck.Kind (Kind)
-import LambdaBuffers.Compiler.KindCheck.Type (Type, Variable)
+import LambdaBuffers.Compiler.KindCheck.Type (Type, Variable (QualifiedTyClassRef))
 import LambdaBuffers.Compiler.ProtoCompat.InfoLess (InfoLess)
 import Prettyprinter (
   Doc,
@@ -33,9 +38,13 @@ import Prettyprinter (
   (<+>),
  )
 
+-- | Qualified Class Name.
+data QClassName = QClassName
+
 data Context = Context
   { _context :: M.Map (InfoLess Variable) Kind
   , _addContext :: M.Map (InfoLess Variable) Kind
+  , _classContext :: M.Map (InfoLess Variable) Kind
   }
   deriving stock (Show, Eq)
 
@@ -50,14 +59,18 @@ instance Pretty Context where
       setPretty = hsep . punctuate comma . fmap (\(v, t) -> pretty v <> ":" <+> pretty t)
 
 instance Semigroup Context where
-  (Context a1 b1) <> (Context a2 b2) = Context (a1 <> a2) (b1 <> b2)
+  c1 <> c2 =
+    c1
+      & context %~ (<> c2 ^. context)
+      & addContext %~ (<> c2 ^. addContext)
+      & classContext %~ (<> c2 ^. classContext)
 
 instance Monoid Context where
-  mempty = Context mempty mempty
+  mempty = Context mempty mempty mempty
 
--- | Utility to unify the two.
+-- | Utility to unify the two T.
 getAllContext :: Context -> M.Map (InfoLess Variable) Kind
-getAllContext c = c ^. context <> c ^. addContext
+getAllContext c = c ^. context <> c ^. addContext <> c ^. classContext
 
 data Judgement = Judgement
   { _j'ctx :: Context