Typecheck work; solver is incorrect

1 files changed, 55 insertions, 28 deletions

diff --git a/src/HSVIS/Typecheck.hs b/src/HSVIS/Typecheck.hs
index ba853a0..c97064a 100644
--- a/src/HSVIS/Typecheck.hs
+++ b/src/HSVIS/Typecheck.hs
@@ -78,6 +78,9 @@ type TPattern = Pattern StageTyped
 type TRHS     = RHS     StageTyped
 type TExpr    = Expr    StageTyped
 
+instance Pretty (E Type StageTC) where
+  prettysPrec _ (TUniVar n) = showString ("?t" ++ show n)
+
 instance Pretty (E Kind StageTC) where
   prettysPrec _ (KUniVar n) = showString ("?k" ++ show n)
 
@@ -144,7 +147,7 @@ putFullEnv :: Env -> TCM ()
 putFullEnv env = TCM $ \_ i _ -> (mempty, mempty, i, env, ())
 
 genId :: TCM Int
-genId = TCM $ \_ i env -> (mempty, mempty, i, env, i)
+genId = TCM $ \_ i env -> (mempty, mempty, i + 1, env, i)
 
 getKind :: Name -> TCM (Maybe CKind)
 getKind name = do
@@ -208,6 +211,8 @@ tcProgram (Program ddefs fdefs) = do
 
   solveKindVars kconstrs
 
+  traceM (unlines (map pretty ddefs'))
+
   fdefs' <- mapM tcFunDef fdefs
 
   return (Program ddefs' fdefs')
@@ -232,40 +237,59 @@ tcDataDef (DataDef rng name params cons) = do
 
   cons' <- scopeTEnv $ do
     modifyTEnv (Map.fromList (zip (map snd params) pkinds) <>)
-    mapM (\(cname, ty) -> (cname,) <$> mapM kcType ty) cons
+    mapM (\(cname, fieldtys) -> (cname,) <$> mapM (kcType (Just (KType ()))) fieldtys) cons
   return (DataDef () name (zip pkinds (map snd params)) cons')
 
-kcType :: PType -> TCM CType
-kcType = \case
+promoteDown :: Maybe CKind -> TCM CKind
+promoteDown Nothing = genKUniVar
+promoteDown (Just k) = return k
+
+downEqK :: Range -> Maybe CKind -> CKind -> TCM ()
+downEqK _ Nothing _ = return ()
+downEqK rng (Just k1) k2 = emit $ CEqK k1 k2 rng
+
+-- | Given (maybe) the expected kind of this type, and a type, check it for
+-- kind-correctness.
+kcType :: Maybe CKind -> PType -> TCM CType
+kcType mdown = \case
   TApp rng t ts -> do
-    t' <- kcType t
-    ts' <- mapM kcType ts
-    retk <- genKUniVar
+    t' <- kcType Nothing t
+    ts' <- mapM (kcType Nothing) ts
+    retk <- promoteDown mdown
     let expected = foldr (KFun ()) retk (map extOf ts')
     emit $ CEqK (extOf t') expected rng
     return (TApp retk t' ts')
 
-  TTup _ ts -> do
-    ts' <- mapM kcType ts
+  TTup rng ts -> do
+    ts' <- mapM (kcType (Just (KType ()))) ts
     forM_ (zip (map extOf ts) ts') $ \(trng, ct) ->
       emit $ CEqK (extOf ct) (KType ()) trng
+    downEqK rng mdown (KType ())
     return (TTup (KType ()) ts')
 
-  TList _ t -> do
-    t' <- kcType t
+  TList rng t -> do
+    t' <- kcType (Just (KType ())) t
     emit $ CEqK (extOf t') (KType ()) (extOf t)
+    downEqK rng mdown (KType ())
     return (TList (KType ()) t')
 
-  TFun _ t1 t2 -> do
-    t1' <- kcType t1
-    t2' <- kcType t2
+  TFun rng t1 t2 -> do
+    t1' <- kcType (Just (KType ())) t1
+    t2' <- kcType (Just (KType ())) t2
     emit $ CEqK (extOf t1') (KType ()) (extOf t1)
     emit $ CEqK (extOf t2') (KType ()) (extOf t2)
+    downEqK rng mdown (KType ())
     return (TFun (KType ()) t1' t2')
 
-  TCon rng n -> TCon <$> getKind' rng n <*> pure n
+  TCon rng n -> do
+    k <- getKind' rng n
+    downEqK rng mdown k
+    return (TCon k n)
 
-  TVar rng n -> TVar <$> getKind' rng n <*> pure n
+  TVar rng n -> do
+    k <- getKind' rng n
+    downEqK rng mdown k
+    return (TVar k n)
 
 tcFunDef :: PFunDef -> TCM CFunDef
 tcFunDef (FunDef _ name msig eqs) = do
@@ -273,7 +297,7 @@ tcFunDef (FunDef _ name msig eqs) = do
     raise (sconcatne (fmap extOf eqs)) "Function equations have differing numbers of arguments"
 
   typ <- case msig of
-    TypeSig sig -> kcType sig
+    TypeSig sig -> kcType (Just (KType ())) sig
     TypeSigExt NoTypeSig -> genUniVar (KType ())
 
   eqs' <- mapM (tcFunEq typ) eqs
@@ -326,18 +350,21 @@ solveKindVars cs = do
                  (\case KExt () (KUniVar v) -> Just v
                         _ -> Nothing)
                  kindSize
-                 (map (\(a, b, _) -> (a, b)) (toList cs))
+                 (toList cs)
   where
-    reduce :: CKind -> CKind -> (Bag (Int, CKind), Bag (CKind, CKind))
-    -- unification variables produce constraints on a unification variable
-    reduce (KExt () (KUniVar i)) (KExt () (KUniVar j)) | i == j = mempty
-    reduce (KExt () (KUniVar i)) k = (pure (i, k), mempty)
-    reduce k (KExt () (KUniVar i)) = (pure (i, k), mempty)
-    -- if lhs and rhs have equal prefixes, recurse
-    reduce (KType ()) (KType ()) = mempty
-    reduce (KFun () a b) (KFun () c d) = reduce a c <> reduce b d
-    -- otherwise, this is a kind mismatch
-    reduce k1 k2 = (mempty, pure (k1, k2))
+    reduce :: CKind -> CKind -> Range -> (Bag (Int, CKind, Range), Bag (CKind, CKind, Range))
+    reduce lhs rhs rng = case (lhs, rhs) of
+      -- unification variables produce constraints on a unification variable
+      (KExt () (KUniVar i), KExt () (KUniVar j)) | i == j -> mempty
+      (KExt () (KUniVar i), k                  ) -> (pure (i, k, rng), mempty)
+      (k                  , KExt () (KUniVar i)) -> (pure (i, k, rng), mempty)
+
+      -- if lhs and rhs have equal prefixes, recurse
+      (KType ()   , KType ()   ) -> mempty
+      (KFun () a b, KFun () c d) -> reduce a c rng <> reduce b d rng
+
+      -- otherwise, this is a kind mismatch
+      (k1, k2) -> (mempty, pure (k1, k2, rng))
 
     kindSize :: CKind -> Int
     kindSize KType{} = 1