From e8f09ff3f9d40922238d646c8fbcbacf9cfdfb62 Mon Sep 17 00:00:00 2001
From: Tom Smeding <tom@tomsmeding.com>
Date: Fri, 1 Mar 2024 22:25:02 +0100
Subject: Little typecheck work

---
 src/HSVIS/Typecheck.hs | 32 ++++++++++++++++++++++++++++----
 1 file changed, 28 insertions(+), 4 deletions(-)

(limited to 'src/HSVIS/Typecheck.hs')

diff --git a/src/HSVIS/Typecheck.hs b/src/HSVIS/Typecheck.hs
index 2b05793..de9d7db 100644
--- a/src/HSVIS/Typecheck.hs
+++ b/src/HSVIS/Typecheck.hs
@@ -7,10 +7,10 @@
 module HSVIS.Typecheck where
 
 import Control.Monad
-import Data.Bifunctor (first)
+import Data.Bifunctor (first, second)
 import Data.Foldable (toList)
-import Data.List (partition)
 import Data.Map.Strict (Map)
+import Data.Monoid (First(..))
 import qualified Data.Map.Strict as Map
 
 import Data.Bag
@@ -78,8 +78,11 @@ typecheck fp source prog =
   in (toList (ds1 <> ds2), substProg sub progtc)
 
 data Constr
-  = CEq CType CType Range  -- ^ These types must be equal because of the expression here
-  | CEqK CKind CKind Range  -- ^ These kinds must be equal because of the type here
+  -- Equality constraints: "left" must be equal to "right" because of the thing
+  -- at the given range. "left" is the expected thing; "right" is the observed
+  -- thing.
+  = CEq CType CType Range
+  | CEqK CKind CKind Range
   deriving (Show)
 
 data Env = Env (Map Name CKind) (Map Name CType)
@@ -268,6 +271,27 @@ tcFunDef (FunDef _ name msig eqs) = do
 tcFunEq :: CType -> PFunEq -> TCM CFunEq
 tcFunEq = _
 
+solveKindVars :: Bag (CKind, CKind, Range) -> TCM ()
+solveKindVars =
+  mapM_ $ \(a, b, rng) -> do
+    let (subst, First merr) = reduce a b
+    forM_ merr $ \(erra, errb) ->
+      raise rng $
+        "Kind mismatch:\n\
+        \- Expected: " ++ pretty a ++ "\n\
+        \- Observed: " ++ pretty b ++ "\n\
+        \because '" ++ pretty erra ++ "' and '" ++ pretty errb ++ "' don't match"
+    let collected :: [(Int, Bag CKind)]
+        collected = Map.assocs $ Map.fromListWith (<>) (fmap (second pure) (toList subst))
+    _
+  where
+    reduce :: CKind -> CKind -> (Bag (Int, CKind), First (CKind, CKind))
+    reduce (KType ()) (KType ()) = mempty
+    reduce (KFun () a b) (KFun () c d) = reduce a c <> reduce b d
+    reduce (KExt () (KUniVar i)) k = (pure (i, k), mempty)
+    reduce k (KExt () (KUniVar i)) = (pure (i, k), mempty)
+    reduce k1 k2 = (mempty, pure (k1, k2))
+
 allEq :: (Eq a, Foldable t) => t a -> Bool
 allEq l = case toList l of
             [] -> True
-- 
cgit v1.2.3-70-g09d2