Type constructors

5 files changed, 42 insertions, 8 deletions

diff --git a/erebos-tester.cabal b/erebos-tester.cabal
index 0f17c87..32f1934 100644
--- a/erebos-tester.cabal
+++ b/erebos-tester.cabal
@@ -100,6 +100,7 @@ executable erebos-tester
         MultiParamTypeClasses
         MultiWayIf
         OverloadedStrings
+        QuantifiedConstraints
         RankNTypes
         RecordWildCards
         ScopedTypeVariables
diff --git a/src/Parser.hs b/src/Parser.hs
index bb8288e..e38f1ef 100644
--- a/src/Parser.hs
+++ b/src/Parser.hs
@@ -102,10 +102,18 @@ parseDefinition href = label "symbol definition" $ do
         let err msg = do
                 registerParseError . FancyError off . S.singleton . ErrorFail $ T.unpack msg
                 return ( vname, SomeArgumentType (OptionalArgument @DynamicType) )
+        let getConcreteType = \case
+                (ExprTypeApp (ExprTypeConstr1 (Proxy :: Proxy a)) [ pb ])
+                    | ExprTypePrim (_ :: Proxy b) <- getConcreteType pb
+                    -> ExprTypePrim (Proxy :: Proxy (a b))
+                t -> t
         gets (M.lookup tvar . testTypeUnif) >>= \case
-            Just (ExprTypePrim (_ :: Proxy a)) -> return ( vname, SomeArgumentType (RequiredArgument @a) )
-            Just (ExprTypeVar (TypeVar tvar')) -> err $ "ambiguous type for ‘" <> textVarName vname <> " : " <> tvar' <> "’"
-            Just (ExprTypeFunction {}) -> err $ "unsupported function type of ‘" <> textVarName vname <> "’"
+            Just t
+                | ExprTypePrim (_ :: Proxy a) <- getConcreteType t
+                -> return ( vname, SomeArgumentType (RequiredArgument @a) )
+
+                | otherwise
+                -> err $ "expected concrete type for ‘" <> textVarName vname <> " : " <> textSomeExprType t <> "’"
             Nothing -> err $ "ambiguous type for ‘" <> textVarName vname <> " : " <> tvarname <> "’"
 
     replaceDynArgs :: forall a. Expr a -> TestParser (Expr a)
diff --git a/src/Parser/Core.hs b/src/Parser/Core.hs
index 562923d..1d93797 100644
--- a/src/Parser/Core.hs
+++ b/src/Parser/Core.hs
@@ -104,17 +104,27 @@ lookupVarExpr off sline name = do
     ( fqn, etype ) <- lookupVarType off name
     case etype of
         ExprTypePrim (Proxy :: Proxy a) -> return $ SomeExpr $ (Variable sline fqn :: Expr a)
+        ExprTypeConstr1 _ -> return $ SomeExpr $ (Undefined "incomplete type" :: Expr DynamicType)
         ExprTypeVar tvar -> return $ SomeExpr $ DynVariable tvar sline fqn
         ExprTypeFunction args (_ :: Proxy a) -> return $ SomeExpr $ (FunVariable args sline fqn :: Expr (FunctionType a))
+        stype@ExprTypeApp {} -> do
+            tvar <- newTypeVar
+            modify $ \s -> s { testTypeUnif = M.insert tvar stype $ testTypeUnif s }
+            return $ SomeExpr $ DynVariable tvar sline fqn
 
 lookupScalarVarExpr :: Int -> SourceLine -> VarName -> TestParser SomeExpr
 lookupScalarVarExpr off sline name = do
     ( fqn, etype ) <- lookupVarType off name
     case etype of
         ExprTypePrim (Proxy :: Proxy a) -> return $ SomeExpr $ (Variable sline fqn :: Expr a)
+        ExprTypeConstr1 _ -> return $ SomeExpr $ (Undefined "incomplete type" :: Expr DynamicType)
         ExprTypeVar tvar -> return $ SomeExpr $ DynVariable tvar sline fqn
         ExprTypeFunction args (pa :: Proxy a) -> do
             SomeExpr <$> unifyExpr off pa (FunVariable args sline fqn :: Expr (FunctionType a))
+        stype@ExprTypeApp {} -> do
+            tvar <- newTypeVar
+            modify $ \s -> s { testTypeUnif = M.insert tvar stype $ testTypeUnif s }
+            return $ SomeExpr $ DynVariable tvar sline fqn
 
 unify :: Int -> SomeExprType -> SomeExprType -> TestParser SomeExprType
 unify _ (ExprTypeVar aname) (ExprTypeVar bname) | aname == bname = do
diff --git a/src/Script/Expr.hs b/src/Script/Expr.hs
index bc4f9cb..cc37f73 100644
--- a/src/Script/Expr.hs
+++ b/src/Script/Expr.hs
@@ -253,8 +253,10 @@ newtype TypeVar = TypeVar Text
 
 data SomeExprType
     = forall a. ExprType a => ExprTypePrim (Proxy a)
+    | forall a. ExprTypeConstr1 a => ExprTypeConstr1 (Proxy a)
     | ExprTypeVar TypeVar
     | forall a. ExprType a => ExprTypeFunction (FunctionArguments SomeArgumentType) (Proxy a)
+    | ExprTypeApp SomeExprType [ SomeExprType ]
 
 someExprType :: SomeExpr -> SomeExprType
 someExprType (SomeExpr expr) = go expr
@@ -285,9 +287,14 @@ someExprType (SomeExpr expr) = go expr
     proxyOfFunctionType _ = Proxy
 
 textSomeExprType :: SomeExprType -> Text
-textSomeExprType (ExprTypePrim p) = textExprType p
-textSomeExprType (ExprTypeVar (TypeVar name)) = name
-textSomeExprType (ExprTypeFunction _ r) = "function:" <> textExprType r
+textSomeExprType = go []
+  where
+    go _ (ExprTypePrim p) = textExprType p
+    go (x : _) (ExprTypeConstr1 c) = textExprTypeConstr1 c x
+    go [] (ExprTypeConstr1 _) = "<incomplte type>"
+    go _ (ExprTypeVar (TypeVar name)) = name
+    go _ (ExprTypeFunction _ r) = "function:" <> textExprType r
+    go _ (ExprTypeApp c xs) = go (map textSomeExprType xs) c
 
 data AsFunType a
     = forall b. (a ~ FunctionType b, ExprType b) => IsFunType
diff --git a/src/Script/Expr/Class.hs b/src/Script/Expr/Class.hs
index 810b0c8..fd128f1 100644
--- a/src/Script/Expr/Class.hs
+++ b/src/Script/Expr/Class.hs
@@ -1,10 +1,12 @@
 module Script.Expr.Class (
     ExprType(..),
+    ExprTypeConstr1(..),
     RecordSelector(..),
     ExprListUnpacker(..),
     ExprEnumerator(..),
 ) where
 
+import Data.Kind
 import Data.Maybe
 import Data.Scientific
 import Data.Text (Text)
@@ -31,6 +33,9 @@ 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
+    textExprTypeConstr1 :: proxy a -> Text -> Text
+
 
 data RecordSelector a = forall b. ExprType b => RecordSelector (a -> b)
 
@@ -74,12 +79,15 @@ instance ExprType Void where
     textExprType _ = T.pack "void"
     textExprValue _ = T.pack "<void>"
 
-instance ExprType a => ExprType [a] where
-    textExprType _ = "[" <> textExprType @a Proxy <> "]"
+instance ExprType a => ExprType [ a ] where
+    textExprType _ = textExprTypeConstr1 @[] Proxy (textExprType @a Proxy)
     textExprValue x = "[" <> T.intercalate ", " (map textExprValue x) <> "]"
 
     exprListUnpacker _ = Just $ ExprListUnpacker id (const Proxy)
 
+instance ExprTypeConstr1 [] where
+    textExprTypeConstr1 _ x = "[" <> x <> "]"
+
 instance ExprType a => ExprType (Maybe a) where
     textExprType _ = textExprType @a Proxy <> "?"
     textExprValue (Just x) = textExprValue x