Compiler: additional Tests

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

@@ -225,9 +225,17 @@ derive x = deriveTyAbs x
 
     deriveTyApp :: PC.TyApp -> Derive Derivation
     deriveTyApp ap = do
-      f <- deriveTy (ap ^. #tyFunc)
-      args <- deriveTy `traverse` (ap ^. #tyArgs)
-      applyDerivation f args
+      c <- ask
+      df <- deriveTy (ap ^. #tyFunc)
+      foldrM
+        ( \arg df' -> do
+            darg <- deriveTy arg
+            v <- KVar <$> fresh
+            tell [Constraint ((darg ^. d'kind) :->: v, df' ^. d'kind)]
+            return $ Application (Judgement c (App (df' ^. d'type) (darg ^. d'type)) v) df' darg
+        )
+        df
+        (ap ^. #tyArgs)
 
     deriveTuple :: PC.Tuple -> Derive Derivation
     deriveTuple t = do
@@ -257,16 +265,6 @@ derive x = deriveTyAbs x
       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
-
 {- | Gets the binding from the context - if the variable is not bound throw an
  error.
 -}

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

@@ -17,6 +17,9 @@ import Test.Utils.CompilerInput (
   compilerInput'either,
   compilerInput'incoherent,
   compilerInput'maybe,
+  compilerInput'newTypeEither,
+  compilerInput'newTypeEither',
+  compilerInput'newTypeEither'',
   compilerInput'recDef,
  )
 import Test.Utils.Constructors (_CompilerInput)
@@ -46,6 +49,9 @@ testCheck =
     , kcTestEither
     , kcTestMaybe'n'Either
     , kcTestRec
+    , kcWrappedTestEither
+    , kcWrappedTestEither'
+    , kcWrappedTestEither''
     ]
 
 trivialKCTest :: TestTree
@@ -63,6 +69,21 @@ kcTestEither =
   testCase "Kind check Either." $
     check_ compilerInput'either @?= Right ()
 
+kcWrappedTestEither :: TestTree
+kcWrappedTestEither =
+  testCase "Kind check Either + Wrapped Either." $
+    check_ compilerInput'newTypeEither @?= Right ()
+
+kcWrappedTestEither' :: TestTree
+kcWrappedTestEither' =
+  testCase "Kind check Either (defined Opaque) + Wrapped Either." $
+    check_ compilerInput'newTypeEither' @?= Right ()
+
+kcWrappedTestEither'' :: TestTree
+kcWrappedTestEither'' =
+  testCase "Kind check Either + Wrapped (Either Int Int) ." $
+    check_ compilerInput'newTypeEither'' @?= Right ()
+
 kcTestMaybe'n'Either :: TestTree
 kcTestMaybe'n'Either =
   testCase "Kind check Maybe and Either." $

lambda-buffers-compiler/test/Test/Utils/CompilerInput.hs

@@ -6,6 +6,9 @@ module Test.Utils.CompilerInput (
   compilerInput'either,
   compilerInput'undefinedForeignTyRef,
   compilerInput'recDef,
+  compilerInput'newTypeEither,
+  compilerInput'newTypeEither',
+  compilerInput'newTypeEither'',
 ) where
 
 import LambdaBuffers.Compiler.ProtoCompat qualified as P
@@ -14,6 +17,9 @@ import Test.Utils.Module (
   module'either,
   module'incoherent,
   module'maybe,
+  module'newTypeEither,
+  module'newTypeEither',
+  module'newTypeEither'',
   module'recDef,
   module'undefinedForeignTyRef,
   module'undefinedLocalTyRef,
@@ -28,6 +34,15 @@ compilerInput'maybe = _CompilerInput [module'maybe]
 compilerInput'either :: P.CompilerInput
 compilerInput'either = _CompilerInput [module'either]
 
+compilerInput'newTypeEither :: P.CompilerInput
+compilerInput'newTypeEither = _CompilerInput [module'newTypeEither]
+
+compilerInput'newTypeEither' :: P.CompilerInput
+compilerInput'newTypeEither' = _CompilerInput [module'newTypeEither']
+
+compilerInput'newTypeEither'' :: P.CompilerInput
+compilerInput'newTypeEither'' = _CompilerInput [module'newTypeEither'']
+
 -- | Compiler Input containing 1 module with 1 definition - Either.
 compilerInput'recDef :: P.CompilerInput
 compilerInput'recDef = _CompilerInput [module'recDef]

lambda-buffers-compiler/test/Test/Utils/Constructors.hs

@@ -23,6 +23,8 @@ module Test.Utils.Constructors (
   _LocalRef',
   _ForeignRef',
   _TyApp,
+  _Opaque,
+  _TyAbs',
 ) where
 
 import Control.Lens ((^.))
@@ -99,6 +101,9 @@ _TupleI x =
       , PC.sourceInfo = def
       }
 
+_Opaque :: PC.TyBody
+_Opaque = PC.OpaqueI def
+
 _Constructor :: Text -> PC.Product -> PC.Constructor
 _Constructor c f =
   PC.Constructor
@@ -138,6 +143,14 @@ _TyAbs args body =
     , sourceInfo = def
     }
 
+_TyAbs' :: [(Text, PC.KindType)] -> PC.TyBody -> PC.TyAbs
+_TyAbs' args body =
+  PC.TyAbs
+    { PC.tyArgs = OMap.fromList [(PC.mkInfoLess $ ta ^. #argName, ta) | ta <- _TyArg <$> args]
+    , PC.tyBody = body
+    , sourceInfo = def
+    }
+
 _TyArg :: (Text, PC.KindType) -> PC.TyArg
 _TyArg (a, k) =
   PC.TyArg

lambda-buffers-compiler/test/Test/Utils/Module.hs

@@ -6,14 +6,21 @@ module Test.Utils.Module (
   module'undefinedForeignTyRef,
   module'either,
   module'recDef,
+  module'newTypeEither,
+  module'newTypeEither',
+  module'newTypeEither'',
 ) where
 
 import LambdaBuffers.Compiler.ProtoCompat qualified as P
 import Test.Utils.Constructors (_Module, _ModuleName)
 import Test.Utils.TyDef (
+  tyDef'Int,
   tyDef'either,
+  tyDef'either'opaque,
   tyDef'incoherent,
   tyDef'maybe,
+  tyDef'ntEither,
+  tyDef'ntEither'saturated,
   tyDef'recDef,
   tyDef'undefinedForeignTyRef,
   tyDef'undefinedLocalTyRef,
@@ -28,6 +35,15 @@ module'maybe = _Module (_ModuleName ["Prelude"]) [tyDef'maybe] mempty mempty
 module'either :: P.Module
 module'either = _Module (_ModuleName ["Prelude"]) [tyDef'either] mempty mempty
 
+module'newTypeEither :: P.Module
+module'newTypeEither = _Module (_ModuleName ["Prelude"]) [tyDef'either, tyDef'ntEither] mempty mempty
+
+module'newTypeEither' :: P.Module
+module'newTypeEither' = _Module (_ModuleName ["Prelude"]) [tyDef'either'opaque, tyDef'ntEither] mempty mempty
+
+module'newTypeEither'' :: P.Module
+module'newTypeEither'' = _Module (_ModuleName ["Prelude"]) [tyDef'either'opaque, tyDef'Int, tyDef'ntEither'saturated] mempty mempty
+
 module'recDef :: P.Module
 module'recDef = _Module (_ModuleName ["Prelude"]) [tyDef'recDef] mempty mempty
 

lambda-buffers-compiler/test/Test/Utils/TyDef.hs

@@ -9,6 +9,10 @@ module Test.Utils.TyDef (
   tyDef'undefinedForeignTyRef'TyRef,
   tyDef'recDef,
   tyDef'either,
+  tyDef'ntEither,
+  tyDef'either'opaque,
+  tyDef'Int,
+  tyDef'ntEither'saturated,
 ) where
 
 import LambdaBuffers.Compiler.ProtoCompat.Types (Ty (TyVarI))
@@ -17,9 +21,11 @@ import Test.Utils.Constructors (
   _ForeignRef',
   _LocalRef',
   _ModuleName,
+  _Opaque,
   _SourceInfo,
   _TupleI,
   _TyAbs,
+  _TyAbs',
   _TyApp,
   _TyDef,
   _TyName,
@@ -41,6 +47,17 @@ tyDef'maybe =
         ]
     )
 
+tyDef'either'opaque :: P.TyDef
+tyDef'either'opaque =
+  _TyDef
+    (_TyName "Either")
+    ( _TyAbs'
+        [ ("a", _Type)
+        , ("b", _Type)
+        ]
+        _Opaque
+    )
+
 tyDef'either :: P.TyDef
 tyDef'either =
   _TyDef
@@ -54,6 +71,41 @@ tyDef'either =
         ]
     )
 
+tyDef'Int :: P.TyDef
+tyDef'Int = _TyDef (_TyName "Int") (_TyAbs' mempty _Opaque)
+
+tyDef'ntEither'saturated :: P.TyDef
+tyDef'ntEither'saturated =
+  _TyDef
+    (_TyName "WrapEither")
+    ( _TyAbs
+        mempty
+        [
+          ( "Foo"
+          , _TupleI
+              [ _TyApp
+                  ( _TyApp
+                      (_TyRefILocal "Either")
+                      (_TyRefILocal "Int")
+                  )
+                  (_TyRefILocal "Int")
+              ]
+          )
+        ]
+    )
+
+tyDef'ntEither :: P.TyDef
+tyDef'ntEither =
+  _TyDef
+    (_TyName "WrapEither")
+    ( _TyAbs
+        [ ("a", _Type)
+        , ("b", _Type)
+        ]
+        [ ("Foo", _TupleI [_TyApp (_TyApp (_TyRefILocal "Either") (_TyVarI "a")) (_TyVarI "b")])
+        ]
+    )
+
 -- data F a = Rec F (F a)
 tyDef'recDef :: P.TyDef
 tyDef'recDef =