Update to GEB version 0.3.2 (#2244)

GEB 0.3.2 introduces the following changes.
* The STLC frontend no longer requires full type information in terms.
The syntax of the terms changed.
* An error node has been introduced which allows to compile Juvix `fail`
nodes.

The following features required for compilation from Juvix are still
missing in GEB.
* Modular arithmetic types ([GEB issue
#61](anoma/geb#61)).
* Functor/algebra iteration to implement bounded inductive types ([GEB
issue #62](anoma/geb#62)).

app/Commands/Dev/Geb/Check.hs

@@ -3,7 +3,7 @@ module Commands.Dev.Geb.Check where
 import Commands.Base
 import Commands.Dev.Geb.Infer.Options
 import Juvix.Compiler.Backend.Geb qualified as Geb
-import Juvix.Compiler.Backend.Geb.Analysis.TypeChecking.Error
+import Juvix.Compiler.Backend.Geb.Pretty
 
 runCommand ::
   forall r.
@@ -16,9 +16,11 @@ runCommand opts = do
   f :: Path Abs File <- fromAppPathFile b
   content :: Text <- embed (readFile (toFilePath f))
   case Geb.runParser f content of
-    Right (Geb.ExpressionTypedMorphism tyMorph) -> do
-      case run . runError @CheckingError $ (Geb.check' tyMorph) of
+    Right (Geb.ExpressionMorphism morph) -> do
+      case Geb.inferObject' morph of
         Left err -> exitJuvixError (JuvixError err)
-        Right _ -> renderStdOut ("Well done! It typechecks\n" :: Text)
-    Right _ -> exitJuvixError (error @JuvixError "Not a typed morphism")
+        Right ty -> do
+          renderStdOut (ppOutDefault ty)
+          embed (putStrLn "")
+    Right _ -> exitJuvixError (error @JuvixError "Not a morphism")
     Left err -> exitJuvixError (JuvixError err)

src/Juvix/Compiler/Backend/Geb/Analysis/TypeChecking/Checker.hs

@@ -19,13 +19,16 @@ check :: Members '[Reader CheckingEnv, Error CheckingError] r => Morphism -> Obj
 check morph obj' = do
   ctx <- ask @CheckingEnv
   obj <- runReader ctx (inferObject morph)
+  checkTypesEqual obj obj'
+
+checkTypesEqual :: Members '[Reader CheckingEnv, Error CheckingError] r => Object -> Object -> Sem r ()
+checkTypesEqual obj obj' =
   unless
     (obj == obj')
     ( throw $
         CheckingErrorTypeMismatch
           TypeMismatch
-            { _typeMismatchMorphism = morph,
-              _typeMismatchExpected = obj,
+            { _typeMismatchExpected = obj,
               _typeMismatchActual = obj'
             }
     )
@@ -69,23 +72,28 @@ inferObjectAbsurd x = do
 
 inferObjectApplication :: InferEffects r => Application -> Sem r Object
 inferObjectApplication app = do
-  let lType = app ^. applicationDomainType
-      rType = app ^. applicationCodomainType
-      homTy =
-        ObjectHom $
-          Hom {_homDomain = lType, _homCodomain = rType}
-  check (app ^. applicationLeft) homTy
-  check (app ^. applicationRight) lType
-  return rType
+  homTy <- inferObject (app ^. applicationLeft)
+  lType <- inferObject (app ^. applicationRight)
+  case homTy of
+    ObjectHom Hom {..} -> do
+      checkTypesEqual _homDomain lType
+      return _homCodomain
+    _ ->
+      throw $
+        CheckingErrorExpectedType
+          ExpectedType
+            { _expectedTypeObject = homTy,
+              _expectedTypeKind = "hom object"
+            }
 
 inferObjectLambda :: InferEffects r => Lambda -> Sem r Object
 inferObjectLambda l = do
   let aType = l ^. lambdaVarType
-      bType = l ^. lambdaBodyType
   ctx <- ask @CheckingEnv
-  local
-    (const (Context.cons aType ctx))
-    (check (l ^. lambdaBody) bType)
+  bType <-
+    local
+      (const (Context.cons aType ctx))
+      (inferObject (l ^. lambdaBody))
   return $
     ObjectHom $
       Hom
@@ -95,10 +103,8 @@ inferObjectLambda l = do
 
 inferObjectPair :: InferEffects r => Pair -> Sem r Object
 inferObjectPair pair = do
-  let lType = pair ^. pairLeftType
-      rType = pair ^. pairRightType
-  check (pair ^. pairLeft) lType
-  check (pair ^. pairRight) rType
+  lType <- inferObject (pair ^. pairLeft)
+  rType <- inferObject (pair ^. pairRight)
   return $
     ObjectProduct
       Product
@@ -108,57 +114,55 @@ inferObjectPair pair = do
 
 inferObjectCase :: InferEffects r => Case -> Sem r Object
 inferObjectCase c = do
-  let aType = c ^. caseLeftType
-      bType = c ^. caseRightType
-      vType =
-        ObjectCoproduct $
-          Coproduct
-            { _coproductLeft = aType,
-              _coproductRight = bType
-            }
-      cType = c ^. caseCodomainType
-      leftType =
-        ObjectHom $
-          Hom
-            { _homDomain = aType,
-              _homCodomain = cType
-            }
-      rightType =
-        ObjectHom $
-          Hom
-            { _homDomain = bType,
-              _homCodomain = cType
+  vType <- inferObject (c ^. caseOn)
+  case vType of
+    ObjectCoproduct Coproduct {..} -> do
+      ctx <- ask @CheckingEnv
+      leftType <-
+        local
+          (const (Context.cons _coproductLeft ctx))
+          (inferObject (c ^. caseLeft))
+      rightType <-
+        local
+          (const (Context.cons _coproductRight ctx))
+          (inferObject (c ^. caseRight))
+      checkTypesEqual leftType rightType
+      return leftType
+    _ ->
+      throw $
+        CheckingErrorExpectedType
+          ExpectedType
+            { _expectedTypeObject = vType,
+              _expectedTypeKind = "coproduct"
             }
-  check (c ^. caseOn) vType
-  check (c ^. caseLeft) leftType
-  check (c ^. caseRight) rightType
-  return cType
 
 inferObjectFirst :: InferEffects r => First -> Sem r Object
 inferObjectFirst p = do
-  let leftType = p ^. firstLeftType
-      rightType = p ^. firstRightType
-      pairType =
-        ObjectProduct $
-          Product
-            { _productLeft = leftType,
-              _productRight = rightType
+  pairType <- inferObject (p ^. firstValue)
+  case pairType of
+    ObjectProduct Product {..} ->
+      return _productLeft
+    _ ->
+      throw $
+        CheckingErrorExpectedType
+          ExpectedType
+            { _expectedTypeObject = pairType,
+              _expectedTypeKind = "product"
             }
-  check (p ^. firstValue) pairType
-  return leftType
 
 inferObjectSecond :: InferEffects r => Second -> Sem r Object
 inferObjectSecond p = do
-  let leftType = p ^. secondLeftType
-      rightType = p ^. secondRightType
-      pairType =
-        ObjectProduct $
-          Product
-            { _productLeft = leftType,
-              _productRight = rightType
+  pairType <- inferObject (p ^. secondValue)
+  case pairType of
+    ObjectProduct Product {..} ->
+      return _productRight
+    _ ->
+      throw $
+        CheckingErrorExpectedType
+          ExpectedType
+            { _expectedTypeObject = pairType,
+              _expectedTypeKind = "product"
             }
-  check (p ^. secondValue) pairType
-  return rightType
 
 inferObjectVar :: InferEffects r => Var -> Sem r Object
 inferObjectVar v = do
@@ -197,20 +201,20 @@ inferObjectBinop opApp = do
 
 inferObjectLeft :: InferEffects r => LeftInj -> Sem r Object
 inferObjectLeft LeftInj {..} = do
-  check _leftInjValue _leftInjLeftType
+  lType <- inferObject _leftInjValue
   return $
     ObjectCoproduct $
       Coproduct
-        { _coproductLeft = _leftInjLeftType,
+        { _coproductLeft = lType,
           _coproductRight = _leftInjRightType
         }
 
 inferObjectRight :: InferEffects r => RightInj -> Sem r Object
 inferObjectRight RightInj {..} = do
-  check _rightInjValue _rightInjRightType
+  rType <- inferObject _rightInjValue
   return $
     ObjectCoproduct $
       Coproduct
         { _coproductLeft = _rightInjLeftType,
-          _coproductRight = _rightInjRightType
+          _coproductRight = rType
         }

src/Juvix/Compiler/Backend/Geb/Analysis/TypeChecking/Error.hs

@@ -6,14 +6,20 @@ import Juvix.Compiler.Backend.Geb.Pretty
 -- | Errors that can occur during type checking / inference
 data CheckingError
   = CheckingErrorTypeMismatch TypeMismatch
+  | CheckingErrorExpectedType ExpectedType
   | CheckingErrorLackOfInformation LackOfInformation
   | CheckingErrorWrongObject WrongObject
   deriving stock (Show, Eq)
 
 data TypeMismatch = TypeMismatch
   { _typeMismatchExpected :: Object,
-    _typeMismatchActual :: Object,
-    _typeMismatchMorphism :: Morphism
+    _typeMismatchActual :: Object
+  }
+  deriving stock (Show, Eq)
+
+data ExpectedType = ExpectedType
+  { _expectedTypeObject :: Object,
+    _expectedTypeKind :: Text
   }
   deriving stock (Show, Eq)
 
@@ -33,6 +39,7 @@ data WrongObject = WrongObject
   deriving stock (Show, Eq)
 
 makeLenses ''TypeMismatch
+makeLenses ''ExpectedType
 makeLenses ''LackOfInformation
 makeLenses ''WrongObject
 
@@ -48,18 +55,36 @@ instance ToGenericError TypeMismatch where
             }
         where
           opts' = fromGenericOptions opts
-          morph = e ^. typeMismatchMorphism
           expected = e ^. typeMismatchExpected
           actual = e ^. typeMismatchActual
           msg =
-            ppCode' opts' morph
-              <+> "has object:"
-                <> line
-                <> ppCode' opts' actual
-                <> line
-                <> "but is expected to have as object:"
-                <> line
-                <> ppCode' opts' expected
+            "Object:"
+              <> line
+              <> ppCode' opts' actual
+              <> line
+              <> "is expected to be equal to:"
+              <> line
+              <> ppCode' opts' expected
+
+instance ToGenericError ExpectedType where
+  genericError e = ask >>= generr
+    where
+      generr opts =
+        return
+          GenericError
+            { _genericErrorLoc = defaultLoc,
+              _genericErrorMessage = ppOutput msg,
+              _genericErrorIntervals = [defaultLoc]
+            }
+        where
+          opts' = fromGenericOptions opts
+          expected = e ^. expectedTypeObject
+          msg =
+            "Expected "
+              <> pretty (e ^. expectedTypeKind)
+              <> ", got:"
+              <> line
+              <> ppCode' opts' expected
 
 instance ToGenericError LackOfInformation where
   genericError e = ask >>= generr
@@ -130,6 +155,7 @@ instance ToGenericError WrongObject where
 instance ToGenericError CheckingError where
   genericError = \case
     CheckingErrorTypeMismatch e -> genericError e
+    CheckingErrorExpectedType e -> genericError e
     CheckingErrorLackOfInformation e -> genericError e
     CheckingErrorWrongObject e -> genericError e