Updated the tests, added an overlapping test. (Note: Conversion to monadic solve increased number of subgoals emitted upon failure. This does not seem to be a problem)

Author: gnumonik

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

@@ -1,6 +1,6 @@
 {-# LANGUAGE PatternSynonyms #-}
 
-module Test.TypeClassCheck (test) where
+module Test.TypeClassCheck {- (test) -} where
 
 import Control.Lens ((.~))
 import Data.Function ((&))
@@ -19,6 +19,7 @@ import LambdaBuffers.Compiler.TypeClass.Pat (
     RecP,
     RefP,
     SumP,
+    TyVarP,
     VarP,
     (:*),
     (:=)
@@ -31,7 +32,7 @@ import LambdaBuffers.Compiler.TypeClass.Rules (
   Rule ((:<=)),
  )
 import LambdaBuffers.Compiler.TypeClass.Rules qualified as R
-import LambdaBuffers.Compiler.TypeClass.Solve (solve)
+import LambdaBuffers.Compiler.TypeClass.Solve (Overlap (Overlap), solve)
 import LambdaBuffers.Compiler.TypeClassCheck (detectSuperclassCycles')
 import Proto.Compiler (ClassDef, Constraint, Kind, Kind'KindRef (Kind'KIND_REF_TYPE))
 import Proto.Compiler_Fields (argKind, argName, arguments, classArgs, className, classRef, kindRef, localClassRef, name, supers, tyVar, varName)
@@ -109,60 +110,77 @@ solveTests =
   testGroup
     "Solver tests"
     [ testCase "1: C [Maybe Int] (completeRules)" $
-        solveTest1 @?= []
+        solveTest1 @?= solved
     , testCase "2: D [Maybe Int] (partialRules)" $
-        solveTest2 @?= [dInt]
+        solveTest2 @?= Right [cListMaybeInt, cMaybeInt, dInt]
     , testCase "3: D [Maybe Int] (complete D, partial C)" $
-        solveTest3 @?= [cInt]
+        solveTest3 @?= Right [cInt]
     , testCase "4: C [[[Bool]]] (completeRules)" $
-        solveTest4 @?= []
+        solveTest4 @?= solved
     , testCase "5: C (Either (Either Int Bool) (Either Bool Int)) (completeRules)" $
-        solveTest5 @?= []
+        solveTest5 @?= solved
     , testCase "6: C (Either l x) (completeRules)" $
-        solveTest6 @?= [cL, cX]
+        solveTest6 @?= Right [cL, cX]
     , testCase "7: Sum test (completeRules)" $
-        solveTest7 @?= []
+        solveTest7 @?= solved
     , testCase "8: Sum test (partialRules)" $
-        solveTest8 @?= [cBool, cInt]
+        solveTest8 @?= Right [cBool, cInt]
     , testCase "9: Rec test (completeRules)" $
-        solveTest9 @?= []
+        solveTest9 @?= solved
     , testCase "10: Rec test (partialRules)" $
-        solveTest10 @?= [cBool, cInt]
+        solveTest10 @?= Right [cBool, cInt]
     , testCase "11: Prod test (completeRules)" $
-        solveTest11 @?= []
+        solveTest11 @?= solved
     , testCase "12: Prod test (partialRules)" $
-        solveTest12 @?= [cBool, cInt]
+        solveTest12 @?= Right [cBool, cInt]
     , testCase "13: Dec test (completeRules)" $
-        solveTest13 @?= []
+        solveTest13 @?= solved
     , testCase "14: Dec test (partialRules)" $
-        solveTest14 @?= [cBool, cInt]
+        solveTest14 @?= Right [cBool, cInt]
+    , testCase "15: Overlap test (specialrules)" $
+        solveTest15 @?= Left overlap
     ]
   where
+    solved :: Either Overlap [R.Constraint]
+    solved = Right []
+    cListMaybeInt = C _c (List (Maybe Int))
+    cMaybeInt = C _c (Maybe Int)
     cInt = C _c Int
     cBool = C _c Bool
-    cL = C _c _l
-    cX = C _c _x
+    cL = C _c vl
+    cX = C _c vr
     dInt = C _d Int
-
--- hardcoded variables, easier to read than (VarP "blah") everywhere
-_x, _xs, _vars, _name, _l, _body :: Pat
-_x = VarP "x"
-_xs = VarP "xs"
-_vars = VarP "vars"
-_name = VarP "name"
-_l = VarP "l"
-_body = VarP "body"
+    overlap =
+      Overlap
+        cMaybeInt
+        [ C _c (Maybe _X) :<= [C _c _X]
+        , C _c (Maybe Int) :<= []
+        ]
+
+-- hardcoded PATTERN variables, easier to read than (VarP "blah") everywhere
+_X, _XS, _VARS, _NAME, _L, _BODY :: Pat
+_X = VarP "x"
+_XS = VarP "xs"
+_VARS = VarP "vars"
+_NAME = VarP "name"
+_L = VarP "l"
+_BODY = VarP "body"
+
+-- hardcoded TYPE variables
+vl, vr :: Pat
+vl = TyVarP "l"
+vr = TyVarP "r"
 
 -- TODO(@gnumonik): Import this from somewhere else when that somewhere else module exists
 mkStructuralRules :: Class -> [Rule]
 mkStructuralRules c =
   [ C c Nil :<= []
-  , C c (_x :* _xs) :<= [C c _x, C c _xs]
-  , C c (_l := _x) :<= [C c _x]
-  , C c (RecP _xs) :<= [C c _xs]
-  , C c (ProdP _xs) :<= [C c _xs]
-  , C c (SumP _xs) :<= [C c _xs]
-  , C c (DecP _name _vars _body) :<= [C c _body]
+  , C c (_X :* _XS) :<= [C c _X, C c _XS]
+  , C c (_L := _X) :<= [C c _X]
+  , C c (RecP _XS) :<= [C c _XS]
+  , C c (ProdP _XS) :<= [C c _XS]
+  , C c (SumP _XS) :<= [C c _XS]
+  , C c (DecP _NAME _VARS _BODY) :<= [C c _BODY]
   ]
 
 pattern (:@) :: Pat -> Pat -> Pat
@@ -196,16 +214,16 @@ userRules1 :: Class -> [Rule]
 userRules1 c =
   [ NoConstraints c Int
   , NoConstraints c Bool
-  , C c (Maybe _x) :<= [C c _x]
-  , C c (Either _l _x) :<= [C c _l, C c _x]
-  , C c (List _x) :<= [C c _x]
+  , C c (Maybe _X) :<= [C c _X]
+  , C c (Either _L _X) :<= [C c _L, C c _X]
+  , C c (List _X) :<= [C c _X]
   ]
 
 userRules2 :: Class -> [Rule]
 userRules2 c =
-  [ C c (Maybe _x) :<= [C c _x]
-  , C c (Either _l _x) :<= [C c _l, C c _x]
-  , C c (List _x) :<= [C c _x]
+  [ C c (Maybe _X) :<= [C c _X]
+  , C c (Either _L _X) :<= [C c _L, C c _X]
+  , C c (List _X) :<= [C c _X]
   ]
 
 completeRules :: Class -> [Rule]
@@ -223,49 +241,48 @@ _d :: Class
 _d = Class (FQClassName "D" []) [_c]
 
 -- C [Maybe Int] w/ complete rules (expected: [])
-solveTest1 :: [R.Constraint]
+solveTest1 :: Either Overlap [R.Constraint]
 solveTest1 = solve (completeRules _c) (C _c $ List (Maybe Int))
 
--- D [Maybe Int] w/ incomplete rules (expected: [D Int])
-solveTest2 :: [R.Constraint]
+-- D [Maybe Int] w/ incomplete rules (expected: [C [Maybe Int], C (Maybe Int), D Int])
+solveTest2 :: Either Overlap [R.Constraint]
 solveTest2 = solve (partialRules _d) (C _d $ List (Maybe Int))
 
 -- D [Maybe Int] w/ complete D rules & incomplete C rules (expected: [C Int])
-solveTest3 :: [R.Constraint]
+solveTest3 :: Either Overlap [R.Constraint]
 solveTest3 = solve rules (C _d $ List (Maybe Int))
   where
     rules = completeRules _d <> partialRules _c
 
 -- C [[[Bool]]] w/ complete rules (expected: [])
-solveTest4 :: [R.Constraint]
+solveTest4 :: Either Overlap [R.Constraint]
 solveTest4 = solve (completeRules _c) $ C _c $ List (List (List Bool))
 
 -- C (Either (Either Int Bool) (Either Bool Int)) w/ complete rules (expected: [])
-solveTest5 :: [R.Constraint]
+solveTest5 :: Either Overlap [R.Constraint]
 solveTest5 = solve (completeRules _c) $ C _c $ Either (Either Int Bool) (Either Bool Int)
 
 -- NOTE(@bladyjoker): This one shows that we never need to "freshen" variables
---                    (if you study it you might also see why we never need to bind them)
 -- C (Either l x) w/ complete rules (expected: [C l, C x])
-solveTest6 :: [R.Constraint]
-solveTest6 = solve (completeRules _c) $ C _c $ Either _l _x
+solveTest6 :: Either Overlap [R.Constraint]
+solveTest6 = solve (completeRules _c) $ C _c $ Either vl vr
 
 -- tests for structural subcomponents of types. Can't write Haskell equivalents (w/o row-types)
 
 -- expected: []
-solveTest7 :: [R.Constraint]
+solveTest7 :: Either Overlap [R.Constraint]
 solveTest7 = solve (completeRules _c) $ C _c sumBody
   where
     sumBody = SumP $ Labeled "Ctor1" Int :* Labeled "Ctor2" (List Bool) :* Nil
 
 -- expected [C Bool, C Int]
-solveTest8 :: [R.Constraint]
+solveTest8 :: Either Overlap [R.Constraint]
 solveTest8 = solve (partialRules _c) $ C _c sumBody
   where
     sumBody = SumP $ Labeled "Ctor1" Int :* Labeled "Ctor2" (List Bool) :* Nil
 
 -- expected []
-solveTest9 :: [R.Constraint]
+solveTest9 :: Either Overlap [R.Constraint]
 solveTest9 = solve (completeRules _c) $ C _c recBody
   where
     recBody =
@@ -275,7 +292,7 @@ solveTest9 = solve (completeRules _c) $ C _c recBody
           :* Nil
 
 -- expected [C Bool, C Int]
-solveTest10 :: [R.Constraint]
+solveTest10 :: Either Overlap [R.Constraint]
 solveTest10 = solve (partialRules _c) $ C _c recBody
   where
     recBody =
@@ -285,19 +302,19 @@ solveTest10 = solve (partialRules _c) $ C _c recBody
           :* Nil
 
 -- expected []
-solveTest11 :: [R.Constraint]
+solveTest11 :: Either Overlap [R.Constraint]
 solveTest11 = solve (completeRules _c) $ C _c prodBody
   where
     prodBody = ProdP $ List Bool :* Either Int Bool :* Nil
 
 -- expected [C Bool, C Int]
-solveTest12 :: [R.Constraint]
+solveTest12 :: Either Overlap [R.Constraint]
 solveTest12 = solve (partialRules _c) $ C _c prodBody
   where
     prodBody = ProdP $ List Bool :* Either Int Bool :* Nil
 
 -- expected []
-solveTest13 :: [R.Constraint]
+solveTest13 :: Either Overlap [R.Constraint]
 solveTest13 = solve (completeRules _c) $ C _c testDec
   where
     testDec =
@@ -308,7 +325,7 @@ solveTest13 = solve (completeRules _c) $ C _c testDec
             :* Nil
 
 -- expected [C Int, C Bool]
-solveTest14 :: [R.Constraint]
+solveTest14 :: Either Overlap [R.Constraint]
 solveTest14 = solve (partialRules _c) $ C _c testDec
   where
     testDec =
@@ -317,3 +334,14 @@ solveTest14 = solve (partialRules _c) $ C _c testDec
           Labeled "Ctor1" (ProdP $ Maybe Int :* Nil)
             :* Labeled "Ctor2" (RecP $ Labeled "field1" Bool :* Nil)
             :* Nil
+
+-- expected overlap
+solveTest15 :: Either Overlap [R.Constraint]
+solveTest15 = solve cOverlapRules (C _c $ List (Maybe Int))
+  where
+    cOverlapRules =
+      [ C _c (Maybe _X) :<= [C _c _X]
+      , C _c (Maybe Int) :<= []
+      , C _c Int :<= []
+      , C _c (List _X) :<= [C _c _X]
+      ]