fix: ensure type variables kinds are consistent (#1055)

Previously, we didn't check that type variables had consistent kinds in
type definitions, which could lead to improper types. For example, one
could define:

    (deftype (Foo f a b) [x (f a) y f])

without issues even though this type is invalid since the variable `f`
is assigned two distinct kinds (nullary: * and unary: *->*).

This commit adds a check to ensure all of the instances of a type
variable in a type definition have the same kind. It also fixes an issue
whereby only higher-kinded types of one argument were allowed as type
members; now higher-kinded types of any arity are permitted (again
assuming variable kinds are consistent).

When a user writes a type that has variables with inconsistent kinds,
they will be hit with an error:

    (deftype (Foo (f a) b) [x (f a) y f])
    Invalid type definition for 'Foo':

    The type variable `f` is used inconsistently: (f a), f Type
    variables must be applied to the same number of arguments.

    Traceback:
    (deftype (Foo (f a) b) [x (f a) y f]) at REPL:1:1.

src/TypeError.hs

@@ -58,6 +58,7 @@ data TypeError
   | DefinitionsMustBeAtToplevel XObj
   | UsingDeadReference XObj String
   | UninhabitedConstructor Ty XObj Int Int
+  | InconsistentKinds String [XObj]
 
 instance Show TypeError where
   show (SymbolMissingType xobj env) =
@@ -312,6 +313,8 @@ instance Show TypeError where
     "The reference '" ++ pretty xobj ++ "' (depending on the variable '" ++ dependsOn ++ "') isn't alive at " ++ prettyInfoFromXObj xobj ++ "."
   show (UninhabitedConstructor ty xobj got wanted) =
     "Can't use a struct or sumtype constructor without arguments as a member type at " ++ prettyInfoFromXObj xobj ++ ". The type constructor " ++ show ty ++ " expects " ++ show wanted ++ " arguments but got " ++ show got
+  show (InconsistentKinds varName xobjs) =
+    " The type variable `" ++ varName ++ "` is used inconsistently: " ++ joinWithComma (map pretty (filter (doesTypeContainTyVarWithName varName . fromMaybe Universe . xobjToTy) xobjs)) ++ " Type variables must be applied to the same number of arguments."
 
 machineReadableErrorStrings :: FilePathPrintLength -> TypeError -> [String]
 machineReadableErrorStrings fppl err =
@@ -428,6 +431,8 @@ machineReadableErrorStrings fppl err =
       [machineReadableInfoFromXObj fppl xobj ++ " The reference '" ++ pretty xobj ++ "' isn't alive."]
     (UninhabitedConstructor ty xobj got wanted) ->
       [machineReadableInfoFromXObj fppl xobj ++ "Can't use a struct or sumtype constructor without arguments as a member type at " ++ prettyInfoFromXObj xobj ++ ". The type constructor " ++ show ty ++ " expects " ++ show wanted ++ " arguments but got " ++ show got]
+    (InconsistentKinds varName xobjs) ->
+      [machineReadableInfoFromXObj fppl (head xobjs) ++ " The type variable `" ++ varName ++ "` is used inconsistently: " ++ joinWithComma (map pretty (filter (doesTypeContainTyVarWithName varName . fromMaybe Universe . xobjToTy) xobjs)) ++ " Type variables must be applied to the same number of arguments."]
     _ ->
       [show err]
 

src/Types.hs

@@ -19,6 +19,7 @@ module Types
     consPath,
     Kind,
     tyToKind,
+    areKindsConsistent,
   )
 where
 
@@ -72,6 +73,56 @@ tyToKind (PointerTy _) = Higher
 tyToKind (RefTy _ _) = Higher -- Refs may also be treated as a data constructor
 tyToKind _ = Base
 
+-- | Check whether or not the kinds of type variables are consistent.
+-- This function will return Left as soon as a variable is used inconsistently,
+-- reporting which variable triggered the issue.
+-- If all variables are used consistently, it will process the whole list and
+-- return ().
+--
+-- Kind arity matters; that is, `(f a b)` is not consistent with
+-- `(f b)`. So long as the kind of a variable is the same across its uses,
+-- everything is OK, for example:
+--     ((Foo f a b) [x (f a) y (f b)])
+-- is valid, and so is
+--     ((Foo f a b) [x f y a z b])
+-- But a definition such as:
+--     ((Foo f a b) [x (f a b) y (f a)])
+-- is inconsistent (kind of `f` differs) and so is
+--     ((Foo f a b) [x (f a) y b (b a)])
+-- (kind of `b` is inconsistent.
+areKindsConsistent :: [Ty] -> Either String ()
+areKindsConsistent typeVars =
+  assignKinds typeVars Map.empty
+  where
+    assignKinds :: [Ty] -> Map.Map String Int -> Either String ()
+    assignKinds (struct@(StructTy (VarTy name) vars) : rest) arityMap =
+      case Map.lookup name arityMap of
+        Nothing -> assignKinds next (Map.insert name kind arityMap)
+        Just k ->
+          if k == kind
+            then assignKinds next arityMap
+            else (Left name)
+      where
+        next = (vars ++ rest)
+        kind = (length vars)
+    assignKinds (var@(VarTy v) : rest) arityMap =
+      case Map.lookup v arityMap of
+        Nothing -> assignKinds rest (Map.insert v kind arityMap)
+        Just k ->
+          if k == kind
+            then assignKinds rest arityMap
+            else (Left v)
+      where
+        kind = 0
+    assignKinds (FuncTy args ret _ : rest) arityMap =
+      assignKinds (args ++ ret : rest) arityMap
+    assignKinds ((PointerTy p) : rest) arityMap =
+      assignKinds (p : rest) arityMap
+    assignKinds ((RefTy r _) : rest) arityMap =
+      assignKinds (r : rest) arityMap
+    assignKinds (_ : rest) arityMap = assignKinds rest arityMap
+    assignKinds [] _ = pure ()
+
 -- Exactly like '==' for Ty, but ignore lifetime parameter
 typeEqIgnoreLifetimes :: Ty -> Ty -> Bool
 typeEqIgnoreLifetimes (RefTy a _) (RefTy b _) = a == b
@@ -83,10 +134,11 @@ typeEqIgnoreLifetimes (StructTy a tyVarsA) (StructTy b tyVarsB) =
     && all (== True) (zipWith typeEqIgnoreLifetimes tyVarsA tyVarsB)
 typeEqIgnoreLifetimes a b = a == b
 
-data SumTyCase = SumTyCase
-  { caseName :: String,
-    caseMembers :: [(String, Ty)]
-  }
+data SumTyCase
+  = SumTyCase
+      { caseName :: String,
+        caseMembers :: [(String, Ty)]
+      }
   deriving (Show, Ord, Eq)
 
 fnOrLambda :: String

src/Validate.hs

@@ -1,12 +1,15 @@
 module Validate where
 
+import Control.Monad (foldM)
 import Data.Function (on)
-import Data.List (nubBy, (\\))
+import Data.List ((\\), nubBy)
+import Data.Maybe (fromJust)
 import Lookup
 import Managed
 import Obj
 import TypeError
 import Types
+import TypePredicates
 import Util
 
 {-# ANN validateMembers "HLint: ignore Eta reduce" #-}
@@ -24,26 +27,36 @@ validateMemberCases typeEnv typeVariables rest = mapM_ visit rest
 
 validateMembers :: TypeEnv -> [Ty] -> [XObj] -> Either TypeError ()
 validateMembers typeEnv typeVariables membersXObjs =
-  checkUnevenMembers >> checkDuplicateMembers >> checkMembers
+  checkUnevenMembers >> checkDuplicateMembers >> checkKindConsistency >> checkMembers
   where
+    pairs = pairwise membersXObjs
+    -- Are the number of members even?
+    checkUnevenMembers :: Either TypeError ()
     checkUnevenMembers =
       if length membersXObjs `mod` 2 == 0
         then Right ()
         else Left (UnevenMembers membersXObjs)
-    pairs = pairwise membersXObjs
-    fields = fst <$> pairs
-    uniqueFields = nubBy ((==) `on` xobjObj) fields
-    dups = fields \\ uniqueFields
+    -- Are any members duplicated?
+    checkDuplicateMembers :: Either TypeError ()
     checkDuplicateMembers =
       if length fields == length uniqueFields
         then Right ()
         else Left (DuplicatedMembers dups)
+      where
+        fields = fst <$> pairs
+        uniqueFields = nubBy ((==) `on` xobjObj) fields
+        dups = fields \\ uniqueFields
+    -- Do all type variables have consistent kinds?
+    checkKindConsistency :: Either TypeError ()
+    checkKindConsistency =
+      case areKindsConsistent varsOnly of
+        Left var -> Left (InconsistentKinds var membersXObjs)
+        _ -> pure ()
+      where
+        varsOnly = filter isTypeGeneric (map (fromJust . xobjToTy . snd) pairs)
+    checkMembers :: Either TypeError ()
     checkMembers = mapM_ (okXObjForType typeEnv typeVariables . snd) pairs
 
--- validateOneCase :: XObj -> a
--- validateOneCase XObj {} =
---   error "Type members must be defined using array syntax: [member1 type1 member2 type2 ...]" -- | TODO: How to reach this case?
-
 okXObjForType :: TypeEnv -> [Ty] -> XObj -> Either TypeError ()
 okXObjForType typeEnv typeVariables xobj =
   case xobjToTy xobj of
@@ -53,66 +66,77 @@ okXObjForType typeEnv typeVariables xobj =
 -- | Can this type be used as a member for a deftype?
 canBeUsedAsMemberType :: TypeEnv -> [Ty] -> Ty -> XObj -> Either TypeError ()
 canBeUsedAsMemberType typeEnv typeVariables ty xobj =
-  case ty of
-    UnitTy -> pure ()
-    IntTy -> pure ()
-    FloatTy -> pure ()
-    DoubleTy -> pure ()
-    ByteTy -> pure ()
-    LongTy -> pure ()
-    BoolTy -> pure ()
-    StringTy -> pure ()
-    PatternTy -> pure ()
-    CharTy -> pure ()
-    FuncTy {} -> pure ()
-    PointerTy UnitTy -> pure ()
-    PointerTy inner -> do
-      _ <- canBeUsedAsMemberType typeEnv typeVariables inner xobj
-      pure ()
-    StructTy (ConcreteNameTy "Array") [inner] -> do
-      _ <- canBeUsedAsMemberType typeEnv typeVariables inner xobj
-      pure ()
-    StructTy name [tyVars] ->
-      case name of
-        (ConcreteNameTy name') ->
-          -- ensure structs are filled with values
-          -- Prevents deftypes such as (deftype Player [pos Vector3])
-          do
-            _ <- canBeUsedAsMemberType typeEnv typeVariables tyVars xobj
-            case lookupBinder (SymPath [] name') (getTypeEnv typeEnv) of
-              Just _ -> pure ()
-              Nothing -> Left (NotAmongRegisteredTypes ty xobj)
-        -- e.g. (deftype (Higher (f a)) (Of [(f a)]))
-        (VarTy _) -> pure ()
-    s@(StructTy name tyvar) ->
-      if isExternalType typeEnv s
-        then pure ()
-        else case name of
-          (ConcreteNameTy n) ->
-            case lookupBinder (SymPath [] n) (getTypeEnv typeEnv) of
-              Just (Binder _ (XObj (Lst (XObj (Deftype t) _ _ : _)) _ _)) ->
-                checkInhabitants t
-              Just (Binder _ (XObj (Lst (XObj (DefSumtype t) _ _ : _)) _ _)) ->
-                checkInhabitants t
-              _ -> Left (InvalidMemberType ty xobj)
-            where
-              -- Make sure any struct types have arguments before they can be used as members.
-
-              checkInhabitants t =
-                case t of
-                  (StructTy _ vars) ->
-                    if length vars == length tyvar
-                      then pure ()
-                      else Left (UninhabitedConstructor ty xobj (length tyvar) (length vars))
-                  _ -> Left (InvalidMemberType ty xobj)
-          _ -> Left (InvalidMemberType ty xobj)
-    VarTy _ ->
-      if foldr (||) False (map (isCaptured ty) typeVariables)
+  if isExternalType typeEnv ty
+    then pure ()
+    else case ty of
+      UnitTy -> pure ()
+      IntTy -> pure ()
+      FloatTy -> pure ()
+      DoubleTy -> pure ()
+      ByteTy -> pure ()
+      LongTy -> pure ()
+      BoolTy -> pure ()
+      StringTy -> pure ()
+      PatternTy -> pure ()
+      CharTy -> pure ()
+      FuncTy {} -> pure ()
+      PointerTy UnitTy -> pure ()
+      PointerTy inner ->
+        canBeUsedAsMemberType typeEnv typeVariables inner xobj
+          >> pure ()
+      -- Struct variables may appear as complete applications or individual
+      -- components in the head of a definition; that is the forms:
+      --     ((Foo (f a b)) [x (f a b)])
+      --     ((Foo f a b) [x f y a z b])
+      -- are both valid, but restrict their types differently. In the former,
+      -- `f` may only appear in complete applications over `a` and `b`, in
+      -- other words, `f` is closed over `a` and `b`. In the latter, f may
+      -- flexibly be used as a type variable of nullary kind, or as a type
+      -- variable of unary kind `(Foo f a b) [x (f a) y (f b)])` so long as
+      -- the kinds of each occasion of `f` are consistent.
+      --
+      -- Likewise, the types denoted by:
+      --     ((Foo (f a) b) ...)
+      -- and
+      --     ((Foo (f a) (f b)) ...)
+      -- differ.
+      -- Attempt the first, more restrictive formulation first.
+      struct@(StructTy name tyVars) ->
+        checkVar struct <> checkStruct name tyVars
+      v@(VarTy _) -> checkVar v
+      _ -> Left (InvalidMemberType ty xobj)
+  where
+    checkStruct :: Ty -> [Ty] -> Either TypeError ()
+    checkStruct (ConcreteNameTy "Array") [innerType] =
+      canBeUsedAsMemberType typeEnv typeVariables innerType xobj
+        >> pure ()
+    checkStruct (ConcreteNameTy n) vars =
+      case lookupBinder (SymPath [] n) (getTypeEnv typeEnv) of
+        Just (Binder _ (XObj (Lst (XObj (Deftype t) _ _ : _)) _ _)) ->
+          checkInhabitants t >> foldM (\_ typ -> canBeUsedAsMemberType typeEnv typeVariables typ xobj) () vars
+        Just (Binder _ (XObj (Lst (XObj (DefSumtype t) _ _ : _)) _ _)) ->
+          checkInhabitants t >> foldM (\_ typ -> canBeUsedAsMemberType typeEnv typeVariables typ xobj) () vars
+        _ -> Left (NotAmongRegisteredTypes ty xobj)
+      where
+        checkInhabitants :: Ty -> Either TypeError ()
+        checkInhabitants (StructTy _ vs) =
+          if (length vs == length vars)
+            then pure ()
+            else Left (UninhabitedConstructor ty xobj (length vs) (length vars))
+        checkInhabitants _ = Left (InvalidMemberType ty xobj)
+    checkStruct v@(VarTy _) vars =
+      canBeUsedAsMemberType typeEnv typeVariables v xobj
+        >> foldM (\_ typ -> canBeUsedAsMemberType typeEnv typeVariables typ xobj) () vars
+    checkVar :: Ty -> Either TypeError ()
+    checkVar variable =
+      if foldr (||) False (map (isCaptured variable) typeVariables)
         then pure ()
         else Left (InvalidMemberType ty xobj)
       where
         -- If a variable `a` appears in a higher-order polymorphic form, such as `(f a)`
-        -- `a` may be used as a member, sans `f`.
+        -- `a` may be used as a member, sans `f`, but `f` may not appear
+        -- without `a`.
+        isCaptured :: Ty -> Ty -> Bool
         isCaptured t v@(VarTy _) = t == v
+        isCaptured sa@(StructTy (VarTy _) _) sb@(StructTy (VarTy _) _) = sa == sb
         isCaptured t (StructTy (VarTy _) vars) = any (== t) vars
-    _ -> Left (InvalidMemberType ty xobj)