diff --git a/src/lib/AbstractSyntax.hs b/src/lib/AbstractSyntax.hs
index 7647b5958..d9755ecde 100644
--- a/src/lib/AbstractSyntax.hs
+++ b/src/lib/AbstractSyntax.hs
@@ -112,7 +112,7 @@ topDecl = dropSrc topDecl' where
     tyConParams' <- aExplicitParams tyConParams
     givens' <- aOptGivens givens
     constructors' <- forM constructors \(v, ps) -> do
-      ps' <- toNest <$> mapM tyOptBinder ps
+      ps' <- toNest <$> mapM (tyOptBinder Explicit) ps
       return (v, ps')
     return $ UDataDefDecl
       (UDataDef name (givens' >>> tyConParams') $
@@ -134,8 +134,6 @@ topDecl = dropSrc topDecl' where
       return (fromString methodName, ty')
     return $ UInterface params' methodTys (fromString name) (toNest methodNames)
   topDecl' (CInstanceDecl def) = aInstanceDef def
-  topDecl' (CEffectDecl _ _) = error "not implemented"
-  topDecl' (CHandlerDecl _ _ _ _ _ _) = error "not implemented"
 
 decl :: LetAnn -> CSDecl -> SyntaxM (UDecl VoidS VoidS)
 decl ann = propagateSrcB \case
@@ -167,14 +165,14 @@ aInstanceDef (CInstanceDef clName args givens methods instNameAndParams) = do
 
 aDef :: CDef -> SyntaxM (SourceName, ULamExpr VoidS)
 aDef (CDef name params optRhs optGivens body) = do
-  explicitParams <- aExplicitParams params
+  explicitParams <- explicitBindersOptAnn params
   let rhsDefault = (ExplicitApp, Nothing, Nothing)
   (expl, effs, resultTy) <- fromMaybeM optRhs rhsDefault \(expl, optEffs, resultTy) -> do
     effs <- fromMaybeM optEffs UPure aEffects
     resultTy' <- expr resultTy
     return (expl, Just effs, Just resultTy')
   implicitParams <- aOptGivens optGivens
-  let allParams = fmapNest asOptAnn $ implicitParams >>> explicitParams
+  let allParams = fmapNest asOptAnn implicitParams >>> explicitParams
   body' <- block body
   return (name, ULamExpr allParams expl effs resultTy body')
 
@@ -185,53 +183,85 @@ stripParens :: Group -> Group
 stripParens (WithSrc _ (CParens [g])) = stripParens g
 stripParens g = g
 
+-- === combinators for different sorts of binder lists ===
+
+aOptGivens :: Maybe GivenClause -> SyntaxM (Nest UReqAnnBinder VoidS VoidS)
+aOptGivens optGivens = fromMaybeM optGivens Empty aGivens
+
+binderList
+  :: [Group] -> (Group -> SyntaxM (Nest (UAnnBinder req) VoidS VoidS))
+  -> SyntaxM (Nest (UAnnBinder req) VoidS VoidS)
+binderList gs cont = concatNests <$> forM gs \case
+  WithSrc _ (CGivens gs') -> aGivens gs'
+  g -> cont g
+
+withTrailingConstraints
+  :: Group -> (Group -> SyntaxM ((UAnnBinder req) VoidS VoidS))
+  -> SyntaxM (Nest (UAnnBinder req) VoidS VoidS)
+withTrailingConstraints g cont = case g of
+  Binary Pipe lhs c -> do
+    bs@(Nest (UAnnBinder _ b _) _) <- withTrailingConstraints lhs cont
+    (ctx, s) <- case b of
+      UBindSource ctx s -> return (ctx, s)
+      UIgnore     -> throw SyntaxErr "Can't constrain anonymous binders"
+      UBind _ _ _ -> error "Shouldn't have internal names until renaming pass"
+    c' <- expr c
+    let v = WithSrcE ctx $ UVar (SourceName ctx s)
+    return $ bs >>> UnaryNest (fromReqAnnBinder $ asConstraintBinder  v c')
+  _ -> UnaryNest <$> cont g
+  where
+    asConstraintBinder :: UExpr VoidS -> UConstraint VoidS -> UReqAnnBinder VoidS VoidS
+    asConstraintBinder v c = do
+      let t = ns $ UApp c [v] []
+      UAnnBinder (Inferred Nothing (Synth Full)) UIgnore (UAnn t)
+
+defaultAnn :: UExpr VoidS -> UOptAnnBinder VoidS VoidS -> UReqAnnBinder VoidS VoidS
+defaultAnn dAnn (UAnnBinder expl b ann) = do
+  let ann' = case ann of
+        UNoAnn -> dAnn
+        UAnn t -> t
+  UAnnBinder expl b (UAnn ann')
+
+aGivens :: GivenClause -> SyntaxM (Nest (UAnnBinder req) VoidS VoidS)
+aGivens (implicits, optConstraints) = do
+  implicits' <- concatNests <$> forM implicits \b -> withTrailingConstraints b implicitArgBinder
+  constraints <- fromMaybeM optConstraints Empty (\gs -> toNest <$> mapM synthBinder gs)
+  return $ fmapNest fromReqAnnBinder $ implicits' >>> constraints
+
+synthBinder :: Group -> SyntaxM (UReqAnnBinder VoidS VoidS)
+synthBinder g = tyOptBinder (Inferred Nothing (Synth Full)) g
+
+fromReqAnnBinder :: UReqAnnBinder n l -> UAnnBinder req n l
+fromReqAnnBinder (UAnnBinder expl b ann) = do
+  let ann' = case ann of
+        UAnn t -> UAnn t
+  UAnnBinder expl b ann'
+
+concatNests :: [Nest b VoidS VoidS] -> Nest b VoidS VoidS
+concatNests [] = Empty
+concatNests (b:bs) = b >>> concatNests bs
+
+implicitArgBinder :: Group -> SyntaxM (UReqAnnBinder VoidS VoidS)
+implicitArgBinder g = do
+  UAnnBinder _ b ann <- defaultAnn (ns tyKind) <$> binderOptTy (Inferred Nothing Unify) g
+  s <- case b of
+    UBindSource _ s -> return $ Just s
+    _               -> return Nothing
+  return $ UAnnBinder (Inferred s Unify) b ann
+
 aExplicitParams :: ExplicitParams -> SyntaxM (Nest UReqAnnBinder VoidS VoidS)
-aExplicitParams gs = generalBinders DataParam Explicit gs
+aExplicitParams bs = binderList bs \b -> withTrailingConstraints b \b' ->
+  defaultAnn (ns tyKind) <$> binderOptTy Explicit b'
 
-aOptAnnExplicitParams :: ExplicitParams -> SyntaxM (Nest UOptAnnBinder VoidS VoidS)
-aOptAnnExplicitParams gs = undefined
+aPiBinders :: ExplicitParams -> SyntaxM (Nest UReqAnnBinder VoidS VoidS)
+aPiBinders bs = binderList bs \b ->
+  UnaryNest <$> tyOptBinder Explicit b
 
-aOptGivens :: Maybe GivenClause -> SyntaxM (Nest UReqAnnBinder VoidS VoidS)
-aOptGivens optGivens = undefined
--- aOptGivens optGivens = do
---   (expls, implicitParams) <- unzip <$> fromMaybeM optGivens [] aGivens
---   return (expls, toNest implicitParams)
-
-aGivens :: GivenClause -> SyntaxM [Nest UReqAnnBinder VoidS VoidS]
-aGivens (implicits, optConstraints) = undefined
--- aGivens (implicits, optConstraints) = do
---   implicits' <- mapM (generalBinder DataParam (Inferred Nothing Unify)) implicits
---   constraints <- fromMaybeM optConstraints [] \gs -> do
---     mapM (generalBinder TypeParam (Inferred Nothing (Synth Full))) gs
---   return $ implicits' <> constraints
-
-generalBinders
-  :: ParamStyle -> Explicitness -> [Group]
-  -> SyntaxM (Nest UReqAnnBinder VoidS VoidS)
-generalBinders paramStyle expl params = undefined
--- generalBinders paramStyle expl params = do
---   (expls, bs) <- unzip . concat <$> forM params \case
---     WithSrc _ (CGivens gs) -> aGivens gs
---     p -> (:[]) <$> generalBinder paramStyle expl p
---   return (expls, toNest bs)
-
-optAnnBinder :: Group -> SyntaxM (UOptAnnBinder VoidS VoidS)
-optAnnBinder = undefined
-
-generalBinder :: ParamStyle -> Explicitness -> Group
-              -> SyntaxM (UReqAnnBinder VoidS VoidS)
-generalBinder paramStyle expl g = undefined
--- generalBinder paramStyle expl g = case expl of
---   Inferred _ (Synth _) -> (expl,) <$> tyOptBinder g
---   Inferred _ Unify -> do
---     b <- binderOptTy g
---     expl' <- return case b of
---       UAnnBinder (UBindSource _ s) _ _ -> Inferred (Just s) Unify
---       _ -> expl
---     return (expl', b)
---   Explicit -> (expl,) <$> case paramStyle of
---     TypeParam -> tyOptBinder g
---     DataParam -> binderOptTy g
+explicitBindersOptAnn :: ExplicitParams -> SyntaxM (Nest UOptAnnBinder VoidS VoidS)
+explicitBindersOptAnn bs = binderList bs \b -> withTrailingConstraints b \b' ->
+  binderOptTy Explicit b'
+
+-- ===
 
 -- Binder pattern with an optional type annotation
 patOptAnn :: Group -> SyntaxM (UPat VoidS VoidS, Maybe (UType VoidS))
@@ -290,45 +320,33 @@ pat = propagateSrcB pat' where
       _ -> error "unexpected postfix group (should be ruled out at grouping stage)"
   pat' _ = throw SyntaxErr "Illegal pattern"
 
-data ParamStyle
- = TypeParam  -- binder optional, used in pi types
- | DataParam  -- type optional  , used in lambda
-
-tyOptBinder :: Group -> SyntaxM (UAnnBinder req VoidS VoidS)
-tyOptBinder = \case
+tyOptBinder :: Explicitness -> Group -> SyntaxM (UAnnBinder req VoidS VoidS)
+tyOptBinder expl = \case
   Binary Pipe  _ _     -> throw SyntaxErr "Unexpected constraint"
   Binary Colon name ty -> do
     b <- uBinder name
     ann <- UAnn <$> expr ty
-    return $ UAnnBinder Explicit b ann
+    return $ UAnnBinder expl b ann
   g -> do
     ty <- expr g
-    return $ UAnnBinder Explicit UIgnore (UAnn ty)
-
-binderOptTy :: Group -> SyntaxM (UOptAnnBinder VoidS VoidS)
-binderOptTy g = undefined
--- binderOptTy g = do
---   (g', constraints) <- trailingConstraints g
---   case g' of
---     Binary Colon name ty -> do
---       b <- uBinder name
---       ann <- UAnn <$> expr ty
---       return $ UAnnBinder b ann constraints
---     _ -> do
---       b <- uBinder g'
---       return $ UAnnBinder b UNoAnn constraints
-
-binderReqTy :: Group -> SyntaxM (UReqAnnBinder VoidS VoidS)
-binderReqTy = undefined
-
-trailingConstraints :: Group -> SyntaxM (Group, [UConstraint VoidS])
-trailingConstraints gTop = go [] gTop where
-  go :: [UConstraint VoidS] -> Group -> SyntaxM (Group, [UConstraint VoidS])
-  go cs = \case
-    Binary Pipe lhs c -> do
-      c' <- expr c
-      go (c':cs) lhs
-    g -> return (g, cs)
+    return $ UAnnBinder expl UIgnore (UAnn ty)
+
+binderOptTy :: Explicitness -> Group -> SyntaxM (UOptAnnBinder VoidS VoidS)
+binderOptTy expl = \case
+  Binary Colon name ty -> do
+    b <- uBinder name
+    ann <- UAnn <$> expr ty
+    return $ UAnnBinder expl b ann
+  g -> do
+    b <- uBinder g
+    return $ UAnnBinder expl b UNoAnn
+
+binderReqTy :: Explicitness -> Group -> SyntaxM (UReqAnnBinder VoidS VoidS)
+binderReqTy expl (Binary Colon name ty) = do
+  b <- uBinder name
+  ann <- UAnn <$> expr ty
+  return $ UAnnBinder expl b ann
+binderReqTy _ _ = throw SyntaxErr $ "Expected an annotated binder"
 
 argList :: [Group] -> SyntaxM ([UExpr VoidS], [UNamedArg VoidS])
 argList gs = partitionEithers <$> mapM singleArg gs
@@ -391,7 +409,7 @@ blockDecls [WithSrc src d] = addSrcContext src case d of
   CExpr g -> (Empty,) <$> expr g
   _ -> throw SyntaxErr "Block must end in expression"
 blockDecls (WithSrc pos (CBind b rhs):ds) = do
-  b' <- optAnnBinder b
+  b' <- binderOptTy Explicit b
   rhs' <- asExpr <$> block rhs
   body <- block $ IndentedBlock ds
   let lam = ULam $ ULamExpr (UnaryNest b') ExplicitApp Nothing Nothing body
@@ -425,7 +443,7 @@ expr = propagateSrcE expr' where
   expr' (CArrow lhs effs rhs) = do
     case lhs of
       WithSrc _ (CParens gs) -> do
-        bs <- generalBinders TypeParam Explicit gs
+        bs <- aPiBinders gs
         effs' <- fromMaybeM effs UPure aEffects
         resultTy <- expr rhs
         return $ UPi $ UPiExpr bs ExplicitApp effs' resultTy
@@ -465,7 +483,7 @@ expr = propagateSrcE expr' where
       Colon         -> throw SyntaxErr "Colon separates binders from their type annotations, is not a standalone operator.\nIf you are trying to write a dependent type, use parens: (i:Fin 4) => (..i)"
       ImplicitArrow -> case lhs of
         WithSrc _ (CParens gs) -> do
-          bs <- generalBinders TypeParam Explicit gs
+          bs <- aPiBinders gs
           resultTy <- expr rhs
           return $ UPi $ UPiExpr bs ImplicitApp UPure resultTy
         _ -> throw SyntaxErr "Argument types should be in parentheses"
@@ -505,7 +523,7 @@ expr = propagateSrcE expr' where
       range :: UExpr VoidS -> UExpr VoidS -> UExpr' VoidS
       range rangeName lim = explicitApp rangeName [ns UHole, lim]
   expr' (CLambda params body) = do
-    params' <- aOptAnnExplicitParams $ map stripParens params
+    params' <- explicitBindersOptAnn $ map stripParens params
     body' <- block body
     return $ ULam $ ULamExpr params' ExplicitApp Nothing Nothing body'
   expr' (CFor kind indices body) = do
@@ -515,7 +533,7 @@ expr = propagateSrcE expr' where
           KRof  -> (Rev, False)
           KRof_ -> (Rev, True)
     -- TODO: Can we fetch the source position from the error context, to feed into `buildFor`?
-    e <- buildFor (0, 0) dir <$> mapM binderOptTy indices <*> block body
+    e <- buildFor (0, 0) dir <$> mapM (binderOptTy Explicit) indices <*> block body
     if trailingUnit
       then return $ UDo $ ns $ UBlock (UnaryNest (nsB $ UExprDecl e)) (ns unitExpr)
       else return $ dropSrcE e
@@ -534,7 +552,7 @@ expr = propagateSrcE expr' where
     ty <- expr lhs
     case rhs of
       [b] -> do
-        b' <- binderReqTy b
+        b' <- binderReqTy Explicit b
         return $ UDepPairTy $ UDepPairType ImplicitDepPair b' ty
       _ -> error "n-ary dependent pairs not implemented"
 
@@ -544,6 +562,9 @@ charExpr c = ULit $ Word8Lit $ fromIntegral $ fromEnum c
 unitExpr :: UExpr' VoidS
 unitExpr = UPrim (UCon $ P.ProdCon) []
 
+tyKind :: UExpr' VoidS
+tyKind = UPrim (UPrimTC P.TypeKind) []
+
 -- === Builders ===
 
 -- TODO Does this generalize?  Swap list for Nest?
diff --git a/src/lib/CheapReduction.hs b/src/lib/CheapReduction.hs
index 56c0e8505..99559bc17 100644
--- a/src/lib/CheapReduction.hs
+++ b/src/lib/CheapReduction.hs
@@ -309,6 +309,9 @@ instance (CheaplyReducibleE r e1 e1', CheaplyReducibleE r e2 e2')
     cheapReduceE (LeftE e) = LeftE <$> cheapReduceE e
     cheapReduceE (RightE e) = RightE <$> cheapReduceE e
 
+instance CheaplyReducibleE r e e' => CheaplyReducibleE r (ListE e) (ListE e') where
+  cheapReduceE (ListE xs) = ListE <$> mapM cheapReduceE xs
+
 -- XXX: TODO: figure out exactly what our normalization invariants are. We
 -- shouldn't have to choose `normalizeProj` or `asNaryProj` on a
 -- case-by-case basis. This is here for now because it makes it easier to switch
diff --git a/src/lib/ConcreteSyntax.hs b/src/lib/ConcreteSyntax.hs
index 06cbc702b..32eabb071 100644
--- a/src/lib/ConcreteSyntax.hs
+++ b/src/lib/ConcreteSyntax.hs
@@ -199,7 +199,6 @@ topDecl' =
   <|> interfaceDef
   <|> (CInstanceDecl <$> instanceDef True)
   <|> (CInstanceDecl <$> instanceDef False)
-  <|> effectDef
 
 proseBlock :: Parser SourceBlock'
 proseBlock = label "prose block" $ char '\'' >> fmap (Misc . ProseBlock . fst) (withSource consumeTillBreak)
@@ -291,26 +290,6 @@ interfaceDef = do
       return (methodName, ty)
   return $ CInterface className params methodDecls
 
-effectDef :: Parser CTopDecl'
-effectDef = do
-  keyWord EffectKW
-  effName <- anyName
-  sigs <- opSigList
-  return $ CEffectDecl (fromString effName) sigs
-
-opSigList :: Parser [(SourceName, UResumePolicy, Group)]
-opSigList = onePerLine do
-  policy <- resumePolicy
-  v <- anyName
-  void $ sym ":"
-  ty <- cGroup
-  return (fromString v, policy, ty)
-
-resumePolicy :: Parser UResumePolicy
-resumePolicy =  (keyWord JmpKW $> UNoResume)
-            <|> (keyWord DefKW $> ULinearResume)
-            <|> (keyWord CtlKW $> UAnyResume)
-
 nameAndType :: Parser (SourceName, Group)
 nameAndType = do
   n <- anyName
@@ -693,11 +672,11 @@ ops =
   , [symOpL   "@"]
   , [symOpN  "::"]
   , [symOpR   "$"]
-  , [symOpL   "|"]
   , [symOpN  "+=", symOpN  ":="]
   -- Associate right so the mistaken utterance foo : i:Fin 4 => (..i)
   -- groups as a bad pi type rather than a bad binder
   , [symOpR   ":"]
+  , [symOpL   "|"]
   , [symOpR  ",>"]
   , [symOpR  "&>"]
   , [withClausePostfix]
diff --git a/src/lib/Inference.hs b/src/lib/Inference.hs
index a29faeb96..40ba8a770 100644
--- a/src/lib/Inference.hs
+++ b/src/lib/Inference.hs
@@ -97,9 +97,9 @@ inferTopUDecl (UInterface paramBs methodTys className methodNames) result = do
 inferTopUDecl (UInstance className bs params methods maybeName expl) result = do
   let (InternalName _ _ className') = className
   def <- liftInfererM $ withRoleUBinders bs \(ZipB roleExpls bs') -> do
-    ClassDef _ _ _ roleExpls paramBinders _ _ <- lookupClassDef (sink className')
-    let expls = snd <$> roleExpls
-    params' <- checkInstanceParams expls paramBinders params
+    ClassDef _ _ _ classRoleExpls paramBinders _ _ <- lookupClassDef (sink className')
+    let classExpls = snd <$> classRoleExpls
+    params' <- checkInstanceParams classExpls paramBinders params
     body <- checkInstanceBody (sink className') params' methods
     return $ InstanceDef className' roleExpls bs' params' body
   UDeclResultDone <$> case maybeName of
@@ -170,6 +170,7 @@ data Solution (n::S) =
 
 data InfState (n::S) = InfState
   { infSolverSubst :: SolverSubst n
+  , givens         :: Givens n
   , infEffects     :: EffectRow CoreIR n }
 
 data InfStateUpdate (n::S) =
@@ -200,7 +201,7 @@ liftInfererMSubst cont = do
   liftM fst $ liftExcept $ liftM fromJust $ runSearcherM ansM
  where
   emptyInfState :: InfState n
-  emptyInfState = InfState emptySolverSubst Pure
+  emptyInfState = InfState emptySolverSubst (Givens HM.empty) Pure
 
 liftInfererM :: (EnvReader m, Fallible1 m)
              => InfererM n n a -> m n a
@@ -230,14 +231,14 @@ maybeZonk e = do
 
 requireZonked :: CAtomName n -> InfererM i n ()
 requireZonked v = do
-  InfState (SolverSubst s) effs <- getInfState
+  InfState (SolverSubst s) g effs <- getInfState
   case M.lookup v s of
     Just (Solved x) -> do
       maybeZonk x >>= \case
         Nothing -> return ()
         Just x' -> do
           let s' = M.insert v (Solved x') s
-          setInfState $ InfState (SolverSubst s') effs
+          setInfState $ InfState (SolverSubst s') g effs
     _ -> return ()
 
 -- XXX: This lets us zonk things that don't implement SubstE AtomSubstVal but
@@ -295,7 +296,11 @@ withFreshBinderInf
   :: NameHint -> Explicitness -> CType o -> InfererCPSB CBinder i o a
 withFreshBinderInf hint expl ty cont = builderToInfererM \subst s -> do
   withFreshBinder hint ty \b -> do
-    (ans, diff) <- infererMToBuilder (sink subst) (sink s) $ cont b
+    (ans, diff) <- infererMToBuilder (sink subst) (sink s) do
+      givens <- case expl of
+        Inferred _ (Synth _) -> return [Var $ binderVar b]
+        _ -> return []
+      extendGivens givens $ cont b
     diff' <- hoistInfDiffState b diff
     return (ans, diff')
 {-# INLINE withFreshBinderInf #-}
@@ -364,8 +369,15 @@ withFreshInferenceNameEmits desc k cont =
 {-# INLINE withFreshInferenceNameEmits #-}
 
 withFreshSkolemName :: Zonkable e => Kind CoreIR o -> InfererCPSE CAtomVar i o e
-withFreshSkolemName k cont = undefined
--- emitSolver $ SkolemBound k
+withFreshSkolemName ty cont = builderToInfererM \subst s -> do
+  withFreshBinder noHint (SkolemBound ty) \b -> do
+    (ans, diff) <- infererMToBuilder (sink subst) (sink s) do
+      v <- toAtomVar $ binderName b
+      ans <- cont v
+      zonk ans
+      liftHoistExcept $ hoist b ans
+    diff' <- hoistInfDiffState b diff
+    return (ans, diff')
 {-# INLINE withFreshSkolemName #-}
 
 updateInfState :: InfStateUpdate o -> InfererM i o ()
@@ -392,16 +404,12 @@ withInfState f cont = InfererM do
   return ans
 {-# INLINE withInfState #-}
 
-extendSynthCandidatesInf :: Explicitness -> CAtomName n -> InfOutMap n -> InfOutMap n
-extendSynthCandidatesInf c v = undefined
-{-# INLINE extendSynthCandidatesInf #-}
-
 withoutEffects :: InfererM i o a -> InfererM i o a
 withoutEffects cont = withAllowedEffects Pure cont
 {-# INLINE withoutEffects #-}
 
 withAllowedEffects :: EffectRow CoreIR o -> InfererM i o a -> InfererM i o a
-withAllowedEffects effs cont = withInfState (\(InfState s _) -> InfState s effs) cont
+withAllowedEffects effs cont = withInfState (\(InfState s g _) -> InfState s g effs) cont
 {-# INLINE withAllowedEffects #-}
 
 -- === actual inference pass ===
@@ -512,10 +520,10 @@ checkOrInferRho
 checkOrInferRho hint uExprWithSrc@(WithSrcE pos expr) reqTy = do
  addSrcContext pos $ confuseGHC >>= \_ -> case expr of
   UVar _ -> inferAndInstantiate
-  ULit l -> matchRequirement $ Con $ Lit l
+  ULit l -> matchReq reqTy $ Con $ Lit l
   ULam lamExpr -> case reqTy of
     Check (Pi piTy) -> Lam <$> checkULam lamExpr piTy
-    _               -> Lam <$> inferULam lamExpr >>= matchRequirement
+    _               -> Lam <$> inferULam lamExpr >>= matchReq reqTy
   UFor dir uFor -> do
     lam@(UnaryLamExpr b' _) <- case reqTy of
       Check (TabPi tabPiTy) -> do checkUForExpr uFor tabPiTy
@@ -523,14 +531,14 @@ checkOrInferRho hint uExprWithSrc@(WithSrcE pos expr) reqTy = do
       Infer   -> inferUForExpr uFor
     ixTy <- asIxType $ binderType b'
     result <- emitHof $ For dir ixTy lam
-    matchRequirement result
+    matchReq reqTy result
   UApp f posArgs namedArgs -> do
     f' <- inferWithoutInstantiation f >>= zonk
     checkOrInferApp f' posArgs namedArgs reqTy
   UTabApp tab args -> do
     tab' <- inferRho noHint tab >>= zonk
-    inferTabApp (srcPos tab) tab' args >>= matchRequirement
-  UPi (UPiExpr bs appExpl effs ty) -> matchRequirement =<< do
+    inferTabApp (srcPos tab) tab' args >>= matchReq reqTy
+  UPi (UPiExpr bs appExpl effs ty) -> matchReq reqTy =<< do
     -- TODO: check explicitness constraints
     withUBinders bs \(ZipB expls bs') -> do
       effTy' <- EffTy <$> checkUEffRow effs <*> checkUType ty
@@ -540,8 +548,8 @@ checkOrInferRho hint uExprWithSrc@(WithSrcE pos expr) reqTy = do
       liftM (Abs b') $ withoutEffects $ checkUType ty
     d <- getIxDict $ binderType b'
     let piTy = TabPiType d b' ty'
-    matchRequirement $ Type $ TabPi piTy
-  UDepPairTy (UDepPairType expl b rhs) -> matchRequirement =<< do
+    matchReq reqTy $ Type $ TabPi piTy
+  UDepPairTy (UDepPairType expl b rhs) -> matchReq reqTy =<< do
     withUBinder b \(WithAttrB _ b') -> withoutEffects do
       rhs' <- checkUType rhs
       return $ Type $ DepPairTy $ DepPairType expl b' rhs'
@@ -561,24 +569,27 @@ checkOrInferRho hint uExprWithSrc@(WithSrcE pos expr) reqTy = do
       scrut'' <- zonk scrut'
       buildSortedCase scrut'' alts' reqTy'
   UDo block -> withBlockDecls block \result -> checkOrInferRho hint result (sink reqTy)
-  UTabCon xs -> inferTabCon hint xs reqTy >>= matchRequirement
+  UTabCon xs -> inferTabCon hint xs reqTy >>= matchReq reqTy
   UTypeAnn val ty -> do
     ty' <- zonk =<< checkUType ty
     val' <- checkSigma hint val ty'
-    matchRequirement val'
+    matchReq reqTy val'
   UPrim UTuple xs -> case reqTy of
     Check TyKind -> Type . ProdTy <$> mapM checkUType xs
+    Check (ProdTy reqTys) -> do
+      when (length reqTys /= length xs) $ throw TypeErr "Tuple length mismatch"
+      ProdVal <$> forM (zip reqTys xs) \(reqTy', x) -> checkSigma noHint x reqTy'
     _ -> do
       xs' <- mapM (inferRho noHint) xs
-      matchRequirement $ ProdVal xs'
+      matchReq reqTy $ ProdVal xs'
   UPrim UMonoLiteral [WithSrcE _ l] -> case l of
-    UIntLit x -> matchRequirement $ Con $ Lit $ Int32Lit $ fromIntegral x
-    UNatLit x -> matchRequirement $ Con $ Lit $ Word32Lit $ fromIntegral x
+    UIntLit x -> matchReq reqTy $ Con $ Lit $ Int32Lit $ fromIntegral x
+    UNatLit x -> matchReq reqTy $ Con $ Lit $ Word32Lit $ fromIntegral x
     _ -> throw MiscErr "argument to %monoLit must be a literal"
   UPrim UExplicitApply (f:xs) -> do
     f' <- inferWithoutInstantiation f
     xs' <- mapM (inferRho noHint) xs
-    applySigmaAtom f' xs' >>= matchRequirement
+    applySigmaAtom f' xs' >>= matchReq reqTy
   UPrim UProjNewtype [x] -> do
     x' <- inferRho hint x >>= emitHinted hint . Atom
     unwrapNewtype $ Var x'
@@ -589,7 +600,7 @@ checkOrInferRho hint uExprWithSrc@(WithSrcE pos expr) reqTy = do
           LetBound (DeclBinding _ (Atom e)) -> return e
           _ -> return $ Var v
         x' -> return x'
-    matchRequirement =<< matchPrimApp prim xs'
+    matchReq reqTy =<< matchPrimApp prim xs'
   UFieldAccess _ _ -> inferAndInstantiate
   UNatLit x -> do
     let defaultVal = Con $ Lit $ Word32Lit $ fromIntegral x
@@ -599,41 +610,42 @@ checkOrInferRho hint uExprWithSrc@(WithSrcE pos expr) reqTy = do
     let defaultVal = Con $ Lit $ Int32Lit $ fromIntegral x
     let litVal     = Con $ Lit $ Int64Lit $ fromIntegral x
     applyFromLiteralMethod reqTy "from_integer" defaultVal IntDefault litVal
-  UFloatLit x -> matchRequirement $ Con $ Lit  $ Float32Lit $ realToFrac x
+  UFloatLit x -> matchReq reqTy $ Con $ Lit  $ Float32Lit $ realToFrac x
   -- TODO: Make sure that this conversion is not lossy!
   where
-    matchRequirement :: Ext o o' => CAtom o' -> InfererM i o' (CAtom o')
-    matchRequirement x = return x <*
-      case reqTy of
-        Infer -> return ()
-        Check req -> do
-          ty <- return $ getType x
-          req' <- sinkM req
-          constrainTypesEq req' ty
-    {-# INLINE matchRequirement #-}
-
     inferAndInstantiate :: InfererM i o (CAtom o)
     inferAndInstantiate = do
       sigmaAtom <- maybeInterpretPunsAsTyCons reqTy =<< inferWithoutInstantiation uExprWithSrc
-      instantiateSigma sigmaAtom >>= matchRequirement
+      instantiateSigma reqTy sigmaAtom
     {-# INLINE inferAndInstantiate #-}
 
+matchReq :: Ext o o' => RequiredTy CType o -> CAtom o' -> InfererM i o' (CAtom o')
+matchReq reqTy x = return x <*
+  case reqTy of
+    Infer -> return ()
+    Check req -> do
+      ty <- return $ getType x
+      req' <- sinkM req
+      constrainTypesEq req' ty
+{-# INLINE matchReq #-}
+
 applyFromLiteralMethod
   :: Emits n => RequiredTy CType n
   -> SourceName -> CAtom n -> DefaultType -> CAtom n -> InfererM i n (CAtom n)
 applyFromLiteralMethod Infer methodName defaultVal _ _  = return defaultVal
--- applyFromLiteralMethod (Check resultTy) methodName  defaultVal defaultTy litVal = do
---   lookupSourceMap methodName >>= \case
---     Nothing -> return defaultVal
---     Just ~(UMethodVar methodName') -> do
---       MethodBinding className _ <- lookupEnv methodName'
---       dictTy <- DictTy <$> dictType className [TypeAsAtom resultTy]
---       case resultTy of
---         TyVar (AtomVar v _) -> isInferenceName v >>= \case
---           True -> updateInfState $ AddDefault v defaultTy
---           False -> return ()
---         _ -> return ()
---       emitExpr =<< mkApplyMethod (DictHole (AlwaysEqual emptySrcPosCtx) dictTy Full) 0 [litVal]
+applyFromLiteralMethod (Check resultTy) methodName  defaultVal defaultTy litVal = do
+  lookupSourceMap methodName >>= \case
+    Nothing -> return defaultVal
+    Just ~(UMethodVar methodName') -> do
+      MethodBinding className _ <- lookupEnv methodName'
+      dictTy <- DictTy <$> dictType className [TypeAsAtom resultTy]
+      case resultTy of
+        TyVar (AtomVar v _) -> isInferenceName v >>= \case
+          True -> updateInfState $ AddDefault v defaultTy
+          False -> return ()
+        _ -> return ()
+      d <- trySynthTerm dictTy Full
+      emitExpr =<< mkApplyMethod d 0 [litVal]
 
 -- atom that requires instantiation to become a rho type
 data SigmaAtom n =
@@ -716,14 +728,14 @@ getFieldDefs ty = case ty of
   where
     noFields s = throw TypeErr $ "Can't get fields for type " ++ pprint ty ++ s
 
-instantiateSigma :: Emits o => SigmaAtom o -> InfererM i o (CAtom o)
-instantiateSigma sigmaAtom = case getType sigmaAtom of
+instantiateSigma :: Emits o => RequiredTy CType o -> SigmaAtom o -> InfererM i o (CAtom o)
+instantiateSigma reqTy sigmaAtom = case getType sigmaAtom of
   Pi piTy@(CorePiType ExplicitApp _ _ _) -> do
     Lam <$> etaExpandExplicits fDesc piTy \args ->
-      applySigmaAtom (sink sigmaAtom) args
-  Pi (CorePiType ImplicitApp expls bs (EffTy _ resultTy)) -> do
-    inferMixedArgs @UExpr fDesc expls (Abs bs resultTy) ([], []) \args ->
-      applySigmaAtom (sink sigmaAtom) args
+      applySigmaAtom (sink sigmaAtom) args >>= matchReq reqTy
+  Pi (CorePiType ImplicitApp expls bs _) -> do
+    inferMixedArgs @UExpr fDesc expls (Abs bs UnitE) ([], []) \args ->
+      applySigmaAtom (sink sigmaAtom) args >>= matchReq reqTy
   DepPairTy (DepPairType ImplicitDepPair _ _) ->
     -- TODO: we should probably call instantiateSigma again here in case
     -- we have nested dependent pairs. Also, it looks like this doesn't
@@ -731,7 +743,7 @@ instantiateSigma sigmaAtom = case getType sigmaAtom of
     fallback >>= getSnd
   _ -> fallback
   where
-   fallback = case sigmaAtom of
+   fallback = matchReq reqTy =<< case sigmaAtom of
      SigmaAtom _ x -> return x
      SigmaUVar _ _ v -> case v of
        UAtomVar v' -> do
@@ -808,16 +820,16 @@ checkOrInferApp
 checkOrInferApp f' posArgs namedArgs reqTy = do
   f <- maybeInterpretPunsAsTyCons reqTy f'
   case getType f of
-    Pi (CorePiType appExpl expls bs effTy) -> case appExpl of
+    Pi (CorePiType appExpl expls bs _) -> case appExpl of
       ExplicitApp -> do
         checkArity expls posArgs
-        inferMixedArgs fDesc expls (Abs bs effTy) (posArgs, namedArgs) \args' ->
-          applySigmaAtom (sink f) args' >>= matchRequirement
+        inferMixedArgs fDesc expls (Abs bs UnitE) (posArgs, namedArgs) \args' ->
+          applySigmaAtom (sink f) args' >>= matchReq reqTy
       ImplicitApp -> do
         -- TODO: should this already have been done by the time we get `f`?
-        inferMixedArgs @UExpr fDesc expls (Abs bs effTy) ([], []) \implicitArgs -> do
+        inferMixedArgs @UExpr fDesc expls (Abs bs UnitE) ([], []) \implicitArgs -> do
           f'' <- SigmaAtom (Just fDesc) <$> applySigmaAtom (sink f) implicitArgs
-          checkOrInferApp f'' posArgs namedArgs Infer >>= matchRequirement
+          checkOrInferApp f'' posArgs namedArgs Infer >>= matchReq reqTy
     -- TODO: special-case error for when `fTy` can't possibly be a function
     fTy -> do
       when (not $ null namedArgs) do
@@ -833,15 +845,6 @@ checkOrInferApp f' posArgs namedArgs reqTy = do
   fDesc :: SourceName
   fDesc = getSourceName f'
 
-  matchRequirement :: Ext o o' => CAtom o' -> InfererM i o' (CAtom o')
-  matchRequirement x = return x <*
-    case reqTy of
-      Infer -> return ()
-      Check req -> do
-        ty <- return $ getType x
-        req' <- sinkM req
-        constrainTypesEq req' ty
-
 maybeInterpretPunsAsTyCons :: RequiredTy CType n -> SigmaAtom n -> InfererM i n (SigmaAtom n)
 maybeInterpretPunsAsTyCons (Check TyKind) (SigmaUVar sn _ (UPunVar v)) = do
   let v' = UTyConVar v
@@ -938,19 +941,19 @@ type MixedArgs arg = ([arg], [(SourceName, arg)])  -- positional args, named arg
 
 -- TODO: check that there are no extra named args provided
 inferMixedArgs
-  :: (ExplicitArg arg, Emits o, SubstE (SubstVal Atom) e, Zonkable e, Zonkable e')
+  :: (ExplicitArg arg, Emits o, Zonkable e)
   => SourceName -> [Explicitness]
-  -> Abs (Nest CBinder) e o -> MixedArgs (arg i)
-  -> (forall o'. (Emits o', DExt o o') => [CAtom o'] -> InfererM i o' (e' o'))
-  -> InfererM i o (e' o)
+  -> EmptyAbs (Nest CBinder) o -> MixedArgs (arg i)
+  -> (forall o'. (Emits o', DExt o o') => [CAtom o'] -> InfererM i o' (e o'))
+  -> InfererM i o (e o)
 inferMixedArgs fSourceName explsTop bsAbs argsTop@(_, namedArgs) cont = do
   checkNamedArgValidity explsTop (map fst namedArgs)
   go explsTop bsAbs argsTop \args -> cont args
  where
-  go :: (Emits o, ExplicitArg arg, SubstE (SubstVal Atom) e, Zonkable e, Zonkable e')
-     => [Explicitness] -> Abs (Nest CBinder) e o -> MixedArgs (arg i)
-     -> (forall o'. (Emits o', DExt o o') => [CAtom o'] -> InfererM i o' (e' o'))
-     -> InfererM i o (e' o)
+  go :: (Emits o, ExplicitArg arg, Zonkable e)
+     => [Explicitness] -> EmptyAbs (Nest CBinder) o -> MixedArgs (arg i)
+     -> (forall o'. (Emits o', DExt o o') => [CAtom o'] -> InfererM i o' (e o'))
+     -> InfererM i o (e o)
   go [] (Abs Empty _) _ cont = withDistinct $ cont []
   go (expl:expls) (Abs (Nest b bs) result) args cont = do
     let restBs = Abs bs result
@@ -1321,16 +1324,29 @@ withRoleUBinders bs cont = do
     {-# INLINE inferRole #-}
 
 requireAnn :: UOptAnnBinder l l' -> InfererM i o (UReqAnnBinder l l')
-requireAnn = undefined
+requireAnn (UAnnBinder expl b (UAnn ann)) = return $ UAnnBinder expl b (UAnn ann)
+requireAnn (UAnnBinder _ b UNoAnn) = addSrcContext (srcPos b) $
+  throw TypeErr "Binder requires annotation"
 
-checkOptAnnBinders
+checkLamBinders
   :: [Explicitness] -> Nest CBinder o any -> Nest UOptAnnBinder i i'
   -> InfererCPSB2 (Nest CBinder) i i' o a
-checkOptAnnBinders [] Empty Empty cont = withDistinct $ cont Empty
--- checkOptAnnBinders (expl:expls) (Nest b bs) (Nest ub ubs) =
---   checkOptAnnBinder
---   [] Empty Empty cont = withDistinct $ cont Empty
---   _ _ _ _ = undefined
+checkLamBinders [] Empty Empty cont = withDistinct $ cont Empty
+checkLamBinders (piExpl:piExpls) (Nest (piB:>piAnn) piBs) lamBs cont = do
+  case piExpl of
+    Inferred _ _ -> do
+      withFreshBinderInf (getNameHint piB) piExpl piAnn \b -> do
+        Abs piBs' UnitE <- applyRename (piB@>binderName b) (EmptyAbs piBs)
+        checkLamBinders piExpls piBs' lamBs \bs -> cont (Nest b bs)
+    Explicit -> case lamBs of
+      Nest (UAnnBinder Explicit lamB lamAnn) lamBsRest -> do
+        case lamAnn of
+          UAnn lamAnn' -> checkUType lamAnn' >>= constrainTypesEq piAnn
+          UNoAnn -> return ()
+        withFreshBinderInf (getNameHint lamB) Explicit piAnn \b -> do
+          Abs piBs' UnitE <- applyRename (piB@>binderName b) (EmptyAbs piBs)
+          extendRenamer (lamB@>sink (binderName b)) $
+            checkLamBinders piExpls piBs' lamBsRest \bs -> cont (Nest b bs)
 
 inferUForExpr :: Emits o => UForExpr i -> InfererM i o (LamExpr CoreIR o)
 inferUForExpr (UForExpr b body) = do
@@ -1357,7 +1373,7 @@ inferULam (ULamExpr bs appExpl effs resultTy body) = do
 
 checkUForExpr :: Emits o => UForExpr i -> TabPiType CoreIR o -> InfererM i o (LamExpr CoreIR o)
 checkUForExpr (UForExpr bFor body) tabPi@(TabPiType _ bPi _) = do
-  checkOptAnnBinders [Explicit] (UnaryNest bPi) (UnaryNest bFor) \(UnaryNest bFor') -> do
+  checkLamBinders [Explicit] (UnaryNest bPi) (UnaryNest bFor) \(UnaryNest bFor') -> do
     resultTy' <- instantiate (sink tabPi) [Var $ binderVar bFor']
     body' <- buildBlockInf $ withBlockDecls body \result ->
       checkSigma noHint result (sink resultTy')
@@ -1369,7 +1385,7 @@ checkULam (ULamExpr lamBs lamAppExpl lamEffs lamResultTy body)
   checkArity expls (nestToList (const ()) lamBs)
   when (piAppExpl /= lamAppExpl) $ throw TypeErr $ "Wrong arrow. Expected "
      ++ pprint piAppExpl ++ " got " ++ pprint lamAppExpl
-  checkOptAnnBinders expls piBs lamBs \lamBs' -> do
+  checkLamBinders expls piBs lamBs \lamBs' -> do
     EffTy piEffs piResultTy <- instantiate (sink piTy) (Var <$> bindersVars lamBs')
     forM_ lamResultTy \lamResultTy' ->
       checkUType lamResultTy' >>= constrainTypesEq piResultTy
@@ -1643,15 +1659,12 @@ openEffectRow (EffectRow effs NoTail) = undefined
 openEffectRow effRow = return effRow
 
 getIxDict :: CType o -> InfererM i o (IxDict CoreIR o)
-getIxDict = undefined
+getIxDict t = do
+  dictTy <- DictTy <$> ixDictType t
+  IxDictAtom <$> trySynthTerm dictTy Full
 
 asIxType :: CType o -> InfererM i o (IxType CoreIR o)
-asIxType ty = undefined
--- asIxType ty = do
---   dictTy <- DictTy <$> ixDictType ty
---   ctx <- srcPosCtx <$> getErrCtx
---   return $ IxType ty $ IxDictAtom $ DictHole (AlwaysEqual ctx) dictTy Full
--- {-# SCC asIxType #-}
+asIxType ty = IxType ty <$> getIxDict ty
 
 -- === Solver ===
 
@@ -1684,7 +1697,7 @@ constrainEq t1 t2 = do
          ++ (case infVars of
                Empty -> ""
                _ -> "\n(Solving for: " ++ pprint (nestToList pprint infVars) ++ ")")
-  void $ addContext msg $ withSubst (newSubst absurdNameFunction) $ unify t1' t2'
+  void $ addContext msg $ withVoidSubst $ unify t1' t2'
 
 class (AlphaEqE e, Zonkable e) => Unifiable (e::E) where
   unifyZonked :: e n -> e n -> SolverM n ()
@@ -1946,14 +1959,10 @@ emitInstanceDef instanceDef@(InstanceDef className _ _ _ _) = do
   emitBinding (getNameHint className) $ InstanceBinding instanceDef ty
 
 -- main entrypoint to dictionary synthesizer
-trySynthTerm :: (Fallible1 m, EnvReader m) => CType n -> RequiredMethodAccess -> m n (SynthAtom n)
+trySynthTerm :: CType n -> RequiredMethodAccess -> InfererM i n (SynthAtom n)
 trySynthTerm ty reqMethodAccess = do
   synthTy <- liftExcept $ typeAsSynthType ty
-  solutions <- liftSyntherM $ synthTerm synthTy reqMethodAccess
-  case solutions of
-    [] -> throw TypeErr $ "Couldn't synthesize a class dictionary for: " ++ pprint ty
-    [d] -> cheapNormalize d -- normalize to reduce code size
-    _ -> throw TypeErr $ "Multiple candidate class dictionaries for: " ++ pprint ty
+  withVoidSubst $ synthTerm synthTy reqMethodAccess
 {-# SCC trySynthTerm #-}
 
 type SynthAtom = CAtom
@@ -1965,39 +1974,13 @@ data SynthType n =
 
 data Givens n = Givens { fromGivens :: HM.HashMap (EKey SynthType n) (SynthAtom n) }
 
-class (Alternative1 m, Searcher1 m, EnvReader m, EnvExtender m)
-    => Synther m where
-  getGivens :: m n (Givens n)
-  withGivens :: Givens n -> m n a -> m n a
-
-newtype SyntherM (n::S) (a:: *) = SyntherM
-  { runSyntherM' :: OutReaderT Givens (EnvReaderT []) n a }
-  deriving ( Functor, Applicative, Monad, EnvReader, EnvExtender
-           , ScopeReader, MonadFail
-           , Alternative, Searcher, OutReader Givens)
-
-instance Synther SyntherM where
-  getGivens = askOutReader
-  {-# INLINE getGivens #-}
-  withGivens givens cont = localOutReader givens cont
-  {-# INLINE withGivens #-}
-
-liftSyntherM :: EnvReader m => SyntherM n a -> m n [a]
-liftSyntherM cont =
-  liftEnvReaderT do
-    initGivens <- givensFromEnv
-    runOutReaderT initGivens $ runSyntherM' cont
-{-# INLINE liftSyntherM #-}
-
-givensFromEnv :: EnvReader m => m n (Givens n)
-givensFromEnv = undefined
--- givensFromEnv = do
---   env <- withEnv moduleEnv
---   givens <- mapM toAtomVar $ lambdaDicts $ envSynthCandidates env
---   getSuperclassClosure (Givens HM.empty) (Var <$> givens)
--- {-# SCC givensFromEnv #-}
-
-extendGivens :: Synther m => [SynthAtom n] -> m n a -> m n a
+getGivens :: InfererM i o (Givens o)
+getGivens = givens <$> getInfState
+
+withGivens :: Givens o -> InfererM i o a -> InfererM i o a
+withGivens givens cont = withInfState (\s -> s { givens = givens }) cont
+
+extendGivens :: [SynthAtom o] -> InfererM i o a -> InfererM i o a
 extendGivens newGivens cont = do
   prevGivens <- getGivens
   finalGivens <- getSuperclassClosure prevGivens newGivens
@@ -2055,7 +2038,7 @@ getSuperclassClosurePure env givens newGivens =
       forM (enumerate superclasses) \(i, ty) -> do
         return $ DictCon ty $ SuperclassProj synthExpr i
 
-synthTerm :: SynthType n -> RequiredMethodAccess -> SyntherM n (SynthAtom n)
+synthTerm :: SynthType n -> RequiredMethodAccess -> SolverM n (SynthAtom n)
 synthTerm targetTy reqMethodAccess = confuseGHC >>= \_ -> case targetTy of
   SynthPiType (expls, ab) -> do
     ab' <- withGivenBinders expls ab \bs targetTy' -> do
@@ -2083,29 +2066,30 @@ synthTerm targetTy reqMethodAccess = confuseGHC >>= \_ -> case targetTy of
 
 withGivenBinders
   :: HasNamesE e => [Explicitness] -> Abs (Nest CBinder) e n
-  -> (forall l. DExt n l => Nest CBinder n l -> e l -> SyntherM l a)
-  -> SyntherM n a
-withGivenBinders explsTop (Abs bsTop e) contTop =
-  runSubstReaderT idSubst $ go explsTop bsTop \bsTop' -> do
-    e' <- renameM e
-    liftSubstReaderT $ contTop bsTop' e'
- where
-   go :: [Explicitness] -> Nest CBinder i i'
-      -> (forall o'. DExt o o' => Nest CBinder o o' -> SubstReaderT Name SyntherM i' o' a)
-      -> SubstReaderT Name SyntherM i o a
-   go expls bs cont = case (expls, bs) of
-     ([], Empty) -> getDistinct >>= \Distinct -> cont Empty
-     (expl:explsRest, Nest b rest) -> do
-       argTy <- renameM $ binderType b
-       withFreshBinder (getNameHint b) argTy \b' -> do
-         givens <- case expl of
-           Inferred _ (Synth _) -> return [Var $ binderVar b']
-           _ -> return []
-         s <- getSubst
-         liftSubstReaderT $ extendGivens givens $
-           runSubstReaderT (s <>> b@>binderName b') $
-             go explsRest rest \rest' -> cont (Nest b' rest')
-     _ -> error "zip error"
+  -> (forall l. DExt n l => Nest CBinder n l -> e l -> SolverM l a)
+  -> SolverM n a
+withGivenBinders explsTop (Abs bsTop e) contTop = undefined
+-- withGivenBinders explsTop (Abs bsTop e) contTop =
+--   runSubstReaderT idSubst $ go explsTop bsTop \bsTop' -> do
+--     e' <- renameM e
+--     liftSubstReaderT $ contTop bsTop' e'
+--  where
+--    go :: [Explicitness] -> Nest CBinder i i'
+--       -> (forall o'. DExt o o' => Nest CBinder o o' -> SubstReaderT Name SyntherM i' o' a)
+--       -> SubstReaderT Name SyntherM i o a
+--    go expls bs cont = case (expls, bs) of
+--      ([], Empty) -> getDistinct >>= \Distinct -> cont Empty
+--      (expl:explsRest, Nest b rest) -> do
+--        argTy <- renameM $ binderType b
+--        withFreshBinder (getNameHint b) argTy \b' -> do
+--          givens <- case expl of
+--            Inferred _ (Synth _) -> return [Var $ binderVar b']
+--            _ -> return []
+--          s <- getSubst
+--          liftSubstReaderT $ extendGivens givens $
+--            runSubstReaderT (s <>> b@>binderName b') $
+--              go explsRest rest \rest' -> cont (Nest b' rest')
+--      _ -> error "zip error"
 
 isMethodAccessAllowedBy :: EnvReader m =>  RequiredMethodAccess -> InstanceName n -> m n Bool
 isMethodAccessAllowedBy access instanceName = do
@@ -2117,7 +2101,7 @@ isMethodAccessAllowedBy access instanceName = do
     Full                  -> return $ numClassMethods == numInstanceMethods
     Partial numReqMethods -> return $ numReqMethods   <= numInstanceMethods
 
-synthDictFromGiven :: DictType n -> SyntherM n (SynthAtom n)
+synthDictFromGiven :: DictType n -> SolverM n (SynthAtom n)
 synthDictFromGiven targetTy = do
   givens <- ((HM.elems . fromGivens) <$> getGivens)
   asum $ givens <&> \given -> do
@@ -2129,43 +2113,28 @@ synthDictFromGiven targetTy = do
         args <- instantiateSynthArgs targetTy givenPiTy
         return $ DictCon (DictTy targetTy) $ InstantiatedGiven given args
 
-synthDictFromInstance :: DictType n -> SyntherM n (SynthAtom n)
-synthDictFromInstance targetTy@(DictType _ targetClass _) = undefined
--- synthDictFromInstance targetTy@(DictType _ targetClass _) = do
---   instances <- getInstanceDicts targetClass
---   asum $ instances <&> \candidate -> do
---     CorePiType _ expls bs (EffTy _ (DictTy candidateTy)) <- lookupInstanceTy candidate
---     args <- instantiateSynthArgs targetTy (expls, Abs bs candidateTy)
---     return $ DictCon (DictTy targetTy) $ InstanceDict candidate args
-
-instantiateSynthArgs :: DictType n -> SynthPiType n -> SyntherM n [CAtom n]
-instantiateSynthArgs targetTop (explsTop, Abs bsTop resultTyTop) = undefined
--- instantiateSynthArgs targetTop (explsTop, Abs bsTop resultTyTop) = do
---   ListE args <- (liftExceptAlt =<<) $ liftSolverM do
---     args <- runSubstReaderT idSubst $ go targetTop explsTop $ Abs bsTop resultTyTop
---     zonk $ ListE args
---   forM args \case
---     DictHole _ argTy req -> liftExceptAlt (typeAsSynthType argTy) >>= flip synthTerm req
---     arg -> return arg
---  where
---    go :: DictType o -> [Explicitness] -> Abs (Nest CBinder) DictType i
---       -> SubstReaderT AtomSubstVal SolverM i o [CAtom o]
---    go target allExpls (Abs bs proposed) = undefined
---    -- go target allExpls (Abs bs proposed) = case (allExpls, bs) of
---    --   ([], Empty) -> do
---    --     proposed' <- substM proposed
---    --     liftSubstReaderT $ unify target proposed'
---    --     return []
---    --   (expl:expls, Nest b rest) -> do
---    --     argTy <- substM $ binderType b
---    --     arg <- liftSubstReaderT case expl of
---    --       Explicit -> error "instances shouldn't have explicit args"
---    --       Inferred _ Unify -> Var <$> freshInferenceName MiscInfVar argTy
---    --       Inferred _ (Synth req) -> return $ DictHole (AlwaysEqual emptySrcPosCtx) argTy req
---    --     liftM (arg:) $ extendSubst (b@>SubstVal arg) $ go target expls (Abs rest proposed)
---    --   _ -> error "zip error"
-
-synthDictForData :: forall n. DictType n -> SyntherM n (SynthAtom n)
+synthDictFromInstance :: DictType n -> SolverM n (SynthAtom n)
+synthDictFromInstance targetTy@(DictType _ targetClass _) = do
+  instances <- getInstanceDicts targetClass
+  asum $ instances <&> \candidate -> do
+    CorePiType _ expls bs (EffTy _ (DictTy candidateTy)) <- lookupInstanceTy candidate
+    args <- instantiateSynthArgs targetTy (expls, Abs bs candidateTy)
+    return $ DictCon (DictTy targetTy) $ InstanceDict candidate args
+
+getInstanceDicts :: EnvReader m => ClassName n -> m n [InstanceName n]
+getInstanceDicts name = do
+  env <- withEnv moduleEnv
+  return $ M.findWithDefault [] name $ instanceDicts $ envSynthCandidates env
+{-# INLINE getInstanceDicts #-}
+
+instantiateSynthArgs :: DictType n -> SynthPiType n -> SolverM n [CAtom n]
+instantiateSynthArgs targetTop (explsTop, Abs bsTop resultTyTop) = do
+  liftM fromListE $ withReducibleEmissions "dict args" $
+    inferMixedArgs "dict" explsTop (sink (EmptyAbs bsTop)) emptyMixedArgs \args -> return $ ListE args
+    where emptyMixedArgs :: MixedArgs (CAtom n)
+          emptyMixedArgs = ([], [])
+
+synthDictForData :: forall n. DictType n -> SolverM n (SynthAtom n)
 synthDictForData dictTy@(DictType "Data" dName [Type ty]) = case ty of
   -- TODO Deduplicate vs CheckType.checkDataLike
   -- The "Var" case is different
@@ -2186,10 +2155,12 @@ synthDictForData dictTy@(DictType "Data" dName [Type ty]) = case ty of
   _   -> notData
   where
     recur ty' = synthDictForData $ DictType "Data" dName [Type ty']
-    recurBinder :: (RenameB b, BindsEnv b) => Abs b CType n -> SyntherM n (SynthAtom n)
-    recurBinder bAbs = refreshAbs bAbs \b' ty'' -> do
-      ans <- synthDictForData $ DictType "Data" (sink dName) [Type ty'']
-      return $ ignoreHoistFailure $ hoist b' ans
+    recurBinder :: Abs CBinder CType n -> SolverM n (SynthAtom n)
+    recurBinder (Abs b body) =
+      withFreshBinderInf noHint Explicit (binderType b) \b' -> do
+        body' <- applyRename (b@>binderName b') body
+        ans <- synthDictForData $ DictType "Data" (sink dName) [Type body']
+        return $ ignoreHoistFailure $ hoist b' ans
     notData = empty
     success = return $ DictCon (DictTy dictTy) $ DataData ty
 synthDictForData dictTy = error $ "Malformed Data dictTy " ++ pprint dictTy
@@ -2293,8 +2264,8 @@ instance DiffStateE InfState InfStateUpdates where
   updateDiffStateE _ initState (RListE diffs) = foldl updateInfStateImpl initState (unsnoc diffs)
     where
      updateInfStateImpl :: Distinct n => InfState n -> InfStateUpdate n -> InfState n
-     updateInfStateImpl (InfState (SolverSubst subst) effs) update =
-       InfState (SolverSubst subst') effs where
+     updateInfStateImpl (InfState (SolverSubst subst) givens effs) update =
+       InfState (SolverSubst subst') givens effs where
        subst' = case update of
          AddConstraint v x -> M.insert v (Solved x) subst
          AddDefault v d -> case M.lookup v subst of
diff --git a/src/lib/PPrint.hs b/src/lib/PPrint.hs
index 3fe2d3299..5f0123b62 100644
--- a/src/lib/PPrint.hs
+++ b/src/lib/PPrint.hs
@@ -233,9 +233,6 @@ instance IRRep r => PrettyPrec (DepPairType r n) where
   prettyPrec (DepPairType _ b rhs) =
     atPrec ArgPrec $ align $ group $ parensSep (spaceIfColinear <> "&> ") [p b, p rhs]
 
-instance Pretty (EffectOpType n) where
-  pretty (EffectOpType pol ty) = "[" <+> p pol <+> ":" <+> p ty <+> "]"
-
 instance Pretty (CoreLamExpr n) where
   pretty (CoreLamExpr _ lam) = p lam
 
@@ -648,15 +645,6 @@ instance Pretty (UDecl' n l) where
   pretty (UExprDecl expr) = p expr
   pretty UPass = "pass"
 
-instance Pretty (UEffectOpDef n) where
-  pretty (UEffectOpDef rp n body) = p rp <+> p n <+> "=" <+> p body
-  pretty (UReturnOpDef body) = "return =" <+> p body
-
-instance Pretty UResumePolicy where
-  pretty UNoResume = "jmp"
-  pretty ULinearResume = "def"
-  pretty UAnyResume = "ctl"
-
 instance Pretty (UEffectRow n) where
   pretty (UEffectRow x Nothing) = encloseSep "<" ">" "," $ (p <$> toList x)
   pretty (UEffectRow x (Just y)) = "{" <> (hsep $ punctuate "," (p <$> toList x)) <+> "|" <+> p y <> "}"
diff --git a/src/lib/Subst.hs b/src/lib/Subst.hs
index 24f5c71fd..9612b77c3 100644
--- a/src/lib/Subst.hs
+++ b/src/lib/Subst.hs
@@ -36,6 +36,10 @@ dropSubst :: (SubstReader v m, FromName v) => m o o a -> m i o a
 dropSubst cont = withSubst idSubst cont
 {-# INLINE dropSubst #-}
 
+withVoidSubst :: (SubstReader v m, FromName v) => m VoidS o a -> m i o a
+withVoidSubst cont = withSubst (newSubst absurdNameFunction) cont
+{-# INLINE withVoidSubst #-}
+
 extendSubst :: SubstReader v m => SubstFrag v i i' o -> m i' o a -> m i o a
 extendSubst frag cont = do
   env <- (<>>frag) <$> getSubst
diff --git a/src/lib/Types/Source.hs b/src/lib/Types/Source.hs
index df215f745..b0554def4 100644
--- a/src/lib/Types/Source.hs
+++ b/src/lib/Types/Source.hs
@@ -95,13 +95,6 @@ data CTopDecl'
       SourceName  -- Interface name
       ExplicitParams
       [(SourceName, Group)]  -- Method declarations
-  | CEffectDecl SourceName [(SourceName, UResumePolicy, Group)]
-  | CHandlerDecl SourceName -- Handler name
-      SourceName -- Effect name
-      SourceName -- Body type parameter
-      Group -- Handler arguments
-      Group -- Handler type annotation
-      [(SourceName, Maybe UResumePolicy, CSBlock)] -- Handler methods
   -- header, givens (may be empty), methods, optional name.  The header should contain
   -- the prerequisites, class name, and class arguments.
   | CInstanceDecl CInstanceDef
@@ -340,10 +333,6 @@ data UTopDecl (n::S) (l::S) where
 type UType = UExpr
 type UConstraint = UExpr
 
-data UEffectOpType (n::S) where
-  UEffectOpType :: UResumePolicy -> UType s -> UEffectOpType s
-  deriving (Show, Generic)
-
 data UResumePolicy =
     UNoResume
   | ULinearResume
@@ -360,11 +349,6 @@ type UMethodDef = WithSrcE UMethodDef'
 data UMethodDef' (n::S) = UMethodDef (SourceNameOr (Name MethodNameC) n) (ULamExpr n)
   deriving (Show, Generic)
 
-data UEffectOpDef (n::S) =
-    UEffectOpDef UResumePolicy (SourceNameOr (Name EffectOpNameC) n) (UExpr n)
-  | UReturnOpDef (UExpr n)
-  deriving (Show, Generic)
-
 data AnnRequirement = AnnRequired | AnnOptional
 
 data UAnn (annReq::AnnRequirement) (n::S) where
@@ -429,6 +413,12 @@ instance HasSrcPos (WithSrcE (a::E) (n::S)) where
 instance HasSrcPos (WithSrcB (b::B) (n::S) (n::S)) where
   srcPos (WithSrcB pos _) = pos
 
+instance HasSrcPos (UBinder c n l) where
+  srcPos = \case
+    UBindSource ctx _ -> ctx
+    UIgnore -> SrcPosCtx Nothing Nothing
+    UBind ctx _ _ -> ctx
+
 -- === SourceMap ===
 
 data SourceNameDef n =