Implemented solution to 'What do we do w/ the C a in instance C a => C (F a) puzzle, wrote tests for derive check, cleaned up modules

Author: gnumonik

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

@@ -153,9 +153,10 @@ test-suite tests
   main-is:        Test.hs
   build-depends:
     , containers
+    , generic-lens
     , lambda-buffers-compiler
     , lambda-buffers-compiler-pb  >=0.1
-    , prettyprinter
+    , lens
     , proto-lens                  >=0.7
     , QuickCheck                  >=2.14
     , tasty                       >=1.4

lambda-buffers-compiler/src/LambdaBuffers/Compiler/TypeClass/Compat.hs

@@ -1,14 +1,33 @@
 {-# LANGUAGE OverloadedLabels #-}
 
-module LambdaBuffers.Compiler.TypeClass.Compat where
+module LambdaBuffers.Compiler.TypeClass.Compat (
+  modulename,
+  defToExp,
+  tyToExp,
+  appToExp,
+  defToPat,
+  tyToPat,
+  appToPat,
+) where
 
 import Control.Lens ((^.))
 import Control.Lens.Combinators (view)
 import Data.List.NonEmpty (NonEmpty ((:|)))
 import Data.List.NonEmpty qualified as NE
 import Data.Text qualified as T
 import LambdaBuffers.Compiler.ProtoCompat qualified as P
-import LambdaBuffers.Compiler.TypeClass.Pat
+import LambdaBuffers.Compiler.TypeClass.Pat (
+  Exp (AppE, DecE, LitE, NilE, RefE),
+  ExpressionLike (nil, (*:), (*=)),
+  Literal (ModuleName, Name, Opaque, TyVar),
+  Pat (AppP, DecP, LitP, NilP, RefP, VarP),
+  toProdE,
+  toProdP,
+  toRecE,
+  toRecP,
+  toSumE,
+  toSumP,
+ )
 
 {-
     TyDefs

lambda-buffers-compiler/src/LambdaBuffers/Compiler/TypeClass/Pat.hs

@@ -1,6 +1,21 @@
 {-# LANGUAGE LambdaCase #-}
 
-module LambdaBuffers.Compiler.TypeClass.Pat where
+module LambdaBuffers.Compiler.TypeClass.Pat (
+  Pat (..),
+  Exp (..),
+  Literal (..),
+  ExpressionLike (..),
+  toProdP,
+  toSumP,
+  toRecP,
+  patList,
+  toProdE,
+  toSumE,
+  toRecE,
+  getLocalRefE,
+  expList,
+  matches,
+) where
 
 import Data.Kind (Type)
 import Data.Text (Text)
@@ -126,6 +141,22 @@ toRecE = RecE . foldr ConsE NilE
 toSumE :: [Exp] -> Exp
 toSumE = SumE . foldr ConsE NilE
 
+-- | Extract the "type function" from an AppE Expr
+tyFunE :: Exp -> Maybe Exp
+tyFunE = \case
+  AppE e1 _ -> case tyFunE e1 of
+    Nothing -> Just e1
+    Just e2 -> Just e2
+  _ -> Nothing
+
+getLocalRefE :: Exp -> Maybe Text
+getLocalRefE = \case
+  RefE NilE (LitE (Name t)) -> Just t
+  app@(AppE _ _) -> case tyFunE app of
+    Just (RefE NilE (LitE (Name t))) -> Just t
+    _ -> Nothing
+  _ -> Nothing
+
 {- Converts a pattern that consists of a well formed pattern list
    (i.e. patterns formed from :* and Nil) into a list of patterns.
 -}

lambda-buffers-compiler/src/LambdaBuffers/Compiler/TypeClass/Pretty.hs

@@ -13,7 +13,13 @@ import Control.Lens.Operators ((^.))
 import Data.Generics.Labels ()
 import Data.Text qualified as T
 import LambdaBuffers.Compiler.ProtoCompat qualified as P
-import LambdaBuffers.Compiler.TypeClass.Pat
+import LambdaBuffers.Compiler.TypeClass.Pat (
+  Exp (AppE, ConsE, DecE, LabelE, LitE, NilE, ProdE, RecE, RefE, SumE),
+  Literal (ModuleName, Name, Opaque, TyVar),
+  Pat (AppP, ConsP, DecP, LabelP, LitP, NilP, ProdP, RecP, RefP, SumP, VarP),
+  expList,
+  patList,
+ )
 import LambdaBuffers.Compiler.TypeClass.Rules (
   Class (Class),
   Constraint (C),

lambda-buffers-compiler/src/LambdaBuffers/Compiler/TypeClass/Rules.hs

@@ -1,7 +1,14 @@
 {-# LANGUAGE GADTs #-}
 {-# LANGUAGE TypeFamilies #-}
 
-module LambdaBuffers.Compiler.TypeClass.Rules where
+module LambdaBuffers.Compiler.TypeClass.Rules (
+  FQClassName (..),
+  Class (..),
+  Constraint (..),
+  Rule (..),
+  ruleHead,
+  ruleClass,
+) where
 
 import Data.Text (Text)
 

lambda-buffers-compiler/src/LambdaBuffers/Compiler/TypeClass/Solve.hs

@@ -1,20 +1,18 @@
 {-# LANGUAGE LambdaCase #-}
 
-module LambdaBuffers.Compiler.TypeClass.Solve where
+module LambdaBuffers.Compiler.TypeClass.Solve (solve, inst, Overlap (..)) where
 
 import Control.Monad.Except (throwError)
 import Control.Monad.Reader (ReaderT, runReaderT)
 import Control.Monad.Reader.Class (MonadReader (ask))
 import Control.Monad.Writer.Class (MonadWriter (tell))
 import Control.Monad.Writer.Strict (WriterT, execWriterT)
 import Data.Foldable (traverse_)
-import Data.List (foldl')
 import Data.Map qualified as M
 import Data.Set qualified as S
 import Data.Text (Text)
-import Debug.Trace (traceM)
-import LambdaBuffers.Compiler.TypeClass.Pat
-import LambdaBuffers.Compiler.TypeClass.Rules
+import LambdaBuffers.Compiler.TypeClass.Pat (Exp (AppE, ConsE, DecE, LabelE, LitE, NilE, ProdE, RecE, RefE, SumE), ExpressionLike ((*:), (*=)), Literal (TyVar), Pat (AppP, ConsP, DecP, LabelP, LitP, NilP, ProdP, RecP, RefP, SumP, VarP), matches)
+import LambdaBuffers.Compiler.TypeClass.Rules (Class (csupers), Constraint (C), Rule ((:<=)), ruleClass, ruleHead)
 
 {- Pattern/Template/Unification variable  substitution.
    Given a string that represents a variable name,
@@ -38,18 +36,7 @@ subV cxt = \case
   NilP -> NilE
 
 inst :: Pat -> Exp
-inst = \case
-  VarP v -> LitE (TyVar v)
-  ConsP x xs -> ConsE (inst x) (inst xs)
-  LabelP l x -> LabelE (inst l) (inst x)
-  ProdP xs -> ProdE (inst xs)
-  RecP xs -> RecE (inst xs)
-  SumP xs -> SumE (inst xs)
-  AppP t1 t2 -> AppE (inst t1) (inst t2)
-  RefP n x -> RefE (inst n) (inst x)
-  DecP a b c -> DecE (inst a) (inst b) (inst c)
-  LitP l -> LitE l
-  NilP -> NilE
+inst = subV M.empty
 
 {- Performs substitution on an entire instance (the first argument) given the
    concrete types from a Pat (the second argument).
@@ -111,23 +98,20 @@ type SolveM = ReaderT [Rule Pat] (WriterT (S.Set (Constraint Exp)) (Either Overl
          `class Bar y => Foo y` without an `instance Bar X`)
 -}
 solveM :: Constraint Exp -> SolveM ()
+-- TODO(@gnumonik): Explain why we have this TyVar rule here
+solveM (C _ (LitE (TyVar _))) = pure ()
 solveM cst@(C c pat) =
   ask >>= \inScope ->
-    -- First, we look for the most specific instance...
     case selectMatchingInstance pat c inScope of
       Left e -> case e of
         NoMatch -> tell $ S.singleton cst
         OverlappingMatches olps -> throwError $ Overlap cst olps
-      -- If there is, we substitute the argument of the constraint to be solved into the matching rules
       Right rule -> case subst rule pat of
-        -- If there are no additional constraints on the rule, we try to solve the superclasses
         C _ p :<= [] -> solveClassesFor p (csupers c)
-        -- If there are additional constraints on the rule, we try to solve them
         C _ _ :<= is -> do
           traverse_ solveM is
           solveClassesFor pat (csupers c)
   where
-    -- NOTE(@bladyjoker): The version w/ flip is more performant...
     -- Given a Pat and a list of Classes, attempt to solve the constraints
     -- constructed from the Pat and each Class
     solveClassesFor :: Exp -> [Class] -> SolveM ()

lambda-buffers-compiler/src/LambdaBuffers/Compiler/TypeClass/Utils.hs

@@ -27,8 +27,17 @@ import Data.Map qualified as M
 import Data.Set qualified as S
 import Data.Text qualified as T
 
-import LambdaBuffers.Compiler.TypeClass.Compat
-import LambdaBuffers.Compiler.TypeClass.Rules
+import LambdaBuffers.Compiler.TypeClass.Compat (
+  defToExp,
+  modulename,
+  tyToPat,
+ )
+import LambdaBuffers.Compiler.TypeClass.Rules (
+  Class (Class),
+  Constraint (C),
+  FQClassName (FQClassName),
+  Rule ((:<=)),
+ )
 
 import Data.Text (Text)
 import LambdaBuffers.Compiler.ProtoCompat.Types qualified as P (
@@ -41,7 +50,8 @@ import LambdaBuffers.Compiler.ProtoCompat.Types qualified as P (
   SourceInfo,
   TyClassRef (ForeignCI, LocalCI),
  )
-import LambdaBuffers.Compiler.TypeClass.Pat
+import LambdaBuffers.Compiler.TypeClass.Pat (Exp, Literal (ModuleName), Pat (AppP, ConsP, DecP, LabelP, LitP, NilP, ProdP, RecP, RefP, SumP, VarP))
+
 import LambdaBuffers.Compiler.TypeClass.Pretty (pointies, (<///>))
 import LambdaBuffers.Compiler.TypeClass.Solve (Overlap (Overlap))
 import Prettyprinter (
@@ -70,8 +80,9 @@ data TypeClassError
   | LocalTyRefNotFound T.Text P.ModuleName
   | SuperclassCycleDetected [[FQClassName]]
   | CouldntSolveConstraints P.ModuleName [Constraint Exp] Instance
+  | MalformedTyDef P.ModuleName Exp
   | BadInstance BasicConditionViolation
-  deriving stock (Show)
+  deriving stock (Show, Eq, Generic)
 
 instance Pretty TypeClassError where
   pretty = \case
@@ -116,13 +127,19 @@ instance Pretty TypeClassError where
           <> line
           <> line
           <> indent 2 (vcat $ map pretty cs)
+    MalformedTyDef mn xp ->
+      "Error: Encountered malformed type definition:"
+        <> line
+        <> indent 2 (pretty xp)
+        <> line
+        <> indent 2 ("in module" <+> pretty mn)
     BadInstance bcv -> pretty bcv
 
 data BasicConditionViolation
   = TyConInContext Instance (Constraint Pat)
   | OnlyTyVarsInHead Instance (Constraint Pat)
   | OverlapDetected Overlap
-  deriving stock (Show)
+  deriving stock (Show, Eq, Generic)
 
 instance Pretty BasicConditionViolation where
   pretty = \case
@@ -156,23 +173,23 @@ all the type variables are distinct.
 3. The instance declarations must not overlap.
 -}
 
-checkInstance :: Rule Pat -> Either BasicConditionViolation ()
+checkInstance :: Rule Pat -> Either TypeClassError ()
 checkInstance rule@(C cls hd :<= constraints) =
   case traverse cond1 constraints of
     Left e -> Left e
     Right _ -> case hd of
-      VarP _ -> Left $ OnlyTyVarsInHead rule (C cls hd)
+      VarP _ -> Left . BadInstance $ OnlyTyVarsInHead rule (C cls hd)
       -- NOTE: THIS ASSUMES THAT EVERYTHING HAS BEEN KIND-CHECKED AND
       --       THAT NO TYVARS HAVE KIND (* -> *). If every tyvar
       --       is of kind * and we have no MPTCs then the
       --       only case we have to worry about for condition 2 is
       --       a bare type variable in the head
       _ -> Right ()
   where
-    cond1 :: Constraint Pat -> Either BasicConditionViolation ()
+    cond1 :: Constraint Pat -> Either TypeClassError ()
     cond1 cst@(C _ p) = case p of
       VarP _ -> Right ()
-      _ -> Left $ TyConInContext rule cst
+      _ -> Left . BadInstance $ TyConInContext rule cst
 
 {- This contains:
      - Everything needed to validate instances (in the form needed to do so)
@@ -269,11 +286,10 @@ getInstances ctable mn = foldM go S.empty
         let p = tyToPat h
         cs <- traverse goConstraint csts
         let inst = C cls p :<= cs
-        check inst
+        checkInstance inst
         pure $ S.insert inst acc
       where
         cref = tyRefToFQClassName (modulename mn) cn
-        check = either (Left . BadInstance) pure . checkInstance
 
     goConstraint :: P.Constraint -> Either TypeClassError (Constraint Pat)
     goConstraint (P.Constraint cn arg si') = case ctable ^? ix cref of