Compiles, all but two typechecker tests pass - gets rid of effect generalization in favor of existentializing unadorned arrows

parser-typechecker/src/Unison/Builtin.hs

@@ -58,9 +58,7 @@ t :: Var v => String -> Type v
 t s = ABT.amap (const Intrinsic) .
           Names.bindType names . either (error . showParseError s) tweak $
           Parser.run (Parser.root TypeParser.valueType) s mempty
-  -- lowercase vars become forall'd, and we assume the function is pure up
-  -- until it returns its result.
-  where tweak = Type.generalizeEffects 100000 . Type.generalizeLowercase
+  where tweak = Type.generalizeLowercase
 
 -- parse a term, hard-coding the builtins defined in this file
 tm :: Var v => String -> Term v

parser-typechecker/src/Unison/PrintError.hs

@@ -279,7 +279,7 @@ renderTypeError e env src = case e of
     ]
   FunctionApplication {..}
     -> let
-         fte         = Type.ungeneralizeEffects ft
+         fte         = Type.removePureEffects ft
          fteFreeVars = Set.map TypeVar.underlying $ ABT.freeVars fte
          showVar (v, _t) = Set.member v fteFreeVars
          solvedVars' = filter showVar solvedVars
@@ -442,14 +442,14 @@ renderTypeError e env src = case e of
            , annotatedAsErrorSite src termSite
            , "\n"
            , "Its type is: "
-           , style ErrorSite (renderType' env (Type.ungeneralizeEffects i))
+           , style ErrorSite (renderType' env (Type.removePureEffects i))
            , ".\n\n"
            , case o of
              Type.Existential' _ _ ->
                "It can be replaced with a value of any type.\n"
              _ ->
                "A well-typed replacement must conform to: "
-                 <> style Type2 (renderType' env (Type.ungeneralizeEffects o))
+                 <> style Type2 (renderType' env (Type.removePureEffects o))
                  <> ".\n"
            ]
   UnknownTerm {..} | Var.isKind Var.missingResult unknownTermV -> mconcat
@@ -724,7 +724,7 @@ renderType
   -> (loc -> AnnotatedText a -> AnnotatedText a)
   -> Type.AnnotatedType v loc
   -> AnnotatedText a
-renderType env f t = renderType0 env f (0 :: Int) (Type.ungeneralizeEffects t)
+renderType env f t = renderType0 env f (0 :: Int) (Type.removePureEffects t)
  where
   wrap :: (IsString a, Semigroup a) => a -> a -> Bool -> a -> a
   wrap start end test s = if test then start <> s <> end else s

parser-typechecker/src/Unison/Type.hs

@@ -359,97 +359,11 @@ dependencies t = Set.fromList . Writer.execWriter $ ABT.visit' f t
   where f t@(Ref r) = Writer.tell [r] *> pure t
         f t = pure t
 
--- Adds effect polymorphism to a type signature. That is, converts a signature like:
---
--- map : (a -> b) -> List a -> List b
---
--- to:
---
--- map : (a ->{e} b) ->{e} List a ->{e} (List b)
---
--- The `arity` is the number of arguments the function takes which
--- are assumed to be pure. Applying `generalizeEffects 2` to the
--- signature of `map` would give:
--- map : (a ->{e} b) -> List a ->{e} List b
---
--- Notice the arrow before `List a` has no effects on it. This is
--- a strictly more general type, as it's equivalent to:
---
--- map : ∀ a b e e2 . (a ->{e} b) ->{e2} List a ->{e} List b
---
--- `1` is a conservative lower bound, but if you have a type formed
--- from a lambda like `x y -> ...`, then it's safe to assume arity 2.
--- Without `arity`, it's not safe to assume that partial applications
--- of a function type are all pure except the last one. For instance,
--- consider:
---
--- hof : (a -> a) -> a -> [a] -> [a]
---
--- Can we generalize this to `(a ->{e} a) -> a -> List a ->{e} List a` ?
--- Not necessarily, since the implementation of `hof` could be:
--- hof f a =
---   out = [f a]
---   as -> out
---
--- In general, higher order function types might apply some of their input
--- functions before receiving all the arguments to the function, so if
--- we make any of these input functions effectful, some of the partial
--- applications of the function type may need to become effectful in the same way.
---
--- If the function result mentions effects anywhere (if it contains any `{}`),
--- we leave the signature alone as it's unclear what transformation the user might
--- want. The user is responsible for using effect variables as they wish.
-generalizeEffects :: forall v a . Var v => Int -> AnnotatedType v a -> AnnotatedType v a
-generalizeEffects _arity t | usesEffects t = t
-generalizeEffects  arity t =
-  let
-    at = ABT.annotation t
-    e = ABT.freshEverywhere t (Var.named "𝛆")
-    evar = var at e
-    ev t = effect at [evar] t
-    go :: Int -> AnnotatedType v a -> AnnotatedType v a
-    go remPure t = let at = ABT.annotation t in case t of
-      Arrow' i o -> case o of
-        Effect' _ _ -> t
-        _ | remPure <= 0 -> arrow at (go 0 i) (ev $ go 0 o)
-          | otherwise    -> arrow at (go 0 i) (go (remPure - 1) o)
-      Ann' t k -> ann at (go remPure t) k
-      Effect1' e e2 -> effect1 at (go 0 e) (go 0 e2)
-      Effects' es -> effects at (go 0 <$> es)
-      ForallNamed' v body -> forall at v (go remPure body)
-      _ -> t
-    t' = go (arity - 1) t
-    tr = if Set.member e (ABT.freeVars t') then forall at e t'
-         else t'
-  in tr
-
 usesEffects :: Var v => AnnotatedType v a -> Bool
 usesEffects t = getAny . getConst $ ABT.visit go t where
   go (Effect1' _ _) = Just (Const (Any True))
   go _ = Nothing
 
-ungeneralizeEffects :: Var v => AnnotatedType v a -> AnnotatedType v a
-ungeneralizeEffects t = case functionResult t of
-  Just (Effect' [Var' e] _)
-    | Var.name e == "𝛆" -> stripE e t
-    | otherwise -> t
-    where
-    isVar v (Var' e) = e == v
-    isVar _ _ = False
-    unE :: Var v => v -> AnnotatedType v a -> Maybe (AnnotatedType v a)
-    unE e et@(Effect' es v) = case filter (not . isVar e) es of
-      [] -> Just (ABT.visitPure (unE e) v)
-      es -> Just (effect (ABT.annotation et) es (ABT.visitPure (unE e) v))
-    unE _ _ = Nothing
-    stripE :: Var v => v -> AnnotatedType v a -> AnnotatedType v a
-    stripE e t = ABT.visitPure (unE e) t
-    -- a bit more restrictive version which requires that the effects be forall'd
-    -- stripE e t@(ForallNamed' e0 body) | e == e0 = ABT.visitPure (unE e) body
-    --                                   | otherwise = t
-    -- stripE _e t = t
-  Just _ -> t
-  Nothing -> t
-
 -- Returns free effect variables in the given type, for instance, in:
 --
 --   ∀ e3 . a ->{e,e2} b ->{e3} c
@@ -466,6 +380,18 @@ freeEffectVars t =
       in pure . Set.toList $ frees `Set.difference` ABT.annotation t
     go _ = pure []
 
+existentializeArrows :: (Var v, Monad m)
+                     => m v
+                     -> AnnotatedType v a
+                     -> m (AnnotatedType v a)
+existentializeArrows freshVar t = ABT.visit go t
+  where
+  go t@(Arrow' a b) = case b of
+    Effect1' _ _ -> Nothing
+    _ -> Just . fmap (arrow (ABT.annotation t) a)
+              $ existentializeArrows freshVar b
+  go _ = Nothing
+
 -- Remove free effect variables from the type that are in the set
 removeEffectVars :: Var v => Set v -> AnnotatedType v a -> AnnotatedType v a
 removeEffectVars removals t =
@@ -473,7 +399,9 @@ removeEffectVars removals t =
       t' = ABT.substs ((,z) <$> Set.toList removals) t
       removeEmpty t@(Effect1' e v) =
         let es = flattenEffects e
-        in Just (effect (ABT.annotation t) es $ ABT.visitPure removeEmpty v)
+        in case es of
+             [] -> Just (ABT.visitPure removeEmpty v)
+             _ -> Just (effect (ABT.annotation t) es $ ABT.visitPure removeEmpty v)
       removeEmpty _ = Nothing
   in ABT.visitPure removeEmpty t'
 
@@ -492,9 +420,6 @@ functionResult t = go False t where
   go _inArr (Arrow' _i o) = go True o
   go inArr t = if inArr then Just t else Nothing
 
-generalizeEffects' :: Var v => AnnotatedType v a -> AnnotatedType v a
-generalizeEffects' = generalizeEffects 1
-
 
 -- | Bind all free variables that start with a lowercase letter with an outer `forall`.
 generalizeLowercase :: Var v => AnnotatedType v a -> AnnotatedType v a

parser-typechecker/src/Unison/TypePrinter.hs

@@ -74,7 +74,7 @@ pretty n p tp = case tp of
       paren True
       $         ("∀ " <> l (Text.unpack (Var.name v)) <> ".")
       `PP.hang` pretty n (-1) body
-  t@(Arrow' _ _) -> case (ungeneralizeEffects t) of
+  t@(Arrow' _ _) -> case removePureEffects t of
     EffectfulArrows' (Ref' DD.UnitRef) rest -> arrows True True rest
     EffectfulArrows' fst rest ->
       PP.parenthesizeIf (p >= 0) $ pretty n 0 fst <> arrows False False rest

parser-typechecker/src/Unison/Typechecker/Context.hs

@@ -615,6 +615,10 @@ extendExistential v = do
   modifyContext (pure . extend (Existential B.Blank v'))
   pure v'
 
+extendExistentialTV :: Var v => Text -> M v loc (TypeVar v loc)
+extendExistentialTV name =
+  TypeVar.Existential B.Blank <$> extendExistential (Var.named name)
+
 extendMarker :: (Var v, Ord loc) => v -> M v loc v
 extendMarker v = do
   v' <- freshenVar v
@@ -755,10 +759,10 @@ synthesize e = scope (InSynthesize e) $
   go (Term.Ref' h) = compilerCrash $ UnannotatedReference h
   go (Term.Constructor' r cid) = do
     t <- getDataConstructorType r cid
-    pure $ Type.generalizeEffects (Type.arity t) t
+    Type.existentializeArrows (extendExistentialTV "𝛆") t
   go (Term.Request' r cid) = do
     t <- ungeneralize =<< getEffectConstructorType r cid
-    pure $ Type.generalizeEffects (Type.arity t) t
+    Type.existentializeArrows (extendExistentialTV "𝛆") t
   go (Term.Ann' e' t) = t <$ check e' t
   go (Term.Float' _) = pure $ Type.float l -- 1I=>
   go (Term.Int' _) = pure $ Type.int l -- 1I=>
@@ -1029,28 +1033,27 @@ annotateLetRecBindings isTop letrec =
     (bindings, body) <- letrec freshenVar
     let vs = map fst bindings
     -- generate a fresh existential variable `e1, e2 ...` for each binding
-    es  <- traverse freshenVar vs
     e1  <- freshNamed "bindings-start"
     ctx <- getContext
+    appendContext $ context [Marker e1]
     -- Introduce these existentials into the context and
     -- annotate each term variable w/ corresponding existential
     -- [marker e1, 'e1, 'e2, ... v1 : 'e1, v2 : 'e2 ...]
-    let f e (_, binding) = case binding of
-          -- TODO: Think about whether `apply` here is always correct
-          -- Used to have a guard that would only do this if t had no free vars
-          Term.Ann' _ t | useUserAnnotations -> apply ctx t
-          _ -> Type.existential' (loc binding) B.Blank e
-    let bindingTypes   = zipWith f es bindings
-        bindingArities = Term.arity . snd <$> bindings
-    appendContext $ context
-      (Marker e1 : map existential es ++ zipWith Ann vs bindingTypes)
+    let f (v, binding) = case binding of
+          Term.Ann' _ t | useUserAnnotations ->
+            Type.existentializeArrows (extendExistentialTV "𝛆") $ apply ctx t
+          _ -> do
+            vt <- extendExistential v
+            pure $ Type.existential' (loc binding) B.Blank vt
+    bindingTypes <- traverse f bindings
+    let bindingArities = Term.arity . snd <$> bindings
+    appendContext $ context (zipWith Ann vs bindingTypes)
     -- check each `bi` against `ei`; sequencing resulting contexts
     Foldable.for_ (zip bindings bindingTypes) $ \((_, b), t) -> check b t
     -- compute generalized types `gt1, gt2 ...` for each binding `b1, b2...`;
     -- add annotations `v1 : gt1, v2 : gt2 ...` to the context
     (_, _, ctx2) <- breakAt (Marker e1) <$> getContext
-    let gen bindingType arity =
-          Type.generalizeEffects arity $ generalizeExistentials ctx2 bindingType
+    let gen bindingType _arity = generalizeExistentials ctx2 bindingType
         bindingTypesGeneralized = zipWith gen bindingTypes bindingArities
         annotations             = zipWith Ann vs bindingTypesGeneralized
     marker <- Marker <$> freshenVar (ABT.v' "let-rec-marker")
@@ -1058,7 +1061,6 @@ annotateLetRecBindings isTop letrec =
     appendContext . context $ marker : annotations
     pure (marker, body, vs `zip` bindingTypesGeneralized)
 
-
 ungeneralize :: (Var v, Ord loc) => Type v loc -> M v loc (Type v loc)
 ungeneralize t = snd <$> ungeneralize' t
 
@@ -1468,7 +1470,7 @@ annotateRefs synth = ABT.visit f where
   f r@(Term.Ann' (Term.Ref' _) _) = Just (pure r)
   f r@(Term.Ref' h) = Just (Term.ann ra (Term.ref ra h) <$> (ge <$> synth h))
     where ra = ABT.annotation r
-          ge t = ABT.vmap TypeVar.Universal $ Type.generalizeEffects (Type.arity t) t
+          ge t = ABT.vmap TypeVar.Universal $ t
   f _ = Nothing
 
 run
@@ -1486,11 +1488,6 @@ run builtinLoc ambient datas effects m =
     . const
     $ pure True
 
-generalizeEffectSignatures :: Var v => Term v loc -> Term v loc
-generalizeEffectSignatures t = ABT.rebuildUp go t
-  where go (Term.Ann e t) = Term.Ann e (Type.generalizeEffects (Term.arity e) t)
-        go e = e
-
 synthesizeClosed' :: (Var v, Ord loc)
                   => [Type v loc]
                   -> Term v loc
@@ -1500,7 +1497,7 @@ synthesizeClosed' abilities term = do
   ctx0 <- getContext
   setContext $ context []
   v <- extendMarker $ Var.named "start"
-  t <- withEffects0 abilities (synthesize $ generalizeEffectSignatures term)
+  t <- withEffects0 abilities (synthesize term)
   ctx <- getContext
   -- retract will cause notes to be written out for
   -- any `Blank`-tagged existentials passing out of scope