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))

klister.cabal

@@ -81,6 +81,7 @@ library
       PartialType
       Phase
       Pretty
+      Pretty.Renumber
       Scope
       ScopeSet
       ShortShow

src/Expander.hs

@@ -544,15 +544,17 @@ initializeKernel outputChannel = do
       | (name, fun) <- [("<", (<)), ("<=", (<=)), (">", (>)), (">=", (>=)), ("=", (==)), ("/=", (/=))]
       ] ++
       [ ("pure-IO"
-        , Scheme [KStar, KStar] $ tFun [tSchemaVar 0 []] (tIO (tSchemaVar 0 []))
+        , let a = tSchemaVar firstSchemeVar []
+          in Scheme [KStar, KStar] $ tFun [a] (tIO a)
         , ValueClosure $ HO $ \v -> ValueIOAction (pure v)
         )
       , ("bind-IO"
-        , Scheme [KStar, KStar] $
-          tFun [ tIO (tSchemaVar 0 [])
-               , tFun [tSchemaVar 0 []] (tIO (tSchemaVar 1 []))
-               ]
-               (tIO (tSchemaVar 1 []))
+        , let a:b:_ = [tSchemaVar i [] | i <- [firstSchemeVar..]]
+          in Scheme [KStar, KStar] $
+             tFun [ tIO a
+                  , tFun [a] (tIO b)
+                  ]
+                  (tIO b)
         , ValueClosure $ HO $ \(ValueIOAction mx) -> do
             ValueClosure $ HO $ \(ValueClosure f) -> do
               ValueIOAction $ do
@@ -596,22 +598,25 @@ initializeKernel outputChannel = do
       , ("Unit", [], [("unit", [])])
       , ("Bool", [], [("true", []), ("false", [])])
       , ("Problem", [], [("module", []), ("declaration", []), ("type", []), ("expression", [tType]), ("pattern", []), ("type-pattern", [])])
-      , ("Maybe", [KStar], [("nothing", []), ("just", [tSchemaVar 0 []])])
-      , ("List"
-        , [KStar]
-        , [ ("nil", [])
-          , ("::", [tSchemaVar 0 [], Prims.primitiveDatatype "List" [tSchemaVar 0 []]])
-          ]
-        )
+      , let a = tSchemaVar firstSchemeVar []
+        in ("Maybe", [KStar], [("nothing", []), ("just", [a])])
+      , let a = tSchemaVar firstSchemeVar []
+        in ("List"
+           , [KStar]
+           , [ ("nil", [])
+             , ("::", [a, Prims.primitiveDatatype "List" [a]])
+             ]
+           )
       , ("Syntax-Contents"
         , [KStar]
-        , [ ("list-contents", [Prims.primitiveDatatype "List" [tSchemaVar 0 []]])
-          , ("integer-contents", [tInteger])
-          , ("string-contents", [tString])
-          , ("identifier-contents", [tString])
-          -- if you add a constructor here, remember to also add a
-          -- corresponding pattern in close-syntax!
-          ]
+        , let a = tSchemaVar firstSchemeVar []
+          in [ ("list-contents", [Prims.primitiveDatatype "List" [a]])
+             , ("integer-contents", [tInteger])
+             , ("string-contents", [tString])
+             , ("identifier-contents", [tString])
+             -- if you add a constructor here, remember to also add a
+             -- corresponding pattern in close-syntax!
+             ]
         )
       ]
 
@@ -1211,8 +1216,9 @@ expandOneForm prob stx
           case prob of
             ExprDest t dest -> do
               argTys <- traverse makeTypeMeta argKinds
+              let tyStore = S.fromList $ zip [firstSchemeVar..] argTys
               unify dest t $ tDatatype dt argTys
-              args' <- for args \a -> inst dest (Scheme argKinds a) argTys
+              args' <- for args \a -> inst dest (Scheme argKinds a) tyStore
               Stx _ _ (foundName, foundArgs) <- mustBeCons stx
               _ <- mustBeIdent foundName
               argDests <-
@@ -1225,8 +1231,9 @@ expandOneForm prob stx
             PatternDest patTy dest -> do
               Stx _ loc (_cname, subPats) <- mustBeCons stx
               tyArgs <- traverse makeTypeMeta argKinds
+              let tyStore = S.fromList $ zip [firstSchemeVar..] tyArgs
               argTypes <- for args \ a ->
-                            inst loc (Scheme argKinds a) tyArgs
+                            inst loc (Scheme argKinds a) tyStore
               unify loc (tDatatype dt tyArgs) patTy
               if length subPats /= length argTypes
                 then throwError $ WrongArgCount stx ctor (length argTypes) (length subPats)

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 v k) =
+    hang 2 $ group $ vsep [ text "Infinite kind detected:"
+                          , group (vsep [viaShow v, "=", pp env k])
+                          ]
 
 instance Pretty VarInfo SyntacticCategory where
   pp _env ExpressionCat = text "an expression"

src/Expander/Monad.hs

@@ -240,7 +240,7 @@ data EValue
   | EPrimPatternMacro (Either (Ty, PatternPtr) TypePatternPtr -> Syntax -> Expand ())
   | EPrimUniversalMacro (MacroDest -> Syntax -> Expand ())
   | EVarMacro !Var -- ^ For bound variables (the Unique is the binding site of the var)
-  | ETypeVar !Kind !Natural
+  | ETypeVar !Kind !SchemeVar
   -- ^ For bound type variables (user-written Skolem variables or in datatype definitions)
   | EUserMacro !MacroVar -- ^ For user-written macros
   | EIncompleteMacro !MacroVar !Ident !SplitCorePtr -- ^ Macros that are themselves not yet ready to go

src/Expander/Primitives.hs

@@ -68,7 +68,6 @@ import Control.Monad.Except
 import Data.Text (Text)
 import qualified Data.Text as T
 import Data.Traversable
-import Numeric.Natural
 
 import Binding
 import Core
@@ -130,7 +129,7 @@ datatype dest outScopesDest stx = do
   Stx scs loc (_ :: Syntax, more) <- mustBeCons stx
   Stx _ _ (nameAndArgs, ctorSpecs) <- mustBeCons (Syntax (Stx scs loc (List more)))
   Stx _ _ (name, args) <- mustBeCons nameAndArgs
-  typeArgs <- for (zip [0..] args) $ \(i, a) ->
+  typeArgs <- for (zip [firstSchemeVar..] args) $ \(i, a) ->
     prepareTypeVar i a
   sc <- freshScope $ T.pack $ "For datatype at " ++ shortShow (stxLoc stx)
   let typeScopes = map (view _1) typeArgs ++ [sc]
@@ -712,7 +711,7 @@ scheduleTypePattern exprTy (Stx _ _ (patStx, rhsStx@(Syntax (Stx _ loc _)))) = d
   forkExpanderTask $ AwaitingTypePattern dest exprTy rhsDest rhsStx
   return (dest, rhsDest)
 
-prepareTypeVar :: Natural -> Syntax -> Expand (Scope, Ident, Kind)
+prepareTypeVar :: SchemeVar -> Syntax -> Expand (Scope, Ident, Kind)
 prepareTypeVar i varStx = do
   (sc, α, b) <- varPrepHelper varStx
   k <- KMetaVar <$> liftIO newKindVar

src/Expander/Syntax.hs

@@ -3,6 +3,7 @@
 {-# LANGUAGE MultiParamTypeClasses #-}
 {-# LANGUAGE OverloadedStrings #-}
 {-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE TypeOperators #-}
 
 -- | Utilities for analyzing the form of syntax in the expander monad
 module Expander.Syntax where