Cleaned up PR in accordance w/ Drazen's comments (minus module renaming, doing that last)

Author: gnumonik

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

@@ -71,8 +71,6 @@ data Pat
     DecP Pat Pat Pat
   deriving stock (Show, Eq, Ord)
 
--- infixr 5 :*
-
 {- Utility functions. Turn a list of types into a product/record/sum type.
 -}
 toProdP :: [Pat] -> Pat
@@ -166,13 +164,6 @@ expList = \case
   p1 `ConsE` p2 -> (p1 :) <$> expList p2
   _ -> Nothing
 
-{- This is used as a predicate to filter instances or Gens which are structurally compatible
-   with the argument type.
-   The first argument is the inner Pat from an instance head or Gen.
-   The second argument is the Pat representation of a type that we want to derive an instance / generate code for.
-   NOTE: Is not bidirectional! The first Pat has to be more general than the first
-         (more specifically: The second Pat should be a substitution instance of the first)
--}
 matches :: Pat -> Exp -> Bool
 matches (LitP l1) (LitE l2) = l1 == l2
 matches (VarP _) _ = True

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

@@ -44,16 +44,13 @@ inst = subV M.empty
    are replaced in the instance superclasses as well (if they occur there).
 -}
 subst :: Rule Pat -> Exp -> Rule Exp
-subst cst@(C _ t :<= _) ty = fmap (go (getSubs t ty)) cst
-  where
-    go :: [(Text, Exp)] -> Pat -> Exp
-    go subs = subV (M.fromList subs)
+subst cst@(C _ t :<= _) ty = fmap (subV (getSubs t ty)) cst
 
 {- Given two patterns (which are hopefully structurally similar), gather a list of all substitutions
    from the PatVars in the first argument to the concrete types (hopefully!) in the second argument
 -}
-getSubs :: Pat -> Exp -> [(Text, Exp)] -- should be a set, whatever
-getSubs (VarP s) t = [(s, t)]
+getSubs :: Pat -> Exp -> M.Map Text Exp -- should be a set, whatever
+getSubs (VarP s) t = M.fromList [(s, t)]
 getSubs (ConsP x xs) (ConsE x' xs') = getSubs x x' <> getSubs xs xs'
 getSubs (LabelP l t) (LabelE l' t') = getSubs l l' <> getSubs t t'
 getSubs (ProdP xs) (ProdE xs') = getSubs xs xs'
@@ -62,22 +59,23 @@ getSubs (SumP xs) (SumE xs') = getSubs xs xs'
 getSubs (AppP t1 t2) (AppE t1' t2') = getSubs t1 t1' <> getSubs t2 t2'
 getSubs (RefP n t) (RefE n' t') = getSubs n n' <> getSubs t t'
 getSubs (DecP a b c) (DecE a' b' c') = getSubs a a' <> getSubs b b' <> getSubs c c'
-getSubs _ _ = []
+getSubs _ _ = M.empty
 
 -- NoMatch isn't fatal but OverlappingMatches is (i.e. we need to stop when we encounter it)
-data MatchError
+data MatchResult
   = NoMatch
   | OverlappingMatches [Rule Pat]
+  | MatchFound (Rule Pat)
 
 -- for SolveM, since we catch NoMatch
 data Overlap = Overlap (Constraint Exp) [Rule Pat]
   deriving stock (Show, Eq)
 
-selectMatchingInstance :: Exp -> Class -> [Rule Pat] -> Either MatchError (Rule Pat)
+selectMatchingInstance :: Exp -> Class -> [Rule Pat] -> MatchResult
 selectMatchingInstance e c rs = case filter matchPatAndClass rs of
-  [] -> Left NoMatch
-  [r] -> Right r
-  overlaps -> Left $ OverlappingMatches overlaps
+  [] -> NoMatch
+  [r] -> MatchFound r
+  overlaps -> OverlappingMatches overlaps
   where
     matchPatAndClass :: Rule Pat -> Bool
     matchPatAndClass r =
@@ -103,10 +101,9 @@ solveM (C _ (LitE (TyVar _))) = pure ()
 solveM cst@(C c pat) =
   ask >>= \inScope ->
     case selectMatchingInstance pat c inScope of
-      Left e -> case e of
-        NoMatch -> tell $ S.singleton cst
-        OverlappingMatches olps -> throwError $ Overlap cst olps
-      Right rule -> case subst rule pat of
+      NoMatch -> tell $ S.singleton cst
+      OverlappingMatches olps -> throwError $ Overlap cst olps
+      MatchFound rule -> case subst rule pat of
         C _ p :<= [] -> solveClassesFor p (csupers c)
         C _ _ :<= is -> do
           traverse_ solveM is

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

@@ -79,7 +79,7 @@ data TypeClassError
   | ClassNotFoundInModule Text [Text]
   | LocalTyRefNotFound T.Text P.ModuleName
   | SuperclassCycleDetected [[FQClassName]]
-  | CouldntSolveConstraints P.ModuleName [Constraint Exp] Instance
+  | FailedToSolveConstraints P.ModuleName [Constraint Exp] Instance
   | MalformedTyDef P.ModuleName Exp
   | BadInstance BasicConditionViolation
   deriving stock (Show, Eq, Generic)
@@ -114,7 +114,7 @@ instance Pretty TypeClassError where
               . map (hcat . punctuate " => " . map pretty)
               $ crs
           )
-    CouldntSolveConstraints mn cs i ->
+    FailedToSolveConstraints mn cs i ->
       "Error: Could not derive instance:"
         <+> pointies (pretty i)
           <> line

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

@@ -64,8 +64,14 @@ constraintClass (C c _) = c
 --       half of Haskell's orphan instances rule. We could relax that in various ways
 --       but it would require reworking a lot of the utilities above.
 checkDerive :: P.ModuleName -> ModuleBuilder -> Rule Pat -> Either TypeClassError [Constraint Exp]
-checkDerive mn mb i = concat <$> (traverse solveRef =<< catchOverlap (solve assumptions c))
+checkDerive mn mb i = concat <$> secondPass
   where
+    secondPass :: Either TypeClassError [[Constraint Exp]]
+    secondPass = traverse solveRef =<< firstPass
+
+    firstPass :: Either TypeClassError [Constraint Exp]
+    firstPass = catchOverlap (solve assumptions c)
+
     catchOverlap :: Either Overlap a -> Either TypeClassError a
     catchOverlap = either (Left . BadInstance . OverlapDetected) pure
 

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

@@ -23,7 +23,7 @@ import LambdaBuffers.Compiler.TypeClass.Pretty (spaced, (<//>))
 import LambdaBuffers.Compiler.TypeClass.Utils (
   Instance,
   ModuleBuilder (mbInstances),
-  TypeClassError (CouldntSolveConstraints),
+  TypeClassError (FailedToSolveConstraints),
   checkInstance,
   mkBuilders,
  )
@@ -89,7 +89,7 @@ runDeriveCheck mn mb = mconcat <$> traverse go (S.toList $ mbInstances mb)
         >> checkDerive mn mb i
         >>= \case
           [] -> pure ()
-          xs -> Left $ CouldntSolveConstraints mn xs i
+          xs -> Left $ FailedToSolveConstraints mn xs i
 
 -- ModuleBuilder is suitable codegen input,
 -- and is (relatively) computationally expensive to