Dynamic type in Core (#1508)

src/Juvix/Compiler/Core/Evaluator.hs

@@ -72,6 +72,7 @@ eval !ctx !env0 = convertRuntimeNodes . eval' env0
       NPi {} -> substEnv env n
       NUniv {} -> n
       NTyp (TypeConstr i sym args) -> mkTypeConstr i sym (map' (eval' env) args)
+      NDyn {} -> n
       Closure {} -> n
 
     branch :: Node -> Env -> [Node] -> Tag -> Maybe Node -> [CaseBranch] -> Node

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

@@ -90,6 +90,12 @@ mkTypeConstr i sym args = NTyp (TypeConstr i sym args)
 mkTypeConstr' :: Symbol -> [Type] -> Type
 mkTypeConstr' = mkTypeConstr Info.empty
 
+mkDynamic :: Info -> Type
+mkDynamic i = NDyn (Dynamic i)
+
+mkDynamic' :: Type
+mkDynamic' = mkDynamic Info.empty
+
 {------------------------------------------------------------------------}
 {- functions on Type -}
 
@@ -214,6 +220,8 @@ destruct = \case
     NodeDetails i [] [] [] (\i' _ -> mkUniv i' l)
   NTyp (TypeConstr i sym args) ->
     NodeDetails i args (map (const 0) args) (map (const []) args) (`mkTypeConstr` sym)
+  NDyn (Dynamic i) ->
+    NodeDetails i [] [] [] (\i' _ -> mkDynamic i')
   Closure env (Lambda i b) ->
     NodeDetails
       i

src/Juvix/Compiler/Core/Language.hs

@@ -82,6 +82,11 @@ data TypeConstr = TypeConstr
     _typeConstrArgs :: ![Type]
   }
 
+-- | Dynamic type. A Node with a dynamic type has an unknown type. Useful
+-- for transformations that introduce partial type information, e.g., one can
+-- have types `* -> *` and `* -> * -> Nat` where `*` is the dynamic type.
+newtype Dynamic = Dynamic {_dynamicInfo :: Info}
+
 -- | `Node` is the type of nodes in the program tree. The nodes themselves
 -- contain only runtime-relevant information. Runtime-irrelevant annotations
 -- (including all type information) are stored in the infos associated with each
@@ -99,6 +104,7 @@ data Node
   | NPi {-# UNPACK #-} !Pi
   | NUniv {-# UNPACK #-} !Univ
   | NTyp {-# UNPACK #-} !TypeConstr
+  | NDyn !Dynamic -- Dynamic is already a newtype, so it's unpacked.
   | -- Evaluation only: `Closure env body`
     Closure
       { _closureEnv :: !Env,
@@ -180,6 +186,9 @@ instance HasAtomicity Univ where
 instance HasAtomicity TypeConstr where
   atomicity _ = Aggregate lambdaFixity
 
+instance HasAtomicity Dynamic where
+  atomicity _ = Atom
+
 instance HasAtomicity Node where
   atomicity = \case
     NVar x -> atomicity x
@@ -194,6 +203,7 @@ instance HasAtomicity Node where
     NPi x -> atomicity x
     NUniv x -> atomicity x
     NTyp x -> atomicity x
+    NDyn x -> atomicity x
     Closure {} -> Aggregate lambdaFixity
 
 lambdaFixity :: Fixity
@@ -235,6 +245,9 @@ instance Eq Univ where
 instance Eq TypeConstr where
   (TypeConstr _ sym1 args1) == (TypeConstr _ sym2 args2) = sym1 == sym2 && args1 == args2
 
+instance Eq Dynamic where
+  Dynamic _ == Dynamic _ = True
+
 makeLenses ''Var
 makeLenses ''Ident
 makeLenses ''Constant

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

@@ -155,6 +155,7 @@ instance PrettyCode Node where
           Just ni -> ppCode (ni ^. NameInfo.infoName)
           Nothing -> return $ kwUnnamedIdent <> pretty _typeConstrSymbol
       return $ foldl' (<+>) n' args'
+    NDyn {} -> return kwDynamic
     Closure env l@Lambda {} ->
       ppCode (substEnv env (NLam l))
 
@@ -253,3 +254,6 @@ kwTrace = keyword Str.trace_
 
 kwFail :: Doc Ann
 kwFail = keyword Str.fail_
+
+kwDynamic :: Doc Ann
+kwDynamic = keyword Str.mul

src/Juvix/Compiler/Core/Translation/FromSource.hs

@@ -43,9 +43,6 @@ runParser root fileName tab input =
         { _parserParamsRoot = root
         }
 
-starType :: Type
-starType = mkPi Info.empty (mkUniv Info.empty 0) (mkVar Info.empty 0)
-
 binderNameInfo :: Name -> Info
 binderNameInfo name =
   Info.singleton (BinderInfo (Info.singleton (NameInfo name)))
@@ -79,7 +76,7 @@ declareBuiltinConstr btag nameTxt i = do
     ( ConstructorInfo
         { _constructorName = name,
           _constructorTag = BuiltinTag btag,
-          _constructorType = starType,
+          _constructorType = mkDynamic',
           _constructorArgsNum = builtinConstrArgsNum btag
         }
     )
@@ -143,7 +140,7 @@ statementDef = do
             IdentifierInfo
               { _identifierName = name,
                 _identifierSymbol = sym,
-                _identifierType = starType,
+                _identifierType = mkDynamic',
                 _identifierArgsNum = 0,
                 _identifierArgsInfo = [],
                 _identifierIsExported = False
@@ -190,7 +187,7 @@ statementConstr = do
         ConstructorInfo
           { _constructorName = name,
             _constructorTag = tag,
-            _constructorType = starType,
+            _constructorType = mkDynamic',
             _constructorArgsNum = argsNum
           }
   lift $ registerConstructor info