Separate hide/expose expressions for primitive and function types

3 files changed, 49 insertions, 31 deletions

diff --git a/src/Parser/Core.hs b/src/Parser/Core.hs
index 6f12af1..3a3450b 100644
--- a/src/Parser/Core.hs
+++ b/src/Parser/Core.hs
@@ -215,19 +215,20 @@ unifyExpr off pa expr = if
     , ExprTypeForall qvar itype <- stype
     -> do
         tvar <- newTypeVar
-        _ <- unify off (ExprTypePrim (Proxy :: Proxy a)) $ renameVarInType qvar tvar itype
+        res <- unify off (ExprTypePrim (Proxy :: Proxy a)) $ renameVarInType qvar tvar itype
         rtype <- M.lookup tvar <$> gets testTypeUnif
-        return $ TypeApp (Variable sline name) $ fromMaybe (ExprTypeVar tvar) rtype
+        return $ ExposePrimType $ TypeApp res (fromMaybe (ExprTypeVar tvar) rtype) (Variable sline name)
 
     | DynVariable stype sline name <- expr
     -> do
         _ <- unify off (ExprTypePrim (Proxy :: Proxy a)) stype
         return $ Variable sline name
 
-    | HideType (ExprTypePrim (_ :: Proxy b'')) (expr' :: Expr b') <- expr
-    , Just (Refl :: b'' :~: b') <- eqT
-    -> do
-        unifyExpr off pa expr'
+    | HidePrimType (_ :: Expr b') <- expr
+    -> unifyExpr off pa (ExposePrimType expr :: Expr b')
+
+    | HideFunType args (_ :: Expr (FunctionType b')) <- expr
+    -> unifyExpr off pa (ExposeFunType args expr :: Expr (FunctionType b'))
 
     | TypeLambda tvar t f <- expr
     -> do
@@ -284,13 +285,7 @@ unifySomeExpr off stype sexpr@(SomeExpr (expr :: Expr a))
         tvar <- newTypeVar
         itype' <- unify off stype $ renameVarInType qvar tvar itype
         rtype <- M.lookup tvar <$> gets testTypeUnif
-        case itype' of
-            ExprTypeFunction _ (ExprTypePrim (Proxy :: Proxy r)) ->
-                return $ SomeExpr (TypeApp expr (fromMaybe (ExprTypeVar tvar) rtype) :: Expr (FunctionType a))
-            ExprTypeFunction _ _ ->
-                return $ SomeExpr (TypeApp expr (fromMaybe (ExprTypeVar tvar) rtype) :: Expr (FunctionType DynamicType))
-            _ ->
-                return $ SomeExpr (TypeApp expr (fromMaybe (ExprTypeVar tvar) rtype) :: Expr DynamicType)
+        return $ SomeExpr (TypeApp itype' (fromMaybe (ExprTypeVar tvar) rtype) expr)
 
     | ExprTypeFunction args res <- stype
     = case someExprType sexpr of
diff --git a/src/Parser/Expr.hs b/src/Parser/Expr.hs
index 16c2b45..c8a9e85 100644
--- a/src/Parser/Expr.hs
+++ b/src/Parser/Expr.hs
@@ -195,7 +195,7 @@ list = label "list" $ do
             return $ SomeExpr $
                 TypeLambda tvar (ExprTypeApp (ExprTypeConstr1 (Proxy :: Proxy [])) [ ExprTypeVar tvar ]) $
                     \case
-                        (ExprTypePrim (Proxy :: Proxy a)) -> HideType (ExprTypePrim (Proxy @[ a ])) $ Pure ([] :: [ a ])
+                        (ExprTypePrim (Proxy :: Proxy a)) -> HidePrimType $ Pure ([] :: [ a ])
                         _ -> Undefined "incomplete type"
 
         ,do SomeExpr x <- someExpr FunctionTerm
diff --git a/src/Script/Expr.hs b/src/Script/Expr.hs
index 3e56f8e..bff363c 100644
--- a/src/Script/Expr.hs
+++ b/src/Script/Expr.hs
@@ -63,9 +63,12 @@ data Expr a where
     ArgsApp :: ExprType a => FunctionArguments SomeExpr -> Expr (FunctionType a) -> Expr (FunctionType a)
     FunctionAbstraction :: ExprType a => Expr a -> Expr (FunctionType a)
     FunctionEval :: ExprType a => SourceLine -> Expr (FunctionType a) -> Expr a
-    HideType :: forall a. Typeable a => SomeExprType -> Expr a -> Expr DynamicType
+    HidePrimType :: forall a. ExprType a => Expr a -> Expr DynamicType
+    HideFunType :: forall a. ExprType a => FunctionArguments SomeArgumentType -> Expr (FunctionType a) -> Expr DynamicType
+    ExposePrimType :: forall a. ExprType a => Expr DynamicType -> Expr a
+    ExposeFunType :: forall a. ExprType a => FunctionArguments SomeArgumentType -> Expr DynamicType -> Expr (FunctionType a)
     TypeLambda :: TypeVar -> SomeExprType -> (SomeExprType -> Expr DynamicType) -> Expr DynamicType
-    TypeApp :: forall a. ExprType a => Expr DynamicType -> SomeExprType -> Expr a
+    TypeApp :: SomeExprType {- result type -} -> SomeExprType {- type argument -} -> Expr DynamicType -> Expr DynamicType
     LambdaAbstraction :: ExprType a => TypedVarName a -> Expr b -> Expr (a -> b)
     Pure :: a -> Expr a
     App :: AppAnnotation b -> Expr (a -> b) -> Expr a -> Expr b
@@ -107,9 +110,12 @@ mapExpr f = go
         ArgsApp args expr -> f $ ArgsApp (fmap (\(SomeExpr e) -> SomeExpr (go e)) args) (go expr)
         FunctionAbstraction expr -> f $ FunctionAbstraction (go expr)
         FunctionEval sline expr -> f $ FunctionEval sline (go expr)
-        HideType stype expr -> HideType stype $ go expr
+        HidePrimType expr -> f $ HidePrimType $ go expr
+        HideFunType args expr -> f $ HideFunType args $ go expr
+        ExposePrimType expr -> f $ ExposePrimType $ go expr
+        ExposeFunType args expr -> f $ ExposeFunType args $ go expr
         TypeLambda tvar stype efun -> TypeLambda tvar stype (go . efun)
-        TypeApp expr stype -> TypeApp (go expr) stype
+        TypeApp restype arg expr -> TypeApp restype arg (go expr)
         LambdaAbstraction tvar expr -> f $ LambdaAbstraction tvar (go expr)
         e@Pure {} -> f e
         App ann efun earg -> f $ App ann (go efun) (go earg)
@@ -204,19 +210,26 @@ eval = \case
         let cs' = CallStack (( sline, vars ) : cs)
         FunctionType fun <- withVar callStackVarName cs' $ eval efun
         return $ fun cs' mempty
-    HideType _ expr -> DynamicType <$> eval expr
+    HidePrimType expr -> DynamicType <$> eval expr
+    HideFunType _ expr -> DynamicType <$> eval expr
+    ExposePrimType expr -> do
+        DynamicType x <- eval expr
+        case cast x of
+            Just x' -> return x'
+            n@Nothing -> fail $ "type error in expose primitive type result " <> show ( typeOf x, typeOf n )
+    ExposeFunType _ expr -> do
+        DynamicType x <- eval expr
+        case cast x of
+            Just x' -> return x'
+            n@Nothing -> fail $ "type error in expose function type result " <> show ( typeOf x, typeOf n )
     TypeLambda _ _ f -> do
         gdefs <- askGlobalDefs
         dict <- askDictionary
         return $ DynamicType $ \t -> runSimpleEval (eval $ f t) gdefs dict
-    TypeApp expr stype -> do
+    TypeApp _ arg expr -> do
         DynamicType f <- eval expr
         case cast f of
-            Just f' -> do
-                case f' stype of
-                    DynamicType x -> case cast x of
-                        Just x' -> return x'
-                        n@Nothing -> fail $ "type error in type application result " <> show ( typeOf x, typeOf n )
+            Just f' -> return (f' arg)
             n@Nothing -> fail $ "type error in type application " <> show ( typeOf f, typeOf n )
     LambdaAbstraction (TypedVarName name) expr -> do
         gdefs <- askGlobalDefs
@@ -298,8 +311,11 @@ someExprType (SomeExpr expr) = go expr
     go = \case
         DynVariable stype _ _ -> stype
         e@(FunVariable args _ _) -> ExprTypeFunction args (ExprTypePrim (proxyOfFunctionType e))
-        HideType stype _ -> stype
+        HidePrimType (_ :: Expr a) -> ExprTypePrim (Proxy @a)
+        HideFunType args e -> ExprTypeFunction (ExprTypeArguments args) (ExprTypePrim (proxyOfFunctionType e))
+        e@(ExposeFunType args _) -> ExprTypeFunction (ExprTypeArguments args) (ExprTypePrim (proxyOfFunctionType e))
         TypeLambda tvar stype _ -> ExprTypeForall tvar stype
+        TypeApp stype _ _ -> stype
 
         ArgsReq args inner -> exprTypeFunction (fmap snd args) (go inner)
         ArgsApp (FunctionArguments used) inner
@@ -333,12 +349,15 @@ renameTypeVar a b = go
         ArgsApp args fun -> ArgsApp (fmap (renameTypeVarInSomeExpr a b) args) (go fun)
         FunctionAbstraction expr -> FunctionAbstraction (go expr)
         FunctionEval sline expr -> FunctionEval sline (go expr)
-        HideType stype expr -> HideType (renameVarInType a b stype) (go expr)
+        HidePrimType expr -> HidePrimType (go expr)
+        HideFunType args expr -> HideFunType args (go expr)
+        ExposePrimType {} -> orig
+        ExposeFunType {} -> orig
         TypeLambda tvar stype expr
             | tvar == a -> orig
             | tvar == b -> error "type var collision"
             | otherwise -> TypeLambda tvar (renameVarInType a b stype) (go . expr)
-        TypeApp expr stype -> TypeApp (go expr) (renameVarInType a b stype)
+        TypeApp restype arg expr -> TypeApp (renameVarInType a b restype) (renameVarInType a b arg) (go expr)
         LambdaAbstraction vname expr -> LambdaAbstraction vname (go expr)
         Pure {} -> orig
         App ann f x -> App ann (go f) (go x)
@@ -460,7 +479,8 @@ exprArgs = \case
          in FunctionArguments (args `M.difference` applied)
     FunctionAbstraction {} -> mempty
     FunctionEval {} -> mempty
-    TypeApp {} -> error "exprArgs: type application"
+    ExposePrimType {} -> mempty
+    ExposeFunType args _ -> args
     Pure {} -> error "exprArgs: pure"
     App {} -> error "exprArgs: app"
     Undefined {} -> error "exprArgs: undefined"
@@ -501,9 +521,12 @@ gatherVars = fmap (uniqOn fst . sortOn fst) . helper
             return $ concat (v : vs)
         FunctionAbstraction expr -> helper expr
         FunctionEval _ efun -> helper efun
-        HideType _ expr -> helper expr
+        HidePrimType expr -> helper expr
+        HideFunType _ expr -> helper expr
+        ExposePrimType expr -> helper expr
+        ExposeFunType _ expr -> helper expr
         TypeLambda {} -> return []
-        TypeApp expr _ -> helper expr
+        TypeApp _ _ expr -> helper expr
         LambdaAbstraction (TypedVarName var) expr -> withDictionary (filter ((var /=) . fst)) $ helper expr
         Pure _ -> return []
         e@(App (AnnRecord sel) _ x)