Working kind inference

1 files changed, 9 insertions, 6 deletions

diff --git a/src/HSVIS/Typecheck/Solve.hs b/src/HSVIS/Typecheck/Solve.hs
index 5f51abe..7250e79 100644
--- a/src/HSVIS/Typecheck/Solve.hs
+++ b/src/HSVIS/Typecheck/Solve.hs
@@ -9,7 +9,7 @@ module HSVIS.Typecheck.Solve (
 import Control.Monad (guard, (>=>))
 import Data.Bifunctor (Bifunctor(..))
 import Data.Foldable (toList, foldl')
-import Data.List (sortBy, minimumBy, groupBy)
+import Data.List (sortBy, minimumBy, groupBy, intercalate)
 import Data.Ord (comparing)
 import Data.Map.Strict (Map)
 import qualified Data.Map.Strict as Map
@@ -66,8 +66,8 @@ solveConstraints
   => (t -> t -> Range -> (Bag (v, t, Range), Bag (t, t, Range)))
      -- | Free variables in a type
   -> (t -> Bag v)
-     -- | \v repl term -> Substitute v by repl in term
-  -> (v -> t -> t -> t)
+     -- | \mapping term -> term with variables in the mapping substituted by their values
+  -> (Map v t -> t -> t)
      -- | Detect bare-variable types
   -> (t -> Maybe v)
      -- | Some kind of size measure on types
@@ -118,19 +118,22 @@ solveConstraints reduce frees subst detect size = \tupcs ->
             $ Map.assocs m'
 
       case msmallestvar of
-        Nothing -> return $ applyLog eqlog mempty
+        Nothing -> do
+          traceM $ "[solver] Log = [" ++ intercalate ", " [show v ++ " = " ++ pretty t | (v, t) <- eqlog] ++ "]"
+          return $ applyLog eqlog mempty
         Just (var, RConstr smallrhs _) -> do
+          traceM $ "[solver] Retiring " ++ show var ++ " = " ++ pretty smallrhs
           let (_, otherrhss) = bagPartition (guard . (== smallrhs) . rconType) (m' Map.! var)
           let (newcs, errs) = foldMap (reduce' . unsplitConstr smallrhs) (dedupRCs (toList otherrhss))
           (fmap constrUnequal errs, ())  -- write the errors
           let m'' = Map.unionWith (<>)
-                      (Map.map (fmap @Bag (fmap @RConstr (subst var smallrhs)))
+                      (Map.map (fmap @Bag (fmap @RConstr (subst (Map.singleton var smallrhs))))
                                (Map.delete var m'))
                       (Map.fromListWith (<>) (map (second pure . splitConstr) (toList newcs)))
           loop m'' ((var, smallrhs) : eqlog)
 
     applyLog :: [(v, t)] -> Map v t -> Map v t
-    applyLog ((v, t) : l) m = applyLog l $ Map.insert v t (Map.map (subst v t) m)
+    applyLog ((v, t) : l) m = applyLog l $ Map.insert v (subst m t) m
     applyLog [] m = m
 
     -- If there are multiple sources for the same cosntraint, only one of them is kept.