Rename kinds: Star -> Type, Effect -> Ability

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,

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

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 #-}

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 #-}
 

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.

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 #-}

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 [email protected] {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 [email protected] {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,24 +420,24 @@ 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")))
         input <- freshVar inputTypeVar
         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

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)