diff --git a/parser-typechecker/src/Unison/Typechecker/Context.hs b/parser-typechecker/src/Unison/Typechecker/Context.hs index aea81f1f1a..0baec810ef 100644 --- a/parser-typechecker/src/Unison/Typechecker/Context.hs +++ b/parser-typechecker/src/Unison/Typechecker/Context.hs @@ -1393,38 +1393,41 @@ synthesizeBinding top binding = do (tb, wb) <- synthesize binding if not (null wb) then fmap (\t -> ((t, wb), id)) (applyM tb) - else if top then do - ctx <- retract - pure ((generalizeExistentials ctx tb, []), substituteSolved ctx) - else do - ctx <- retract - -- Note: this is conservative about what we avoid - -- generalizing. Right now only TDNR causes variables to be - -- retained. It might be possible to make this happen for any - -- `Recorded` to do more inference for unknown variable errors - -- (or whatever the other cases are for), at the expense of - -- less generalization in the process of reporting those. - let retain (B.Recorded B.Resolve{}) = True - retain B.Retain = True - retain _ = False - - erecs = [ v | Existential b v <- ctx, retain b ] - srecs = - [ v - | Solved b _ sa <- ctx - , retain b - , TypeVar.Existential _ v <- - Set.toList . ABT.freeVars . applyCtx ctx $ Type.getPolytype sa ] - keep = Set.fromList (erecs ++ srecs) - p (Existential _ v) - | v `Set.member` keep = - Left . Var $ TypeVar.Existential B.Retain v - p e = Right e - (repush, discard) = partitionEithers $ fmap p ctx - appendContext repush - markRetained keep - let tf = generalizeExistentials discard (applyCtx ctx tb) - pure ((tf, []), substituteSolved ctx) + else + if top + then do + ctx <- retract + pure ((generalizeExistentials ctx tb, []), substituteSolved ctx) + else do + ctx <- retract + -- Note: this is conservative about what we avoid + -- generalizing. Right now only TDNR causes variables to be + -- retained. It might be possible to make this happen for any + -- `Recorded` to do more inference for unknown variable errors + -- (or whatever the other cases are for), at the expense of + -- less generalization in the process of reporting those. + let retain (B.Recorded B.Resolve {}) = True + retain B.Retain = True + retain _ = False + + erecs = [v | Existential b v <- ctx, retain b] + srecs = + [ v + | Solved b _ sa <- ctx, + retain b, + TypeVar.Existential _ v <- + Set.toList . ABT.freeVars . applyCtx ctx $ Type.getPolytype sa + ] + keep = Set.fromList (erecs ++ srecs) + p (Existential _ v) + | v `Set.member` keep = + Left . Var $ TypeVar.Existential B.Retain v + p e = Right e + (repush, discard) = partitionEithers $ fmap p ctx + appendContext repush + markRetained keep + let tf = generalizeExistentials discard (applyCtx ctx tb) + pure ((tf, []), substituteSolved ctx) getDataConstructorsAtType :: forall v loc. (Ord loc, Var v) => Type v loc -> M v loc (EnumeratedConstructors (TypeVar v loc) v loc) getDataConstructorsAtType t0 = do diff --git a/unison-core/src/Unison/Blank.hs b/unison-core/src/Unison/Blank.hs index 63469b32aa..6ab996e7c0 100644 --- a/unison-core/src/Unison/Blank.hs +++ b/unison-core/src/Unison/Blank.hs @@ -28,12 +28,12 @@ data Recorded loc -- - Recorded indicates that we want to remember the variable's solution -- for some kind of data Blank loc - = Blank - -- ^ just a dummy annotation - | Recorded (Recorded loc) - -- ^ indicates that we want to remember the variable's solution for - -- some reason - | Retain - -- ^ indicates that we want to prefer keeping the variable in the - -- context to better refine the above recorded solutions + = -- | just a dummy annotation + Blank + | -- | indicates that we want to remember the variable's solution for + -- some reason + Recorded (Recorded loc) + | -- | indicates that we want to prefer keeping the variable in the + -- context to better refine the above recorded solutions + Retain deriving (Show, Eq, Ord, Functor, Generic)