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/AST.hs       |  6 ++++++
 src/HSVIS/Pretty.hs    |  7 ++++++-
 src/HSVIS/Typecheck.hs | 32 ++++++++++++++++++++++++++++----
 3 files changed, 40 insertions(+), 5 deletions(-)

diff --git a/src/HSVIS/AST.hs b/src/HSVIS/AST.hs
index a789c82..f95a3cc 100644
--- a/src/HSVIS/AST.hs
+++ b/src/HSVIS/AST.hs
@@ -141,6 +141,12 @@ data Operator = OAdd | OSub | OMul | ODiv | OMod | OEqu | OPow
 instance Pretty Name where
   prettysPrec _ (Name n) = showString ("\"" ++ n ++ "\"")
 
+instance (X Kind s ~ (), Pretty (E Kind s)) => Pretty (Kind s) where
+  prettysPrec _ (KType ()) = showString "Type"
+  prettysPrec d (KFun () a b) =
+    showParen (d > -1) $ prettysPrec 0 a . showString " -> " . prettysPrec 0 b
+  prettysPrec d (KExt () e) = prettysPrec d e
+
 instance HasExt DataDef where
   type HasXField DataDef = 'True
   type HasECon DataDef = 'False
diff --git a/src/HSVIS/Pretty.hs b/src/HSVIS/Pretty.hs
index ffde90e..0f98da3 100644
--- a/src/HSVIS/Pretty.hs
+++ b/src/HSVIS/Pretty.hs
@@ -1,11 +1,16 @@
 module HSVIS.Pretty where
 
+import Data.Void
+
 
 class Pretty a where
   prettysPrec :: Int -> a -> ShowS
 
+instance Pretty Void where
+  prettysPrec _ = absurd
+
 prettyPrec :: Pretty a => Int -> a -> String
 prettyPrec d x = prettysPrec d x ""
 
 pretty :: Pretty a => a -> String
-pretty x = prettyPrec 0 x
+pretty x = prettyPrec minBound x
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