forbid kind loops

.github/workflows/ci.yml

@@ -31,10 +31,6 @@ jobs:
             ghc: "9.2.5"
             os: ubuntu-latest
 
-          - cabal: "3.2"
-            ghc: "8.10.7"
-            os: ubuntu-latest
-
             # latest GHC, non-default OS
           - cabal: "3.8"
             ghc: "9.6"

examples/non-examples/kind-occurs-check.golden

@@ -0,0 +1,2 @@
+Infinite kind detected:
+  (KindVar 55708) = (META(KindVar 55708) → META(KindVar 55701))

examples/non-examples/kind-occurs-check.kl

@@ -0,0 +1,17 @@
+#lang "prelude.kl"
+
+(datatype (Phantom A)
+  (mk-phantom))
+
+-- causes the kind equality ?1 ~ ?2 to be unified twice, which previously
+-- caused ?2 to point to itself, thus causing zonking ?2 to run forever.
+-- should be accepted.
+(example
+  (with-unknown-type [A]
+    (the (Phantom A)
+      (mk-phantom))))
+
+-- causes the kind equality ?1 ~ (-> ?1 *).
+-- should be accepted by the occurs-check.
+(datatype (InfiniteKind A)
+  (mk-infinite-kind (Phantom (A A))))

examples/non-examples/type-occurs-check.golden

@@ -0,0 +1 @@
+Infinite type detected: (MetaPtr 57868) = (List META(MetaPtr 57868))

examples/non-examples/type-occurs-check.kl

@@ -0,0 +1,13 @@
+#lang "prelude.kl"
+
+-- accepted, thanks to let-generalization
+(example
+  (let [xs (nil)]
+    (:: xs  -- (the (List A) xs)
+        xs  -- (the (List (List A)) xs)
+        )))
+
+-- causes the type equality ?1 ~ List ?1, which must be rejected by the
+-- occurs-check.
+(defun infinite-type (xs)
+  (:: xs xs))

src/Expander/Error.hs

@@ -6,6 +6,7 @@ module Expander.Error
   ( ExpansionErr(..)
   , SyntacticCategory(..)
   , TypeCheckError(..)
+  , KindCheckError(..)
   , Tenon, tenon, Mortise, mortise
   , notRightLength
   ) where
@@ -63,10 +64,10 @@ data ExpansionErr
       (Mortise SyntacticCategory)
   | NotValidType Syntax
   | TypeCheckError TypeCheckError
+  | KindCheckError KindCheckError
   | WrongArgCount Syntax Constructor Int Int
   | NotAConstructor Syntax
   | WrongTypeArity Syntax TypeConstructor Natural Int
-  | KindMismatch (Maybe SrcLoc) Kind Kind
   | CircularImports ModuleName [ModuleName]
   deriving (Show)
 
@@ -97,6 +98,10 @@ data TypeCheckError
   | OccursCheckFailed MetaPtr Ty
   deriving (Show)
 
+data KindCheckError
+  = KindMismatch (Maybe SrcLoc) Kind Kind
+  | KindOccursCheckFailed KindVar Kind
+  deriving (Show)
 
 data SyntacticCategory
   = ModuleCat
@@ -216,6 +221,7 @@ instance Pretty VarInfo ExpansionErr where
   pp env (NotValidType stx) =
     hang 2 $ group $ vsep [text "Not a type:", pp env stx]
   pp env (TypeCheckError err) = pp env err
+  pp env (KindCheckError err) = pp env err
   pp env (WrongArgCount stx ctor wanted got) =
     hang 2 $
     vsep [ text "Wrong number of arguments for constructor" <+> pp env ctor
@@ -231,11 +237,6 @@ instance Pretty VarInfo ExpansionErr where
                   , text "Got" <+> viaShow got
                   , text "In" <+> align (pp env stx)
                   ]
-  pp env (KindMismatch loc k1 k2) =
-    hang 2 $ group $ vsep [ text "Kind mismatch at" <+>
-                            maybe (text "unknown location") (pp env) loc <> text "."
-                          , group $ vsep [pp env k1, text "≠", pp env k2]
-                          ]
   pp env (CircularImports current stack) =
     hang 2 $ vsep [ group $ vsep [ text "Circular imports while importing", pp env current]
                   , group $ hang 2 $ vsep (text "Context:" : map (pp env) stack)]
@@ -265,10 +266,21 @@ instance Pretty VarInfo TypeCheckError where
                  ]
 
   pp env (OccursCheckFailed ptr ty) =
-    hang 2 $ group $ vsep [ text "Occurs check failed:"
-                          , group (vsep [viaShow ptr, "≠", pp env ty])
+    hang 2 $ group $ vsep [ text "Infinite type detected:"
+                          , group (vsep [viaShow ptr, "=", pp env ty])
                           ]
 
+instance Pretty VarInfo KindCheckError where
+  pp env (KindMismatch loc k1 k2) =
+    hang 2 $ group $ vsep [ text "Kind mismatch at" <+>
+                            maybe (text "unknown location") (pp env) loc <> text "."
+                          , group $ vsep [pp env k1, text "≠", pp env k2]
+                          ]
+
+  pp env (KindOccursCheckFailed ptr ty) =
+    hang 2 $ group $ vsep [ text "Infinite kind detected:"
+                          , group (vsep [viaShow ptr, "=", pp env ty])
+                          ]
 
 instance Pretty VarInfo SyntacticCategory where
   pp _env ExpressionCat = text "an expression"

src/Expander/TC.hs

@@ -306,15 +306,57 @@ typeVarKind ptr =
     Just v -> pure $ view varKind v
 
 
-setKindVar :: KindVar -> Kind -> Expand ()
-setKindVar v k@(KMetaVar v') =
-  (view (expanderKindStore . at v') <$> getState) >>=
-  \case
-    Nothing -> modifyState $ set (expanderKindStore . at v) (Just k)
-    -- Path compression step
-    Just k' -> setKindVar v k'
-setKindVar v k = modifyState $ set (expanderKindStore . at v) (Just k)
+kindMetas :: Kind -> Expand [KindVar]
+kindMetas k = do
+  k' <- zonkKind k
+  case k' of
+    KMetaVar v' ->
+      (view (expanderKindStore . at v') <$> getState) >>=
+      \case
+        Nothing -> pure [v']
+        Just k'' -> kindMetas k''
+    KStar -> pure []
+    KFun k1 k2 -> (++) <$> kindMetas k1 <*> kindMetas k2
+
+
+-- pre-condition: 'v' zonks to itself.
+-- post-condition: 'k' zonks to a kind which does not contain 'v'.
+kindOccursCheck :: KindVar -> Kind -> Expand ()
+kindOccursCheck v k = do
+  free <- kindMetas k
+  if v `elem` free
+    then do
+      k' <- zonkKind k
+      throwError $ KindCheckError $ KindOccursCheckFailed v k'
+    else pure ()
 
+-- pre-condition: 'v' zonks to itself.
+-- post-condition: @KMetaVar v@, 'k', and the return value all zonk to the same
+-- kind.
+setKindVar :: KindVar -> Kind -> Expand Kind
+setKindVar v k@(KMetaVar v')
+  | v == v' =
+      pure k
+  | otherwise =
+      (view (expanderKindStore . at v') <$> getState) >>=
+      \case
+        Nothing -> do
+          kindOccursCheck v k
+          modifyState $ set (expanderKindStore . at v) (Just k)
+          pure k
+        Just k' -> do
+          -- Recur to the root, both to compress the path from 'v' and to
+          -- make sure we don't make 'v' point indirectly to itself.
+          k'' <- setKindVar v k'
+          -- Also compress v'
+          modifyState $ set (expanderKindStore . at v') (Just k'')
+          pure k''
+setKindVar v k = do
+  kindOccursCheck v k
+  modifyState $ set (expanderKindStore . at v) (Just k)
+  pure k
+
+-- post-condition: 'kind1' and 'kind2' both zonk to the same kind.
 equateKinds :: UnificationErrorBlame blame => blame -> Kind -> Kind -> Expand ()
 equateKinds blame kind1 kind2 =
   equateKinds' kind1 kind2 >>=
@@ -324,7 +366,7 @@ equateKinds blame kind1 kind2 =
       k1' <- zonkKind kind1
       k2' <- zonkKind kind2
       loc <- getBlameLoc blame
-      throwError $ KindMismatch loc k1' k2'
+      throwError $ KindCheckError $ KindMismatch loc k1' k2'
   where
     -- Rigid-rigid cases
     equateKinds' KStar KStar = pure True