Merge pull request #3149 from unisonweb/fix/3037

Some ability checking adjustments

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

@@ -1215,18 +1215,34 @@ checkCases scrutType outType cases@(Term.MatchCase _ _ t : _) =
   scope (InMatch (ABT.annotation t)) $ do
     mes <- requestType (cases <&> \(Term.MatchCase p _ _) -> p)
     for_ mes $ \es ->
-      applyM scrutType >>= \sty -> do
-        v <- freshenVar Var.inferPatternPureV
-        g <- freshenVar Var.inferAbility
-        let lo = loc scrutType
-            vt = existentialp lo v
-            gt = existentialp lo g
-            es' = gt : es
-        appendContext [existential g, existential v]
-        subtype (Type.effectV lo (lo, Type.effects lo es') (lo, vt)) sty
+      applyM scrutType >>= \sty -> ensureReqEffects sty es
     scrutType' <- applyM =<< ungeneralize scrutType
     coalesceWanteds =<< traverse (checkCase scrutType' outType) cases
 
+-- Checks a scrutinee type against a list of effects from e.g. a list of cases
+-- from a handler.
+--
+-- This opportunistically destructures the scrutinee type if it is of the form
+-- `Request es r` in an effort to avoid introducing ability unification
+-- variables that will be more difficult to infer. In such cases, we just run an
+-- ability check directly against `es`. This works better, for instance, where a
+-- signature has been given for the handler, and es = {A,B,g}, for a universal
+-- g. In such a situation, we have no good way of solving via the general check
+-- for {A,B,e} < {A,B,g} with a fresh `e` existential, but the `e` is actually
+-- useless in this scenario.
+ensureReqEffects :: Var v => Ord loc => Type v loc -> [Type v loc] -> M v loc ()
+ensureReqEffects (Type.Apps' (Type.Ref' req) [hes, _]) res
+  | req == Type.effectRef = expandAbilities [hes] >>= \hes -> abilityCheck' hes res
+ensureReqEffects sty res = do
+  v <- freshenVar Var.inferPatternPureV
+  g <- freshenVar Var.inferAbility
+  let lo = loc sty
+      vt = existentialp lo v
+      gt = existentialp lo g
+      es' = gt : res
+  appendContext [existential g, existential v]
+  subtype (Type.effectV lo (lo, Type.effects lo es') (lo, vt)) sty
+
 getEffect ::
   Var v => Ord loc => ConstructorReference -> M v loc (Type v loc)
 getEffect ref = do
@@ -1389,28 +1405,29 @@ checkPattern scrutineeType p =
       ((v, v') :) <$> checkPattern scrutineeType p'
     -- ex: { a } -> a
     -- ex: { (x, 42) } -> a
-    Pattern.EffectPure loc p -> do
-      vt <- lift $ do
-        v <- freshenVar Var.inferPatternPureV
-        e <- freshenVar Var.inferPatternPureE
-        let vt = existentialp loc v
-        let et = existentialp loc e
-        appendContext [existential v, existential e]
-        subtype (Type.effectV loc (loc, et) (loc, vt)) scrutineeType
-        applyM vt
-      checkPattern vt p
+    Pattern.EffectPure loc p
+      -- Avoid creating extra effect variables when the scrutinee is already
+      -- known to be a Request.
+      --
+      -- TODO: this should actually _always_ be the case, because we do a pass
+      -- across the entire case statement refining the scrutinee type. The
+      -- 'otherwise' still needs to be covered for exhaustivity, however.
+      | Type.Apps' (Type.Ref' req) [_, r] <- scrutineeType
+      , req == Type.effectRef -> checkPattern r p
+      | otherwise -> do
+        vt <- lift $ do
+          v <- freshenVar Var.inferPatternPureV
+          e <- freshenVar Var.inferPatternPureE
+          let vt = existentialp loc v
+          let et = existentialp loc e
+          appendContext [existential v, existential e]
+          subtype (Type.effectV loc (loc, et) (loc, vt)) scrutineeType
+          applyM vt
+        checkPattern vt p
     -- ex: { Stream.emit x -> k } -> ...
     Pattern.EffectBind loc ref args k -> do
       -- scrutineeType should be a supertype of `Effect e vt`
       -- for fresh existentials `e` and `vt`
-      e <- lift $ extendExistential Var.inferPatternBindE
-      v <- lift $ extendExistential Var.inferPatternBindV
-      let evt =
-            Type.effectV
-              loc
-              (loc, existentialp loc e)
-              (loc, existentialp loc v)
-      lift $ subtype evt scrutineeType
       ect <- lift $ getEffectConstructorType ref
       uect <- lift $ skolemize forcedEffect ect
       unless (Type.arity uect == length args)
@@ -1423,27 +1440,23 @@ checkPattern scrutineeType p =
           step _ _ =
             lift . failWith $ PatternArityMismatch loc ect (length args)
       (ctorOutputType, vs) <- foldM step (uect, []) args
+      st <- lift $ applyM scrutineeType
       case ctorOutputType of
         -- an effect ctor should have exactly 1 effect!
-        Type.Effect'' [et] it -> do
+        Type.Effect'' [et] it
           -- expecting scrutineeType to be `Effect et vt`
-
-          -- ensure that the variables in `et` unify with those from
-          -- the scrutinee.
-          lift $ do
-            res <- Type.flattenEffects <$> applyM (existentialp loc e)
-            abilityCheck' res [et]
-
-          st <- lift $ applyM scrutineeType
-          case st of
-            Type.App' (Type.App' _ eff) vt ->
-              let kt =
-                    Type.arrow
-                      (Pattern.loc k)
-                      it
-                      (Type.effect (Pattern.loc k) [eff] vt)
-               in (vs ++) <$> checkPattern kt k
-            _ -> lift . compilerCrash $ PatternMatchFailure
+          | Type.Apps' _ [eff, vt] <- st -> do
+
+            -- ensure that the variables in `et` unify with those from
+            -- the scrutinee.
+            lift $ abilityCheck' [eff] [et]
+            let kt =
+                  Type.arrow
+                    (Pattern.loc k)
+                    it
+                    (Type.effect (Pattern.loc k) [eff] vt)
+            (vs ++) <$> checkPattern kt k
+          | otherwise -> lift . compilerCrash $ PatternMatchFailure
         _ ->
           lift . compilerCrash $
             EffectConstructorHadMultipleEffects
@@ -2666,10 +2679,17 @@ equateAbilities ls rs =
               null vls,
               null vrs ->
                 refine True [(loc t, bc, cv)] [cls ++ crs]
+            | [] <- com, null rs, null cls -> for_ vls defaultAbility
+            | [] <- com, null ls, null crs -> for_ vrs defaultAbility
             | otherwise -> do
-                for_ mlSlack $ \p -> refine False [p] [rs]
-                for_ mrSlack $ \p -> refine False [p] [ls]
+                mrefine mlSlack ls rs
+                mrefine mrSlack rs ls
   where
+    mrefine (Just p) _ es = refine False [p] [es]
+    mrefine Nothing _ [] = pure ()
+    mrefine Nothing hs es =
+      getContext >>= failWith . AbilityCheckFailure hs es
+
     refine common lbvs ess = do
       cv <- traverse freshenVar cn
       ctx <- getContext

unison-src/transcripts/fix3037.md

@@ -0,0 +1,18 @@
+```ucm:hide
+.> builtins.merge
+```
+
+Tests for an unsound case of ability checking that was erroneously being
+accepted before. In certain cases, abilities were able to be added to rows in
+invariant positions.
+
+```unison:error
+structural type Runner g = Runner (forall a. '{g} a -> {} a)
+
+pureRunner : Runner {}
+pureRunner = Runner base.force
+
+-- this compiles, but shouldn't the effect type parameter on Runner be invariant?
+runner : Runner {IO}
+runner = pureRunner
+```

unison-src/transcripts/fix3037.output.md

@@ -0,0 +1,23 @@
+Tests for an unsound case of ability checking that was erroneously being
+accepted before. In certain cases, abilities were able to be added to rows in
+invariant positions.
+
+```unison
+structural type Runner g = Runner (forall a. '{g} a -> {} a)
+
+pureRunner : Runner {}
+pureRunner = Runner base.force
+
+-- this compiles, but shouldn't the effect type parameter on Runner be invariant?
+runner : Runner {IO}
+runner = pureRunner
+```
+
+```ucm
+
+  The expression in red needs the {IO} ability, but this location does not have access to any abilities.
+  
+      8 | runner = pureRunner
+  
+
+```