Add IsInstanceCoercion to Internal

src/Juvix/Compiler/Internal/Data/InfoTable.hs

@@ -37,8 +37,7 @@ functionInfoFromFunctionDef isLocal FunctionDef {..} =
       _functionInfoType = _funDefType,
       _functionInfoArgsInfo = _funDefArgsInfo,
       _functionInfoBuiltin = _funDefBuiltin,
-      _functionInfoCoercion = _funDefCoercion,
-      _functionInfoInstance = _funDefInstance,
+      _functionInfoIsInstanceCoercion = _funDefIsInstanceCoercion,
       _functionInfoTerminating = _funDefTerminating,
       _functionInfoPragmas = _funDefPragmas,
       _functionInfoIsLocal = isLocal

src/Juvix/Compiler/Internal/Extra.hs

@@ -121,8 +121,10 @@ genFieldProjection kind _funDefName _funDefBuiltin mpragmas info fieldIx = do
   cloneFunctionDefSameName
     FunctionDef
       { _funDefTerminating = False,
-        _funDefInstance = False,
-        _funDefCoercion = kind == ProjectionCoercion,
+        _funDefIsInstanceCoercion =
+          if
+              | kind == ProjectionCoercion -> Just IsInstanceCoercionCoercion
+              | otherwise -> Nothing,
         _funDefArgsInfo = mempty,
         _funDefPragmas =
           maybe

src/Juvix/Compiler/Internal/Extra/Base.hs

@@ -227,8 +227,7 @@ instance HasExpressions FunctionDef where
           _funDefType = ty',
           _funDefArgsInfo = infos',
           _funDefTerminating,
-          _funDefInstance,
-          _funDefCoercion,
+          _funDefIsInstanceCoercion,
           _funDefName,
           _funDefBuiltin,
           _funDefPragmas,
@@ -801,8 +800,7 @@ simpleFunDef funName ty body =
   FunctionDef
     { _funDefName = funName,
       _funDefType = ty,
-      _funDefCoercion = False,
-      _funDefInstance = False,
+      _funDefIsInstanceCoercion = Nothing,
       _funDefPragmas = mempty,
       _funDefArgsInfo = mempty,
       _funDefTerminating = False,

src/Juvix/Compiler/Internal/Extra/Clonable.hs

@@ -261,8 +261,7 @@ instance Clonable FunctionDef where
             _funDefBody = body',
             _funDefArgsInfo = defaultSig',
             _funDefTerminating,
-            _funDefInstance,
-            _funDefCoercion,
+            _funDefIsInstanceCoercion,
             _funDefBuiltin,
             _funDefPragmas,
             _funDefDocComment

src/Juvix/Compiler/Internal/Language.hs

@@ -94,13 +94,23 @@ instance Serialize AxiomDef
 
 instance NFData AxiomDef
 
+data IsInstanceCoercion
+  = IsInstanceCoercionInstance
+  | IsInstanceCoercionCoercion
+  deriving stock (Eq, Generic, Data)
+
+instance Hashable IsInstanceCoercion
+
+instance Serialize IsInstanceCoercion
+
+instance NFData IsInstanceCoercion
+
 data FunctionDef = FunctionDef
   { _funDefName :: FunctionName,
     _funDefType :: Expression,
     _funDefBody :: Expression,
     _funDefTerminating :: Bool,
-    _funDefInstance :: Bool,
-    _funDefCoercion :: Bool,
+    _funDefIsInstanceCoercion :: Maybe IsInstanceCoercion,
     _funDefBuiltin :: Maybe BuiltinFunction,
     _funDefArgsInfo :: [ArgInfo],
     _funDefPragmas :: Pragmas,

src/Juvix/Compiler/Internal/Pretty/Base.hs

@@ -14,6 +14,7 @@ import Juvix.Compiler.Internal.Pretty.Options
 import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.TypeChecking.CheckerNew.Arity qualified as New
 import Juvix.Compiler.Store.Internal.Data.InfoTable
 import Juvix.Data.CodeAnn
+import Juvix.Data.Keyword.All qualified as Kw
 import Juvix.Prelude
 
 doc :: (PrettyCode c) => Options -> c -> Doc Ann
@@ -281,14 +282,27 @@ instance PrettyCode Pattern where
 instance PrettyCode BuiltinFunction where
   ppCode = return . annotate AnnKeyword . pretty
 
+instance PrettyCode Keyword where
+  ppCode = return . annotate AnnKeyword . pretty
+
+instance PrettyCode IsInstanceCoercion where
+  ppCode p = case p of
+    IsInstanceCoercionInstance -> ppCode Kw.kwInstance
+    IsInstanceCoercionCoercion -> do
+      c <- ppCode Kw.kwCoercion
+      i <- ppCode Kw.kwInstance
+      return (c <+> i)
+
 instance PrettyCode FunctionDef where
   ppCode f = do
     builtin' <- fmap (kwBuiltin <+>) <$> mapM ppCode (f ^. funDefBuiltin)
     funDefName' <- ppCode (f ^. funDefName)
     funDefType' <- ppCode (f ^. funDefType)
+    instanceCoercion' <- mapM ppCode (f ^. funDefIsInstanceCoercion)
     body' <- ppCode (f ^. funDefBody)
     return $
       builtin'
+        <?+> instanceCoercion'
         <?+> funDefName'
           <+> kwColon
           <+> funDefType'

src/Juvix/Compiler/Internal/Translation/FromConcrete.hs

@@ -371,7 +371,10 @@ goFunctionDef ::
 goFunctionDef FunctionDef {..} = do
   let _funDefName = goSymbol _signName
       _funDefTerminating = isJust _signTerminating
-      _funDefInstance = isJust _signInstance && isNothing _signCoercion
+      _funDefIsInstanceCoercion
+        | isJust _signCoercion = Just Internal.IsInstanceCoercionCoercion
+        | isJust _signInstance = Just Internal.IsInstanceCoercionInstance
+        | otherwise = Nothing
       _funDefCoercion = isJust _signCoercion
       _funDefBuiltin = (^. withLocParam) <$> _signBuiltin
   _funDefType <- goDefType

src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/CheckerNew.hs

@@ -331,16 +331,15 @@ checkFunctionDef FunctionDef {..} = do
           _funDefArgsInfo = _funDefArgsInfo',
           _funDefName,
           _funDefTerminating,
-          _funDefInstance,
-          _funDefCoercion,
+          _funDefIsInstanceCoercion,
           _funDefBuiltin,
           _funDefPragmas,
           _funDefDocComment
         }
-  when _funDefInstance $
-    checkInstanceType funDef
-  when _funDefCoercion $
-    checkCoercionType funDef
+  whenJust _funDefIsInstanceCoercion $ \case
+    IsInstanceCoercionCoercion -> checkCoercionType funDef
+    IsInstanceCoercionInstance -> checkInstanceType funDef
+
   registerFunctionDef funDef
   rememberFunctionDef funDef
   return funDef

src/Juvix/Compiler/Store/Internal/Data/InfoTable.hs

@@ -23,8 +23,7 @@ data FunctionInfo = FunctionInfo
   { _functionInfoName :: FunctionName,
     _functionInfoType :: Expression,
     _functionInfoTerminating :: Bool,
-    _functionInfoInstance :: Bool,
-    _functionInfoCoercion :: Bool,
+    _functionInfoIsInstanceCoercion :: Maybe IsInstanceCoercion,
     _functionInfoBuiltin :: Maybe BuiltinFunction,
     _functionInfoArgsInfo :: [ArgInfo],
     _functionInfoPragmas :: Pragmas,