Type application in expressions

3 files changed, 41 insertions, 26 deletions

diff --git a/src/Parser/Core.hs b/src/Parser/Core.hs
index 1b049c8..c317067 100644
--- a/src/Parser/Core.hs
+++ b/src/Parser/Core.hs
@@ -207,6 +207,14 @@ unifyExpr off pa expr = if
     -> return expr
 
     | DynVariable stype sline name <- expr
+    , ExprTypeForall qvar itype <- stype
+    -> do
+        tvar <- newTypeVar
+        _ <- 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
+
+    | DynVariable stype sline name <- expr
     -> do
         _ <- unify off (ExprTypePrim (Proxy :: Proxy a)) stype
         return $ Variable sline name
@@ -215,12 +223,7 @@ unifyExpr off pa expr = if
     -> do
         unifyExpr off pa expr'
 
-    | TypeQuant qvar expr' <- expr
-    -> do
-        tvar <- newTypeVar
-        unifyExpr off pa $ renameTypeVar qvar tvar expr'
-
-    | TypeLambda t tvar f <- expr
+    | TypeLambda tvar t f <- expr
     -> do
         _ <- unify off (ExprTypePrim (Proxy :: Proxy a)) t
         Just (ExprTypePrim pt) <- M.lookup tvar <$> gets testTypeUnif
diff --git a/src/Parser/Expr.hs b/src/Parser/Expr.hs
index 5e27457..c57aa97 100644
--- a/src/Parser/Expr.hs
+++ b/src/Parser/Expr.hs
@@ -189,11 +189,10 @@ list = label "list" $ do
         [do symbol "]"
             tvar <- newTypeVar
             return $ SomeExpr $
-                TypeQuant tvar $
-                    TypeLambda (ExprTypeApp (ExprTypeConstr1 (Proxy :: Proxy [])) [ ExprTypeVar tvar ]) tvar $
-                        \case
-                            (ExprTypePrim (Proxy :: Proxy a)) -> HideType $ Pure ([] :: [ a ])
-                            _ -> Undefined "incomplete type"
+                TypeLambda tvar (ExprTypeApp (ExprTypeConstr1 (Proxy :: Proxy [])) [ ExprTypeVar tvar ]) $
+                    \case
+                        (ExprTypePrim (Proxy :: Proxy a)) -> HideType $ Pure ([] :: [ a ])
+                        _ -> Undefined "incomplete type"
 
         ,do SomeExpr x <- someExpr
             let enumErr off = parseError $ FancyError off $ S.singleton $ ErrorFail $ T.unpack $
diff --git a/src/Script/Expr.hs b/src/Script/Expr.hs
index 0941ffa..9e4ffa0 100644
--- a/src/Script/Expr.hs
+++ b/src/Script/Expr.hs
@@ -8,7 +8,7 @@ module Script.Expr (
     FunctionType, DynamicType,
     ExprType(..), SomeExpr(..),
     TypeVar(..), SomeExprType(..), someExprType, textSomeExprType,
-    renameTypeVar,
+    renameTypeVar, renameVarInType,
 
     VarValue(..), SomeVarValue(..),
     svvVariables, svvArguments,
@@ -63,8 +63,8 @@ data Expr a where
     FunctionAbstraction :: ExprType a => Expr a -> Expr (FunctionType a)
     FunctionEval :: ExprType a => SourceLine -> Expr (FunctionType a) -> Expr a
     HideType :: forall a. ExprType a => Expr a -> Expr DynamicType
-    TypeLambda :: forall a. ExprType a => SomeExprType -> TypeVar -> (SomeExprType -> Expr a) -> Expr DynamicType
-    TypeQuant :: forall a. ExprType a => TypeVar -> Expr a -> Expr DynamicType
+    TypeLambda :: TypeVar -> SomeExprType -> (SomeExprType -> Expr DynamicType) -> Expr DynamicType
+    TypeApp :: forall a. ExprType a => Expr DynamicType -> SomeExprType -> Expr a
     LambdaAbstraction :: ExprType a => TypedVarName a -> Expr b -> Expr (a -> b)
     Pure :: a -> Expr a
     App :: AppAnnotation b -> Expr (a -> b) -> Expr a -> Expr b
@@ -106,8 +106,8 @@ mapExpr f = go
         FunctionAbstraction expr -> f $ FunctionAbstraction (go expr)
         FunctionEval sline expr -> f $ FunctionEval sline (go expr)
         HideType expr -> HideType $ go expr
-        TypeLambda stype tvar efun -> TypeLambda stype tvar $ (go . efun)
-        TypeQuant tvar expr -> TypeQuant tvar $ go expr
+        TypeLambda tvar stype efun -> TypeLambda tvar stype (go . efun)
+        TypeApp expr stype -> TypeApp (go expr) stype
         LambdaAbstraction tvar expr -> f $ LambdaAbstraction tvar (go expr)
         e@Pure {} -> f e
         App ann efun earg -> f $ App ann (go efun) (go earg)
@@ -201,9 +201,20 @@ eval = \case
         let cs' = CallStack (( sline, vars ) : cs)
         FunctionType fun <- withVar callStackVarName cs' $ eval efun
         return $ fun cs' mempty
-    HideType expr -> return $ DynamicType expr
-    e@TypeLambda {} -> return $ DynamicType e
-    e@TypeQuant {} -> return $ DynamicType e
+    HideType expr -> DynamicType <$> eval expr
+    TypeLambda _ _ f -> do
+        gdefs <- askGlobalDefs
+        dict <- askDictionary
+        return $ DynamicType $ \t -> runSimpleEval (eval $ f t) gdefs dict
+    TypeApp expr stype -> 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 )
+            n@Nothing -> fail $ "type error in type application " <> show ( typeOf f, typeOf n )
     LambdaAbstraction (TypedVarName name) expr -> do
         gdefs <- askGlobalDefs
         dict <- askDictionary
@@ -249,7 +260,7 @@ instance ExprType a => ExprType (FunctionType a) where
     textExprType _ = "function type"
     textExprValue _ = "<function type>"
 
-data DynamicType = forall a. ExprType a => DynamicType (Expr a)
+data DynamicType = forall a. Typeable a => DynamicType a
 
 instance ExprType DynamicType where
     textExprType _ = "ambiguous type"
@@ -275,6 +286,8 @@ someExprType (SomeExpr expr) = go expr
     go :: forall e. ExprType e => Expr e -> SomeExprType
     go = \case
         DynVariable stype _ _ -> stype
+        HideType e -> go e
+        TypeLambda tvar stype _ -> ExprTypeForall tvar stype
         (e :: Expr a)
             | IsFunType <- asFunType e -> ExprTypeFunction (gof e) (proxyOfFunctionType e)
             | otherwise -> ExprTypePrim (Proxy @a)
@@ -290,6 +303,7 @@ someExprType (SomeExpr expr) = go expr
              in FunctionArguments $ args `M.difference` used
         FunctionAbstraction {} -> mempty
         FunctionEval {} -> error "someExprType: gof: function eval"
+        TypeApp {} -> error "someExprType: gof: type application"
         Pure {} -> error "someExprType: gof: pure"
         App {} -> error "someExprType: gof: app"
         Undefined {} -> error "someExprType: gof: undefined"
@@ -311,13 +325,11 @@ renameTypeVar a b = go
         FunctionAbstraction expr -> FunctionAbstraction (go expr)
         FunctionEval sline expr -> FunctionEval sline (go expr)
         HideType expr -> HideType (go expr)
-        TypeLambda stype tvar expr
-            | tvar == a -> TypeLambda (renameVarInType a b stype) b expr
-            | otherwise -> TypeLambda (renameVarInType a b stype) tvar (go . expr)
-        TypeQuant tvar expr
+        TypeLambda tvar stype expr
             | tvar == a -> orig
             | tvar == b -> error "type var collision"
-            | otherwise -> TypeQuant tvar (go expr)
+            | otherwise -> TypeLambda tvar (renameVarInType a b stype) (go . expr)
+        TypeApp expr stype -> TypeApp (go expr) (renameVarInType a b stype)
         LambdaAbstraction vname expr -> LambdaAbstraction vname (go expr)
         Pure {} -> orig
         App ann f x -> App ann (go f) (go x)
@@ -436,6 +448,7 @@ exprArgs = \case
          in FunctionArguments (args `M.difference` applied)
     FunctionAbstraction {} -> mempty
     FunctionEval {} -> mempty
+    TypeApp {} -> error "exprArgs: type application"
     Pure {} -> error "exprArgs: pure"
     App {} -> error "exprArgs: app"
     Undefined {} -> error "exprArgs: undefined"
@@ -494,7 +507,7 @@ gatherVars = fmap (uniqOn fst . sortOn fst) . helper
         FunctionEval _ efun -> helper efun
         HideType expr -> helper expr
         TypeLambda {} -> return []
-        TypeQuant _ expr -> helper expr
+        TypeApp expr _ -> helper expr
         LambdaAbstraction (TypedVarName var) expr -> withDictionary (filter ((var /=) . fst)) $ helper expr
         Pure _ -> return []
         e@(App (AnnRecord sel) _ x)