diff --git a/dummy b/dummy new file mode 100644 index 00000000..e69de29b diff --git a/lambda-buffers-compiler/lambda-buffers-compiler.cabal b/lambda-buffers-compiler/lambda-buffers-compiler.cabal index b987a2f4..9026c945 100644 --- a/lambda-buffers-compiler/lambda-buffers-compiler.cabal +++ b/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 diff --git a/lambda-buffers-compiler/src/LambdaBuffers/Compiler/KindCheck.hs b/lambda-buffers-compiler/src/LambdaBuffers/Compiler/KindCheck.hs index 3c824f29..298ab635 100644 --- a/lambda-buffers-compiler/src/LambdaBuffers/Compiler/KindCheck.hs +++ b/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,9 +61,9 @@ 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 @@ -60,8 +71,12 @@ 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,8 +119,10 @@ 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 @@ -113,57 +130,67 @@ localStrategy = reinterpret $ \case 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,11 +250,11 @@ 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) @@ -231,7 +262,35 @@ tyDef2NameAndKind tyDef = do 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 diff --git a/lambda-buffers-compiler/src/LambdaBuffers/Compiler/KindCheck/Derivation.hs b/lambda-buffers-compiler/src/LambdaBuffers/Compiler/KindCheck/Derivation.hs index 03b94ba2..b86a27e4 100644 --- a/lambda-buffers-compiler/src/LambdaBuffers/Compiler/KindCheck/Derivation.hs +++ b/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 diff --git a/lambda-buffers-compiler/src/LambdaBuffers/Compiler/KindCheck/Inference.hs b/lambda-buffers-compiler/src/LambdaBuffers/Compiler/KindCheck/Inference.hs index 99e99237..4ce69c1e 100644 --- a/lambda-buffers-compiler/src/LambdaBuffers/Compiler/KindCheck/Inference.hs +++ b/lambda-buffers-compiler/src/LambdaBuffers/Compiler/KindCheck/Inference.hs @@ -3,51 +3,63 @@ -- This pragma^ is needed due to redundant constraint in Getters and Eff. module LambdaBuffers.Compiler.KindCheck.Inference ( + -- * API functions + infer, + runClassDefCheck, + runClassInstanceCheck, + + -- * Types Kind (..), Context (..), Atom, Type (..), - infer, - DeriveM, DeriveEff, - context, - addContext, InferErr (..), Constraint (..), + + -- * Utility functions + protoKind2Kind, ) where -import Control.Lens (view, (%~), (&), (.~), (^.)) +import Control.Lens ((%~), (&), (.~), (^.)) +import Control.Lens.Combinators (to) +import Control.Lens.Iso (withIso) +import Control.Monad (void) import Control.Monad.Freer (Eff, Member, Members, run) 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 Data.Bifunctor (Bifunctor (second)) -import Data.Foldable (foldrM) +import Data.Foldable (foldrM, traverse_) import Data.Map qualified as M +import Data.Set qualified as S +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 (KType, KVar, (:->:))) +import LambdaBuffers.Compiler.KindCheck.Kind (Atom, Kind (KConstraint, KType, KVar, (:->:))) import LambdaBuffers.Compiler.KindCheck.Type ( + QualifiedTyClassRefName, Type (Abs, App, Constructor, Opaque, Product, Sum, UnitT, Var, VoidT), - Variable (QualifiedTyRef, TyVar), + Variable (QualifiedTyClassRef, QualifiedTyRef, TyVar), + fcrISOqtcr, + ftrISOqtr, + lcrISOqtcr, + ltrISOqtr, ) -import LambdaBuffers.Compiler.ProtoCompat.InfoLess (InfoLess, mkInfoLess) -import LambdaBuffers.Compiler.ProtoCompat.Types (localRef2ForeignRef) +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 @@ -67,205 +79,257 @@ 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 Kind - , 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. -runDerive :: - Context -> - PC.TyAbs -> - Kind -> - PC.ModuleName -> - Either InferErr (Derivation, [Constraint]) -runDerive ctx t k localMod = - run $ - runError $ - runWriter $ - evalState (DC startAtom) $ - 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 +-- | 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 + +infer :: Context -> PC.TyDef -> PC.ModuleName -> Either InferErr Kind +infer ctx t localMod = do + (d, c) <- runDerive ctx localMod (deriveTyAbs (t ^. #tyAbs)) s <- runUnify' c let res = foldl (flip substitute) d s pure $ res ^. d'kind --- | Default KC Context. -defContext :: Context -defContext = mempty - -------------------------------------------------------------------------------- -- Implementation --- | Creates the derivation -derive :: PC.TyAbs -> Derive Derivation -derive x = deriveTyAbs x - where - fresh :: Derive Atom - fresh = do - DC a <- get - put (DC $ a + 1) - pure a - - deriveTyAbs :: PC.TyAbs -> Derive Derivation - deriveTyAbs tyabs = do - case M.toList (tyabs ^. #tyArgs) of - [] -> deriveTyBody (x ^. #tyBody) - a@(n, ar) : as -> do - let argK = protoKind2Kind (ar ^. #argKind) - bodyK <- KVar <$> fresh - ctx <- ask - - let newContext = ctx & addContext %~ (<> M.singleton (mkInfoLess (TyVar n)) argK) - let newAbs = tyabs & #tyArgs .~ uncurry M.singleton a - let restAbs = tyabs & #tyArgs .~ M.fromList as - - restF <- local (const newContext) $ deriveTyAbs restAbs - - let uK = restF ^. d'kind - tell [Constraint (bodyK, uK)] - pure $ Abstraction (Judgement ctx (Abs newAbs) (argK :->: bodyK)) restF - - deriveTyBody :: PC.TyBody -> Derive Derivation - deriveTyBody = \case - PC.OpaqueI si -> do - ctx <- ask - pure $ Axiom $ Judgement ctx (Opaque si) KType - PC.SumI s -> deriveSum s - - deriveSum :: PC.Sum -> Derive Derivation - deriveSum s = do - case M.toList (s ^. #constructors) of - [] -> voidDerivation - c : cs -> do - dc <- deriveConstructor $ snd c - restDc <- deriveSum $ s & #constructors .~ M.fromList cs - sumDerivation dc restDc - - deriveConstructor :: PC.Constructor -> Derive Derivation - deriveConstructor c = do - ctx <- ask - d <- deriveProduct (c ^. #product) - tell $ Constraint <$> [(KType, d ^. d'kind)] - pure $ Implication (Judgement ctx (Constructor c) (d ^. d'kind)) d - - deriveProduct :: PC.Product -> Derive Derivation - deriveProduct = \case - PC.RecordI r -> deriveRecord r - PC.TupleI t -> deriveTuple t - - deriveRecord :: PC.Record -> Derive Derivation - deriveRecord r = do - case M.toList (r ^. #fields) of - [] -> unitDerivation - f : fs -> do - d1 <- deriveField $ snd f - d2 <- deriveRecord $ r & #fields .~ M.fromList fs - productDerivation d1 d2 - - deriveField :: PC.Field -> Derive Derivation - deriveField f = deriveTy $ f ^. #fieldTy - - deriveTy :: PC.Ty -> Derive Derivation - deriveTy = \case - PC.TyVarI tv -> deriveTyVar tv - PC.TyAppI ta -> deriveTyApp ta - PC.TyRefI tr -> deriveTyRef tr - - deriveTyRef :: PC.TyRef -> Derive Derivation - deriveTyRef = \case - PC.LocalI r -> do - localModule <- ask - let ty = QualifiedTyRef . view (localRef2ForeignRef localModule) $ r - v <- getKind ty - c <- ask - pure . Axiom $ Judgement c (Var ty) v - PC.ForeignI r -> do - let ty = QualifiedTyRef r - v <- getKind ty - c <- ask - pure . Axiom $ Judgement c (Var ty) v - - deriveTyVar :: PC.TyVar -> Derive Derivation - deriveTyVar tv = do - let varName = tv ^. #varName - v <- getKind $ TyVar varName - c <- ask - pure . Axiom $ Judgement c (Var $ TyVar varName) v - - deriveTyApp :: PC.TyApp -> Derive Derivation - deriveTyApp ap = do - f <- deriveTy (ap ^. #tyFunc) - args <- deriveTy `traverse` (ap ^. #tyArgs) - applyDerivation f args - - deriveTuple :: PC.Tuple -> Derive Derivation - deriveTuple t = do - voidD <- voidDerivation - ds <- deriveTy `traverse` (t ^. #fields) - foldrM productDerivation voidD ds - - voidDerivation :: Derive Derivation - voidDerivation = (\ctx -> Axiom $ Judgement ctx VoidT KType) <$> ask - - unitDerivation :: Derive Derivation - unitDerivation = (\ctx -> Axiom $ Judgement ctx UnitT KType) <$> ask - - productDerivation :: Derivation -> Derivation -> Derive Derivation - productDerivation d1 d2 = do +fresh :: Derive Atom +fresh = do + DC a <- get + put (DC $ a + 1) + pure a + +deriveTyAbs :: PC.TyAbs -> Derive Derivation +deriveTyAbs tyabs = do + case M.toList (tyabs ^. #tyArgs) of + [] -> deriveTyBody (tyabs ^. #tyBody) + a@(n, ar) : as -> do + let argK = protoKind2Kind (ar ^. #argKind) + bodyK <- KVar <$> fresh ctx <- ask - let t1 = d1 ^. d'type - let t2 = d2 ^. d'type - tell $ Constraint <$> [(d1 ^. d'kind, KType), (d2 ^. d'kind, KType)] - pure $ Application (Judgement ctx (Product t1 t2) KType) d1 d2 - sumDerivation :: Derivation -> Derivation -> Derive Derivation - sumDerivation d1 d2 = do + let newContext = ctx & addContext %~ (<> M.singleton (mkInfoLess (TyVar n)) argK) + let newAbs = tyabs & #tyArgs .~ uncurry M.singleton a + let restAbs = tyabs & #tyArgs .~ M.fromList as + + restF <- local (const newContext) $ deriveTyAbs restAbs + + let uK = restF ^. d'kind + tell [Constraint (bodyK, uK)] + pure $ Abstraction (Judgement ctx (Abs newAbs) (argK :->: bodyK)) restF + +deriveTyBody :: PC.TyBody -> Derive Derivation +deriveTyBody = \case + PC.OpaqueI si -> do + ctx <- ask + pure $ Axiom $ Judgement ctx (Opaque si) KType + PC.SumI s -> deriveSum s + +deriveSum :: PC.Sum -> Derive Derivation +deriveSum s = do + case M.toList (s ^. #constructors) of + [] -> voidDerivation + c : cs -> do + dc <- deriveConstructor $ snd c + restDc <- deriveSum $ s & #constructors .~ M.fromList cs + sumDerivation dc restDc + +deriveConstructor :: PC.Constructor -> Derive Derivation +deriveConstructor c = do + ctx <- ask + d <- deriveProduct (c ^. #product) + tell $ Constraint <$> [(KType, d ^. d'kind)] + pure $ Implication (Judgement ctx (Constructor c) (d ^. d'kind)) d + +deriveProduct :: PC.Product -> Derive Derivation +deriveProduct = \case + PC.RecordI r -> deriveRecord r + PC.TupleI t -> deriveTuple t + +deriveRecord :: PC.Record -> Derive Derivation +deriveRecord r = do + case M.toList (r ^. #fields) of + [] -> unitDerivation + f : fs -> do + d1 <- deriveField $ snd f + d2 <- deriveRecord $ r & #fields .~ M.fromList fs + productDerivation d1 d2 + +deriveField :: PC.Field -> Derive Derivation +deriveField f = deriveTy $ f ^. #fieldTy + +deriveTy :: PC.Ty -> Derive Derivation +deriveTy = \case + PC.TyVarI tv -> deriveTyVar tv + PC.TyAppI ta -> deriveTyApp ta + PC.TyRefI tr -> deriveTyRef tr + +deriveTyRef :: PC.TyRef -> Derive Derivation +deriveTyRef = \case + PC.LocalI r -> do + localModule <- ask + let ty = QualifiedTyRef . withIso ltrISOqtr const $ (r, localModule) + v <- getKind ty + c <- ask + pure . Axiom $ Judgement c (Var ty) v + PC.ForeignI r -> do + let ty = QualifiedTyRef . withIso ftrISOqtr const $ r + v <- getKind ty + c <- ask + pure . Axiom $ Judgement c (Var ty) v + +deriveTyVar :: PC.TyVar -> Derive Derivation +deriveTyVar tv = do + let varName = tv ^. #varName + v <- getKind $ TyVar varName + c <- ask + pure . Axiom $ Judgement c (Var $ TyVar varName) v + +deriveTyApp :: PC.TyApp -> Derive Derivation +deriveTyApp ap = do + f <- deriveTy (ap ^. #tyFunc) + args <- deriveTy `traverse` (ap ^. #tyArgs) + applyDerivation f args + +deriveTuple :: PC.Tuple -> Derive Derivation +deriveTuple t = do + voidD <- voidDerivation + ds <- deriveTy `traverse` (t ^. #fields) + foldrM productDerivation voidD ds + +voidDerivation :: Derive Derivation +voidDerivation = (\ctx -> Axiom $ Judgement ctx VoidT KType) <$> ask + +unitDerivation :: Derive Derivation +unitDerivation = (\ctx -> Axiom $ Judgement ctx UnitT KType) <$> ask + +productDerivation :: Derivation -> Derivation -> Derive Derivation +productDerivation d1 d2 = do + ctx <- ask + let t1 = d1 ^. d'type + let t2 = d2 ^. d'type + tell $ Constraint <$> [(d1 ^. d'kind, KType), (d2 ^. d'kind, KType)] + pure $ Application (Judgement ctx (Product t1 t2) KType) d1 d2 + +sumDerivation :: Derivation -> Derivation -> Derive Derivation +sumDerivation d1 d2 = do + ctx <- ask + let t1 = d1 ^. d'type + let t2 = d2 ^. d'type + tell $ Constraint <$> [(d1 ^. d'kind, KType), (d2 ^. d'kind, KType)] + pure $ Application (Judgement ctx (Sum t1 t2) KType) d1 d2 + +applyDerivation :: Derivation -> [Derivation] -> Derive Derivation +applyDerivation d1 = \case + [] -> pure d1 + d : ds -> do + c <- ask + d2 <- applyDerivation d ds + v <- KVar <$> fresh + tell [Constraint ((d2 ^. d'kind) :->: v, d1 ^. d'kind)] + pure $ Application (Judgement c (App (d ^. d'type) (d2 ^. d'type)) v) d1 d2 + +-------------------------------------------------------------------------------- +-- Class Checking + +runClassDefCheck :: Context -> PC.ModuleName -> PC.ClassDef -> Either InferErr () +runClassDefCheck ctx modName classDef = do + (_, c) <- runDerive ctx modName $ deriveClassDef classDef + void $ runUnify' c + +runClassInstanceCheck :: Context -> PC.ModuleName -> PC.InstanceClause -> Either InferErr () +runClassInstanceCheck ctx modName classInst = do + (_, c) <- runDerive ctx modName $ deriveClassInst classInst + void $ runUnify' c + +deriveClassInst :: PC.InstanceClause -> Derive () +deriveClassInst instClause = do + let vs = getTyVariables (instClause ^. #head) + extraContext <- generateKinds vs + void $ local (<> extraContext) $ do + void $ deriveClassInstDef instClause + traverse_ deriveConstraint $ instClause ^. #constraints + where + getTyVariables :: PC.Ty -> S.Set PC.TyVar + getTyVariables = \case + PC.TyVarI v -> S.singleton v + PC.TyAppI l -> getTyVariables (l ^. #tyFunc) <> mconcat (getTyVariables <$> l ^. #tyArgs) + PC.TyRefI _ -> mempty + + generateKinds :: S.Set PC.TyVar -> Derive Context + generateKinds s = fmap mconcat $ traverse generateKind $ S.toList s + where + generateKind :: PC.TyVar -> Derive Context + generateKind tv = do + freshK <- KVar <$> fresh + pure $ mempty & addContext .~ M.singleton (mkInfoLess $ TyVar $ tv ^. #varName) freshK + + deriveClassInstDef :: PC.InstanceClause -> Derive Derivation + deriveClassInstDef ic = do ctx <- ask - let t1 = d1 ^. d'type - let t2 = d2 ^. d'type - tell $ Constraint <$> [(d1 ^. d'kind, KType), (d2 ^. d'kind, KType)] - pure $ Application (Judgement ctx (Sum t1 t2) KType) d1 d2 - - applyDerivation :: Derivation -> [Derivation] -> Derive Derivation - applyDerivation d1 = \case - [] -> pure d1 - d : ds -> do - c <- ask - d2 <- applyDerivation d ds - v <- KVar <$> fresh - tell [Constraint ((d2 ^. d'kind) :->: v, d1 ^. d'kind)] - pure $ Application (Judgement c (App (d ^. d'type) (d2 ^. d'type)) v) d1 d2 + qcr <- QualifiedTyClassRef <$> classRef2Quantified (ic ^. #classRef) + dConstraint <- deriveVar qcr + argD <- deriveTy (ic ^. #head) + 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 + +-- | Checks the class definition for correct typedness. +deriveClassDef :: PC.ClassDef -> Derive () +deriveClassDef classDef = do + vars <- createLocalConstraintContext classDef + traverse_ (local (<> vars) . deriveConstraint) (classDef ^. #supers) + +-- | Adds the kind of the variable to the local context. +createLocalConstraintContext :: PC.ClassDef -> Derive Context +createLocalConstraintContext cd = do + let arg = cd ^. #classArgs + let n = mkInfoLess $ TyVar $ arg ^. #argName + let k = arg ^. #argKind . to protoKind2Kind + return $ mempty & addContext .~ M.singleton n k + +classRef2Quantified :: PC.TyClassRef -> Derive QualifiedTyClassRefName +classRef2Quantified cr = do + mn <- ask + let qcr = case cr of + PC.LocalCI lcr -> withIso lcrISOqtcr const (lcr, mn) + PC.ForeignCI fcr -> withIso fcrISOqtcr const fcr + pure qcr + +deriveConstraint :: PC.Constraint -> Derive Derivation +deriveConstraint constraint = do + qcr <- QualifiedTyClassRef <$> classRef2Quantified (constraint ^. #classRef) + ctx <- ask + 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 + +-------------------------------------------------------------------------------- +-- {- | Gets the binding from the context - if the variable is not bound throw an error. @@ -284,6 +348,7 @@ type Unifier a = forall effs. Member (Error InferErr) effs => Eff effs a getVariables :: Kind -> [Atom] getVariables = \case KType -> mempty + KConstraint -> mempty x :->: y -> getVariables x <> getVariables y KVar x -> [x] @@ -294,14 +359,25 @@ getVariables = \case unify :: [Constraint] -> Unifier [Substitution] unify [] = pure [] unify (constraint@(Constraint (l, r)) : xs) = case l of + -- Constants KType -> case r of KType -> unify xs + KConstraint -> nope constraint (_ :->: _) -> nope constraint KVar v -> let sub = Substitution (v, KType) in (sub :) <$> unify (sub `substituteIn` xs) + KConstraint -> case r of + KType -> nope constraint + KConstraint -> unify xs + (_ :->: _) -> nope constraint + KVar v -> + let sub = Substitution (v, KConstraint) + in (sub :) <$> unify (sub `substituteIn` xs) + -- Arrows x :->: y -> case r of KType -> nope constraint + KConstraint -> nope constraint KVar v -> if v `appearsIn` l then appearsErr v l @@ -312,6 +388,7 @@ unify (constraint@(Constraint (l, r)) : xs) = case l of let c1 = Constraint (x, m) c2 = Constraint (y, n) in unify (c1 : c2 : xs) + -- Variables KVar a -> case r of KVar b -> if a == b @@ -326,19 +403,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 @@ -349,6 +420,7 @@ unify (constraint@(Constraint (l, r)) : xs) = case l of applySubstitution :: Substitution -> Kind -> Kind applySubstitution s@(Substitution (a, t)) k = case k of KType -> KType + KConstraint -> KConstraint l :->: r -> applySubstitution s l :->: applySubstitution s r KVar v -> if v == a then t else k @@ -368,11 +440,7 @@ substitute s d = case d of where applySubsToJudgement sub (Judgement ctx t k) = Judgement (applySubstitutionCtx s ctx) t (applySubstitution sub k) - applySubstitutionCtx subs c@(Context ctx addCtx) = case M.toList addCtx of - [] -> c - xs -> Context ctx $ M.fromList $ second (applySubstitution subs) <$> xs - --- FIXME(cstml) not avoiding any clashes + applySubstitutionCtx subs ctx = ctx & addContext %~ fmap (applySubstitution subs) -- | Fresh startAtom startAtom :: Atom @@ -384,4 +452,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 inferred and unified + PC.KindRef PC.KConstraint -> KConstraint + PC.KindRef PC.KUnspecified -> KType diff --git a/lambda-buffers-compiler/src/LambdaBuffers/Compiler/KindCheck/Kind.hs b/lambda-buffers-compiler/src/LambdaBuffers/Compiler/KindCheck/Kind.hs index 8e1558a5..babb517f 100644 --- a/lambda-buffers-compiler/src/LambdaBuffers/Compiler/KindCheck/Kind.hs +++ b/lambda-buffers-compiler/src/LambdaBuffers/Compiler/KindCheck/Kind.hs @@ -1,7 +1,6 @@ -module LambdaBuffers.Compiler.KindCheck.Kind (Kind (KType, (:->:), KVar), kind2ProtoKind, Atom) where +module LambdaBuffers.Compiler.KindCheck.Kind (Kind (KType, (:->:), KVar, KConstraint), Atom) where import GHC.Generics (Generic) -import LambdaBuffers.Compiler.ProtoCompat.Types qualified as PC import Prettyprinter (Pretty (pretty), parens, (<+>)) import Test.QuickCheck.Arbitrary.Generic (Arbitrary, GenericArbitrary (GenericArbitrary)) @@ -13,6 +12,7 @@ data Kind = KType | Kind :->: Kind | KVar Atom + | KConstraint deriving stock (Eq, Show, Generic) deriving (Arbitrary) via GenericArbitrary Kind @@ -22,10 +22,4 @@ instance Pretty Kind where ((x :->: y) :->: z) -> parens (pretty $ x :->: y) <+> "→" <+> pretty z x :->: y -> pretty x <+> "→" <+> pretty y KVar a -> pretty a - --- | Convert from internal Kind to Proto Kind. -kind2ProtoKind :: Kind -> PC.Kind -kind2ProtoKind = \case - k1 :->: k2 -> PC.Kind $ PC.KindArrow (kind2ProtoKind k1) (kind2ProtoKind k2) - KType -> PC.Kind . PC.KindRef $ PC.KType - KVar _ -> PC.Kind . PC.KindRef $ PC.KUnspecified -- this shouldn't happen. + KConstraint -> "Constraint" diff --git a/lambda-buffers-compiler/src/LambdaBuffers/Compiler/KindCheck/Type.hs b/lambda-buffers-compiler/src/LambdaBuffers/Compiler/KindCheck/Type.hs index 709ffac6..b5de91a4 100644 --- a/lambda-buffers-compiler/src/LambdaBuffers/Compiler/KindCheck/Type.hs +++ b/lambda-buffers-compiler/src/LambdaBuffers/Compiler/KindCheck/Type.hs @@ -1,40 +1,82 @@ +{-# OPTIONS_GHC -Wno-redundant-constraints #-} + module LambdaBuffers.Compiler.KindCheck.Type ( Type (Abs, VoidT, Product, Sum, Constructor, Opaque, Var, UnitT, App), tyProd, tyUnit, tySum, tyVoid, - Variable (TyVar, QualifiedTyRef), + Variable (TyVar, QualifiedTyRef, QualifiedTyClassRef), + QualifiedTyRefName (..), + QualifiedTyClassRefName (..), + + -- * Qualified TyRef + qTyRef'tyName, + qTyRef'moduleName, + qTyRef'sourceInfo, + ltrISOqtr, + ftrISOqtr, + ltrISOftr, + + -- * Qualified TyClass + qTyClass'className, + qTyClass'moduleName, + qTyClass'sourceInfo, + fcrISOqtcr, + lcrISOftcr, + lcrISOqtcr, ) where +import Control.Lens (iso, makeLenses, withIso, (^.)) +import Control.Lens.Combinators (Iso') import GHC.Generics (Generic) import Generics.SOP qualified as SOP import LambdaBuffers.Compiler.ProtoCompat.InfoLess (InfoLess, InfoLessC, withInfoLess) import LambdaBuffers.Compiler.ProtoCompat.Types qualified as PC import Prettyprinter (Pretty (pretty), viaShow) -import Test.QuickCheck (Arbitrary) -import Test.QuickCheck.Arbitrary.Generic (GenericArbitrary (GenericArbitrary)) --- 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 Variable - = -- | All TyRefs are fully qualified. The context determines if they're local - -- or not. - QualifiedTyRef PC.ForeignRef - | TyVar PC.VarName +data QualifiedTyRefName = QualifiedTyRefName + { _qTyRef'tyName :: PC.TyName + , _qTyRef'moduleName :: PC.ModuleName + , _qTyRef'sourceInfo :: PC.SourceInfo + } deriving stock (Eq, Ord, Show, Generic) - deriving (Arbitrary) via GenericArbitrary Variable deriving anyclass (SOP.Generic) +instance InfoLessC QualifiedTyRefName -instance Pretty Variable where - pretty = viaShow +makeLenses ''QualifiedTyRefName -instance InfoLessC Variable +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 + deriving stock (Eq, Show, Ord, Generic) + deriving anyclass (SOP.Generic) + +instance InfoLessC Variable + +instance Pretty Variable where + pretty = viaShow + data Type = Abs PC.TyAbs | App Type Type @@ -61,3 +103,68 @@ tyVoid = VoidT instance Pretty Type where pretty = viaShow + +-------------------------------------------------------------------------------- +-- Qualified TyRef ISOs. + +ltrISOqtr :: Iso' (PC.LocalRef, PC.ModuleName) QualifiedTyRefName +ltrISOqtr = iso goRight goLeft + where + goRight :: (PC.LocalRef, PC.ModuleName) -> QualifiedTyRefName + goRight (lr, mn) = QualifiedTyRefName (lr ^. #tyName) mn (lr ^. #sourceInfo) + + goLeft qtr = + ( PC.LocalRef (qtr ^. qTyRef'tyName) (qtr ^. qTyRef'sourceInfo) + , qtr ^. qTyRef'moduleName + ) + +ltrISOftr :: Iso' (PC.LocalRef, PC.ModuleName) PC.ForeignRef +ltrISOftr = iso goRight goLeft + where + goRight :: (PC.LocalRef, PC.ModuleName) -> PC.ForeignRef + goRight (lr, m) = PC.ForeignRef (lr ^. #tyName) m (lr ^. #sourceInfo) + + goLeft :: PC.ForeignRef -> (PC.LocalRef, PC.ModuleName) + goLeft fr = (PC.LocalRef (fr ^. #tyName) (fr ^. #sourceInfo), fr ^. #moduleName) + +ftrISOqtr :: Iso' PC.ForeignRef QualifiedTyRefName +ftrISOqtr = iso goRight goLeft + where + goRight :: PC.ForeignRef -> QualifiedTyRefName + goRight = withIso ltrISOftr $ \_ f2l -> withIso ltrISOqtr $ \l2q _ -> l2q . f2l + + 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 diff --git a/lambda-buffers-compiler/src/LambdaBuffers/Compiler/ProtoCompat/FromProto.hs b/lambda-buffers-compiler/src/LambdaBuffers/Compiler/ProtoCompat/FromProto.hs index fba02d7a..a2c92147 100644 --- a/lambda-buffers-compiler/src/LambdaBuffers/Compiler/ProtoCompat/FromProto.hs +++ b/lambda-buffers-compiler/src/LambdaBuffers/Compiler/ProtoCompat/FromProto.hs @@ -330,6 +330,7 @@ instance IsMessage P.Kind'KindRef PC.KindRefType where ( \case P.Kind'KIND_REF_TYPE -> pure PC.KType P.Kind'KIND_REF_UNSPECIFIED -> pure PC.KUnspecified + P.Kind'KIND_REF_CONSTRAINT -> pure PC.KConstraint P.Kind'KindRef'Unrecognized v -> throwError [ FPProtoParseError $ @@ -343,6 +344,7 @@ instance IsMessage P.Kind'KindRef PC.KindRefType where toProto = \case PC.KType -> P.Kind'KIND_REF_TYPE PC.KUnspecified -> P.Kind'KIND_REF_UNSPECIFIED + PC.KConstraint -> P.Kind'KIND_REF_CONSTRAINT instance IsMessage P.Kind PC.Kind where fromProto k = do @@ -660,37 +662,42 @@ instance IsMessage P.CompilerInput PC.CompilerInput where Outputs -} -instance IsMessage P.KindCheckError PC.KindCheckError where +instance IsMessage P.KindCheckErrorTyDef (PC.KindCheckError PC.TyDef) where fromProto kce = case kce ^. P.maybe'kindCheckError of Just x -> case x of - P.KindCheckError'UnboundTyVarError' err -> + P.KindCheckErrorTyDef'UnboundTyVarError' err -> PC.UnboundTyVarError <$> fromProto (err ^. P.tyDef) <*> fromProto (err ^. P.tyVar) <*> fromProto (err ^. P.moduleName) - P.KindCheckError'UnboundTyRefError' err -> + P.KindCheckErrorTyDef'UnboundTyRefError' err -> PC.UnboundTyRefError <$> fromProto (err ^. P.tyDef) <*> fromProto (err ^. P.tyRef) <*> fromProto (err ^. P.moduleName) - P.KindCheckError'UnificationError' err -> + P.KindCheckErrorTyDef'UnboundTyClassRefError' err -> + PC.UnboundTyClassRefError + <$> fromProto (err ^. P.tyDef) + <*> fromProto (err ^. P.tyClassRef) + <*> fromProto (err ^. P.moduleName) + P.KindCheckErrorTyDef'UnificationError' err -> PC.IncorrectApplicationError <$> fromProto (err ^. P.tyDef) <*> fromProto (err ^. P.tyKindLhs) <*> fromProto (err ^. P.tyKindRhs) <*> fromProto (err ^. P.moduleName) - P.KindCheckError'CyclicKindError' err -> + P.KindCheckErrorTyDef'CyclicKindError' err -> PC.RecursiveKindError <$> fromProto (err ^. P.tyDef) <*> fromProto (err ^. P.moduleName) - P.KindCheckError'InconsistentTypeError' err -> + P.KindCheckErrorTyDef'InconsistentTypeError' err -> PC.InconsistentTypeError <$> fromProto (err ^. P.tyDef) <*> fromProto (err ^. P.actualKind) <*> fromProto (err ^. P.expectedKind) <*> fromProto (err ^. P.moduleName) - Nothing -> throwOneOfError (messageName (Proxy @P.KindCheckError)) "kind_check_error" + Nothing -> throwOneOfError (messageName (Proxy @P.KindCheckErrorTyDef)) "kind_check_error" toProto = \case PC.UnboundTyVarError tydef tyvar modname -> @@ -703,6 +710,11 @@ instance IsMessage P.KindCheckError PC.KindCheckError where & (P.unboundTyRefError . P.tyDef) .~ toProto tydef & (P.unboundTyRefError . P.tyRef) .~ toProto tyref & (P.unboundTyRefError . P.moduleName) .~ toProto modname + PC.UnboundTyClassRefError tydef tyClassRef modname -> + defMessage + & (P.unboundTyClassRefError . P.tyDef) .~ toProto tydef + & (P.unboundTyClassRefError . P.tyClassRef) .~ toProto tyClassRef + & (P.unboundTyClassRefError . P.moduleName) .~ toProto modname PC.IncorrectApplicationError tydef k1 k2 modname -> defMessage & (P.unificationError . P.tyDef) .~ toProto tydef @@ -720,12 +732,154 @@ instance IsMessage P.KindCheckError PC.KindCheckError where & (P.inconsistentTypeError . P.expectedKind) .~ toProto kd & (P.inconsistentTypeError . P.moduleName) .~ toProto modname +instance IsMessage P.KindCheckErrorClassDef (PC.KindCheckError PC.ClassDef) where + fromProto kce = + case kce ^. P.maybe'kindCheckError of + Just x -> case x of + P.KindCheckErrorClassDef'UnboundTyVarError' err -> + PC.UnboundTyVarError + <$> fromProto (err ^. P.classDef) + <*> fromProto (err ^. P.tyVar) + <*> fromProto (err ^. P.moduleName) + P.KindCheckErrorClassDef'UnboundTyRefError' err -> + PC.UnboundTyRefError + <$> fromProto (err ^. P.classDef) + <*> fromProto (err ^. P.tyRef) + <*> fromProto (err ^. P.moduleName) + P.KindCheckErrorClassDef'UnboundTyClassRefError' err -> + PC.UnboundTyClassRefError + <$> fromProto (err ^. P.classDef) + <*> fromProto (err ^. P.tyClassRef) + <*> fromProto (err ^. P.moduleName) + P.KindCheckErrorClassDef'UnificationError' err -> + PC.IncorrectApplicationError + <$> fromProto (err ^. P.classDef) + <*> fromProto (err ^. P.tyKindLhs) + <*> fromProto (err ^. P.tyKindRhs) + <*> fromProto (err ^. P.moduleName) + P.KindCheckErrorClassDef'CyclicKindError' err -> + PC.RecursiveKindError + <$> fromProto (err ^. P.classDef) + <*> fromProto (err ^. P.moduleName) + P.KindCheckErrorClassDef'InconsistentTypeError' err -> + PC.InconsistentTypeError + <$> fromProto (err ^. P.classDef) + <*> fromProto (err ^. P.actualKind) + <*> fromProto (err ^. P.expectedKind) + <*> fromProto (err ^. P.moduleName) + Nothing -> throwOneOfError (messageName (Proxy @P.KindCheckErrorClassDef)) "kind_check_error" + + toProto = \case + PC.UnboundTyVarError classDef tyvar modname -> + defMessage + & (P.unboundTyVarError . P.classDef) .~ toProto classDef + & (P.unboundTyVarError . P.tyVar) .~ toProto tyvar + & (P.unboundTyVarError . P.moduleName) .~ toProto modname + PC.UnboundTyRefError classDef tyref modname -> + defMessage + & (P.unboundTyRefError . P.classDef) .~ toProto classDef + & (P.unboundTyRefError . P.tyRef) .~ toProto tyref + & (P.unboundTyRefError . P.moduleName) .~ toProto modname + PC.UnboundTyClassRefError classDef classRef modName -> + defMessage + & (P.unboundTyClassRefError . P.classDef) .~ toProto classDef + & (P.unboundTyClassRefError . P.tyClassRef) .~ toProto classRef + & (P.unboundTyClassRefError . P.moduleName) .~ toProto modName + PC.IncorrectApplicationError classDef k1 k2 modname -> + defMessage + & (P.unificationError . P.classDef) .~ toProto classDef + & (P.unificationError . P.tyKindLhs) .~ toProto k1 + & (P.unificationError . P.tyKindRhs) .~ toProto k2 + & (P.unificationError . P.moduleName) .~ toProto modname + PC.RecursiveKindError classDef modname -> + defMessage + & (P.cyclicKindError . P.classDef) .~ toProto classDef + & (P.cyclicKindError . P.moduleName) .~ toProto modname + PC.InconsistentTypeError classDef ki kd modname -> + defMessage + & (P.inconsistentTypeError . P.classDef) .~ toProto classDef + & (P.inconsistentTypeError . P.actualKind) .~ toProto ki + & (P.inconsistentTypeError . P.expectedKind) .~ toProto kd + & (P.inconsistentTypeError . P.moduleName) .~ toProto modname + +instance IsMessage P.KindCheckErrorClassInstance (PC.KindCheckError PC.InstanceClause) where + fromProto kce = + case kce ^. P.maybe'kindCheckError of + Just x -> case x of + P.KindCheckErrorClassInstance'UnboundTyVarError' err -> + PC.UnboundTyVarError + <$> fromProto (err ^. P.instanceClause) + <*> fromProto (err ^. P.tyVar) + <*> fromProto (err ^. P.moduleName) + P.KindCheckErrorClassInstance'UnboundTyRefError' err -> + PC.UnboundTyRefError + <$> fromProto (err ^. P.instanceClause) + <*> fromProto (err ^. P.tyRef) + <*> fromProto (err ^. P.moduleName) + P.KindCheckErrorClassInstance'UnboundTyClassRefError' err -> + PC.UnboundTyClassRefError + <$> fromProto (err ^. P.instanceClause) + <*> fromProto (err ^. P.tyClassRef) + <*> fromProto (err ^. P.moduleName) + P.KindCheckErrorClassInstance'UnificationError' err -> + PC.IncorrectApplicationError + <$> fromProto (err ^. P.instanceClause) + <*> fromProto (err ^. P.tyKindLhs) + <*> fromProto (err ^. P.tyKindRhs) + <*> fromProto (err ^. P.moduleName) + P.KindCheckErrorClassInstance'CyclicKindError' err -> + PC.RecursiveKindError + <$> fromProto (err ^. P.instanceClause) + <*> fromProto (err ^. P.moduleName) + P.KindCheckErrorClassInstance'InconsistentTypeError' err -> + PC.InconsistentTypeError + <$> fromProto (err ^. P.instanceClause) + <*> fromProto (err ^. P.actualKind) + <*> fromProto (err ^. P.expectedKind) + <*> fromProto (err ^. P.moduleName) + Nothing -> throwOneOfError (messageName (Proxy @P.KindCheckErrorClassInstance)) "kind_check_error" + + toProto = \case + PC.UnboundTyVarError instanceClause tyvar modname -> + defMessage + & (P.unboundTyVarError . P.instanceClause) .~ toProto instanceClause + & (P.unboundTyVarError . P.tyVar) .~ toProto tyvar + & (P.unboundTyVarError . P.moduleName) .~ toProto modname + PC.UnboundTyRefError instanceClause tyref modname -> + defMessage + & (P.unboundTyRefError . P.instanceClause) .~ toProto instanceClause + & (P.unboundTyRefError . P.tyRef) .~ toProto tyref + & (P.unboundTyRefError . P.moduleName) .~ toProto modname + PC.UnboundTyClassRefError instanceClause classRef modName -> + defMessage + & (P.unboundTyClassRefError . P.instanceClause) .~ toProto instanceClause + & (P.unboundTyClassRefError . P.tyClassRef) .~ toProto classRef + & (P.unboundTyClassRefError . P.moduleName) .~ toProto modName + PC.IncorrectApplicationError instanceClause k1 k2 modname -> + defMessage + & (P.unificationError . P.instanceClause) .~ toProto instanceClause + & (P.unificationError . P.tyKindLhs) .~ toProto k1 + & (P.unificationError . P.tyKindRhs) .~ toProto k2 + & (P.unificationError . P.moduleName) .~ toProto modname + PC.RecursiveKindError instanceClause modname -> + defMessage + & (P.cyclicKindError . P.instanceClause) .~ toProto instanceClause + & (P.cyclicKindError . P.moduleName) .~ toProto modname + PC.InconsistentTypeError instanceClause ki kd modname -> + defMessage + & (P.inconsistentTypeError . P.instanceClause) .~ toProto instanceClause + & (P.inconsistentTypeError . P.actualKind) .~ toProto ki + & (P.inconsistentTypeError . P.expectedKind) .~ toProto kd + & (P.inconsistentTypeError . P.moduleName) .~ toProto modname + instance IsMessage P.CompilerError PC.CompilerError where fromProto _ = throwInternalError "fromProto CompilerError not implemented" toProto = \case - PC.CompKindCheckError err -> defMessage & P.kindCheckErrors .~ [toProto err] - PC.InternalError err -> defMessage & P.internalErrors .~ [defMessage & P.msg .~ err] + PC.CKC'TyDefError err -> defMessage & P.kindCheckErrorsTyDefs .~ [toProto err] + PC.CKC'ClassDefError err -> defMessage & P.kindCheckErrorsClassDefs .~ [toProto err] + PC.CKC'ClassInstanceError err -> defMessage & P.kindCheckErrorsClassInstances .~ [toProto err] + PC.C'InternalError err -> defMessage & P.internalErrors .~ [defMessage & P.msg .~ err] instance IsMessage P.CompilerResult PC.CompilerResult where fromProto _ = throwInternalError "fromProto CompilerError not implemented" diff --git a/lambda-buffers-compiler/src/LambdaBuffers/Compiler/ProtoCompat/InfoLess.hs b/lambda-buffers-compiler/src/LambdaBuffers/Compiler/ProtoCompat/InfoLess.hs index f5f5cb03..788eb92f 100644 --- a/lambda-buffers-compiler/src/LambdaBuffers/Compiler/ProtoCompat/InfoLess.hs +++ b/lambda-buffers-compiler/src/LambdaBuffers/Compiler/ProtoCompat/InfoLess.hs @@ -7,9 +7,11 @@ module LambdaBuffers.Compiler.ProtoCompat.InfoLess ( withInfoLess, withInfoLessF, mkInfoLess, - InfoLessC, + InfoLessC (infoLessId), ) where +import Control.Monad (join) +import Control.Monad.Identity (Identity (Identity)) import Data.Bifunctor (Bifunctor (bimap)) import Data.Default (Default (def)) import Data.Map qualified as M @@ -66,6 +68,8 @@ import LambdaBuffers.Compiler.ProtoCompat.Types ( newtype InfoLess a = InfoLess {unsafeInfoLess :: a} deriving stock (Show, Eq, Ord) deriving stock (Functor, Traversable, Foldable) + deriving (Applicative) via Identity + deriving (Monad) via Identity {- | SourceInfo Less ID. A TypeClass that provides id for types with SourceInfo - where SI is defaulted - therefore ignored. Can only be derived. @@ -90,6 +94,9 @@ withInfoLess (InfoLess a) f = f . unsafeInfoLess . mkInfoLess $ a withInfoLessF :: forall f {a} {b}. InfoLessC a => InfoLess a -> (a -> f b) -> f b withInfoLessF (InfoLess a) f = f . unsafeInfoLess . mkInfoLess $ a +instance InfoLessC a => InfoLessC (InfoLess a) where + infoLessId = join . mkInfoLess + instance InfoLessC a => InfoLessC [a] where infoLessId = fmap infoLessId @@ -149,6 +156,8 @@ instance InfoLessC Module instance InfoLessC InferenceErr instance InfoLessC KindCheckErr instance InfoLessC CompilerInput -instance InfoLessC KindCheckError +instance InfoLessC (KindCheckError TyDef) +instance InfoLessC (KindCheckError ClassDef) +instance InfoLessC (KindCheckError InstanceClause) instance InfoLessC CompilerError instance InfoLessC CompilerResult diff --git a/lambda-buffers-compiler/src/LambdaBuffers/Compiler/ProtoCompat/Types.hs b/lambda-buffers-compiler/src/LambdaBuffers/Compiler/ProtoCompat/Types.hs index 88a2d757..ee7c60c9 100644 --- a/lambda-buffers-compiler/src/LambdaBuffers/Compiler/ProtoCompat/Types.hs +++ b/lambda-buffers-compiler/src/LambdaBuffers/Compiler/ProtoCompat/Types.hs @@ -6,7 +6,6 @@ {-# OPTIONS_GHC -fconstraint-solver-iterations=0 #-} module LambdaBuffers.Compiler.ProtoCompat.Types ( - localRef2ForeignRef, ClassDef (..), ClassName (..), CompilerError (..), @@ -54,7 +53,7 @@ module LambdaBuffers.Compiler.ProtoCompat.Types ( ) where import Control.Exception (Exception) -import Control.Lens (Getter, to, (^.)) +import Data.Data (Typeable) import Data.Generics.Labels () import Data.Map (Map) import Data.Set (Set) @@ -140,7 +139,7 @@ instance Arbitrary KindType where | n <= 0 = KindRef <$> arbitrary | otherwise = KindArrow <$> resize (n `div` 2) arbitrary <*> resize (n `div` 2) arbitrary -data KindRefType = KUnspecified | KType +data KindRefType = KUnspecified | KType | KConstraint deriving stock (Show, Eq, Ord, Generic) deriving (Arbitrary) via GenericArbitrary KindRefType deriving anyclass (SOP.Generic) @@ -181,17 +180,6 @@ data LocalRef = LocalRef {tyName :: TyName, sourceInfo :: SourceInfo} 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 @@ -360,28 +348,31 @@ instance Arbitrary CompilerInput where where fn n = CompilerInput <$> resize n arbitrary -data KindCheckError - = UnboundTyVarError TyDef TyVar ModuleName - | UnboundTyRefError TyDef TyRef ModuleName - | IncorrectApplicationError TyDef Kind Kind ModuleName - | RecursiveKindError TyDef ModuleName - | InconsistentTypeError TyDef Kind Kind ModuleName +data KindCheckError loc + = UnboundTyVarError loc TyVar ModuleName + | UnboundTyRefError loc TyRef ModuleName + | UnboundTyClassRefError loc TyClassRef ModuleName + | IncorrectApplicationError loc Kind Kind ModuleName + | RecursiveKindError loc ModuleName + | InconsistentTypeError loc Kind Kind ModuleName deriving stock (Show, Eq, Ord, Generic) - deriving (Arbitrary) via GenericArbitrary KindCheckError deriving anyclass (SOP.Generic) -instance Exception KindCheckError +instance (Typeable loc, Show loc) => Exception (KindCheckError loc) -- | All the compiler errors. data CompilerError - = CompKindCheckError KindCheckError - | InternalError Text + = -- | Compiler KindChecker Error - within a Type Definition. + CKC'TyDefError (KindCheckError TyDef) + | -- | Compiler KindChecker Error - within a Class Definition. + CKC'ClassDefError (KindCheckError ClassDef) + | -- | Compiler KindChecker Error - within a Class Instance. + CKC'ClassInstanceError (KindCheckError InstanceClause) + | C'InternalError Text deriving stock (Show, Eq, Ord, Generic) - deriving (Arbitrary) via GenericArbitrary CompilerError deriving anyclass (SOP.Generic) data CompilerResult = CompilerResult deriving stock (Show, Eq, Ord, Generic) - deriving (Arbitrary) via GenericArbitrary CompilerResult deriving anyclass (SOP.Generic) type CompilerOutput = Either CompilerError CompilerResult diff --git a/lambda-buffers-compiler/test/Test/KindCheck.hs b/lambda-buffers-compiler/test/Test/KindCheck.hs index effd90d5..2c29f58b 100644 --- a/lambda-buffers-compiler/test/Test/KindCheck.hs +++ b/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 TyClass 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 + , TyClass.test ] -------------------------------------------------------------------------------- diff --git a/lambda-buffers-compiler/test/Test/KindCheck/Errors.hs b/lambda-buffers-compiler/test/Test/KindCheck/Errors.hs index 5f6680ce..360859bf 100644 --- a/lambda-buffers-compiler/test/Test/KindCheck/Errors.hs +++ b/lambda-buffers-compiler/test/Test/KindCheck/Errors.hs @@ -2,7 +2,8 @@ module Test.KindCheck.Errors (testGKindCheckErrors) where import LambdaBuffers.Compiler.KindCheck (check_) import LambdaBuffers.Compiler.ProtoCompat qualified as PC -import LambdaBuffers.Compiler.ProtoCompat.Types (CompilerError (CompKindCheckError), KindCheckError (UnboundTyRefError, UnboundTyVarError)) +import LambdaBuffers.Compiler.ProtoCompat.Types (CompilerError (CKC'TyDefError), KindCheckError (UnboundTyRefError, UnboundTyVarError)) + import Test.Tasty (TestTree, testGroup) import Test.Tasty.HUnit (testCase, (@?=)) import Test.Utils.CompilerInput (compilerInput'undefinedForeignTyRef, compilerInput'undefinedLocalTyRef, compilerInput'undefinedVariable) @@ -16,19 +17,19 @@ undefinedVariable :: TestTree undefinedVariable = testCase "Catch undefined(free) variable in Type Definition." $ check_ compilerInput'undefinedVariable - @?= (Left . CompKindCheckError . withDefModule) (UnboundTyVarError tyDef'undefinedVar tyDef'undefinedVar'var) + @?= (Left . CKC'TyDefError . withDefModule) (UnboundTyVarError tyDef'undefinedVar tyDef'undefinedVar'var) undefinedLocalTyRef :: TestTree undefinedLocalTyRef = testCase "Catch undefined Local TyRef in Type Definition." $ check_ compilerInput'undefinedLocalTyRef - @?= (Left . CompKindCheckError . withDefModule) (UnboundTyRefError tyDef'undefinedLocalTyRef tyDef'undefinedLocalTyRef'TyRef) + @?= (Left . CKC'TyDefError . withDefModule) (UnboundTyRefError tyDef'undefinedLocalTyRef tyDef'undefinedLocalTyRef'TyRef) undefinedForeignTyRef :: TestTree undefinedForeignTyRef = testCase "Catch undefined Foreign TyRef in Type Definition." $ check_ compilerInput'undefinedForeignTyRef - @?= (Left . CompKindCheckError . withDefModule) (UnboundTyRefError tyDef'undefinedForeignTyRef tyDef'undefinedForeignTyRef'TyRef) + @?= (Left . CKC'TyDefError . withDefModule) (UnboundTyRefError tyDef'undefinedForeignTyRef tyDef'undefinedForeignTyRef'TyRef) withDefModule :: forall a. (PC.ModuleName -> a) -> a withDefModule f = f (_ModuleName ["Module"]) diff --git a/lambda-buffers-compiler/test/Test/KindCheck/TyClass.hs b/lambda-buffers-compiler/test/Test/KindCheck/TyClass.hs new file mode 100644 index 00000000..510ea5f8 --- /dev/null +++ b/lambda-buffers-compiler/test/Test/KindCheck/TyClass.hs @@ -0,0 +1,64 @@ +module Test.KindCheck.TyClass (test) where + +import LambdaBuffers.Compiler.KindCheck (check_) +import LambdaBuffers.Compiler.ProtoCompat.Types (CompilerInput) +import Test.Tasty (TestTree, testGroup) +import Test.Tasty.HUnit (Assertion, testCase, (@?=)) +import Test.Tasty.Providers (TestName) +import Test.Utils.CompilerInput ( + compilerInput'IntEqInstance, + compilerInput'classEq, + compilerInput'classOrd, + compilerInput'classOrdInstanceEq, + compilerInput'failingAdditionalVarConstraint, + compilerInput'unboundEq, + ) +import Test.Utils.Constructors () +import Test.Utils.TyDef () + +test :: TestTree +test = + testGroup + "KC Class Error." + [ testGroup "Class Defs." [ok'Eq, ok'Ord, fail'Ord] + , testGroup "Class Instances." [ok'IntEqInstance, ok'OrdInstanceEq, fail'RedundantVar] + ] + +-------------------------------------------------------------------------------- +-- Class Defs + +ok'Eq :: TestTree +ok'Eq = oKCase "Class Eq definition." compilerInput'classEq + +ok'Ord :: TestTree +ok'Ord = oKCase "Class Ord definition." compilerInput'classOrd + +fail'Ord :: TestTree +fail'Ord = failCase "Unbound reference to eq." compilerInput'unboundEq + +-------------------------------------------------------------------------------- +-- Class Instances + +ok'IntEqInstance :: TestTree +ok'IntEqInstance = oKCase "instance Int Eq." compilerInput'IntEqInstance + +ok'OrdInstanceEq :: TestTree +ok'OrdInstanceEq = oKCase "instance Ord a => Eq a." compilerInput'classOrdInstanceEq + +fail'RedundantVar :: TestTree +fail'RedundantVar = failCase "instance Ord b => Eq a." compilerInput'failingAdditionalVarConstraint + +-------------------------------------------------------------------------------- +-- Utils + +failCase :: TestName -> CompilerInput -> TestTree +failCase n x = testCase n $ justFail x + where + justFail :: CompilerInput -> Assertion + justFail a = either (Left . const ()) Right (check_ a) @?= Left () + +oKCase :: TestName -> CompilerInput -> TestTree +oKCase n x = testCase n $ oK x + where + oK :: CompilerInput -> Assertion + oK a = check_ a @?= Right () diff --git a/lambda-buffers-compiler/test/Test/Utils/ClassDef.hs b/lambda-buffers-compiler/test/Test/Utils/ClassDef.hs new file mode 100644 index 00000000..f1afc03f --- /dev/null +++ b/lambda-buffers-compiler/test/Test/Utils/ClassDef.hs @@ -0,0 +1,19 @@ +module Test.Utils.ClassDef (classDef'Eq, classDef'Ord, classInstance'IntEq, classInstance'OrdEq, classInstance'OrdEqFailing) where + +import LambdaBuffers.Compiler.ProtoCompat qualified as PC +import Test.Utils.Constructors (_ClassDef, _Constraint, _InstanceClause, _InstanceClause', _LocalClassRef, _TyRefILocal, _TyVarI, _Type) + +classDef'Eq :: PC.ClassDef +classDef'Eq = _ClassDef "Eq" ("a", _Type) mempty + +classDef'Ord :: PC.ClassDef +classDef'Ord = _ClassDef "Ord" ("a", _Type) [_Constraint (_LocalClassRef "Eq") (_TyVarI "a")] + +classInstance'IntEq :: PC.InstanceClause +classInstance'IntEq = _InstanceClause "Eq" (_TyRefILocal "Int") + +classInstance'OrdEq :: PC.InstanceClause +classInstance'OrdEq = _InstanceClause' "Eq" (_TyVarI "a") [_Constraint (_LocalClassRef "Ord") (_TyVarI "a")] + +classInstance'OrdEqFailing :: PC.InstanceClause +classInstance'OrdEqFailing = _InstanceClause' "Eq" (_TyVarI "a") [_Constraint (_LocalClassRef "Ord") (_TyVarI "b")] diff --git a/lambda-buffers-compiler/test/Test/Utils/CompilerInput.hs b/lambda-buffers-compiler/test/Test/Utils/CompilerInput.hs index 7785fe19..9b1927a8 100644 --- a/lambda-buffers-compiler/test/Test/Utils/CompilerInput.hs +++ b/lambda-buffers-compiler/test/Test/Utils/CompilerInput.hs @@ -6,44 +6,75 @@ module Test.Utils.CompilerInput ( compilerInput'either, compilerInput'undefinedForeignTyRef, compilerInput'recDef, + compilerInput'classEq, + compilerInput'classOrd, + compilerInput'unboundEq, + compilerInput'IntEqInstance, + compilerInput'classOrdInstanceEq, + compilerInput'failingAdditionalVarConstraint, ) where -import LambdaBuffers.Compiler.ProtoCompat qualified as P +import LambdaBuffers.Compiler.ProtoCompat qualified as PC import Test.Utils.Constructors (_CompilerInput) import Test.Utils.Module ( + module'AdditionalVarEqInstance, + module'Int, + module'IntEqInstance, + module'OrdEqInstance, + module'classEq, + module'classOrd, module'either, module'incoherent, module'maybe, module'recDef, + module'unboundEq, module'undefinedForeignTyRef, module'undefinedLocalTyRef, module'undefinedVar, ) -- | Compiler Input containing 1 module with 1 definition - Maybe. -compilerInput'maybe :: P.CompilerInput +compilerInput'maybe :: PC.CompilerInput compilerInput'maybe = _CompilerInput [module'maybe] -- | Compiler Input containing 1 module with 1 definition - Either. -compilerInput'either :: P.CompilerInput +compilerInput'either :: PC.CompilerInput compilerInput'either = _CompilerInput [module'either] -- | Compiler Input containing 1 module with 1 definition - Either. -compilerInput'recDef :: P.CompilerInput +compilerInput'recDef :: PC.CompilerInput compilerInput'recDef = _CompilerInput [module'recDef] -- | Contains 2 definitions - 1 wrong one. -compilerInput'incoherent :: P.CompilerInput +compilerInput'incoherent :: PC.CompilerInput compilerInput'incoherent = _CompilerInput [module'maybe, module'incoherent] -- | Contains 1 undefined variable. -compilerInput'undefinedVariable :: P.CompilerInput +compilerInput'undefinedVariable :: PC.CompilerInput compilerInput'undefinedVariable = _CompilerInput [module'undefinedVar] -- | Contains 1 undefined Local TyRef. -compilerInput'undefinedLocalTyRef :: P.CompilerInput +compilerInput'undefinedLocalTyRef :: PC.CompilerInput compilerInput'undefinedLocalTyRef = _CompilerInput [module'undefinedLocalTyRef] -- | Contains 1 undefined Foreign TyRef. -compilerInput'undefinedForeignTyRef :: P.CompilerInput +compilerInput'undefinedForeignTyRef :: PC.CompilerInput compilerInput'undefinedForeignTyRef = _CompilerInput [module'undefinedForeignTyRef] + +compilerInput'classEq :: PC.CompilerInput +compilerInput'classEq = _CompilerInput [module'classEq] + +compilerInput'classOrd :: PC.CompilerInput +compilerInput'classOrd = _CompilerInput [module'classOrd] + +compilerInput'classOrdInstanceEq :: PC.CompilerInput +compilerInput'classOrdInstanceEq = _CompilerInput [module'OrdEqInstance] + +compilerInput'unboundEq :: PC.CompilerInput +compilerInput'unboundEq = _CompilerInput [module'unboundEq] + +compilerInput'IntEqInstance :: PC.CompilerInput +compilerInput'IntEqInstance = _CompilerInput [module'classEq, module'IntEqInstance, module'Int] + +compilerInput'failingAdditionalVarConstraint :: PC.CompilerInput +compilerInput'failingAdditionalVarConstraint = _CompilerInput [module'AdditionalVarEqInstance] diff --git a/lambda-buffers-compiler/test/Test/Utils/Constructors.hs b/lambda-buffers-compiler/test/Test/Utils/Constructors.hs index 41f0c44c..2d7c82de 100644 --- a/lambda-buffers-compiler/test/Test/Utils/Constructors.hs +++ b/lambda-buffers-compiler/test/Test/Utils/Constructors.hs @@ -23,22 +23,30 @@ module Test.Utils.Constructors ( _LocalRef', _ForeignRef', _TyApp, + _Opaque, + _TyAbs', + + -- * Class related. + _ClassDef, + _ClassName, + _LocalClassRef, + _ForeignCI, + _Constraint, + _InstanceClause, + _InstanceClause', ) where import Control.Lens ((^.)) +import Data.Default (def) import Data.Map qualified as Map import Data.Text (Text) import LambdaBuffers.Compiler.ProtoCompat qualified as PC import LambdaBuffers.Compiler.ProtoCompat.Types (SourceInfo) import Proto.Compiler_Fields () -import Data.Default (def) - _CompilerInput :: [PC.Module] -> PC.CompilerInput _CompilerInput ms = - PC.CompilerInput - { PC.modules = Map.fromList [(m ^. #moduleName, m) | m <- ms] - } + PC.CompilerInput {PC.modules = Map.fromList [(m ^. #moduleName, m) | m <- ms]} _Module :: PC.ModuleName -> [PC.TyDef] -> [PC.ClassDef] -> [PC.InstanceClause] -> PC.Module _Module mn tds cds ins = @@ -137,6 +145,14 @@ _TyAbs args body = , sourceInfo = PC.defSourceInfo } +_TyAbs' :: [(Text, PC.KindType)] -> PC.TyBody -> PC.TyAbs +_TyAbs' args body = + PC.TyAbs + { PC.tyArgs = Map.fromList [(ta ^. #argName, ta) | ta <- _TyArg <$> args] + , PC.tyBody = body + , sourceInfo = PC.defSourceInfo + } + _TyArg :: (Text, PC.KindType) -> PC.TyArg _TyArg (a, k) = PC.TyArg @@ -175,3 +191,61 @@ _ForeignRef' x m s = , PC.moduleName = m , PC.sourceInfo = s } + +-------------------------------------------------------------------------------- +-- Class related. + +_ClassDef :: Text -> (Text, PC.KindType) -> [PC.Constraint] -> PC.ClassDef +_ClassDef n tyArg cs = + PC.ClassDef + { className = _ClassName n + , classArgs = _TyArg tyArg + , supers = cs + , documentation = mempty + , sourceInfo = def + } + +_ClassName :: Text -> PC.ClassName +_ClassName n = PC.ClassName {name = n, sourceInfo = def} + +_Constraint :: PC.TyClassRef -> PC.Ty -> PC.Constraint +_Constraint cr t = + PC.Constraint + { classRef = cr + , argument = t + , sourceInfo = def + } + +_LocalClassRef :: Text -> PC.TyClassRef +_LocalClassRef n = + PC.LocalCI $ PC.LocalClassRef {className = _ClassName n, sourceInfo = def} + +_ForeignCI :: Text -> PC.ModuleName -> PC.TyClassRef +_ForeignCI n mn = + PC.ForeignCI $ + PC.ForeignClassRef + { className = _ClassName n + , moduleName = mn + , sourceInfo = def + } + +_InstanceClause' :: Text -> PC.Ty -> [PC.Constraint] -> PC.InstanceClause +_InstanceClause' n ty cs = + PC.InstanceClause + { classRef = _LocalClassRef n + , head = ty + , constraints = cs + , sourceInfo = def + } + +_InstanceClause :: Text -> PC.Ty -> PC.InstanceClause +_InstanceClause n ty = + PC.InstanceClause + { classRef = _LocalClassRef n + , head = ty + , constraints = mempty + , sourceInfo = def + } + +_Opaque :: PC.TyBody +_Opaque = PC.OpaqueI def diff --git a/lambda-buffers-compiler/test/Test/Utils/Module.hs b/lambda-buffers-compiler/test/Test/Utils/Module.hs index 95d704cc..38dd16a5 100644 --- a/lambda-buffers-compiler/test/Test/Utils/Module.hs +++ b/lambda-buffers-compiler/test/Test/Utils/Module.hs @@ -6,11 +6,19 @@ module Test.Utils.Module ( module'undefinedForeignTyRef, module'either, module'recDef, + module'classEq, + module'unboundEq, + module'classOrd, + module'IntEqInstance, + module'Int, + module'OrdEqInstance, + module'AdditionalVarEqInstance, ) where -import LambdaBuffers.Compiler.ProtoCompat qualified as P +import LambdaBuffers.Compiler.ProtoCompat qualified as PC import Test.Utils.Constructors (_Module, _ModuleName) import Test.Utils.TyDef ( + tyDef'Int, tyDef'either, tyDef'incoherent, tyDef'maybe, @@ -20,15 +28,23 @@ import Test.Utils.TyDef ( tyDef'undefinedVar, ) +import Test.Utils.ClassDef ( + classDef'Eq, + classDef'Ord, + classInstance'IntEq, + classInstance'OrdEq, + classInstance'OrdEqFailing, + ) + -- _Module mn tds cds ins = -module'maybe :: P.Module +module'maybe :: PC.Module module'maybe = _Module (_ModuleName ["Prelude"]) [tyDef'maybe] mempty mempty -module'either :: P.Module +module'either :: PC.Module module'either = _Module (_ModuleName ["Prelude"]) [tyDef'either] mempty mempty -module'recDef :: P.Module +module'recDef :: PC.Module module'recDef = _Module (_ModuleName ["Prelude"]) [tyDef'recDef] mempty mempty {- | 1 Module containing @@ -40,7 +56,7 @@ module'recDef = _Module (_ModuleName ["Prelude"]) [tyDef'recDef] mempty mempty Should fail as B a defaults to B :: Type -> Type and Maybe is inferred as Type -> Type. This is an inconsistency failure. -} -module'incoherent :: P.Module +module'incoherent :: PC.Module module'incoherent = _Module (_ModuleName ["Module"]) [tyDef'maybe, tyDef'incoherent] mempty mempty {- | 1 Module containing @@ -48,7 +64,7 @@ module'incoherent = _Module (_ModuleName ["Module"]) [tyDef'maybe, tyDef'incoher Should fail as b is undefined. -} -module'undefinedVar :: P.Module +module'undefinedVar :: PC.Module module'undefinedVar = _Module (_ModuleName ["Module"]) [tyDef'undefinedVar] mempty mempty {- | 1 Module containing @@ -56,7 +72,7 @@ module'undefinedVar = _Module (_ModuleName ["Module"]) [tyDef'undefinedVar] memp ^^^ Should fail as Baz is a local undefined Ty Ref. -} -module'undefinedLocalTyRef :: P.Module +module'undefinedLocalTyRef :: PC.Module module'undefinedLocalTyRef = _Module (_ModuleName ["Module"]) [tyDef'undefinedLocalTyRef] mempty mempty {- | 1 Module containing @@ -64,5 +80,36 @@ module'undefinedLocalTyRef = _Module (_ModuleName ["Module"]) [tyDef'undefinedLo ^^^^^^^^^^^^^^^^^^ Should fail as Baz is a foreign undefined Ty Ref. -} -module'undefinedForeignTyRef :: P.Module +module'undefinedForeignTyRef :: PC.Module module'undefinedForeignTyRef = _Module (_ModuleName ["Module"]) [tyDef'undefinedForeignTyRef] mempty mempty + +{- | 1 Module containing: + class Eq a. +-} +module'classEq :: PC.Module +module'classEq = _Module (_ModuleName ["Module"]) mempty [classDef'Eq] mempty + +{- | 1 Module containing: + class Eq a. + class Eq a => Ord a. +-} +module'classOrd :: PC.Module +module'classOrd = _Module (_ModuleName ["Module"]) mempty [classDef'Eq, classDef'Ord] mempty + +module'unboundEq :: PC.Module +module'unboundEq = _Module (_ModuleName ["Module"]) mempty [classDef'Ord] mempty + +module'Int :: PC.Module +module'Int = _Module (_ModuleName ["Module"]) [] mempty mempty + +{- | 1 Module containing: + instance Eq Int. +-} +module'IntEqInstance :: PC.Module +module'IntEqInstance = _Module (_ModuleName ["Module"]) [tyDef'Int] [classDef'Eq] [classInstance'IntEq] + +module'OrdEqInstance :: PC.Module +module'OrdEqInstance = _Module (_ModuleName ["Module"]) mempty [classDef'Eq, classDef'Ord] [classInstance'OrdEq] + +module'AdditionalVarEqInstance :: PC.Module +module'AdditionalVarEqInstance = _Module (_ModuleName ["Module"]) mempty [classDef'Eq, classDef'Ord] [classInstance'OrdEqFailing] diff --git a/lambda-buffers-compiler/test/Test/Utils/TyDef.hs b/lambda-buffers-compiler/test/Test/Utils/TyDef.hs index 56f5e569..487983e9 100644 --- a/lambda-buffers-compiler/test/Test/Utils/TyDef.hs +++ b/lambda-buffers-compiler/test/Test/Utils/TyDef.hs @@ -9,6 +9,7 @@ module Test.Utils.TyDef ( tyDef'undefinedForeignTyRef'TyRef, tyDef'recDef, tyDef'either, + tyDef'Int, ) where import LambdaBuffers.Compiler.ProtoCompat.Types (Ty (TyVarI)) @@ -17,9 +18,11 @@ import Test.Utils.Constructors ( _ForeignRef', _LocalRef', _ModuleName, + _Opaque, _SourceInfo, _TupleI, _TyAbs, + _TyAbs', _TyApp, _TyDef, _TyName, @@ -142,3 +145,7 @@ tyDef'undefinedForeignTyRef = -} tyDef'undefinedForeignTyRef'TyRef :: P.TyRef tyDef'undefinedForeignTyRef'TyRef = P.ForeignI $ _ForeignRef' "Baz" (_ModuleName ["Foreign", "Module"]) (_SourceInfo 1 2) + +-- Int +tyDef'Int :: P.TyDef +tyDef'Int = _TyDef (_TyName "Int") (_TyAbs' [] _Opaque) diff --git a/lambda-buffers-proto/a.cpp b/lambda-buffers-proto/a.cpp new file mode 100644 index 00000000..dcce0994 Binary files /dev/null and b/lambda-buffers-proto/a.cpp differ diff --git a/lambda-buffers-proto/compiler.proto b/lambda-buffers-proto/compiler.proto index b2776e95..0493abaf 100644 --- a/lambda-buffers-proto/compiler.proto +++ b/lambda-buffers-proto/compiler.proto @@ -251,6 +251,8 @@ message Kind { KIND_REF_UNSPECIFIED = 0; // A `Type` kind (also know as `*` in Haskell) built-in. KIND_REF_TYPE = 1; + // A `Constraint` kind - relating to the kind of a Type Class. + KIND_REF_CONSTRAINT = 2; }; // A kind arrow. message KindArrow { @@ -631,8 +633,83 @@ message ProtoParseError { } } -// Kind checking errors. -message KindCheckError { +// Kind checking errors - in a Class definition. +message KindCheckErrorClassDef { + + // Unbound variable ty_var detected in term ty_def. + message UnboundTyVarError { + ModuleName module_name = 1; + ClassDef class_def = 2; + TyVar ty_var = 3; + } + + // Unbound type reference ty_ref detected in term ty_def. + message UnboundTyRefError { + ModuleName module_name = 1; + ClassDef class_def = 2; + TyRef ty_ref = 3; + } + + + // Unbound type class reference ty_class_ref detected in term ty_def. + message UnboundTyClassRefError { + ModuleName module_name = 1; + ClassDef class_def = 2; + TyClassRef ty_class_ref = 3; + } + + // In ty_def an error has occurred when trying to unify kind ty_kind_lhs + // with ty_kind_rhs. + // + // FIXME(cstml): Add source of constraint to the error such that user can see + // where the constraint was generated - therefore where the error precisely + // is. + message UnificationError { + ModuleName module_name = 1; + ClassDef class_def = 2; + Kind ty_kind_lhs = 3; + Kind ty_kind_rhs = 4; + } + + // A cyclic kind was encountered. Infinite kinds like this are not acceptable, + // and we do not support them. We could not construct infinite kind in ty_def. + // + // As the implementation currently stands such an error is (most likely) not + // representable - therefore not reachable. Such an error would usually occur + // for a term like: λa. a a - in which case the inference would try to unify + // two kinds of the form: m and m -> n - because m appears in both terms - + // the cyclic unification error would be thrown. + // + // In the case of LambdaBuffers - such an error is not (currently) achievable + // as the kind of the variable is given by the context - (i.e. λa : m . a a, + // where m is a kind) therefore the unification would fail with Unification + // Error. Nevertheless - future features might require it. + message CyclicKindError { + ModuleName module_name = 1; + ClassDef class_def = 2; + } + + // The actual_kind differs from the expected_kind. + message InconsistentTypeError { + ModuleName module_name = 1; + ClassDef class_def = 2; + Kind actual_kind = 3; + Kind expected_kind = 4; + } + + // One of the errors occurred during kind checking. + oneof kind_check_error { + UnboundTyRefError unbound_ty_ref_error = 1; + UnboundTyVarError unbound_ty_var_error = 2; + UnboundTyClassRefError unbound_ty_class_ref_error = 3; + UnificationError unification_error = 4; + CyclicKindError cyclic_kind_error = 5; + InconsistentTypeError inconsistent_type_error = 6; + } +} + +// Kind checking errors - in a Type definition. +message KindCheckErrorTyDef { // Unbound variable ty_var detected in term ty_def. message UnboundTyVarError { @@ -648,7 +725,16 @@ message KindCheckError { TyRef ty_ref = 3; } - // In ty_def an error has occurred when trying to unify kind ty_kind_lhs + + // Unbound type class reference ty_class_ref detected in term ty_def. + message UnboundTyClassRefError { + ModuleName module_name = 1; + TyDef ty_def = 2; + TyClassRef ty_class_ref = 3; + } + + + // In ty_def an error has occurred when trying to unify kind ty_kind_lhs // with ty_kind_rhs. // // FIXME(cstml): Add source of constraint to the error such that user can see @@ -663,7 +749,7 @@ message KindCheckError { // A cyclic kind was encountered. Infinite kinds like this are not acceptable, // and we do not support them. We could not construct infinite kind in ty_def. - // + // // As the implementation currently stands such an error is (most likely) not // representable - therefore not reachable. Such an error would usually occur // for a term like: λa. a a - in which case the inference would try to unify @@ -675,8 +761,8 @@ message KindCheckError { // where m is a kind) therefore the unification would fail with Unification // Error. Nevertheless - future features might require it. message CyclicKindError { - TyDef ty_def = 1; - ModuleName module_name = 2; + ModuleName module_name = 1; + TyDef ty_def = 2; } // The actual_kind differs from the expected_kind. @@ -691,12 +777,89 @@ message KindCheckError { oneof kind_check_error { UnboundTyRefError unbound_ty_ref_error = 1; UnboundTyVarError unbound_ty_var_error = 2; - UnificationError unification_error = 3; - CyclicKindError cyclic_kind_error = 4; - InconsistentTypeError inconsistent_type_error = 5; + UnboundTyClassRefError unbound_ty_class_ref_error = 3; + UnificationError unification_error = 4; + CyclicKindError cyclic_kind_error = 5; + InconsistentTypeError inconsistent_type_error = 6; + } +} + +// Kind checking errors - in a Class definition. +message KindCheckErrorClassInstance { + + // Unbound variable ty_var detected in term ty_def. + message UnboundTyVarError { + ModuleName module_name = 1; + InstanceClause instance_clause = 2; + TyVar ty_var = 3; + } + + // Unbound type reference ty_ref detected in term ty_def. + message UnboundTyRefError { + ModuleName module_name = 1; + InstanceClause instance_clause = 2; + TyRef ty_ref = 3; + } + + + // Unbound type class reference ty_class_ref detected in term ty_def. + message UnboundTyClassRefError { + ModuleName module_name = 1; + InstanceClause instance_clause = 2; + TyClassRef ty_class_ref = 3; + } + + // In ty_def an error has occurred when trying to unify kind ty_kind_lhs + // with ty_kind_rhs. + // + // FIXME(cstml): Add source of constraint to the error such that user can see + // where the constraint was generated - therefore where the error precisely + // is. + message UnificationError { + ModuleName module_name = 1; + InstanceClause instance_clause = 2; + Kind ty_kind_lhs = 3; + Kind ty_kind_rhs = 4; + } + + // A cyclic kind was encountered. Infinite kinds like this are not acceptable, + // and we do not support them. We could not construct infinite kind in ty_def. + // + // As the implementation currently stands such an error is (most likely) not + // representable - therefore not reachable. Such an error would usually occur + // for a term like: λa. a a - in which case the inference would try to unify + // two kinds of the form: m and m -> n - because m appears in both terms - + // the cyclic unification error would be thrown. + // + // In the case of LambdaBuffers - such an error is not (currently) achievable + // as the kind of the variable is given by the context - (i.e. λa : m . a a, + // where m is a kind) therefore the unification would fail with Unification + // Error. Nevertheless - future features might require it. + message CyclicKindError { + ModuleName module_name = 1; + InstanceClause instance_clause = 2; + } + + // The actual_kind differs from the expected_kind. + message InconsistentTypeError { + ModuleName module_name = 1; + InstanceClause instance_clause = 2; + Kind actual_kind = 3; + Kind expected_kind = 4; + } + + // One of the errors occurred during kind checking. + oneof kind_check_error { + UnboundTyRefError unbound_ty_ref_error = 1; + UnboundTyVarError unbound_ty_var_error = 2; + UnboundTyClassRefError unbound_ty_class_ref_error = 3; + UnificationError unification_error = 4; + CyclicKindError cyclic_kind_error = 5; + InconsistentTypeError inconsistent_type_error = 6; } } + /* Naming error message */ message NamingError { // One of naming errors. @@ -716,10 +879,14 @@ message CompilerError { repeated ProtoParseError proto_parse_errors = 1; // Errors occurred during naming checking. repeated NamingError naming_errors = 2; - // Errors occurred during kind checking. - repeated KindCheckError kind_check_errors = 4; + // Errors occurred during kind checking Type definitions. + repeated KindCheckErrorTyDef kind_check_errors_ty_defs = 4; + // Errors occurred during kind checking Class definitions. + repeated KindCheckErrorClassDef kind_check_errors_class_defs = 5; + // Errors occurred during kind checking Class instances. + repeated KindCheckErrorClassInstance kind_check_errors_class_instances = 6; // Errors internal to the compiler implementation. - repeated InternalError internal_errors = 5; + repeated InternalError internal_errors = 7; } // Compiler Result ~ a successful Compilation Output.