From 3b16d19d8781c6606e923691d882339a6d7219bc Mon Sep 17 00:00:00 2001 From: Dan Doel Date: Thu, 23 Jun 2022 19:46:08 -0400 Subject: [PATCH 1/2] Some adjustments to ability checking - Fixed an erroneous case when equating two sets of abilities. Normally we try to unify pieces of them with pieces of the opposite side to render them equal. However, in certain cases where that wasn't possible, we would just not do anything, and also not fail. This code tries some additional unification cases, and properly throws an error if nothing will work. - This caused some knock-on problems with certain test examples. For instance, if you annotate a handler as `Request {...} r -> ...`, then variables made up in the function body will fail to unify with the rigidly defined row. So ability checking for cases has been modified to avoid making up superfluous variables. --- .../src/Unison/Typechecker/Context.hs | 114 ++++++++++-------- 1 file changed, 67 insertions(+), 47 deletions(-) diff --git a/parser-typechecker/src/Unison/Typechecker/Context.hs b/parser-typechecker/src/Unison/Typechecker/Context.hs index 1c552407f3..e44d2f285c 100644 --- a/parser-typechecker/src/Unison/Typechecker/Context.hs +++ b/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 From d85e17e2563550aadb62d7fe085d520c39dd48f6 Mon Sep 17 00:00:00 2001 From: Dan Doel Date: Thu, 23 Jun 2022 19:57:32 -0400 Subject: [PATCH 2/2] Add test transcript --- unison-src/transcripts/fix3037.md | 18 ++++++++++++++++++ unison-src/transcripts/fix3037.output.md | 23 +++++++++++++++++++++++ 2 files changed, 41 insertions(+) create mode 100644 unison-src/transcripts/fix3037.md create mode 100644 unison-src/transcripts/fix3037.output.md diff --git a/unison-src/transcripts/fix3037.md b/unison-src/transcripts/fix3037.md new file mode 100644 index 0000000000..f9f0b584cc --- /dev/null +++ b/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 +``` diff --git a/unison-src/transcripts/fix3037.output.md b/unison-src/transcripts/fix3037.output.md new file mode 100644 index 0000000000..701bff0f44 --- /dev/null +++ b/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 + + +```