diff options
| author | Roman Smrž <roman.smrz@seznam.cz> | 2026-05-08 09:31:49 +0200 |
|---|---|---|
| committer | Roman Smrž <roman.smrz@seznam.cz> | 2026-05-09 21:32:38 +0200 |
| commit | 5307cfd9de91533ec69e07cafa4d7c0d11481279 (patch) | |
| tree | b4ef462c5d01bb808438166a40d052db16627c2a /src/Parser/Core.hs | |
| parent | 0905fe68591a3dad83f87d5ac805b674c0b88c76 (diff) | |
Unification of function and forall types
Diffstat (limited to 'src/Parser/Core.hs')
| -rw-r--r-- | src/Parser/Core.hs | 27 |
1 files changed, 23 insertions, 4 deletions
diff --git a/src/Parser/Core.hs b/src/Parser/Core.hs index c12afdd..6f12af1 100644 --- a/src/Parser/Core.hs +++ b/src/Parser/Core.hs @@ -178,6 +178,11 @@ unify _ res@(ExprTypeConstr1 (Proxy :: Proxy a)) (ExprTypeConstr1 (Proxy :: Prox | Just (Refl :: a :~: b) <- eqT = return res +unify off (ExprTypeFunction args res) (ExprTypeFunction args' res') + = ExprTypeFunction + <$> unify off args args' + <*> unify off res res' + unify off (ExprTypeApp ac aparams) (ExprTypeApp bc bparams) | length aparams == length bparams = do @@ -198,7 +203,7 @@ unify off (ExprTypePrim aproxy) b@(ExprTypeApp {}) unify off a b = do parseError $ FancyError off $ S.singleton $ ErrorFail $ T.unpack $ - "couldn't match expected type `" <> textSomeExprType a <> "' with actual type `" <> textSomeExprType b <> "'" + "couldn't match expected type ‘" <> textSomeExprType a <> "’ with actual type ‘" <> textSomeExprType b <> "’" unifyExpr :: forall a b proxy. (ExprType a, ExprType b) => Int -> proxy a -> Expr b -> TestParser (Expr a) @@ -261,7 +266,7 @@ unifyExpr off pa expr = if unifySomeExpr :: Int -> SomeExprType -> SomeExpr -> TestParser SomeExpr -unifySomeExpr off stype sexpr@(SomeExpr expr) +unifySomeExpr off stype sexpr@(SomeExpr (expr :: Expr a)) | ExprTypePrim pa <- stype = SomeExpr <$> unifyExpr off pa expr @@ -273,6 +278,20 @@ unifySomeExpr off stype sexpr@(SomeExpr expr) _ <- unify off (ExprTypeVar tvar) (someExprType sexpr) return sexpr + | Just (Refl :: a :~: DynamicType) <- eqT + , ExprTypeForall qvar itype <- someExprType sexpr + = do + 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) + | ExprTypeFunction args res <- stype = case someExprType sexpr of ExprTypeFunction args' res' -> do @@ -286,8 +305,8 @@ unifySomeExpr off stype sexpr@(SomeExpr expr) | otherwise = do - parseError $ FancyError off $ S.singleton $ ErrorFail $ T.unpack $ - "couldn't match expected type ‘" <> textSomeExprType stype <> "’ with actual type ‘" <> textSomeExprType (someExprType sexpr) <> "’" + _ <- unify off stype (someExprType sexpr) + return sexpr skipLineComment :: TestParser () |