From db5d73811c42d640f606ede40f861e1c052f8ca5 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Roman=20Smr=C5=BE?= <roman.smrz@seznam.cz>
Date: Sun, 19 Apr 2026 10:41:11 +0200
Subject: Type application in expressions

---
 src/Parser/Core.hs | 15 +++++++++------
 src/Parser/Expr.hs |  9 ++++-----
 2 files changed, 13 insertions(+), 11 deletions(-)

(limited to 'src/Parser')

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
@@ -206,6 +206,14 @@ unifyExpr off pa expr = if
     | Just (Refl :: a :~: b) <- eqT
     -> 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
@@ -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 $
-- 
cgit v1.2.3