wip: scaffolded the error

Author: cstml

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

@@ -172,6 +172,7 @@ test-suite tests
     Test.DeriveCheck
     Test.KindCheck
     Test.KindCheck.Errors
+    Test.KindCheck.TyClass
     Test.LambdaBuffers.Compiler
     Test.LambdaBuffers.Compiler.Coverage
     Test.LambdaBuffers.Compiler.Mutation

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

@@ -24,7 +24,7 @@ import LambdaBuffers.Compiler.KindCheck.Inference (protoKind2Kind)
 import LambdaBuffers.Compiler.KindCheck.Inference qualified as I
 import LambdaBuffers.Compiler.KindCheck.Kind (Kind (KConstraint, KType, KVar, (:->:)))
 import LambdaBuffers.Compiler.KindCheck.Type (
-  Variable (QualifiedConstraint, QualifiedTyRef, TyVar),
+  Variable (QualifiedTyClassRef, QualifiedTyRef, TyVar),
   ftrISOqtr,
   ltrISOqtr,
   qTyRef'moduleName,
@@ -136,7 +136,8 @@ runKindCheck = interpret $ \case
   CheckClassDefinition modName classDef ctx ->
     either (handleErr2 modName classDef) pure $ I.runClassDefCheck ctx modName classDef
   where
-    handleErr2 = undefined
+    handleErr2 :: forall {b}. PC.ModuleName -> PC.ClassDef -> I.InferErr -> Eff effs b
+    handleErr2 _ _ _err = error "Throw an error"
 
     handleErr :: forall {b}. PC.ModuleName -> PC.TyDef -> I.InferErr -> Eff effs b
     handleErr modName td = \case
@@ -155,7 +156,7 @@ runKindCheck = interpret $ \case
                 throwError . PC.CompKindCheckError $ PC.UnboundTyRefError td foreignRef modName
           TyVar tv ->
             throwError . PC.CompKindCheckError $ PC.UnboundTyVarError td (PC.TyVar tv) modName
-          QualifiedConstraint _ -> error "NOTE(cstml): FIXME."
+          QualifiedTyClassRef _ -> error "NOTE(cstml): FIXME."
       I.InferUnifyTermErr (I.Constraint (k1, k2)) -> do
         err <- PC.IncorrectApplicationError td <$> kind2ProtoKind k1 <*> kind2ProtoKind k2 <*> pure modName
         throwError $ PC.CompKindCheckError err

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

@@ -12,7 +12,6 @@ module LambdaBuffers.Compiler.KindCheck.Inference (
   Context (..),
   Atom,
   Type (..),
-  DeriveM,
   DeriveEff,
   InferErr (..),
   Constraint (..),
@@ -31,30 +30,33 @@ import Control.Monad.Freer.State (State, evalState, get, put)
 import Control.Monad.Freer.Writer (Writer, runWriter, tell)
 import Data.Foldable (foldrM, traverse_)
 import Data.Map qualified as M
+import Data.Text (Text)
 import Data.Text qualified as T
 import LambdaBuffers.Compiler.KindCheck.Derivation (
   Context (Context),
   Derivation (Abstraction, Application, Axiom, Implication),
   Judgement (Judgement),
   addContext,
-  context,
   d'kind,
   d'type,
+  getAllContext,
  )
 import LambdaBuffers.Compiler.KindCheck.Kind (Atom, Kind (KConstraint, KType, KVar, (:->:)))
 import LambdaBuffers.Compiler.KindCheck.Type (
   Type (Abs, App, Constructor, Opaque, Product, Sum, UnitT, Var, VoidT),
-  Variable (QualifiedTyRef, TyVar),
+  Variable (QualifiedTyClassRef, QualifiedTyRef, TyVar),
+  fcrISOqtcr,
   ftrISOqtr,
+  lcrISOftcr,
+  lcrISOqtcr,
   ltrISOqtr,
  )
-import LambdaBuffers.Compiler.ProtoCompat.InfoLess (InfoLess, mkInfoLess)
+import LambdaBuffers.Compiler.ProtoCompat.InfoLess (mkInfoLess)
 import LambdaBuffers.Compiler.ProtoCompat.Types qualified as PC
 import Prettyprinter (Pretty (pretty), (<+>))
 
--- | Utility to unify the two.
-getAllContext :: Context -> M.Map (InfoLess Variable) Kind
-getAllContext c = c ^. context <> c ^. addContext
+--------------------------------------------------------------------------------
+-- Types
 
 data InferErr
   = InferUnboundTermErr Variable
@@ -74,30 +76,20 @@ newtype Substitution = Substitution {getSubstitution :: (Atom, Kind)}
 instance Pretty Substitution where
   pretty (Substitution (a, k)) = pretty a <+> "↦" <+> pretty k
 
-newtype DerivationContext = DC
-  { _startAtom :: Atom
-  }
+--------------------------------------------------------------------------------
+-- Effects
 
-type DeriveEff = '[State Context, State DerivationContext, State [Constraint], Error InferErr]
+newtype DerivationContext = DC {_startAtom :: Atom}
 
-type DeriveM a = Eff DeriveEff a
+type DeriveEff =
+  '[Reader Context, Reader PC.ModuleName, State DerivationContext, Writer [Constraint], Error InferErr]
 
-type Derive a =
-  forall effs.
-  Members
-    '[ Reader Context
-     , Reader PC.ModuleName
-     , State DerivationContext
-     , Writer [Constraint]
-     , Error InferErr
-     ]
-    effs =>
-  Eff effs a
+type Derive a = forall effs. Members DeriveEff effs => Eff effs a
 
 --------------------------------------------------------------------------------
 -- Runners
 
--- | Run derivation builder - not unified yet.
+-- | Run Derive Monad - not unified.
 runDerive :: Context -> PC.ModuleName -> Derive a -> Either InferErr (a, [Constraint])
 runDerive ctx localMod =
   run . runError . runWriter . evalState (DC startAtom) . runReader ctx . runReader localMod
@@ -261,17 +253,24 @@ deriveClassDef :: PC.ClassDef -> Derive ()
 deriveClassDef classDef = traverse_ deriveConstraint (classDef ^. #supers)
 
 deriveConstraint :: PC.Constraint -> Derive Derivation
-deriveConstraint _constraint = do
-  --  ctx <- ask
-  -- FIXME
-  --  k2 <- getKind (ConstraintT undefined)
-  --  argD <- deriveTy (constraint ^. #argument)
-  pure $ error "NOTE(cstml): fixme."
-
---    Application
---      (Judgement ctx (App (Var (QualifiedConstraint undefined))) k2)
---      (Judgement ctx (App (Var (QualifiedConstraint undefined) k2)))
---      argD
+deriveConstraint constraint = do
+  mn <- ask
+  ctx <- ask
+  let qcr = case constraint ^. #classRef of
+        PC.LocalCI lcr -> QualifiedTyClassRef . withIso lcrISOqtcr const $ (lcr, mn)
+        PC.ForeignCI fcr -> QualifiedTyClassRef . withIso fcrISOqtcr const $ fcr
+  dConstraint <- deriveVar qcr
+  argD <- deriveTy (constraint ^. #argument)
+  let argTy = argD ^. d'type
+  freshK <- KVar <$> fresh
+  tell [Constraint (dConstraint ^. d'kind, (argD ^. d'kind) :->: freshK)]
+  pure $ Application (Judgement ctx (App (dConstraint ^. d'type) argTy) freshK) dConstraint argD
+
+deriveVar :: Variable -> Derive Derivation
+deriveVar v = do
+  ctx <- ask
+  k <- getKind v
+  pure . Axiom $ Judgement ctx (Var v) k
 
 --------------------------------------------------------------------------------
 --
@@ -348,19 +347,13 @@ unify (constraint@(Constraint (l, r)) : xs) = case l of
 
     appearsErr :: forall eff a. Member (Error InferErr) eff => Atom -> Kind -> Eff eff a
     appearsErr var ty =
-      throwError $
-        InferRecursiveSubstitutionErr $
-          mconcat
-            [ "Cannot unify: "
-            , T.pack . show . pretty $ var
-            , " with "
-            , T.pack . show . pretty $ ty
-            , ". "
-            , T.pack . show . pretty $ var
-            , " appears in: "
-            , T.pack . show . pretty $ ty
-            , "."
-            ]
+      throwError
+        $ InferRecursiveSubstitutionErr
+          . mconcat
+        $ ["Cannot unify: ", p var, " with ", p ty, ". ", p var, " appears in: ", p ty, "."]
+      where
+        p :: forall b. Pretty b => b -> Text
+        p = T.pack . show . pretty
 
     appearsIn a ty = a `elem` getVariables ty
 
@@ -393,8 +386,6 @@ substitute s d = case d of
 
     applySubstitutionCtx subs ctx = ctx & addContext %~ fmap (applySubstitution subs)
 
--- FIXME(cstml) not avoiding any clashes
-
 -- | Fresh startAtom
 startAtom :: Atom
 startAtom = 0
@@ -405,5 +396,5 @@ protoKind2Kind = \case
   PC.Kind k -> case k of
     PC.KindArrow k1 k2 -> protoKind2Kind k1 :->: protoKind2Kind k2
     PC.KindRef PC.KType -> KType
-    PC.KindRef PC.KUnspecified -> KType -- unspecified kinds get defaulted
+    PC.KindRef PC.KUnspecified -> KType
     PC.KindRef PC.KConstraint -> KConstraint

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

@@ -6,15 +6,20 @@ module LambdaBuffers.Compiler.KindCheck.Type (
   tyUnit,
   tySum,
   tyVoid,
-  Variable (TyVar, QualifiedTyRef, QualifiedConstraint),
+  Variable (TyVar, QualifiedTyRef, QualifiedTyClassRef),
   QualifiedTyRefName (..),
-  QualifiedClassName (..),
+  QualifiedTyClassRefName (..),
   qTyRef'tyName,
   qTyRef'moduleName,
   qTyRef'sourceInfo,
+
+  -- * Isomorphisms.
   ltrISOqtr,
   ftrISOqtr,
   ltrISOftr,
+  fcrISOqtcr,
+  lcrISOftcr,
+  lcrISOqtcr,
 ) where
 
 import Control.Lens (iso, makeLenses, withIso, (^.))
@@ -25,8 +30,7 @@ import LambdaBuffers.Compiler.ProtoCompat.InfoLess (InfoLess, InfoLessC, withInf
 import LambdaBuffers.Compiler.ProtoCompat.Types qualified as PC
 import Prettyprinter (Pretty (pretty), viaShow)
 
--- NOTE(cstml): Let's remove the Arbitrary instances and replaces them with
--- Gens.
+-- NOTE(cstml): Remove the Arbitrary instances and replaces them with Gens.
 
 data QualifiedTyRefName = QualifiedTyRefName
   { _qTyRef'tyName :: PC.TyName
@@ -39,13 +43,27 @@ instance InfoLessC QualifiedTyRefName
 
 makeLenses ''QualifiedTyRefName
 
+data QualifiedTyClassRefName = QualifiedTyClassRefName
+  { _qTyClass'className :: PC.ClassName
+  , _qTyClass'moduleName :: PC.ModuleName
+  , _qTyClass'sourceInfo :: PC.SourceInfo
+  }
+  deriving stock (Eq, Ord, Show, Generic)
+  deriving anyclass (SOP.Generic)
+instance InfoLessC QualifiedTyClassRefName
+
+makeLenses ''QualifiedTyClassRefName
+
+instance Pretty (InfoLess Variable) where
+  pretty x = withInfoLess x pretty
+
 {- | All TyRefs and ClassNames are fully qualified. The context determines if
  they are local or not.
 -}
 data Variable
   = QualifiedTyRef QualifiedTyRefName
+  | QualifiedTyClassRef QualifiedTyClassRefName
   | TyVar PC.VarName
-  | QualifiedConstraint QualifiedClassName
   deriving stock (Eq, Show, Ord, Generic)
   deriving anyclass (SOP.Generic)
 
@@ -54,14 +72,6 @@ instance InfoLessC Variable
 instance Pretty Variable where
   pretty = viaShow
 
-data QualifiedClassName = QualifiedClassName PC.ClassName PC.ModuleName
-  deriving stock (Eq, Ord, Show, Generic)
-  deriving anyclass (SOP.Generic)
-instance InfoLessC QualifiedClassName
-
-instance Pretty (InfoLess Variable) where
-  pretty x = withInfoLess x pretty
-
 data Type
   = Abs PC.TyAbs
   | App Type Type
@@ -89,7 +99,9 @@ tyVoid = VoidT
 instance Pretty Type where
   pretty = viaShow
 
--- | (PC.LocalRef, PC.ModuleName) isomorphism with QualifiedTyRefName.
+--------------------------------------------------------------------------------
+-- Qualified TyRef ISOs.
+
 ltrISOqtr :: Iso' (PC.LocalRef, PC.ModuleName) QualifiedTyRefName
 ltrISOqtr = iso goRight goLeft
   where
@@ -101,7 +113,6 @@ ltrISOqtr = iso goRight goLeft
       , qtr ^. qTyRef'moduleName
       )
 
--- | LocalTyRef isomorphism with ForeignTyRef
 ltrISOftr :: Iso' (PC.LocalRef, PC.ModuleName) PC.ForeignRef
 ltrISOftr = iso goRight goLeft
   where
@@ -119,3 +130,36 @@ ftrISOqtr = iso goRight goLeft
 
     goLeft :: QualifiedTyRefName -> PC.ForeignRef
     goLeft = withIso ltrISOftr $ \l2f _ -> withIso ltrISOqtr $ \_ q2l -> l2f . q2l
+
+--------------------------------------------------------------------------------
+-- Qualified TyClass Name ISOs.
+
+lcrISOqtcr :: Iso' (PC.LocalClassRef, PC.ModuleName) QualifiedTyClassRefName
+lcrISOqtcr = iso goRight goLeft
+  where
+    goRight :: (PC.LocalClassRef, PC.ModuleName) -> QualifiedTyClassRefName
+    goRight (lcr, mn) = QualifiedTyClassRefName (lcr ^. #className) mn (lcr ^. #sourceInfo)
+
+    goLeft :: QualifiedTyClassRefName -> (PC.LocalClassRef, PC.ModuleName)
+    goLeft qtcn =
+      ( PC.LocalClassRef (qtcn ^. qTyClass'className) (qtcn ^. qTyClass'sourceInfo)
+      , qtcn ^. qTyClass'moduleName
+      )
+
+lcrISOftcr :: Iso' (PC.LocalClassRef, PC.ModuleName) PC.ForeignClassRef
+lcrISOftcr = iso goRight goLeft
+  where
+    goRight :: (PC.LocalClassRef, PC.ModuleName) -> PC.ForeignClassRef
+    goRight (lr, mn) = PC.ForeignClassRef (lr ^. #className) mn (lr ^. #sourceInfo)
+
+    goLeft :: PC.ForeignClassRef -> (PC.LocalClassRef, PC.ModuleName)
+    goLeft fr = (PC.LocalClassRef (fr ^. #className) (fr ^. #sourceInfo), fr ^. #moduleName)
+
+fcrISOqtcr :: Iso' PC.ForeignClassRef QualifiedTyClassRefName
+fcrISOqtcr = iso goRight goLeft
+  where
+    goRight :: PC.ForeignClassRef -> QualifiedTyClassRefName
+    goRight = withIso lcrISOftcr $ \_ f2l -> withIso lcrISOqtcr $ \l2q _ -> l2q . f2l
+
+    goLeft :: QualifiedTyClassRefName -> PC.ForeignClassRef
+    goLeft = withIso lcrISOftcr $ \l2f _ -> withIso lcrISOqtcr $ \_ q2l -> l2f . q2l

lambda-buffers-compiler/test/Test/KindCheck.hs

@@ -7,6 +7,7 @@ import LambdaBuffers.Compiler.KindCheck (
 
 import LambdaBuffers.Compiler.KindCheck.Kind (Kind (KType, (:->:)))
 import Test.KindCheck.Errors (testGKindCheckErrors)
+import Test.KindCheck.TyClass qualified as KCTC
 import Test.QuickCheck (Arbitrary (arbitrary), forAll, (===))
 import Test.Tasty (TestTree, testGroup)
 import Test.Tasty.HUnit (assertBool, testCase, (@?=))
@@ -29,6 +30,7 @@ test =
     [ testCheck
     , testFolds
     , testGKindCheckErrors
+    , KCTC.test
     ]
 
 --------------------------------------------------------------------------------

lambda-buffers-compiler/test/Test/KindCheck/TyClass.hs

@@ -0,0 +1,6 @@
+module Test.KindCheck.TyClass (test) where
+
+import Test.Tasty (TestTree, testGroup)
+
+test :: TestTree
+test = testGroup "KC Class definitions Error Group." []