Type deconstruction and matching in unification

2 files changed, 33 insertions, 1 deletions

diff --git a/src/Parser/Core.hs b/src/Parser/Core.hs
index 1d93797..7b4da17 100644
--- a/src/Parser/Core.hs
+++ b/src/Parser/Core.hs
@@ -18,6 +18,7 @@ import qualified Text.Megaparsec.Char.Lexer as L
 
 import Network ()
 import Script.Expr
+import Script.Expr.Class
 import Script.Module
 import Test
 
@@ -181,6 +182,28 @@ unify _ res@(ExprTypePrim (Proxy :: Proxy a)) (ExprTypePrim (Proxy :: Proxy b))
     | Just (Refl :: a :~: b) <- eqT
     = return res
 
+unify _ res@(ExprTypeConstr1 (Proxy :: Proxy a)) (ExprTypeConstr1 (Proxy :: Proxy b))
+    | Just (Refl :: a :~: b) <- eqT
+    = return res
+
+unify off (ExprTypeApp ac aparams) (ExprTypeApp bc bparams)
+    | length aparams == length bparams
+    = do
+        c <- unify off ac bc
+        params <- zipWithM (unify off) aparams bparams
+        return $ case ( c, params ) of
+            ( ExprTypeConstr1 (Proxy :: Proxy c'), [ ExprTypePrim (Proxy :: Proxy p') ] )
+                -> ExprTypePrim (Proxy :: Proxy (c' p'))
+            _ -> ExprTypeApp c params
+
+unify off a@(ExprTypeApp {}) (ExprTypePrim bproxy)
+    | TypeDeconstructor1 c p <- matchTypeConstructor bproxy
+    = unify off a (ExprTypeApp (ExprTypeConstr1 c) [ ExprTypePrim p ])
+
+unify off (ExprTypePrim aproxy) b@(ExprTypeApp {})
+    | TypeDeconstructor1 c p <- matchTypeConstructor aproxy
+    = unify off (ExprTypeApp (ExprTypeConstr1 c) [ ExprTypePrim p ]) b
+
 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 <> "'"
diff --git a/src/Script/Expr/Class.hs b/src/Script/Expr/Class.hs
index fd128f1..5bf8a4b 100644
--- a/src/Script/Expr/Class.hs
+++ b/src/Script/Expr/Class.hs
@@ -1,6 +1,7 @@
 module Script.Expr.Class (
     ExprType(..),
     ExprTypeConstr1(..),
+    TypeDeconstructor(..),
     RecordSelector(..),
     ExprListUnpacker(..),
     ExprEnumerator(..),
@@ -18,6 +19,9 @@ class Typeable a => ExprType a where
     textExprType :: proxy a -> Text
     textExprValue :: a -> Text
 
+    matchTypeConstructor :: proxy a -> TypeDeconstructor a
+    matchTypeConstructor _ = NoTypeDeconstructor
+
     recordMembers :: [(Text, RecordSelector a)]
     recordMembers = []
 
@@ -33,9 +37,13 @@ class Typeable a => ExprType a where
     exprEnumerator :: proxy a -> Maybe (ExprEnumerator a)
     exprEnumerator _ = Nothing
 
-class (forall b. ExprType b => ExprType (a b)) => ExprTypeConstr1 (a :: Type -> Type) where
+class (Typeable a, forall b. ExprType b => ExprType (a b)) => ExprTypeConstr1 (a :: Type -> Type) where
     textExprTypeConstr1 :: proxy a -> Text -> Text
 
+data TypeDeconstructor a
+    = NoTypeDeconstructor
+    | forall c x. (ExprTypeConstr1 c, ExprType x, c x ~ a) => TypeDeconstructor1 (Proxy c) (Proxy x)
+
 
 data RecordSelector a = forall b. ExprType b => RecordSelector (a -> b)
 
@@ -82,6 +90,7 @@ instance ExprType Void where
 instance ExprType a => ExprType [ a ] where
     textExprType _ = textExprTypeConstr1 @[] Proxy (textExprType @a Proxy)
     textExprValue x = "[" <> T.intercalate ", " (map textExprValue x) <> "]"
+    matchTypeConstructor _ = TypeDeconstructor1 Proxy Proxy
 
     exprListUnpacker _ = Just $ ExprListUnpacker id (const Proxy)