Remove Immut constraint, leaning on the monads for safety instead.

The safe-names system has been working well. Now that we have some experience
with it we can reevaluate some of the choices. Specifically, we can ask where
the `Immut` constraint, which add a fair bit of clutter, is actually necessary.

It turns out that `Immut n` served three purposes:
  (1) It gated access to `getEnv` within env-carrying monads
  (2) It gated access to fresh binder creation, like `withFreshBinder`
  (3) It allowed us to work with non-sinkable `DistinctAbs` in some places

Regarding (1), it turned out that we only used `getEnv` in order to immediately
pass it to `runEnvReader` or similar, doing a little dance with `liftImmut`
along the way. It's simpler to just use `liftEnvReader` instead. Instead of
gating `getEnv` with `Immut`, we can just write it as `unsafeGetEnv` and be
careful in the few places we need to use it.

It turns out that (2) is more conservative than necessary. A `Binder n l` isn't
injectable in `l` but it *is* injectable in `n`. So it should be legal to have a
`withFreshBinder` that doesn't require `Immut n`. We still have to make sure
that the `Distinct l` constraint doesn't leak back to the caller, but we can do
that by hiding the distinctness constraint in the monad, just like we hide the
scope/env. (However, this is not currently implemented! See below).

Finally, (3) became a non-issue when we stopped using `DistinctAbs`. We only
used `DistinctAbs` for performance reasons, to save needless refreshing. We
replaced it with a dynamic distinctness check to trigger the fast path when
possible.

On top of all that, `Immut` was already broken, with `liftImmut` not providing
the guarantees I'd originally thought (for example, it makes it very easy to
have both `Immut n` and `Mut n` at the same time!).

The reason to make this change now is that I want to add a bilevel version of
InplaceT that emits to two different levels. We can reason about `Mut n` for
each level, but `Immut` is harder.

There is still one vulnerability: if you reify the `Distinct n` constraint by
capturing it in a GADT, you can return it from functions like `withFreshBinder`,
but it will no longer be valid if you subsequently emit more names. We could
solve this by hiding `Distinct n` in the monad, just like we hide the scope/env.
But this would mean we couldn't use the pure `sink` anymore. We'd have to use
the monadic version, `sinkM` instead. But you have to be a bit devious to
capture `Distinct n` in a GADT (especially now that `DistinctAbs` isn't a thing
anymore). So maybe this is a reasonable convenience-security trade-off?

Author: dougalm

src/lib/Builder.hs

@@ -89,7 +89,7 @@ class (EnvReader m, EnvExtender m, Fallible1 m)
 
 class Builder m => ScopableBuilder (m::MonadKind1) where
   buildScoped
-    :: (SinkableE e, Immut n)
+    :: SinkableE e
     => (forall l. (Emits l, DExt n l) => m l (e l))
     -> m n (Abs (Nest Decl) e n)
 
@@ -138,7 +138,7 @@ class (EnvReader m, MonadFail1 m)
   emitBinding :: Mut n => Color c => NameHint -> Binding c n -> m n (Name c n)
   emitEnv :: (Mut n, SinkableE e, SubstE Name e) => Abs TopEnvFrag e n -> m n (e n)
   emitNamelessEnv :: TopEnvFrag n n -> m n ()
-  localTopBuilder :: (Immut n, SinkableE e)
+  localTopBuilder :: SinkableE e
                   => (forall l. (Mut l, DExt n l) => m l (e l))
                   -> m n (Abs TopEnvFrag e n)
 
@@ -216,7 +216,6 @@ runTopBuilderT
   -> TopBuilderT m n a
   -> m a
 runTopBuilderT bindings cont = do
-  Immut <- return $ toImmutEvidence bindings
   liftM snd $ runInplaceT bindings $ runTopBuilderT' $ cont
 
 type TopBuilder2 (m :: MonadKind2) = forall i. TopBuilder (m i)
@@ -239,7 +238,6 @@ type BuilderM = BuilderT HardFailM
 liftBuilderT :: (Fallible m, EnvReader m') => BuilderT m n a -> m' n (m a)
 liftBuilderT cont = do
   env <- unsafeGetEnv
-  Immut <- return $ toImmutEvidence env
   Distinct <- getDistinct
   return do
     (Empty, result) <- runInplaceT env $ runBuilderT' cont
@@ -345,7 +343,7 @@ buildBlock
   :: ScopableBuilder m
   => (forall l. (Emits l, DExt n l) => m l (Atom l))
   -> m n (Block n)
-buildBlock cont = liftImmut do
+buildBlock cont = do
   Abs decls results <- buildScoped do
     result <- cont
     ty <- cheapNormalize =<< getType result
@@ -411,10 +409,10 @@ buildNullaryPi effs cont =
 buildLamGeneral
   :: ScopableBuilder m
   => NameHint -> Arrow -> Type n
-  -> (forall l. (Immut l, DExt n l) => AtomName l -> m l (EffectRow l))
+  -> (forall l.           DExt n l  => AtomName l -> m l (EffectRow l))
   -> (forall l. (Emits l, DExt n l) => AtomName l -> m l (Atom l))
   -> m n (Atom n)
-buildLamGeneral hint arr ty fEff fBody = liftImmut do
+buildLamGeneral hint arr ty fEff fBody = do
   withFreshBinder hint (LamBinding arr ty) \b -> do
     let v = binderName b
     effs <- fEff v
@@ -443,7 +441,7 @@ buildPi :: (Fallible1 m, Builder m)
         => NameHint -> Arrow -> Type n
         -> (forall l. DExt n l => AtomName l -> m l (EffectRow l, Type l))
         -> m n (PiType n)
-buildPi hint arr ty body = liftImmut do
+buildPi hint arr ty body = do
   withFreshPiBinder hint (PiBinding arr ty) \b -> do
     (effs, resultTy) <- body $ binderName b
     return $ PiType b effs resultTy
@@ -465,7 +463,7 @@ buildNaryPi (Abs (Nest (b:>ty) bs) UnitE) cont = do
 buildNonDepPi :: EnvReader m
               => NameHint -> Arrow -> Type n -> EffectRow n -> Type n
               -> m n (PiType n)
-buildNonDepPi hint arr argTy effs resultTy = liftImmut $ liftBuilder do
+buildNonDepPi hint arr argTy effs resultTy = liftBuilder do
   argTy' <- sinkM argTy
   buildPi hint arr argTy' \_ -> do
     resultTy' <- sinkM resultTy
@@ -477,9 +475,9 @@ buildAbs
      , SinkableE e, Color c, ToBinding binding c)
   => NameHint
   -> binding n
-  -> (forall l. (Immut l, DExt n l) => Name c l -> m l (e l))
+  -> (forall l. DExt n l => Name c l -> m l (e l))
   -> m n (Abs (BinderP c binding) e n)
-buildAbs hint binding cont = liftImmut do
+buildAbs hint binding cont = do
   withFreshBinder hint binding \b -> do
     body <- cont $ binderName b
     return $ Abs (b:>binding) body
@@ -496,9 +494,9 @@ varsAsBinderNest (v:vs) = do
   return $ EmptyAbs (Nest (b:>ty) bs)
 
 typesAsBinderNest :: EnvReader m => [Type n] -> m n (EmptyAbs (Nest Binder) n)
-typesAsBinderNest types = liftImmut $ liftEnvReaderM $ go types
+typesAsBinderNest types = liftEnvReaderM $ go types
   where
-    go :: forall n. Immut n => [Type n] -> EnvReaderM n (EmptyAbs (Nest Binder) n)
+    go :: forall n. [Type n] -> EnvReaderM n (EmptyAbs (Nest Binder) n)
     go tys = case tys of
       [] -> return $ Abs Empty UnitE
       ty:rest -> withFreshBinder NoHint ty \b -> do
@@ -514,12 +512,11 @@ singletonBinderNest hint ty = do
 buildNaryAbs
   :: (ScopableBuilder m, SinkableE e, SubstE Name e, SubstE AtomSubstVal e, HoistableE e)
   => EmptyAbs (Nest Binder) n
-  -> (forall l. (Immut l, Distinct l, DExt n l) => [AtomName l] -> m l (e l))
+  -> (forall l. DExt n l => [AtomName l] -> m l (e l))
   -> m n (Abs (Nest Binder) e n)
-buildNaryAbs (EmptyAbs Empty) body =
-  liftImmut do
-    Distinct <- getDistinct
-    Abs Empty <$> body []
+buildNaryAbs (EmptyAbs Empty) body = do
+  Distinct <- getDistinct
+  Abs Empty <$> body []
 buildNaryAbs (EmptyAbs (Nest (b:>ty) bs)) body = do
   Abs b' (Abs bs' body') <-
     buildAbs (getNameHint b) ty \v -> do
@@ -606,7 +603,7 @@ buildUnaryAtomAlt ty body = do
 buildNewtype :: ScopableBuilder m
              => SourceName
              -> EmptyAbs (Nest Binder) n
-             -> (forall l. (Immut l, DExt n l) => [AtomName l] -> m l (Type l))
+             -> (forall l. DExt n l => [AtomName l] -> m l (Type l))
              -> m n (DataDef n)
 buildNewtype name paramBs body = do
   Abs paramBs' argBs <- buildNaryAbs paramBs \params -> do
@@ -848,7 +845,7 @@ zipPiBinders :: [Arrow] -> Nest Binder i i' -> Nest PiBinder i i'
 zipPiBinders = zipNest \arr (b :> ty) -> PiBinder b ty arr
 
 makeSuperclassGetter :: EnvReader m => Name ClassNameC n -> Int -> m n (Atom n)
-makeSuperclassGetter classDefName methodIdx = liftImmut $ liftBuilder do
+makeSuperclassGetter classDefName methodIdx = liftBuilder do
   classDefName' <- sinkM classDefName
   ClassDef _ _ defName <- getClassDef classDefName'
   DataDef sourceName paramBs _ <- lookupDataDef defName
@@ -865,7 +862,7 @@ emitMethodType hint classDef explicit idx = do
   emitBinding hint $ MethodBinding classDef idx getter
 
 makeMethodGetter :: EnvReader m => Name ClassNameC n -> [Bool] -> Int -> m n (Atom n)
-makeMethodGetter classDefName explicit methodIdx = liftImmut $ liftBuilder do
+makeMethodGetter classDefName explicit methodIdx = liftBuilder do
   classDefName' <- sinkM classDefName
   ClassDef _ _ defName <- getClassDef classDefName'
   DataDef sourceName paramBs _ <- lookupDataDef defName
@@ -1144,7 +1141,7 @@ reduceE monoid xs = liftEmitBuilder do
       emitOp $ PrimEffect (sink $ Var ref) $ MExtend (fmap sink monoid) x
 
 andMonoid :: EnvReader m => m n (BaseMonoid n)
-andMonoid =  liftM (BaseMonoid TrueAtom) $ liftImmut do
+andMonoid =  liftM (BaseMonoid TrueAtom) do
   liftBuilder $
     buildLam "_" PlainArrow BoolTy Pure \x ->
       buildLam "_" PlainArrow BoolTy Pure \y -> do
@@ -1242,14 +1239,14 @@ telescopicCapture bs e = do
   vs <- localVarsAndTypeVars bs e
   vTys <- mapM (getType . Var) vs
   let (vsSorted, tys) = unzip $ toposortAnnVars $ zip vs vTys
-  ty <- liftImmut $ liftEnvReaderM $ buildTelescopeTy vs tys
+  ty <- liftEnvReaderM $ buildTelescopeTy vs tys
   result <- buildTelescopeVal (map Var vsSorted) ty
   let ty' = ignoreHoistFailure $ hoist bs ty
   let ab  = ignoreHoistFailure $ hoist bs $ abstractFreeVarsNoAnn vsSorted e
   return (result, ty', ab)
 
 -- XXX: assumes arguments are toposorted
-buildTelescopeTy :: (EnvReader m, EnvExtender m, Immut n)
+buildTelescopeTy :: (EnvReader m, EnvExtender m)
                  => [AtomName n] -> [Type n] -> m n (Type n)
 buildTelescopeTy [] [] = return UnitTy
 buildTelescopeTy (v:vs) (ty:tys) = do

src/lib/CheapReduction.hs

@@ -62,7 +62,7 @@ newtype CheapReducerM (i :: S) (o :: S) (a :: *) =
             (EnvReaderT Identity)))) i o a)
   deriving ( Functor, Applicative, Monad, Alternative
            , EnvReader, ScopeReader, EnvExtender
-           , SubstReader AtomSubstVal, AlwaysImmut )
+           , SubstReader AtomSubstVal)
 
 newtype FailedDictTypes (n::S) = FailedDictTypes (MaybeE (ESet Type) n)
                                  deriving (SinkableE, HoistableE)
@@ -76,7 +76,7 @@ instance Monoid (FailedDictTypes n) where
 instance FallibleMonoid1 FailedDictTypes where
   mfail = FailedDictTypes $ NothingE
 
-class ( Alternative2 m, SubstReader AtomSubstVal m, AlwaysImmut2 m
+class ( Alternative2 m, SubstReader AtomSubstVal m
       , EnvReader2 m, EnvExtender2 m) => CheapReducer m where
   reportSynthesisFail :: Type o -> m i o ()
   updateCache :: AtomName o -> Maybe (Atom o) -> m i o ()
@@ -101,7 +101,7 @@ liftCheapReducerM subst (CheapReducerM m) = do
 
 cheapReduceFromSubst
   :: forall e m i o .
-     ( SubstReader AtomSubstVal m, EnvReader2 m, AlwaysImmut2 m
+     ( SubstReader AtomSubstVal m, EnvReader2 m
      , SinkableE e, SubstE AtomSubstVal e, HoistableE e)
   => e i -> m i o (e o)
 cheapReduceFromSubst e = traverseNames cheapSubstName =<< substM e
@@ -136,7 +136,6 @@ cheapReduceWithDeclsRec decls cont = case decls of
     optional (cheapReduceE expr) >>= \case
       Nothing -> do
         binding' <- substM binding
-        Immut <- getImmut
         withFreshBinder (getNameHint b) binding' \b' -> do
           updateCache (binderName b') Nothing
           extendSubst (b@>Rename (binderName b')) do

src/lib/GenericTraversal.hs

@@ -28,19 +28,19 @@ class (ScopableBuilder2 m, SubstReader Name m)
   traverseExpr :: Emits o => Expr i -> m i o (Expr o)
   traverseExpr = traverseExprDefault
 
-  traverseAtom :: Immut o => Atom i -> m i o (Atom o)
+  traverseAtom :: Atom i -> m i o (Atom o)
   traverseAtom = traverseAtomDefault
 
 traverseExprDefault :: Emits o => GenericTraverser m => Expr i -> m i o (Expr o)
-traverseExprDefault expr = liftImmut $ case expr of
+traverseExprDefault expr = case expr of
   App g xs -> App <$> tge g <*> mapM tge xs
   Atom x  -> Atom <$> tge x
   Op  op  -> Op   <$> mapM tge op
   Hof hof -> Hof  <$> mapM tge hof
   Case scrut alts resultTy effs ->
     Case <$> tge scrut <*> mapM traverseAlt alts <*> tge resultTy <*> substM effs
 
-traverseAtomDefault :: Immut o => GenericTraverser m => Atom i -> m i o (Atom o)
+traverseAtomDefault :: GenericTraverser m => Atom i -> m i o (Atom o)
 traverseAtomDefault atom = case atom of
   Var v -> Var <$> substM v
   Lam (LamExpr (LamBinder b ty arr eff) body) -> do
@@ -81,12 +81,12 @@ traverseAtomDefault atom = case atom of
   ProjectElt _ _ -> substM atom
   _ -> error $ "not implemented: " ++ pprint atom
 
-tge :: (Immut o, GenericallyTraversableE e, GenericTraverser m)
+tge :: (GenericallyTraversableE e, GenericTraverser m)
     => e i -> m i o (e o)
 tge = traverseGenericE
 
 class GenericallyTraversableE (e::E) where
-  traverseGenericE :: Immut o => GenericTraverser m => e i -> m i o (e o)
+  traverseGenericE :: GenericTraverser m => e i -> m i o (e o)
 
 instance GenericallyTraversableE Atom where
   traverseGenericE = traverseAtom
@@ -121,7 +121,7 @@ traverseDeclNest (Nest (Let b (DeclBinding ann _ expr)) rest) cont = do
   extendSubst (b @> v) $ traverseDeclNest rest cont
 
 traverseAlt
-  :: (Immut o, GenericTraverser m)
+  :: GenericTraverser m
   => Alt i
   -> m i o (Alt o)
 traverseAlt (Abs Empty body) = Abs Empty <$> tge body