From 21942371f0dd5ce2a6cf18a80465844990c6c64c Mon Sep 17 00:00:00 2001 From: Travis Staton Date: Wed, 4 Oct 2023 12:45:30 -0400 Subject: [PATCH] Rename kinds: Star -> Type, Effect -> Ability --- .../src/Unison/KindInference.hs | 2 +- .../Unison/KindInference/Constraint/Pretty.hs | 16 +++--- .../KindInference/Constraint/Provenance.hs | 1 + .../Unison/KindInference/Constraint/Solved.hs | 8 +-- .../Constraint/StarProvenance.hs | 2 +- .../KindInference/Constraint/Unsolved.hs | 14 ++--- .../src/Unison/KindInference/Generate.hs | 54 +++++++++---------- .../src/Unison/KindInference/Solve.hs | 34 ++++++------ .../transcripts/kind-inference.output.md | 43 +++++++-------- 9 files changed, 88 insertions(+), 86 deletions(-) diff --git a/parser-typechecker/src/Unison/KindInference.hs b/parser-typechecker/src/Unison/KindInference.hs index 4ed31a9968..4980c6b323 100644 --- a/parser-typechecker/src/Unison/KindInference.hs +++ b/parser-typechecker/src/Unison/KindInference.hs @@ -1,6 +1,6 @@ -- | Kind inference for Unison -- --- Unison has *, ->, and Effect kinds +-- Unison has Type, ->, and Ability kinds -- -- An algorithm sketch: First break all decls into strongly connected -- components in reverse topological order. Then, for each component, diff --git a/parser-typechecker/src/Unison/KindInference/Constraint/Pretty.hs b/parser-typechecker/src/Unison/KindInference/Constraint/Pretty.hs index bf29cc7363..5f261aa2cb 100644 --- a/parser-typechecker/src/Unison/KindInference/Constraint/Pretty.hs +++ b/parser-typechecker/src/Unison/KindInference/Constraint/Pretty.hs @@ -28,11 +28,11 @@ import Unison.Var (Var) arrPrec :: Int arrPrec = 1 -prettyEffect :: Int -> P.Pretty P.ColorText -prettyEffect _prec = "Effect" +prettyAbility :: Int -> P.Pretty P.ColorText +prettyAbility _prec = "Ability" -prettyStar :: Int -> P.Pretty P.ColorText -prettyStar _prec = "*" +prettyType :: Int -> P.Pretty P.ColorText +prettyType _prec = "Type" prettyUnknown :: Int -> P.Pretty P.ColorText prettyUnknown _prec = "_" @@ -50,8 +50,8 @@ prettyCyclicSolvedConstraint :: Set (UVar v loc) -> Solve v loc (P.Pretty P.ColorText, Set (UVar v loc)) prettyCyclicSolvedConstraint constraint prec nameMap visitingSet = case constraint of - Solved.IsEffect _ -> pure (prettyEffect prec, Set.empty) - Solved.IsStar _ -> pure (prettyStar prec, Set.empty) + Solved.IsAbility _ -> pure (prettyAbility prec, Set.empty) + Solved.IsType _ -> pure (prettyType prec, Set.empty) Solved.IsArr _ a b -> do (pa, cyclicLhs) <- case Set.member a visitingSet of True -> pure (nameMap Map.! a, Set.singleton a) @@ -102,8 +102,8 @@ prettySolvedConstraint ppe constraints c = prettySolvedConstraint' :: Var v => Int -> Solved.Constraint (UVar v loc) v loc -> Solve v loc (P.Pretty P.ColorText) prettySolvedConstraint' prec = \case - Solved.IsEffect _ -> pure (prettyEffect prec) - Solved.IsStar _ -> pure (prettyStar prec) + Solved.IsAbility _ -> pure (prettyAbility prec) + Solved.IsType _ -> pure (prettyType prec) Solved.IsArr _ a b -> do a <- prettyUVarKind' (arrPrec + 1) a b <- prettyUVarKind' arrPrec b diff --git a/parser-typechecker/src/Unison/KindInference/Constraint/Provenance.hs b/parser-typechecker/src/Unison/KindInference/Constraint/Provenance.hs index 7179bd31df..bf35d48bdb 100644 --- a/parser-typechecker/src/Unison/KindInference/Constraint/Provenance.hs +++ b/parser-typechecker/src/Unison/KindInference/Constraint/Provenance.hs @@ -18,3 +18,4 @@ data Provenance v loc loc :: Lens' (Provenance v loc) loc loc f = \case Provenance ctx x -> Provenance ctx <$> f x +{-# INLINE loc #-} diff --git a/parser-typechecker/src/Unison/KindInference/Constraint/Solved.hs b/parser-typechecker/src/Unison/KindInference/Constraint/Solved.hs index 9e2f3c2650..b5fe4ba0eb 100644 --- a/parser-typechecker/src/Unison/KindInference/Constraint/Solved.hs +++ b/parser-typechecker/src/Unison/KindInference/Constraint/Solved.hs @@ -16,8 +16,8 @@ import Unison.KindInference.Constraint.StarProvenance qualified as SP -- These constraints are associated with unification variables during -- kind inference. data Constraint uv v loc - = IsStar (StarProvenance v loc) - | IsEffect (Provenance v loc) + = IsType (StarProvenance v loc) + | IsAbility (Provenance v loc) | IsArr (Provenance v loc) uv uv deriving stock (Show, Eq, Ord) @@ -28,8 +28,8 @@ prov :: (Provenance v loc) (Provenance v loc') prov f = \case - IsStar x -> IsStar <$> SP.prov f x - IsEffect x -> IsEffect <$> f x + IsType x -> IsType <$> SP.prov f x + IsAbility x -> IsAbility <$> f x IsArr l a b -> (\x -> IsArr x a b) <$> f l {-# INLINE prov #-} diff --git a/parser-typechecker/src/Unison/KindInference/Constraint/StarProvenance.hs b/parser-typechecker/src/Unison/KindInference/Constraint/StarProvenance.hs index e18457f7e8..e273d49710 100644 --- a/parser-typechecker/src/Unison/KindInference/Constraint/StarProvenance.hs +++ b/parser-typechecker/src/Unison/KindInference/Constraint/StarProvenance.hs @@ -7,7 +7,7 @@ where import Control.Lens (Traversal) import Unison.KindInference.Constraint.Provenance (Provenance) --- | Provenance of an @IsStar@ constraint. @IsStar@ constraints arise +-- | Provenance of an @IsType@ constraint. @IsType@ constraints arise -- in constraint generation (in which case it will have a -- @Provenance@) and also in the solver through kind-defaulting on -- unconstrained unification variables. diff --git a/parser-typechecker/src/Unison/KindInference/Constraint/Unsolved.hs b/parser-typechecker/src/Unison/KindInference/Constraint/Unsolved.hs index d77d5570fb..a1f8818d0f 100644 --- a/parser-typechecker/src/Unison/KindInference/Constraint/Unsolved.hs +++ b/parser-typechecker/src/Unison/KindInference/Constraint/Unsolved.hs @@ -15,13 +15,13 @@ import Unison.KindInference.Constraint.Provenance qualified as Provenance -- These are produced during constraint generation and given as input -- to the constraint solver. data Constraint uv v loc starProv - = -- | An IsStar constraint may arise from generation or from the + = -- | An IsType constraint may arise from generation or from the -- solver. During generation the provenance is always a real -- source code location, but the solver defaults unconstrained -- kind vars to Star. - IsStar uv (starProv v loc) + IsType uv (starProv v loc) | IsArr uv (Provenance v loc) uv uv - | IsEffect uv (Provenance v loc) + | IsAbility uv (Provenance v loc) | Unify (Provenance v loc) uv uv deriving stock (Show, Eq, Ord) @@ -32,8 +32,8 @@ starProv :: (prov v loc) (prov' v loc) starProv f = \case - IsStar x l -> IsStar x <$> f l - IsEffect x l -> pure (IsEffect x l) + IsType x l -> IsType x <$> f l + IsAbility x l -> pure (IsAbility x l) IsArr s l a b -> pure (IsArr s l a b) Unify l a b -> pure (Unify l a b) {-# INLINE starProv #-} @@ -45,8 +45,8 @@ prov :: (Provenance v loc) (Provenance v loc') prov f = \case - IsStar x l -> IsStar x <$> f l - IsEffect x l -> IsEffect x <$> f l + IsType x l -> IsType x <$> f l + IsAbility x l -> IsAbility x <$> f l IsArr s l a b -> (\x -> IsArr s x a b) <$> f l Unify l a b -> (\x -> Unify x a b) <$> f l {-# INLINE prov #-} diff --git a/parser-typechecker/src/Unison/KindInference/Generate.hs b/parser-typechecker/src/Unison/KindInference/Generate.hs index 6dbc57d75d..4fcf3e8ce1 100644 --- a/parser-typechecker/src/Unison/KindInference/Generate.hs +++ b/parser-typechecker/src/Unison/KindInference/Generate.hs @@ -7,15 +7,15 @@ module Unison.KindInference.Generate where import Control.Lens ((^.)) -import Unison.Kind qualified as Unison -import Unison.ConstructorReference (GConstructorReference (..)) import Data.Foldable (foldlM) import Data.Set qualified as Set import U.Core.ABT qualified as ABT import Unison.Builtin.Decls (rewriteTypeRef) import Unison.Codebase.BuiltinAnnotation (BuiltinAnnotation (builtinAnnotation)) +import Unison.ConstructorReference (GConstructorReference (..)) import Unison.DataDeclaration (Decl, asDataDecl) import Unison.DataDeclaration qualified as DD +import Unison.Kind qualified as Unison import Unison.KindInference.Constraint.Context (ConstraintContext (..)) import Unison.KindInference.Constraint.Provenance (Provenance (..)) import Unison.KindInference.Constraint.Provenance qualified as Provenance @@ -26,7 +26,7 @@ import Unison.Prelude import Unison.Reference (Reference) import Unison.Term qualified as Term import Unison.Type qualified as Type -import Unison.Var +import Unison.Var (Type (User), Var (typed), freshIn) data ConstraintTree v loc = Node [ConstraintTree v loc] @@ -37,7 +37,7 @@ data ConstraintTree v loc newtype TreeWalk = TreeWalk (forall a. ([a] -> [a]) -> [([a] -> [a], [a] -> [a])] -> [a] -> [a]) bottomUp :: TreeWalk -bottomUp = TreeWalk \down pairs0 -> foldr (\(d,u) b -> d . u . b) id pairs0 . down +bottomUp = TreeWalk \down pairs0 -> foldr (\(d, u) b -> d . u . b) id pairs0 . down flatten :: TreeWalk -> ConstraintTree v loc -> [GeneratedConstraint v loc] flatten (TreeWalk f) = ($ []) . flattenTop @@ -81,10 +81,10 @@ typeConstraintTree resultVar term@ABT.Term {annotation, out} = do codConstraints <- typeConstraintTree k2 cod pure $ Constraint - (IsStar resultVar (Provenance ctx annotation)) + (IsType resultVar (Provenance ctx annotation)) ( Node - [ ParentConstraint (IsStar k1 (Provenance ctx $ ABT.annotation dom)) domConstraints, - ParentConstraint (IsStar k2 (Provenance ctx $ ABT.annotation cod)) codConstraints + [ ParentConstraint (IsType k1 (Provenance ctx $ ABT.annotation dom)) domConstraints, + ParentConstraint (IsType k2 (Provenance ctx $ ABT.annotation cod)) codConstraints ] ) Type.App abs arg -> do @@ -128,7 +128,7 @@ typeConstraintTree resultVar term@ABT.Term {annotation, out} = do Node <$> for effs \eff -> do effKind <- freshVar eff effConstraints <- typeConstraintTree effKind eff - pure $ ParentConstraint (IsEffect effKind (Provenance EffectsList $ ABT.annotation eff)) effConstraints + pure $ ParentConstraint (IsAbility effKind (Provenance EffectsList $ ABT.annotation eff)) effConstraints -- | Generate kind constraints arising from a given type. The given -- @UVar@ is constrained to have the kind of the given type. @@ -176,7 +176,7 @@ termConstraintTree = fmap Node . dfAnns processAnn cons nil . hackyStripAnns processAnn ann typ mrest = do instantiateType typ \typ gcs -> do typKind <- freshVar typ - annConstraints <- ParentConstraint (IsStar typKind (Provenance TypeAnnotation ann)) <$> typeConstraintTree typKind typ + annConstraints <- ParentConstraint (IsType typKind (Provenance TypeAnnotation ann)) <$> typeConstraintTree typKind typ let annConstraints' = foldr Constraint annConstraints gcs rest <- mrest pure (annConstraints' : rest) @@ -208,10 +208,10 @@ hackyStripAnns = let argMod = case isHack of True -> stripAnns False -> id - in (isHack, Term.app ann abs (argMod arg)) + in (isHack, Term.app ann abs (argMod arg)) Term.Constructor cref@(ConstructorReference r _) -> let isHack = r == rewriteTypeRef - in (isHack, Term.constructor ann cref) + in (isHack, Term.constructor ann cref) t -> (False, ABT.tm ann (snd <$> t)) where stripAnns = ABT.cata \ann abt0 -> case abt0 of @@ -261,7 +261,7 @@ declComponentConstraintTree decls = do withInstantiatedConstructorType declType tyvarKindsOnly constructorType \constructorType -> do constructorKind <- freshVar constructorType ct <- typeConstraintTree constructorKind constructorType - pure $ ParentConstraint (IsStar constructorKind (Provenance DeclDefinition constructorAnn)) ct + pure $ ParentConstraint (IsType constructorKind (Provenance DeclDefinition constructorAnn)) ct (fullyAppliedKind, _fullyAppliedType, declConstraints) <- let phi (dk, dt, cts) (ak, at) = do @@ -273,8 +273,8 @@ declComponentConstraintTree decls = do in foldlM phi (declKind, declType, Node []) tyvarKinds let finalDeclConstraints = case decl of - Left _effectDecl -> Constraint (IsEffect fullyAppliedKind (Provenance DeclDefinition declAnn)) declConstraints - Right _dataDecl -> Constraint (IsStar fullyAppliedKind (Provenance DeclDefinition declAnn)) declConstraints + Left _effectDecl -> Constraint (IsAbility fullyAppliedKind (Provenance DeclDefinition declAnn)) declConstraints + Right _dataDecl -> Constraint (IsType fullyAppliedKind (Provenance DeclDefinition declAnn)) declConstraints pure (StrictOrder finalDeclConstraints constructorConstraints) pure (Node cts) @@ -352,7 +352,7 @@ builtinConstraintTree :: forall v loc. (Ord loc, BuiltinAnnotation loc, Var v) = builtinConstraintTree = mergeTrees [ traverse - (constrain Star) + (constrain Type) [ Type.nat, Type.int, Type.float, @@ -383,7 +383,7 @@ builtinConstraintTree = flip Type.ref Type.hashAlgorithmRef ], traverse - (constrain (Star :-> Star)) + (constrain (Type :-> Type)) [ Type.list, Type.iarrayType, flip Type.ref Type.mvarRef, @@ -393,18 +393,18 @@ builtinConstraintTree = flip Type.ref Type.patternRef ], traverse - (constrain Effect) + (constrain Ability) [ Type.builtinIO, flip Type.ref Type.stmRef ], traverse - (constrain (Star :-> Effect)) + (constrain (Type :-> Ability)) [flip Type.ref Type.scopeRef], traverse - (constrain (Effect :-> Star)) + (constrain (Ability :-> Type)) [Type.mbytearrayType], traverse - (constrain (Effect :-> Star :-> Star)) + (constrain (Ability :-> Type :-> Type)) [Type.effectType, Type.marrayType, Type.refType] ] where @@ -420,10 +420,10 @@ constrainToKind :: (Var v) => Provenance v loc -> UVar v loc -> Kind -> Gen v lo constrainToKind prov resultVar0 = fmap ($ []) . go resultVar0 where go resultVar = \case - Star -> do - pure (IsStar resultVar prov:) - Effect -> do - pure (IsEffect resultVar prov:) + Type -> do + pure (IsType resultVar prov :) + Ability -> do + pure (IsAbility resultVar prov :) lhs :-> rhs -> do let inputTypeVar = Type.var (prov ^. Provenance.loc) (freshIn Set.empty (typed (User "a"))) let outputTypeVar = Type.var (prov ^. Provenance.loc) (freshIn Set.empty (typed (User "a"))) @@ -431,13 +431,13 @@ constrainToKind prov resultVar0 = fmap ($ []) . go resultVar0 output <- freshVar outputTypeVar ctl <- go input lhs ctr <- go output rhs - pure ((IsArr resultVar prov input output:) . ctl . ctr) + pure ((IsArr resultVar prov input output :) . ctl . ctr) -data Kind = Star | Effect | Kind :-> Kind +data Kind = Type | Ability | Kind :-> Kind infixr 9 :-> fromUnisonKind :: Unison.Kind -> Kind fromUnisonKind = \case - Unison.Star -> Star + Unison.Star -> Type Unison.Arrow a b -> fromUnisonKind a :-> fromUnisonKind b diff --git a/parser-typechecker/src/Unison/KindInference/Solve.hs b/parser-typechecker/src/Unison/KindInference/Solve.hs index b76b1bc857..f4408352f9 100644 --- a/parser-typechecker/src/Unison/KindInference/Solve.hs +++ b/parser-typechecker/src/Unison/KindInference/Solve.hs @@ -46,10 +46,10 @@ type UnsolvedConstraint v loc = Unsolved.Constraint (UVar v loc) v loc StarProve _Generated :: forall v loc. Prism' (UnsolvedConstraint v loc) (GeneratedConstraint v loc) _Generated = prism' (Unsolved.starProv %~ NotDefault) \case - Unsolved.IsStar s l -> case l of + Unsolved.IsType s l -> case l of Default -> Nothing - NotDefault l -> Just (Unsolved.IsStar s l) - Unsolved.IsEffect s l -> Just (Unsolved.IsEffect s l) + NotDefault l -> Just (Unsolved.IsType s l) + Unsolved.IsAbility s l -> Just (Unsolved.IsAbility s l) Unsolved.IsArr s l a b -> Just (Unsolved.IsArr s l a b) Unsolved.Unify l a b -> Just (Unsolved.Unify l a b) @@ -85,15 +85,15 @@ defaultUnconstrainedVars st = phi b a = U.alter a handleNothing handleJust b handleNothing = error "impossible" handleJust _canonK ecSize d = case descriptorConstraint d of - Nothing -> U.Canonical ecSize d {descriptorConstraint = Just $ Solved.IsStar Default} + Nothing -> U.Canonical ecSize d {descriptorConstraint = Just $ Solved.IsType Default} Just _ -> U.Canonical ecSize d in st {constraints = newConstraints, newUnifVars = []} prettyConstraintD' :: Show loc => Var v => PrettyPrintEnv -> UnsolvedConstraint v loc -> P.Pretty P.ColorText prettyConstraintD' ppe = P.wrap . \case - Unsolved.IsStar v p -> prettyUVar ppe v <> " ~ *" <> prettyProv p - Unsolved.IsEffect v p -> prettyUVar ppe v <> " ~ Effect" <> prettyProv p + Unsolved.IsType v p -> prettyUVar ppe v <> " ~ Type" <> prettyProv p + Unsolved.IsAbility v p -> prettyUVar ppe v <> " ~ Ability" <> prettyProv p Unsolved.IsArr v p a b -> prettyUVar ppe v <> " ~ " <> prettyUVar ppe a <> " -> " <> prettyUVar ppe b <> prettyProv p Unsolved.Unify p a b -> prettyUVar ppe a <> " ~ " <> prettyUVar ppe b <> prettyProv p where @@ -178,11 +178,11 @@ occCheck constraints0 = st@OccCheckState {solvedConstraints} <- M.get let handleNothing = error "impossible" handleJust _canonK ecSize d = case descriptorConstraint d of - Nothing -> ([], U.Canonical ecSize d {descriptorConstraint = Just $ Solved.IsStar Default}) + Nothing -> ([], U.Canonical ecSize d {descriptorConstraint = Just $ Solved.IsType Default}) Just v -> let descendants = case v of - Solved.IsStar _ -> [] - Solved.IsEffect _ -> [] + Solved.IsType _ -> [] + Solved.IsAbility _ -> [] Solved.IsArr _ a b -> [a, b] in (descendants, U.Canonical ecSize d) let (descendants, solvedConstraints') = U.alterF u handleNothing handleJust solvedConstraints @@ -277,9 +277,9 @@ addConstraint' :: UnsolvedConstraint v loc -> Solve v loc (Either (ConstraintConflict v loc) [UnsolvedConstraint v loc]) addConstraint' = \case - Unsolved.IsEffect s p0 -> do - handleConstraint s (Solved.IsEffect p0) \case - Solved.IsEffect _ -> Just (Solved.IsEffect p0, []) + Unsolved.IsAbility s p0 -> do + handleConstraint s (Solved.IsAbility p0) \case + Solved.IsAbility _ -> Just (Solved.IsAbility p0, []) _ -> Nothing Unsolved.IsArr s p0 a b -> do handleConstraint s (Solved.IsArr p0 a b) \case @@ -291,9 +291,9 @@ addConstraint' = \case prov = p0 in Just (Solved.IsArr prov a b, implied) _ -> Nothing - Unsolved.IsStar s p0 -> do - handleConstraint s (Solved.IsStar p0) \case - Solved.IsStar _ -> Just (Solved.IsStar p0, []) + Unsolved.IsType s p0 -> do + handleConstraint s (Solved.IsType p0) \case + Solved.IsType _ -> Just (Solved.IsType p0, []) _ -> Nothing Unsolved.Unify l a b -> Right <$> union l a b where @@ -341,11 +341,11 @@ union _unionLoc a b = do Nothing -> [] Just c -> let cd = case c of - Solved.IsStar loc -> Unsolved.IsStar a case loc of + Solved.IsType loc -> Unsolved.IsType a case loc of Default -> Default NotDefault loc -> NotDefault loc Solved.IsArr loc l r -> Unsolved.IsArr a loc l r - Solved.IsEffect loc -> Unsolved.IsEffect a loc + Solved.IsAbility loc -> Unsolved.IsAbility a loc in [cd] pure (Just impliedConstraints) diff --git a/unison-src/transcripts/kind-inference.output.md b/unison-src/transcripts/kind-inference.output.md index 64f177ed40..79e76162b0 100644 --- a/unison-src/transcripts/kind-inference.output.md +++ b/unison-src/transcripts/kind-inference.output.md @@ -62,8 +62,8 @@ unique type Pong = Pong (Ping Optional) Kind mismatch arising from 1 | unique type Ping a = Ping a Pong - The arrow type (->) expects arguments of kind *; however, it - is applied to a which has kind: * -> *. + The arrow type (->) expects arguments of kind Type; however, + it is applied to a which has kind: Type -> Type. ``` Successful example between mutually recursive type and ability @@ -97,8 +97,8 @@ unique ability Pong a where Kind mismatch arising from 3 | pong : Ping Optional -> () - Ping expects an argument of kind: *; however, it is applied - to Optional which has kind: * -> *. + Ping expects an argument of kind: Type; however, it is + applied to Optional which has kind: Type -> Type. ``` Consistent instantiation of `T`'s `a` parameter in `S` @@ -132,8 +132,8 @@ unique type S = S (T Optional) Kind mismatch arising from 3 | unique type S = S (T Optional) - T expects an argument of kind: *; however, it is applied to - Optional which has kind: * -> *. + T expects an argument of kind: Type; however, it is applied + to Optional which has kind: Type -> Type. ``` ## Checking annotations @@ -164,8 +164,8 @@ test _ = () Kind mismatch arising from 1 | test : Optional -> () - The arrow type (->) expects arguments of kind *; however, it - is applied to Optional which has kind: * -> *. + The arrow type (->) expects arguments of kind Type; however, + it is applied to Optional which has kind: Type -> Type. ``` Catch kind error in annotation example 3 @@ -181,8 +181,8 @@ test _ = () Kind mismatch arising from 3 | test : T Nat -> () - T expects an argument of kind: * -> *; however, it is - applied to Nat which has kind: *. + T expects an argument of kind: Type -> Type; however, it is + applied to Nat which has kind: Type. ``` Catch kind error in scoped type variable annotation @@ -202,8 +202,8 @@ test _ = Kind mismatch arising from 6 | buggo : Star a - Star expects an argument of kind: *; however, it is applied - to a which has kind: * -> *. + Star expects an argument of kind: Type; however, it is + applied to a which has kind: Type -> Type. ``` ## Effect/type mismatch @@ -222,8 +222,8 @@ test _ = () Kind mismatch arising from 4 | test : Foo -> () - The arrow type (->) expects arguments of kind *; however, it - is applied to Foo which has kind: Effect. + The arrow type (->) expects arguments of kind Type; however, + it is applied to Foo which has kind: Ability. ``` Types appearing where effects are expected @@ -238,8 +238,8 @@ test _ = () 1 | test : {Nat} () An ability list must consist solely of abilities; however, - this list contains Nat which has kind *. Abilities are of - kind Effect. + this list contains Nat which has kind Type. Abilities are of + kind Ability. ``` ## Cyclic kinds @@ -254,8 +254,8 @@ unique type T a = T (a a) 1 | unique type T a = T (a a) The above application constrains the kind of a to be - infinite, generated by the constraint k = k -> * where k is - the kind of a. + infinite, generated by the constraint k = k -> Type where k + is the kind of a. ``` ```unison @@ -268,8 +268,8 @@ unique type T a b = T (a b) (b a) 1 | unique type T a b = T (a b) (b a) The above application constrains the kind of b to be - infinite, generated by the constraint k = (k -> *) -> * - where k is the kind of b. + infinite, generated by the constraint + k = (k -> Type) -> Type where k is the kind of b. ``` ```unison @@ -284,6 +284,7 @@ unique type Pong a = Pong (a Ping) The above application constrains the kind of a to be infinite, generated by the constraint - k = (((k -> *) -> *) -> *) -> * where k is the kind of a. + k = (((k -> Type) -> Type) -> Type) -> Type where k is the + kind of a. ```