diff --git a/src/lib/AbstractSyntax.hs b/src/lib/AbstractSyntax.hs
index 5a5805b0c..e2143fd9a 100644
--- a/src/lib/AbstractSyntax.hs
+++ b/src/lib/AbstractSyntax.hs
@@ -110,23 +110,23 @@ topDecl = dropSrc topDecl' where
   topDecl' (CSDecl ann d) = ULocalDecl <$> decl ann (WithSrc emptySrcPosCtx d)
   topDecl' (CData name tyConParams givens constructors) = do
     tyConParams' <- aExplicitParams tyConParams
-    givens' <- toNest <$> fromMaybeM givens [] aGivens
+    givens' <- aOptGivens givens
     constructors' <- forM constructors \(v, ps) -> do
       ps' <- toNest <$> mapM tyOptBinder ps
       return (v, ps')
     return $ UDataDefDecl
-      (UDataDef name (givens' >>> tyConParams') $
+      (UDataDef name (catUOptAnnExplBinders givens' tyConParams') $
         map (\(name', cons) -> (name', UDataDefTrail cons)) constructors')
       (fromString name)
       (toNest $ map (fromString . fst) constructors')
   topDecl' (CStruct name params givens fields defs) = do
     params' <- aExplicitParams params
-    givens' <- toNest <$> fromMaybeM givens [] aGivens
+    givens' <- aOptGivens givens
     fields' <- forM fields \(v, ty) -> (v,) <$> expr ty
     methods <- forM defs \(ann, d) -> do
       (methodName, lam) <- aDef d
       return (ann, methodName, Abs (UBindSource emptySrcPosCtx "self") lam)
-    return $ UStructDecl (fromString name) (UStructDef name (givens' >>> params') fields' methods)
+    return $ UStructDecl (fromString name) (UStructDef name (catUOptAnnExplBinders givens' params') fields' methods)
   topDecl' (CInterface name params methods) = do
     params' <- aExplicitParams params
     (methodNames, methodTys) <- unzip <$> forM methods \(methodName, ty) -> do
@@ -153,7 +153,7 @@ aInstanceDef :: CInstanceDef -> SyntaxM (UTopDecl VoidS VoidS)
 aInstanceDef (CInstanceDef clName args givens methods instNameAndParams) = do
   let clName' = fromString clName
   args' <- mapM expr args
-  givens' <- toNest <$> fromMaybeM givens [] aGivens
+  givens' <- aOptGivens givens
   methods' <- catMaybes <$> mapM aMethod methods
   case instNameAndParams of
     Nothing -> return $ UInstance clName' givens' args' methods' NothingB ImplicitApp
@@ -162,7 +162,7 @@ aInstanceDef (CInstanceDef clName args givens methods instNameAndParams) = do
       case optParams of
         Just params -> do
           params' <- aExplicitParams params
-          return $ UInstance clName' (givens' >>> params') args' methods' instName' ExplicitApp
+          return $ UInstance clName' (catUOptAnnExplBinders givens' params') args' methods' instName' ExplicitApp
         Nothing -> return $ UInstance clName' givens' args' methods' instName' ImplicitApp
 
 aDef :: CDef -> SyntaxM (SourceName, ULamExpr VoidS)
@@ -173,19 +173,27 @@ aDef (CDef name params optRhs optGivens body) = do
     effs <- fromMaybeM optEffs UPure aEffects
     resultTy' <- expr resultTy
     return (expl, Just effs, Just resultTy')
-  implicitParams <- toNest <$> fromMaybeM optGivens [] aGivens
-  let allParams = implicitParams >>> explicitParams
+  implicitParams <- aOptGivens optGivens
+  let allParams = catUOptAnnExplBinders implicitParams explicitParams
   body' <- block body
   return (name, ULamExpr allParams expl effs resultTy body')
 
+catUOptAnnExplBinders :: UOptAnnExplBinders n l -> UOptAnnExplBinders l l' -> UOptAnnExplBinders n l'
+catUOptAnnExplBinders (expls, bs) (expls', bs') = (expls <> expls', bs >>> bs')
+
 stripParens :: Group -> Group
 stripParens (WithSrc _ (CParens [g])) = stripParens g
 stripParens g = g
 
-aExplicitParams :: ExplicitParams -> SyntaxM (Nest (WithExpl UOptAnnBinder) VoidS VoidS)
+aExplicitParams :: ExplicitParams -> SyntaxM ([Explicitness], Nest UOptAnnBinder VoidS VoidS)
 aExplicitParams gs = generalBinders DataParam Explicit gs
 
-aGivens :: GivenClause -> SyntaxM [WithExpl UOptAnnBinder VoidS VoidS]
+aOptGivens :: Maybe GivenClause -> SyntaxM (UOptAnnExplBinders VoidS VoidS)
+aOptGivens optGivens = do
+  (expls, implicitParams) <- unzip <$> fromMaybeM optGivens [] aGivens
+  return (expls, toNest implicitParams)
+
+aGivens :: GivenClause -> SyntaxM [(Explicitness, UOptAnnBinder VoidS VoidS)]
 aGivens (implicits, optConstraints) = do
   implicits' <- mapM (generalBinder DataParam (Inferred Nothing Unify)) implicits
   constraints <- fromMaybeM optConstraints [] \gs -> do
@@ -194,23 +202,24 @@ aGivens (implicits, optConstraints) = do
 
 generalBinders
   :: ParamStyle -> Explicitness -> [Group]
-  -> SyntaxM (Nest (WithExpl UOptAnnBinder) VoidS VoidS)
-generalBinders paramStyle expl params = toNest . concat <$>
-  forM params \case
+  -> SyntaxM ([Explicitness], Nest UOptAnnBinder VoidS VoidS)
+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)
 
 generalBinder :: ParamStyle -> Explicitness -> Group
-              -> SyntaxM (WithExpl UOptAnnBinder VoidS VoidS)
+              -> SyntaxM (Explicitness, UOptAnnBinder VoidS VoidS)
 generalBinder paramStyle expl g = case expl of
-  Inferred _ (Synth _) -> WithExpl expl <$> tyOptBinder g
+  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 $ WithExpl expl' b
-  Explicit -> WithExpl expl <$> case paramStyle of
+    return (expl', b)
+  Explicit -> (expl,) <$> case paramStyle of
     TypeParam -> tyOptBinder g
     DataParam -> binderOptTy g
 
@@ -347,7 +356,7 @@ aMethod (WithSrc src d) = Just . WithSrcE src <$> addSrcContext src case d of
     (name, lam) <- aDef def
     return $ UMethodDef (fromString name) lam
   CLet (WithSrc _ (CIdentifier name)) rhs -> do
-    rhs' <- ULamExpr Empty ImplicitApp Nothing Nothing <$> block rhs
+    rhs' <- ULamExpr ([], Empty) ImplicitApp Nothing Nothing <$> block rhs
     return $ UMethodDef (fromString name) rhs'
   _ -> throw SyntaxErr "Unexpected method definition. Expected `def` or `x = ...`."
 
@@ -368,10 +377,10 @@ 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
-  WithExpl _ b' <- generalBinder DataParam Explicit b
+  (_, b') <- generalBinder DataParam Explicit b
   rhs' <- asExpr <$> block rhs
   body <- block $ IndentedBlock ds
-  let lam = ULam $ ULamExpr (UnaryNest (WithExpl Explicit b')) ExplicitApp Nothing Nothing body
+  let lam = ULam $ ULamExpr ([Explicit], UnaryNest b') ExplicitApp Nothing Nothing body
   return (Empty, WithSrcE pos $ extendAppRight rhs' (ns lam))
 blockDecls (d:ds) = do
   d' <- decl PlainLet d
diff --git a/src/lib/Builder.hs b/src/lib/Builder.hs
index b3012cc90..8e7563511 100644
--- a/src/lib/Builder.hs
+++ b/src/lib/Builder.hs
@@ -602,22 +602,13 @@ buildBlock
   -> m n (Block r n)
 buildBlock = buildScoped
 
-coreLamExpr :: EnvReader m => AppExplicitness
-            -> Abs (Nest (WithExpl CBinder)) (PairE (EffectRow CoreIR) CBlock) n
-            -> m n (CoreLamExpr n)
-coreLamExpr appExpl ab = liftEnvReaderM do
-  refreshAbs ab \bs' (PairE effs' body') -> do
-    EffTy _ resultTy <- blockEffTy body'
-    let bs'' = fmapNest withoutExpl bs'
-    return $ CoreLamExpr (CorePiType appExpl bs' (EffTy effs' resultTy)) (LamExpr bs'' body')
-
 buildCoreLam
   :: ScopableBuilder CoreIR m
   => CorePiType n
   -> (forall l. (Emits l, DExt n l) => [CAtomVar l] -> m l (CAtom l))
   -> m n (CoreLamExpr n)
-buildCoreLam piTy@(CorePiType _ bs _) cont = do
-  lam <- buildLamExpr (EmptyAbs $ fmapNest withoutExpl bs) cont
+buildCoreLam piTy@(CorePiType _ _ bs _) cont = do
+  lam <- buildLamExpr (EmptyAbs bs) cont
   return $ CoreLamExpr piTy lam
 
 buildAbs
@@ -1083,7 +1074,7 @@ projectStructRef i x = do
 
 getStructProjections :: EnvReader m => Int -> CType n -> m n [Projection]
 getStructProjections i (NewtypeTyCon (UserADTType _ tyConName _)) = do
-  TyConDef _ _ ~(StructFields fields) <- lookupTyCon tyConName
+  TyConDef _ _ _ ~(StructFields fields) <- lookupTyCon tyConName
   return case fields of
     [_] | i == 0    -> [UnwrapNewtype]
         | otherwise -> error "bad index"
diff --git a/src/lib/CheapReduction.hs b/src/lib/CheapReduction.hs
index bce6dcbed..9a35c2ed5 100644
--- a/src/lib/CheapReduction.hs
+++ b/src/lib/CheapReduction.hs
@@ -240,7 +240,7 @@ cheapReduceDictExpr resultTy d = case d of
     cheapReduceE child >>= \case
       DictCon _ (InstanceDict instanceName args) -> dropSubst do
         args' <- mapM cheapReduceE args
-        InstanceDef _ bs _ body <- lookupInstanceDef instanceName
+        InstanceDef _ _ bs _ body <- lookupInstanceDef instanceName
         let InstanceBody superclasses _ = body
         applySubst (bs@@>(SubstVal <$> args')) (superclasses !! superclassIx)
       child' -> return $ DictCon resultTy $ SuperclassProj child' superclassIx
@@ -285,7 +285,7 @@ instance IRRep r => CheaplyReducibleE r (Expr r) (Atom r) where
       cheapReduceE dict >>= \case
         DictCon _ (InstanceDict instanceName args) -> dropSubst do
           args' <- mapM cheapReduceE args
-          InstanceDef _ bs _ (InstanceBody _ methods) <- lookupInstanceDef instanceName
+          InstanceDef _ _ bs _ (InstanceBody _ methods) <- lookupInstanceDef instanceName
           let method = methods !! i
           extendSubst (bs@@>(SubstVal <$> args')) do
             method' <- cheapReduceE method
@@ -466,7 +466,7 @@ wrapNewtypesData [] x = x
 wrapNewtypesData (c:cs) x = NewtypeCon c $ wrapNewtypesData cs x
 
 instantiateTyConDef :: EnvReader m => TyConDef n -> TyConParams n -> m n (DataConDefs n)
-instantiateTyConDef (TyConDef _ bs conDefs) (TyConParams _ xs) = do
+instantiateTyConDef (TyConDef _ _ bs conDefs) (TyConParams _ xs) = do
   applySubst (bs @@> (SubstVal <$> xs)) conDefs
 {-# INLINE instantiateTyConDef #-}
 
@@ -487,7 +487,7 @@ dataDefRep (StructFields fields) = case map snd fields of
 
 makeStructRepVal :: (Fallible1 m, EnvReader m) => TyConName n -> [CAtom n] -> m n (CAtom n)
 makeStructRepVal tyConName args = do
-  TyConDef _ _ (StructFields fields) <- lookupTyCon tyConName
+  TyConDef _ _ _ (StructFields fields) <- lookupTyCon tyConName
   case fields of
     [_] -> case args of
       [arg] -> return arg
@@ -725,11 +725,9 @@ instance VisitGeneric CoreLamExpr CoreIR where
   visitGeneric (CoreLamExpr t lam) = CoreLamExpr <$> visitGeneric t <*> visitGeneric lam
 
 instance VisitGeneric CorePiType CoreIR where
-  visitGeneric (CorePiType app bsExpl effty) = do
-    let (expls, bs) = unzipExpls bsExpl
+  visitGeneric (CorePiType app expl bs effty) = do
     PiType bs' effty' <- visitGeneric $ PiType bs effty
-    let bsExpl' = zipExpls expls bs'
-    return $ CorePiType app bsExpl' effty'
+    return $ CorePiType app expl bs' effty'
 
 instance IRRep r => VisitGeneric (TabPiType r) r where
   visitGeneric (TabPiType d b eltTy) = do
diff --git a/src/lib/CheckType.hs b/src/lib/CheckType.hs
index 9e088be81..671067d04 100644
--- a/src/lib/CheckType.hs
+++ b/src/lib/CheckType.hs
@@ -256,7 +256,7 @@ instance IRRep r => HasType r (Type r) where
     TC tyCon -> typeCheckPrimTC  tyCon
     DepPairTy ty -> getTypeE ty
     DictTy (DictType _ className params) -> do
-      ClassDef _ _ _ paramBs _ _ <- renameM className >>= lookupClassDef
+      ClassDef _ _ _ _ paramBs _ _ <- renameM className >>= lookupClassDef
       params' <- mapM renameM params
       checkArgTys paramBs params'
       return TyKind
@@ -293,9 +293,6 @@ instance (ToBinding ann c, Color c, CheckableE r ann) => CheckableB r (BinderP c
       extendRenamer (b@>binderName b') $
         cont b'
 
-instance (BindsNames b, CheckableB r b) => CheckableB r (WithExpl b) where
-  checkB (WithExpl expl b) cont = checkB b \b' -> cont (WithExpl expl b')
-
 typeCheckExpr :: (Typer m r, IRRep r) => EffectRow r o -> Expr r i -> m i o (Type r o)
 typeCheckExpr effs expr = addContext ("Checking expr:\n" ++ pprint expr) case expr of
   App (EffTy _ reqTy) f xs -> do
@@ -318,7 +315,7 @@ typeCheckExpr effs expr = addContext ("Checking expr:\n" ++ pprint expr) case ex
     return resultTy'
   ApplyMethod (EffTy _ reqTy) dict i args -> do
     DictTy (DictType _ className params) <- getTypeE dict
-    ClassDef _ _ _ paramBs classBs methodTys <- lookupClassDef className
+    ClassDef _ _ _ _ paramBs classBs methodTys <- lookupClassDef className
     let methodTy = methodTys !! i
     superclassDicts <- getSuperclassDicts =<< renameM dict
     let subst = (    paramBs @@> map SubstVal params
@@ -342,8 +339,8 @@ dictExprType :: Typer m CoreIR => DictExpr i -> m i o (CType o)
 dictExprType e = case e of
   InstanceDict instanceName args -> do
     instanceName' <- renameM instanceName
-    InstanceDef className bs params _ <- lookupInstanceDef instanceName'
-    ClassDef sourceName _ _ _ _ _ <- lookupClassDef className
+    InstanceDef className _ bs params _ <- lookupInstanceDef instanceName'
+    ClassDef sourceName _ _ _ _ _ _ <- lookupClassDef className
     args' <- mapM renameM args
     checkArgTys bs args'
     ListE params' <- applySubst (bs@@>(SubstVal<$>args')) (ListE params)
@@ -353,7 +350,7 @@ dictExprType e = case e of
     checkApp Pure givenTy (toList args)
   SuperclassProj d i -> do
     DictTy (DictType _ className params) <- getTypeE d
-    ClassDef _ _ _ bs superclasses _ <- lookupClassDef className
+    ClassDef _ _ _ _ bs superclasses _ <- lookupClassDef className
     let scType = getSuperclassType REmpty superclasses i
     checkedApplyNaryAbs (Abs bs scType) params
   IxFin n -> do
@@ -370,7 +367,7 @@ instance IRRep r => HasType r (DepPairType r) where
     return TyKind
 
 instance HasType CoreIR CorePiType where
-  getTypeE (CorePiType _ bs (EffTy eff resultTy)) = do
+  getTypeE (CorePiType _ _ bs (EffTy eff resultTy)) = do
     checkB bs \_ -> do
       void $ checkE eff
       resultTy|:TyKind
@@ -407,14 +404,14 @@ checkAgainstGiven givenTy computedTy = do
   return givenTy'
 
 checkCoreLam :: Typer m CoreIR => CorePiType o -> LamExpr CoreIR i -> m i o ()
-checkCoreLam (CorePiType _ Empty (EffTy effs resultTy)) (LamExpr Empty body) = do
+checkCoreLam (CorePiType _ _ Empty (EffTy effs resultTy)) (LamExpr Empty body) = do
   resultTy' <- checkBlockWithEffs effs body
   checkTypesEq resultTy resultTy'
-checkCoreLam (CorePiType expl (Nest piB piBs) effTy) (LamExpr (Nest lamB lamBs) body) = do
+checkCoreLam (CorePiType expl (_:expls) (Nest piB piBs) effTy) (LamExpr (Nest lamB lamBs) body) = do
   argTy <- renameM $ binderType lamB
   checkTypesEq (binderType piB) argTy
   withFreshBinder (getNameHint lamB) argTy \b -> do
-    piTy <- applyRename (piB@>binderName b) (CorePiType expl piBs effTy)
+    piTy <- applyRename (piB@>binderName b) (CorePiType expl expls piBs effTy)
     extendRenamer (lamB@>binderName b) do
       checkCoreLam piTy (LamExpr lamBs body)
 checkCoreLam _ _ = throw TypeErr "zip error"
@@ -446,7 +443,7 @@ typeCheckNewtypeCon con x = case con of
   FinCon n -> n|:NatTy >> x|:NatTy >> renameM (Fin n)
   UserADTData _ d params -> do
     d' <- renameM d
-    def@(TyConDef sn _ _) <- lookupTyCon d'
+    def@(TyConDef sn _ _ _) <- lookupTyCon d'
     params' <- renameM params
     void $ checkedInstantiateTyConDef def params'
     return $ UserADTType sn d' params'
@@ -773,7 +770,7 @@ checkAlt resultTyReq bTyReq effs (Abs b body) = do
 
 checkApp :: (Typer m r, IRRep r) => EffectRow r o -> Type r o -> [Atom r i] -> m i o (Type r o)
 checkApp allowedEffs fTy xs = case fTy of
-  Pi (CorePiType _ bs effTy) -> do
+  Pi (CorePiType _ _ bs effTy) -> do
     xs' <- mapM renameM xs
     checkArgTys bs xs'
     let subst = bs @@> fmap SubstVal xs'
@@ -929,7 +926,7 @@ checkUnOp op x = do
 checkedInstantiateTyConDef
   :: (EnvReader m, Fallible1 m)
   => TyConDef n -> TyConParams n -> m n (DataConDefs n)
-checkedInstantiateTyConDef (TyConDef _ bs cons) (TyConParams _ xs) = do
+checkedInstantiateTyConDef (TyConDef _ _ bs cons) (TyConParams _ xs) = do
   checkedApplyNaryAbs (Abs bs cons) xs
 
 checkedApplyNaryAbs
@@ -995,7 +992,7 @@ asFFIFunType ty = return do
   return (impTy, piTy)
 
 checkFFIFunTypeM :: Fallible m => CorePiType n -> m IFunType
-checkFFIFunTypeM (CorePiType appExpl (Nest b bs) effTy) = do
+checkFFIFunTypeM (CorePiType appExpl (_:expls) (Nest b bs) effTy) = do
   argTy <- checkScalar $ binderType b
   case bs of
     Empty -> do
@@ -1006,7 +1003,7 @@ checkFFIFunTypeM (CorePiType appExpl (Nest b bs) effTy) = do
                  _ -> FFIMultiResultCC
       return $ IFunType cc [argTy] resultTys
     Nest b' rest -> do
-      let naryPiRest = CorePiType appExpl (Nest b' rest) effTy
+      let naryPiRest = CorePiType appExpl expls (Nest b' rest) effTy
       IFunType cc argTys resultTys <- checkFFIFunTypeM naryPiRest
       return $ IFunType cc (argTy:argTys) resultTys
 checkFFIFunTypeM _ = error "expected at least one argument"
diff --git a/src/lib/Core.hs b/src/lib/Core.hs
index 88725c1ca..f6fb57452 100644
--- a/src/lib/Core.hs
+++ b/src/lib/Core.hs
@@ -218,17 +218,13 @@ instance BindsEnv EnvFrag where
   toEnvFrag frag = frag
   {-# INLINE toEnvFrag #-}
 
-instance BindsEnv b => BindsEnv (WithExpl b) where
-  toEnvFrag (WithExpl _ b) = toEnvFrag b
-  {-# INLINE toEnvFrag #-}
-
-instance BindsEnv RolePiBinder where
-  toEnvFrag (RolePiBinder _ b) = toEnvFrag b
-  {-# INLINE toEnvFrag #-}
-
 instance BindsEnv (RecSubstFrag Binding) where
   toEnvFrag frag = EnvFrag frag
 
+instance BindsEnv b => BindsEnv (WithAttrB a b) where
+  toEnvFrag (WithAttrB _ b) = toEnvFrag b
+  {-# INLINE toEnvFrag #-}
+
 instance (BindsEnv b1, BindsEnv b2)
          => (BindsEnv (PairB b1 b2)) where
   toEnvFrag (PairB b1 b2) = do
diff --git a/src/lib/Export.hs b/src/lib/Export.hs
index eba7a718f..42dcc7ba1 100644
--- a/src/lib/Export.hs
+++ b/src/lib/Export.hs
@@ -100,11 +100,11 @@ liftExportSigM cont = do
 
 corePiToExportSig :: CallingConvention
   -> CorePiType i -> ExportSigM CoreIR i o (ExportedSignature o)
-corePiToExportSig cc (CorePiType _ tbs (EffTy effs resultTy)) = do
+corePiToExportSig cc (CorePiType _ expls tbs (EffTy effs resultTy)) = do
     case effs of
       Pure -> return ()
       _    -> throw TypeErr "Only pure functions can be exported"
-    goArgs cc Empty [] tbs resultTy
+    goArgs cc Empty [] (zipAttrs expls tbs) resultTy
 
 simpPiToExportSig :: CallingConvention
   -> PiType SimpIR i -> ExportSigM SimpIR i o (ExportedSignature o)
@@ -112,14 +112,14 @@ simpPiToExportSig cc (PiType bs (EffTy effs resultTy)) = do
   case effs of
     Pure -> return ()
     _    -> throw TypeErr "Only pure functions can be exported"
-  bs' <- return $ fmapNest (\b -> WithExpl Explicit b) bs
+  bs' <- return $ fmapNest (\b -> WithAttrB Explicit b) bs
   goArgs cc Empty [] bs' resultTy
 
 goArgs :: (IRRep r)
   => CallingConvention
   -> Nest ExportArg o o'
   -> [CAtomName o']
-  -> Nest (WithExpl (Binder r)) i i'
+  -> Nest (WithAttrB Explicitness (Binder r)) i i'
   -> Type r i'
   -> ExportSigM r i o' (ExportedSignature o)
 goArgs cc argSig argVs piBs piRes = case piBs of
@@ -128,7 +128,7 @@ goArgs cc argSig argVs piBs piRes = case piBs of
       StandardCC -> (fromListE $ sink $ ListE argVs) ++ nestToList (sink . binderName) resSig
       XLACC      -> []
       _ -> error $ "calling convention not supported: " ++ show cc
-  Nest (WithExpl expl (b:>ty)) bs -> do
+  Nest (WithAttrB expl (b:>ty)) bs -> do
     ety <- toExportType ty
     withFreshBinder (getNameHint b) ety \(v:>_) ->
       extendSubst (b @> Rename (binderName v)) $ do
diff --git a/src/lib/Generalize.hs b/src/lib/Generalize.hs
index 78037c742..dacb584fb 100644
--- a/src/lib/Generalize.hs
+++ b/src/lib/Generalize.hs
@@ -20,6 +20,9 @@ import Subst
 import MTL1
 import Types.Primitives
 
+type RolePiBinder = WithAttrB RoleExpl CBinder
+type RolePiBinders = Nest RolePiBinder
+
 generalizeIxDict :: EnvReader m => Atom CoreIR n -> m n (Generalized CoreIR CAtom n)
 generalizeIxDict dict = liftGeneralizerM do
   dict' <- sinkM dict
@@ -31,12 +34,12 @@ generalizeIxDict dict = liftGeneralizerM do
 
 generalizeArgs ::EnvReader m => CorePiType n -> [Atom CoreIR n] -> m n (Generalized CoreIR (ListE CAtom) n)
 generalizeArgs fTy argsTop = liftGeneralizerM $ runSubstReaderT idSubst do
-  PairE (CorePiType _ bs _) (ListE argsTop') <- sinkM $ PairE fTy (ListE argsTop)
-  ListE <$> go bs argsTop'
+  PairE (CorePiType _ expls bs _) (ListE argsTop') <- sinkM $ PairE fTy (ListE argsTop)
+  ListE <$> go (zipAttrs expls bs) argsTop'
   where
-    go :: Nest (WithExpl CBinder) i i' -> [Atom CoreIR n]
+    go :: Nest (WithAttrB Explicitness CBinder) i i' -> [Atom CoreIR n]
        -> SubstReaderT AtomSubstVal GeneralizerM i n [Atom CoreIR n]
-    go (Nest (WithExpl expl b) bs) (arg:args) = do
+    go (Nest (WithAttrB expl b) bs) (arg:args) = do
       ty' <- substM $ binderType b
       arg' <- case (ty', expl) of
         (TyKind, _) -> liftSubstReaderT case arg of
@@ -172,7 +175,7 @@ traverseRoleBinders f allBinders allParams =
     go :: forall i i'. RolePiBinders i i' -> [Atom CoreIR n]
        -> SubstReaderT AtomSubstVal m i n [Atom CoreIR n]
     go Empty [] = return []
-    go (Nest (RolePiBinder role b) bs) (param:params) = do
+    go (Nest (WithAttrB (role, _) b) bs) (param:params) = do
       ty' <- substM $ binderType b
       Distinct <- getDistinct
       param' <- liftSubstReaderT $ f role ty' param
@@ -183,14 +186,14 @@ traverseRoleBinders f allBinders allParams =
 
 getDataDefRoleBinders :: EnvReader m => TyConName n -> m n (Abs RolePiBinders UnitE n)
 getDataDefRoleBinders def = do
-  TyConDef _ bs _ <- lookupTyCon def
-  return $ Abs bs UnitE
+  TyConDef _ attrs bs _ <- lookupTyCon def
+  return $ Abs (zipAttrs attrs bs) UnitE
 {-# INLINE getDataDefRoleBinders #-}
 
 getClassRoleBinders :: EnvReader m => ClassName n -> m n (Abs RolePiBinders UnitE n)
 getClassRoleBinders def = do
-  ClassDef _ _ _ bs _ _ <- lookupClassDef def
-  return $ Abs bs UnitE
+  ClassDef _ _ _ roleExpls bs _ _ <- lookupClassDef def
+  return $ Abs (zipAttrs roleExpls bs) UnitE
 {-# INLINE getClassRoleBinders #-}
 
 -- === instances ===
diff --git a/src/lib/Inference.hs b/src/lib/Inference.hs
index 6f07dddf9..907f375a9 100644
--- a/src/lib/Inference.hs
+++ b/src/lib/Inference.hs
@@ -74,7 +74,7 @@ inferTopUDecl (UStructDecl tc def) result = do
     extendRenamer (tc@>sink tc') $ inferStructDef def
   def'' <- synthTyConDef def'
   updateTopEnv $ UpdateTyConDef tc' def''
-  UStructDef _ paramBs _ methods <- return def
+  UStructDef _ (_, paramBs) _ methods <- return def
   forM_ methods \(letAnn, methodName, methodDef) -> do
     method <- liftInfererM $ solveLocal $
       extendRenamer (tc@>sink tc') $
@@ -85,7 +85,7 @@ inferTopUDecl (UStructDecl tc def) result = do
   UDeclResultDone <$> applyRename (tc @> tc') result
 inferTopUDecl (UDataDefDecl def tc dcs) result = do
   tcDef <- liftInfererM $ solveLocal $ inferTyConDef def
-  tcDef'@(TyConDef _ _ (ADTCons dataCons)) <- synthTyConDef tcDef
+  tcDef'@(TyConDef _ _ _ (ADTCons dataCons)) <- synthTyConDef tcDef
   tc' <- emitBinding (getNameHint tcDef') $ TyConBinding (Just tcDef') (DotMethods mempty)
   dcs' <- forM (enumerate dataCons) \(i, dcDef) ->
     emitBinding (getNameHint dcDef) $ DataConBinding tc' i
@@ -104,14 +104,16 @@ inferTopUDecl (UInterface paramBs methodTys className methodNames) result = do
 inferTopUDecl (UInstance className instanceBs params methods maybeName expl) result = do
   let (InternalName _ _ className') = className
   ab <- liftInfererM $ solveLocal do
-    withRoleUBinders instanceBs \_ -> do
-      ClassDef _ _ _ paramBinders _ _ <- lookupClassDef (sink className')
-      params' <- checkInstanceParams paramBinders params
+    withRoleUBinders instanceBs do
+      ClassDef _ _ _ roleExpls paramBinders _ _ <- lookupClassDef (sink className')
+      let expls = snd <$> roleExpls
+      params' <- checkInstanceParams expls paramBinders params
       className'' <- sinkM className'
       body <- checkInstanceBody className'' params' methods
       return (ListE params' `PairE` body)
   Abs bs' (ListE params' `PairE` body) <- return ab
-  let def = InstanceDef className' bs' params' body
+  let (roleExpls, bs'') = unzipAttrs bs'
+  let def = InstanceDef className' roleExpls bs'' params' body
   UDeclResultDone <$> case maybeName of
     RightB UnitB  -> do
       void $ synthInstanceDefAndAddSynthCandidate def
@@ -151,13 +153,12 @@ asTopBlock block = do
   return $ TopLam False (PiType Empty effTy) (LamExpr Empty block)
 
 getInstanceType :: EnvReader m => InstanceDef n -> m n (CorePiType n)
-getInstanceType (InstanceDef className bs params _) = liftEnvReaderM do
+getInstanceType (InstanceDef className roleExpls bs params _) = liftEnvReaderM do
   refreshAbs (Abs bs (ListE params)) \bs' (ListE params') -> do
     className' <- sinkM className
-    ClassDef classSourceName _ _ _ _ _ <- lookupClassDef className'
+    ClassDef classSourceName _ _ _ _ _ _ <- lookupClassDef className'
     let dTy = DictTy $ DictType classSourceName className' params'
-    let bs'' = fmapNest (\(RolePiBinder _ b) -> b) bs'
-    return $ CorePiType ImplicitApp bs'' $ EffTy Pure dTy
+    return $ CorePiType ImplicitApp (snd <$> roleExpls) bs' $ EffTy Pure dTy
 
 -- === Inferer interface ===
 
@@ -178,19 +179,40 @@ class ( MonadFail1 m, Fallible1 m, Catchable1 m, CtxReader1 m, Builder CoreIR m
     => EmitsInf n
     => NameHint -> Explicitness -> CType n
     -> (forall l. (EmitsInf l, DExt n l) => CAtomVar l -> m l (e l))
-    -> m n (Abs (WithExpl CBinder) e n)
+    -> m n (Abs CBinder e n)
+
+buildAbsInfWithExpl
+  :: (InfBuilder m, SinkableE e, HoistableE e, RenameE e, SubstE AtomSubstVal e)
+  => EmitsInf n
+  => NameHint -> Explicitness -> CType n
+  -> (forall l. (EmitsInf l, DExt n l) => CAtomVar l -> m l (e l))
+  -> m n (Abs (WithExpl CBinder) e n)
+buildAbsInfWithExpl hint expl ty cont = do
+  Abs b e <- buildAbsInf hint expl ty cont
+  return $ Abs (WithAttrB expl b) e
+
+buildNaryAbsInfWithExpl
+  :: (Inferer m, SinkableE e, HoistableE e, RenameE e, SubstE AtomSubstVal e, Inferer m)
+  => EmitsInf n
+  => [Explicitness] -> EmptyAbs (Nest CBinder) n
+  -> (forall l. (EmitsInf l, DExt n l) => [CAtomVar l] -> m i l (e l))
+  -> m i n (Abs (Nest (WithExpl CBinder)) e n)
+buildNaryAbsInfWithExpl expls bs cont = do
+  Abs bs' e <- buildNaryAbsInf expls bs cont
+  return $ Abs (zipAttrs expls bs') e
 
 buildNaryAbsInf
   :: (SinkableE e, HoistableE e, RenameE e, SubstE AtomSubstVal e, Inferer m)
   => EmitsInf n
-  => EmptyAbs (Nest (WithExpl CBinder)) n
+  => [Explicitness] -> EmptyAbs (Nest CBinder) n
   -> (forall l. (EmitsInf l, DExt n l) => [CAtomVar l] -> m i l (e l))
-  -> m i n (Abs (Nest (WithExpl CBinder)) e n)
-buildNaryAbsInf (Abs Empty UnitE) cont = getDistinct >>= \Distinct -> Abs Empty <$> cont []
-buildNaryAbsInf (Abs (Nest (WithExpl expl (b:>ty)) bs) UnitE) cont =
+  -> m i n (Abs (Nest CBinder) e n)
+buildNaryAbsInf [] (Abs Empty UnitE) cont = getDistinct >>= \Distinct -> Abs Empty <$> cont []
+buildNaryAbsInf (expl:expls) (Abs (Nest (b:>ty) bs) UnitE) cont =
   prependAbs <$> buildAbsInf (getNameHint b) expl ty \v -> do
     bs' <- applyRename (b@>atomVarName v) (Abs bs UnitE)
-    buildNaryAbsInf bs' \vs -> cont (sink v:vs)
+    buildNaryAbsInf expls bs' \vs -> cont (sink v:vs)
+buildNaryAbsInf _ _ _ = error "zip error"
 
 buildDeclsInf
   :: (SubstE AtomSubstVal e, RenameE e, Solver m, InfBuilder m)
@@ -522,7 +544,7 @@ instance InfBuilder (InfererM i) where
                 ++ "\n" ++ pprint infFrag
     Abs b e <- return ab
     ty' <- zonk ty
-    return $ Abs (WithExpl expl (b:>ty')) e
+    return $ Abs (b:>ty') e
 
 dceInfFrag
   :: (EnvReader m, EnvExtender m, Fallible1 m, RenameE e, HoistableE e)
@@ -831,11 +853,12 @@ extendSynthCandidates (Inferred _ (Synth _)) v (Env topEnv (ModuleEnv a b scs))
 extendSynthCandidates _ _ env = env
 {-# INLINE extendSynthCandidates #-}
 
-extendSynthCandidatess :: Distinct n => RolePiBinders n' n -> Env n -> Env n
-extendSynthCandidatess (Nest (RolePiBinder _ (WithExpl expl b)) rest) env =
-  extendSynthCandidatess rest env'
-  where env' = extendSynthCandidates expl (withExtEvidence rest $ sink $ binderName b) env
-extendSynthCandidatess Empty env = env
+extendSynthCandidatess :: Distinct n => [Explicitness] -> Nest CBinder n' n -> Env n -> Env n
+extendSynthCandidatess (expl:expls) (Nest b bs) env =
+  extendSynthCandidatess expls bs env'
+  where env' = extendSynthCandidates expl (withExtEvidence bs $ sink $ binderName b) env
+extendSynthCandidatess [] Empty env = env
+extendSynthCandidatess _ _ _ = error "zip error"
 {-# INLINE extendSynthCandidatess #-}
 
 -- === actual inference pass ===
@@ -848,8 +871,8 @@ data RequiredTy (e::E) (n::S) =
 checkSigma :: EmitsBoth o
            => NameHint -> UExpr i -> CType o -> InfererM i o (CAtom o)
 checkSigma hint expr sTy = confuseGHC >>= \_ -> case sTy of
-  Pi piTy@(CorePiType _ bs _) -> do
-    if all (== Explicit) (nestToList getExpl bs)
+  Pi piTy@(CorePiType _ expls _ _) -> do
+    if all (== Explicit) expls
       then fallback
       else case expr of
         WithSrcE src (ULam lam) -> addSrcContext src $ Lam <$> checkULam lam piTy
@@ -949,7 +972,8 @@ checkOrInferRho hint uExprWithSrc@(WithSrcE pos expr) reqTy = do
     -- TODO: check explicitness constraints
     ab <- withUBinders bs \_ -> EffTy <$> checkUEffRow effs <*> checkUType ty
     Abs bs' effTy' <- return ab
-    matchRequirement $ Type $ Pi $ CorePiType appExpl bs' effTy'
+    let (expls, bs'') = unzipAttrs bs'
+    matchRequirement $ Type $ Pi $ CorePiType appExpl expls bs'' effTy'
   UTabPi (UTabPiExpr (UAnnBinder b ann cs) ty) -> do
     unless (null cs) $ throw TypeErr "`=>` shouldn't have constraints"
     ann' <- asIxType =<< checkAnn (getSourceName b) ann
@@ -1157,11 +1181,11 @@ getFieldDefs ty = case ty of
 
 instantiateSigma :: forall i o. EmitsBoth o => SigmaAtom o -> InfererM i o (CAtom o)
 instantiateSigma sigmaAtom = case getType sigmaAtom of
-  Pi piTy@(CorePiType ExplicitApp _ _) -> do
+  Pi piTy@(CorePiType ExplicitApp _ _ _) -> do
     Lam <$> etaExpandExplicits fDesc piTy \args ->
       applySigmaAtom (sink sigmaAtom) args
-  Pi (CorePiType ImplicitApp bs (EffTy _ resultTy)) -> do
-    args <- inferMixedArgs @UExpr fDesc (Abs bs resultTy) [] []
+  Pi (CorePiType ImplicitApp expls bs (EffTy _ resultTy)) -> do
+    args <- inferMixedArgs @UExpr fDesc expls (Abs bs resultTy) [] []
     applySigmaAtom sigmaAtom args
   DepPairTy (DepPairType ImplicitDepPair _ _) ->
     -- TODO: we should probably call instantiateSigma again here in case
@@ -1198,53 +1222,55 @@ etaExpandExplicits
   :: EmitsInf o => SourceName -> CorePiType o
   -> (forall o'. (EmitsBoth o', DExt o o') => [CAtom o'] -> InfererM i o' (CAtom o'))
   -> InfererM i o (CoreLamExpr o)
-etaExpandExplicits fSourceName (CorePiType _ bsTop (EffTy effs _)) contTop = do
-  ab <- go bsTop \xs -> do
+etaExpandExplicits fSourceName (CorePiType _ explsTop bsTop (EffTy effs _)) contTop = do
+  Abs bs body <- go explsTop bsTop \xs -> do
     effs' <- applySubst (bsTop@@>(SubstVal<$>xs)) effs
     withAllowedEffects effs' do
       body <- buildBlockInf $ contTop $ sinkList xs
       return $ PairE effs' body
-  coreLamExpr ExplicitApp ab
+  let (expls, bs') = unzipAttrs bs
+  coreLamExpr ExplicitApp expls $ Abs bs' body
  where
   go :: (EmitsInf o, SinkableE e, RenameE e, SubstE AtomSubstVal e, HoistableE e )
-     => Nest (WithExpl CBinder) o any
+     => [Explicitness] -> Nest CBinder o any
      -> (forall o'. (EmitsInf o', DExt o o') => [CAtom o'] -> InfererM i o' (e o'))
      -> InfererM i o (Abs (Nest (WithExpl CBinder)) e o)
-  go Empty cont = getDistinct >>= \Distinct -> Abs Empty <$> cont []
-  go (Nest (WithExpl expl (b:>ty)) rest) cont = case expl of
+  go [] Empty cont = getDistinct >>= \Distinct -> Abs Empty <$> cont []
+  go (expl:expls) (Nest (b:>ty) rest) cont = case expl of
     Explicit -> do
-      prependAbs <$> buildAbsInf (getNameHint b) expl ty \v -> do
+      prependAbs <$> buildAbsInfWithExpl (getNameHint b) expl ty \v -> do
         Abs rest' UnitE <- applyRename (b@>atomVarName v) $ Abs rest UnitE
-        go rest' \args -> cont (sink (Var v) : args)
+        go expls rest' \args -> cont (sink (Var v) : args)
     Inferred argSourceName infMech -> do
       arg <- getImplicitArg (fSourceName, fromMaybe "_" argSourceName) infMech ty
       Abs rest' UnitE <- applySubst (b@>SubstVal arg) $ Abs rest UnitE
-      go rest' \args -> cont (sink arg : args)
+      go expls rest' \args -> cont (sink arg : args)
+  go _ _ _ = error "zip error"
 
 buildLamInf
   :: EmitsInf o => CorePiType o
   -> (forall o' .  (EmitsBoth o', DExt o o')
                 => [(Explicitness, CAtom o')] -> CType o' -> InfererM i o' (CAtom o'))
   -> InfererM i o (CoreLamExpr o)
-buildLamInf (CorePiType appExpl bsTop effTy) contTop = do
-  ab <- go bsTop \xs -> do
+buildLamInf (CorePiType appExpl explsTop bsTop effTy) contTop = do
+  ab <- go explsTop bsTop \xs -> do
     let (expls, xs') = unzip xs
     EffTy effs' resultTy' <- applySubst (bsTop@@>(SubstVal<$>xs')) effTy
     withAllowedEffects effs' do
       body <- buildBlockInf $ contTop (zip expls $ sinkList xs') (sink resultTy')
       return $ PairE effs' body
-  coreLamExpr appExpl ab
+  coreLamExpr appExpl explsTop ab
  where
   go :: (EmitsInf o, HoistableE e, SinkableE e, SubstE AtomSubstVal e, RenameE e)
-     => Nest (WithExpl CBinder) o any
-     -> (forall o'. (EmitsInf o', DExt o o')
-           => [(Explicitness, CAtom o')] -> InfererM i o' (e o'))
-     -> InfererM i o (Abs (Nest (WithExpl CBinder)) e o)
-  go Empty cont = getDistinct >>= \Distinct -> Abs Empty <$> cont []
-  go (Nest (WithExpl expl b) rest) cont = do
+     => [Explicitness] -> Nest CBinder o any
+     -> (forall o'. (EmitsInf o', DExt o o') => [(Explicitness, CAtom o')] -> InfererM i o' (e o'))
+     -> InfererM i o (Abs (Nest CBinder) e o)
+  go [] Empty cont = getDistinct >>= \Distinct -> Abs Empty <$> cont []
+  go (expl:expls) (Nest b rest) cont = do
     prependAbs <$> buildAbsInf (getNameHint b) expl (binderType b) \v -> do
       Abs rest' UnitE <- applyRename (b@>atomVarName v) $ Abs rest UnitE
-      go rest' \args -> cont ((expl, sink (Var v)) : args)
+      go expls rest' \args -> cont $ (expl, sink $ Var v) : args
+  go _ _ _ = error "zip error"
 
 class ExplicitArg (e::E) where
   checkExplicitArg :: EmitsBoth o => IsDependent -> e i -> CType o -> InfererM i o (CAtom o)
@@ -1274,14 +1300,14 @@ checkOrInferApp
 checkOrInferApp f' posArgs namedArgs reqTy = do
   f <- maybeInterpretPunsAsTyCons reqTy f'
   case getType f of
-    Pi (CorePiType appExpl bs effTy) -> case appExpl of
+    Pi (CorePiType appExpl expls bs effTy) -> case appExpl of
       ExplicitApp -> do
-        checkArity bs posArgs
-        args' <- inferMixedArgs fDesc (Abs bs effTy) posArgs namedArgs
+        checkArity expls posArgs
+        args' <- inferMixedArgs fDesc expls (Abs bs effTy) posArgs namedArgs
         applySigmaAtom f args' >>= matchRequirement
       ImplicitApp -> do
         -- TODO: should this already have been done by the time we get `f`?
-        implicitArgs <- inferMixedArgs @UExpr fDesc (Abs bs effTy) [] []
+        implicitArgs <- inferMixedArgs @UExpr fDesc expls (Abs bs effTy) [] []
         f'' <- SigmaAtom (Just fDesc) <$> applySigmaAtom f implicitArgs
         checkOrInferApp f'' posArgs namedArgs Infer >>= matchRequirement
     -- TODO: special-case error for when `fTy` can't possibly be a function
@@ -1328,24 +1354,24 @@ applySigmaAtom (SigmaUVar _ _ f) args = case f of
     f'' <- toAtomVar f'
     emitExprWithEffects =<< mkApp (Var f'') args
   UTyConVar f' -> do
-    TyConDef sn bs _ <- lookupTyCon f'
-    let expls = nestToList (\(RolePiBinder _ (WithExpl expl _)) -> expl) bs
+    TyConDef sn roleExpls _ _ <- lookupTyCon f'
+    let expls = snd <$> roleExpls
     return $ Type $ NewtypeTyCon $ UserADTType sn f' (TyConParams expls args)
   UDataConVar v -> do
     (tyCon, i) <- lookupDataCon v
     applyDataCon tyCon i args
   UPunVar tc -> do
-    TyConDef sn _ _ <- lookupTyCon tc
+    TyConDef sn _ _ _ <- lookupTyCon tc
     -- interpret as a data constructor by default
     (params, dataArgs) <- splitParamPrefix tc args
     repVal <- makeStructRepVal tc dataArgs
     return $ NewtypeCon (UserADTData sn tc params) repVal
   UClassVar   f' -> do
-    ClassDef sourceName _ _ _ _ _ <- lookupClassDef f'
+    ClassDef sourceName _ _ _ _ _ _ <- lookupClassDef f'
     return $ Type $ DictTy $ DictType sourceName f' args
   UMethodVar  f' -> do
     MethodBinding className methodIdx <- lookupEnv f'
-    ClassDef _ _ _ paramBs _ _ <- lookupClassDef className
+    ClassDef _ _ _ _ paramBs _ _ <- lookupClassDef className
     let numParams = nestLength paramBs
     -- params aren't needed because they're already implied by the dict argument
     let (dictArg:args') = drop numParams args
@@ -1357,14 +1383,14 @@ applySigmaAtom (SigmaPartialApp _ f prevArgs) args =
 
 splitParamPrefix :: EnvReader m => TyConName n -> [CAtom n] -> m n (TyConParams n, [CAtom n])
 splitParamPrefix tc args = do
-  TyConDef _ paramBs _ <- lookupTyCon tc
+  TyConDef _ _ paramBs _ <- lookupTyCon tc
   let (paramArgs, dataArgs) = splitAt (nestLength paramBs) args
   params <- makeTyConParams tc paramArgs
   return (params, dataArgs)
 
 applyDataCon :: Emits o => TyConName o -> Int -> [CAtom o] -> InfererM i o (CAtom o)
 applyDataCon tc conIx topArgs = do
-  tyDef@(TyConDef sn _ _) <- lookupTyCon tc
+  tyDef@(TyConDef sn _ _ _) <- lookupTyCon tc
   (params, dataArgs) <- splitParamPrefix tc topArgs
   ADTCons conDefs <- instantiateTyConDef tyDef params
   DataConDef _ _ repTy _ <- return $ conDefs !! conIx
@@ -1398,9 +1424,9 @@ emitExprWithEffects expr = do
   addEffects $ getEffects expr
   emitExpr expr
 
-checkArity :: BindsNames b => Nest (WithExpl b) n l -> [a] -> InfererM i o ()
-checkArity bs args = do
-  let arity = length [() | Explicit <- nestToList (\(WithExpl expl _) -> expl) bs]
+checkArity :: [Explicitness] -> [a] -> InfererM i o ()
+checkArity expls args = do
+  let arity = length [() | Explicit <- expls]
   let numArgs = length args
   when (numArgs /= arity) do
     throw TypeErr $ "Wrong number of positional arguments provided. Expected " ++
@@ -1410,24 +1436,25 @@ checkArity bs args = do
 inferMixedArgs
   :: forall arg i o e
   .  (ExplicitArg arg, EmitsBoth o, SubstE (SubstVal Atom) e, SinkableE e, HoistableE e)
-  => SourceName
-  -> Abs (Nest (WithExpl CBinder)) e o -> [arg i] -> [(SourceName, arg i)]
+  => SourceName -> [Explicitness]
+  -> Abs (Nest CBinder) e o -> [arg i] -> [(SourceName, arg i)]
   -> InfererM i o [CAtom o]
-inferMixedArgs fSourceName bsAbs posArgs namedArgs = do
-  checkNamedArgValidity bsAbs (map fst namedArgs)
-  liftM fst $ runStreamReaderT1 posArgs $ go bsAbs
+inferMixedArgs fSourceName explsTop bsAbs posArgs namedArgs = do
+  checkNamedArgValidity explsTop (map fst namedArgs)
+  liftM fst $ runStreamReaderT1 posArgs $ go explsTop bsAbs
  where
   go :: (EmitsBoth o, SubstE (SubstVal Atom) e, SinkableE e, HoistableE e)
-     => Abs (Nest (WithExpl CBinder)) e o
+     => [Explicitness] -> Abs (Nest CBinder) e o
     -> StreamReaderT1 (arg i) (InfererM i) o [CAtom o]
-  go (Abs Empty _) = return []
-  go (Abs (Nest (WithExpl expl b) bs) result) = do
+  go [] (Abs Empty _) = return []
+  go (expl:expls) (Abs (Nest b bs) result) = do
     let rest = Abs bs result
     let isDependent = binderName b `isFreeIn` rest
     arg <- inferMixedArg isDependent (binderType b) expl
     arg' <- lift11 $ zonk arg
     rest' <- applySubst (b @> SubstVal arg') rest
-    (arg:) <$> go rest'
+    (arg:) <$> go expls rest'
+  go _ _ = error "zip error"
 
   inferMixedArg :: EmitsBoth o => IsDependent -> CType o -> Explicitness
                 -> StreamReaderT1 (arg i) (InfererM i) o (CAtom o)
@@ -1445,12 +1472,12 @@ inferMixedArgs fSourceName bsAbs posArgs namedArgs = do
   lookupNamedArg Nothing = Nothing
   lookupNamedArg (Just v) = lookup v namedArgs
 
-checkNamedArgValidity :: (BindsNames b, Fallible m) => Abs (Nest (WithExpl b)) e any -> [SourceName] -> m ()
-checkNamedArgValidity (Abs bs _) offeredNames = do
+checkNamedArgValidity :: Fallible m => [Explicitness] -> [SourceName] -> m ()
+checkNamedArgValidity expls offeredNames = do
   let explToMaybeName = \case
         Explicit -> Nothing
         Inferred v _ -> v
-  let acceptedNames = catMaybes $ nestToList (explToMaybeName . getExpl) bs
+  let acceptedNames = catMaybes $ map explToMaybeName expls
   let duplicates = repeated offeredNames
   when (not $ null duplicates) do
     throw TypeErr $ "Repeated names offered" ++ pprint duplicates
@@ -1618,7 +1645,7 @@ buildSortedCase scrut alts resultTy = do
   scrutTy <- return $ getType scrut
   case scrutTy of
     TypeCon _ defName _ -> do
-      TyConDef _ _ (ADTCons cons) <- lookupTyCon defName
+      TyConDef _ _ _ (ADTCons cons) <- lookupTyCon defName
       case cons of
         [] -> error "case of void?"
         -- Single constructor ADTs are not sum types, so elide the case.
@@ -1631,14 +1658,13 @@ buildSortedCase scrut alts resultTy = do
 
 -- TODO: cache this with the instance def (requires a recursive binding)
 instanceFun :: EnvReader m => InstanceName n -> AppExplicitness -> m n (CAtom n)
-instanceFun instanceName expl = do
-  InstanceDef _ bs _ _ <- lookupInstanceDef instanceName
+instanceFun instanceName appExpl = do
+  InstanceDef _ expls bs _ _ <- lookupInstanceDef instanceName
   ab <- liftEnvReaderM $ refreshAbs (Abs bs UnitE) \bs' UnitE -> do
     args <- mapM toAtomVar $ nestToNames bs'
-    let bs'' = fmapNest (\(RolePiBinder _ b) -> b) bs'
     result <- mkDictAtom $ InstanceDict (sink instanceName) (Var <$> args)
-    return $ Abs bs'' (PairE Pure (WithoutDecls result))
-  Lam <$> coreLamExpr expl ab
+    return $ Abs bs' (PairE Pure (WithoutDecls result))
+  Lam <$> coreLamExpr appExpl (snd<$>expls) ab
 
 checkMaybeAnnExpr :: EmitsBoth o
   => NameHint -> Maybe (UType i) -> UExpr i -> InfererM i o (CAtom o)
@@ -1664,53 +1690,55 @@ inferRole ty = \case
 inferTyConDef :: EmitsInf o => UDataDef i -> InfererM i o (TyConDef o)
 inferTyConDef (UDataDef tyConName paramBs dataCons) = do
   Abs paramBs' dataCons' <-
-    withRoleUBinders paramBs \_ -> do
+    withRoleUBinders paramBs do
       ADTCons <$> mapM inferDataCon dataCons
-  return (TyConDef tyConName paramBs' dataCons')
+  let (roleExpls, paramBs'') = unzipAttrs paramBs'
+  return (TyConDef tyConName roleExpls paramBs'' dataCons')
 
 inferStructDef :: EmitsInf o => UStructDef i -> InfererM i o (TyConDef o)
 inferStructDef (UStructDef tyConName paramBs fields _) = do
   let (fieldNames, fieldTys) = unzip fields
-  Abs paramBs' dataConDefs <- withRoleUBinders paramBs \_ -> do
+  Abs paramBs' dataConDefs <- withRoleUBinders paramBs do
     tys <- mapM checkUType fieldTys
     return $ StructFields $ zip fieldNames tys
-  return $ TyConDef tyConName paramBs' dataConDefs
+  let (roleExpls, paramBs'') = unzipAttrs paramBs'
+  return $ TyConDef tyConName roleExpls paramBs'' dataConDefs
 
 inferDotMethod
   :: EmitsInf o => TyConName o
-  -> Abs (Nest (WithExpl UOptAnnBinder)) (Abs UAtomBinder ULamExpr) i
+  -> Abs (Nest UOptAnnBinder) (Abs UAtomBinder ULamExpr) i
   -> InfererM i o (CoreLamExpr o)
 inferDotMethod tc (Abs uparamBs (Abs selfB lam)) = do
-  TyConDef sn paramBs _ <- lookupTyCon tc
-  let paramBs' = fmapNest (\(RolePiBinder _ b) -> b) paramBs
-  ab <- buildNaryAbsInf (Abs paramBs' UnitE) \paramVs -> do
-    let expls = nestToList (\(WithExpl expl _) -> expl) paramBs'
+  TyConDef sn roleExpls paramBs _ <- lookupTyCon tc
+  let expls = snd <$> roleExpls
+  ab <- buildNaryAbsInfWithExpl expls (Abs paramBs UnitE) \paramVs -> do
     let paramVs' = catMaybes $ zip expls paramVs <&> \(expl, v) -> case expl of
                      Inferred _ (Synth _) -> Nothing
                      _ -> Just v
     extendRenamer (uparamBs @@> (atomVarName <$> paramVs')) do
       let selfTy = NewtypeTyCon $ UserADTType sn (sink tc) (TyConParams expls (Var <$> paramVs))
-      buildAbsInf "self" Explicit selfTy \vSelf ->
+      buildAbsInfWithExpl "self" Explicit selfTy \vSelf ->
         extendRenamer (selfB @> atomVarName vSelf) $ inferULam lam
   Abs paramBs'' (Abs selfB' lam') <- return ab
   return $ prependCoreLamExpr (paramBs'' >>> UnaryNest selfB') lam'
 
 prependCoreLamExpr :: Nest (WithExpl CBinder) n l -> CoreLamExpr l -> CoreLamExpr n
 prependCoreLamExpr bs e = case e of
-  CoreLamExpr (CorePiType appExpl piBs effTy) (LamExpr lamBs body) -> do
-    let piType  = CorePiType appExpl (bs >>> piBs) effTy
-    let lamExpr = LamExpr (fmapNest withoutExpl bs >>> lamBs) body
+  CoreLamExpr (CorePiType appExpl piExpls piBs effTy) (LamExpr lamBs body) -> do
+    let (expls, bs') = unzipAttrs bs
+    let piType  = CorePiType appExpl (expls <> piExpls) (bs' >>> piBs) effTy
+    let lamExpr = LamExpr (fmapNest withoutAttr bs >>> lamBs) body
     CoreLamExpr piType lamExpr
 
 inferDataCon :: EmitsInf o => (SourceName, UDataDefTrail i) -> InfererM i o (DataConDef o)
 inferDataCon (sourceName, UDataDefTrail argBs) = do
-  let argBsExpls = addExpls Explicit argBs
-  Abs argBs' UnitE <- withUBinders argBsExpls \_ -> return UnitE
-  let argBs'' = Abs (fmapNest withoutExpl argBs') UnitE
+  let expls = nestToList (const Explicit) argBs
+  Abs argBs' UnitE <- withUBinders (expls, argBs) \_ -> return UnitE
+  let argBs'' = Abs (fmapNest withoutAttr argBs') UnitE
   let (repTy, projIdxs) = dataConRepTy argBs''
   return $ DataConDef sourceName argBs'' repTy projIdxs
 
-dataConRepTy :: EmptyAbs (Nest (Binder CoreIR)) n -> (CType n, [[Projection]])
+dataConRepTy :: EmptyAbs (Nest CBinder) n -> (CType n, [[Projection]])
 dataConRepTy (Abs topBs UnitE) = case topBs of
   Empty -> (UnitTy, [])
   _ -> go [] [UnwrapNewtype] topBs
@@ -1738,47 +1766,49 @@ dataConRepTy (Abs topBs UnitE) = case topBs of
 inferClassDef
   :: EmitsInf o
   => SourceName -> [SourceName]
-  -> Nest (WithExpl UOptAnnBinder) i i'
+  -> UOptAnnExplBinders i i'
   -> [UType i']
   -> InfererM i o (ClassDef o)
-inferClassDef className methodNames paramBs methods = do
+inferClassDef className methodNames paramBs@(expls, paramBs') methods = do
+  let paramBsWithAttrBs = zipWithNest paramBs' expls \b expl -> WithAttrB expl b
   let paramNames = catMaybes $ nestToList
-        (\(WithExpl expl (UAnnBinder b _ _)) -> case expl of
+        (\(WithAttrB expl (UAnnBinder b _ _)) -> case expl of
              Inferred _ (Synth _) -> Nothing
-             _ -> Just $ Just $ getSourceName b) paramBs
-  ab <- withRoleUBinders paramBs \_ -> do
+             _ -> Just $ Just $ getSourceName b) paramBsWithAttrBs
+  ab <- withRoleUBinders paramBs do
      ListE <$> forM methods \m -> do
        checkUType m >>= \case
          Pi t -> return t
-         t -> return $ CorePiType ImplicitApp Empty (EffTy Pure t)
+         t -> return $ CorePiType ImplicitApp [] Empty (EffTy Pure t)
   Abs (PairB bs scs) (ListE mtys) <- identifySuperclasses ab
-  return $ ClassDef className methodNames paramNames bs scs mtys
+  let (roleExpls, bs') = unzipAttrs bs
+  return $ ClassDef className methodNames paramNames roleExpls bs' scs mtys
 
--- TODO: this is just partitioning the binders. We could write a more general function like this:
---   partitionBinders :: Nest b n l -> (forall n l. b i i' -> EitherB b1 b2 i i')
---                    -> Except (PairB (Nest b1) (Nest b2)) n l
 identifySuperclasses
-  :: RenameE e => Abs RolePiBinders e n
-  -> InfererM i n (Abs (PairB RolePiBinders (Nest CBinder)) e n)
-identifySuperclasses ab = refreshAbs ab \bs e -> do
-  bs' <- partitionBinders bs \b@(RolePiBinder _ (WithExpl expl b')) -> case expl of
-    Explicit -> return $ LeftB b
-    Inferred _ Unify -> throw TypeErr "Interfaces can't have implicit parameters"
-    Inferred _ (Synth _) -> return $ RightB b'
-  return $ Abs bs' e
+  :: RenameE e => Abs (Nest (WithRoleExpl CBinder)) e n
+  -> InfererM i n (Abs (PairB (Nest (WithRoleExpl CBinder)) (Nest CBinder)) e n)
+identifySuperclasses ab = do
+  refreshAbs ab \bs e -> do
+    bs' <- partitionBinders bs \b@(WithAttrB (_, expl) b') -> case expl of
+      Explicit -> return $ LeftB b
+      Inferred _ Unify -> throw TypeErr "Interfaces can't have implicit parameters"
+      Inferred _ (Synth _) -> return $ RightB b'
+    return $ Abs bs' e
 
 withUBinders
   :: (EmitsInf o, HasNamesE e, SubstE AtomSubstVal e, SinkableE e)
-  => Nest (WithExpl (UAnnBinder req)) i i'
+  => UAnnExplBinders req i i'
   -> (forall o'. (EmitsInf o', DExt o o') => [CAtomVar o'] -> InfererM i' o' (e o'))
   -> InfererM i o (Abs (Nest (WithExpl CBinder)) e o)
 withUBinders bs cont = case bs of
-  Empty -> getDistinct >>= \Distinct -> Abs Empty <$> cont []
-  Nest (WithExpl expl (UAnnBinder b ann cs)) rest -> do
+  ([], Empty) -> getDistinct >>= \Distinct -> Abs Empty <$> cont []
+  (expl:expls, Nest (UAnnBinder b ann cs) rest) -> do
     ann' <- checkAnn (getSourceName b) ann
-    prependAbs <$> buildAbsInf (getNameHint b) expl ann' \v ->
+    prependAbs <$> buildAbsInfWithExpl (getNameHint b) expl ann' \v ->
       concatAbs <$> withConstraintBinders cs v do
-        extendSubst (b@>sink (atomVarName v)) $ withUBinders rest \vs -> cont (sink v : vs)
+        extendSubst (b@>sink (atomVarName v)) $ withUBinders (expls, rest) \vs ->
+          cont (sink v : vs)
+  _ -> error "zip error"
 
 withConstraintBinders
   :: (EmitsInf o, HasNamesE e, SubstE AtomSubstVal e, RenameE e, SinkableE e)
@@ -1791,24 +1821,26 @@ withConstraintBinders (c:cs) v cont = do
   Type dictTy <- withReducibleEmissions "Can't reduce interface constraint" do
     c' <- inferWithoutInstantiation c >>= zonk
     dropSubst $ checkOrInferApp c' [Var $ sink v] [] (Check TyKind)
-  prependAbs <$> buildAbsInf "d" (Inferred Nothing (Synth Full)) dictTy \_ ->
+  prependAbs <$> buildAbsInfWithExpl "d" (Inferred Nothing (Synth Full)) dictTy \_ ->
     withConstraintBinders cs (sink v) cont
 
 withRoleUBinders
   :: forall i i' o e req. (EmitsInf o, HasNamesE e, SubstE AtomSubstVal e, SinkableE e)
-  => Nest (WithExpl (UAnnBinder req)) i i'
-  -> (forall o'. (EmitsInf o', DExt o o') => [CAtomVar o'] -> InfererM i' o' (e o'))
-  -> InfererM i o (Abs RolePiBinders e o)
-withRoleUBinders bs cont = case bs of
-  Empty -> getDistinct >>= \Distinct -> Abs Empty <$> cont []
-  Nest (WithExpl expl (UAnnBinder b ann cs)) rest -> do
+  => UAnnExplBinders req i i'
+  -> (forall o'. (EmitsInf o', DExt o o') => InfererM i' o' (e o'))
+  -> InfererM i o (Abs (Nest (WithRoleExpl CBinder)) e o)
+withRoleUBinders roleBs cont = case roleBs of
+  ([], Empty) -> getDistinct >>= \Distinct -> Abs Empty <$> cont
+  (expl:expls, Nest (UAnnBinder b ann cs) rest) -> do
     ann' <- checkAnn (getSourceName b) ann
     Abs b' (Abs bs' e) <- buildAbsInf (getNameHint b) expl ann' \v -> do
       Abs ds (Abs bs' e) <- withConstraintBinders cs v $
-        extendSubst (b@>sink (atomVarName v)) $ withRoleUBinders rest \vs -> cont (sink v : vs)
-      return $ Abs (fmapNest (RolePiBinder DictParam) ds >>> bs') e
+        extendSubst (b@>sink (atomVarName v)) $ withRoleUBinders (expls, rest) cont
+      let ds' = fmapNest (\(WithAttrB expl' b') -> WithAttrB (DictParam, expl') b') ds
+      return $ Abs (ds' >>> bs') e
     role <- inferRole (binderType b') expl
-    return $ Abs (Nest (RolePiBinder role b') bs') e
+    return $ Abs (Nest (WithAttrB (role,expl) b') bs') e
+  _ -> error "zip error"
 
 inferULam :: EmitsInf o => ULamExpr i -> InfererM i o (CoreLamExpr o)
 inferULam (ULamExpr bs appExpl effs resultTy body) = do
@@ -1823,12 +1855,13 @@ inferULam (ULamExpr bs appExpl effs resultTy body) = do
             checkSigma noHint result (sink resultTy'')
     return (PairE effs' body')
   Abs bs' (PairE effs' body') <- return ab
+  let (expls, bs'') = unzipAttrs bs'
   case appExpl of
-    ImplicitApp -> checkImplicitLamRestrictions bs' effs'
+    ImplicitApp -> checkImplicitLamRestrictions bs'' effs'
     ExplicitApp -> return ()
-  coreLamExpr appExpl $ Abs bs' $ PairE effs' body'
+  coreLamExpr appExpl expls $ Abs bs'' $ PairE effs' body'
 
-checkImplicitLamRestrictions :: Nest (WithExpl CBinder) o o' -> EffectRow CoreIR o' -> InfererM i o ()
+checkImplicitLamRestrictions :: Nest CBinder o o' -> EffectRow CoreIR o' -> InfererM i o ()
 checkImplicitLamRestrictions _ _ = return () -- TODO
 
 checkUForExpr :: EmitsBoth o => UForExpr i -> TabPiType CoreIR o -> InfererM i o (LamExpr CoreIR o)
@@ -1845,7 +1878,7 @@ checkUForExpr (UForExpr (UAnnBinder bFor ann cs) body) tabPi@(TabPiType _ bPi _)
       buildBlockInf do
         withBlockDecls body \result ->
           checkSigma noHint result $ sink resultTy'
-  return $ LamExpr (UnaryNest $ withoutExpl b) body'
+  return $ LamExpr (UnaryNest b) body'
 
 inferUForExpr :: EmitsBoth o => UForExpr i -> InfererM i o (LamExpr CoreIR o)
 inferUForExpr (UForExpr (UAnnBinder bFor ann cs) body) = do
@@ -1855,15 +1888,15 @@ inferUForExpr (UForExpr (UAnnBinder bFor ann cs) body) = do
     extendRenamer (bFor@>atomVarName i) $ buildBlockInf $
       withBlockDecls body \result ->
         checkOrInferRho noHint result Infer
-  return $ LamExpr (UnaryNest $ withoutExpl b) body'
+  return $ LamExpr (UnaryNest b) body'
 
 checkULam :: EmitsInf o => ULamExpr i -> CorePiType o -> InfererM i o (CoreLamExpr o)
-checkULam (ULamExpr lamBs lamAppExpl lamEffs lamResultTy body)
-          (CorePiType piAppExpl piBs effTy) = do
-  checkArity piBs (nestToList (const ()) lamBs)
+checkULam (ULamExpr (_, lamBs) lamAppExpl lamEffs lamResultTy body)
+          (CorePiType piAppExpl expls piBs effTy) = do
+  checkArity expls (nestToList (const ()) lamBs)
   when (piAppExpl /= lamAppExpl) $ throw TypeErr $ "Wrong arrow. Expected "
      ++ pprint piAppExpl ++ " got " ++ pprint lamAppExpl
-  ab <- checkLamBinders piBs lamBs \vs -> do
+  Abs explBs body' <- checkLamBinders expls piBs lamBs \vs -> do
     EffTy piEffs' piResultTy' <- applyRename (piBs@@>map atomVarName vs) effTy
     case lamResultTy of
       Nothing -> return ()
@@ -1877,47 +1910,44 @@ checkULam (ULamExpr lamBs lamAppExpl lamEffs lamResultTy body)
         withBlockDecls body \result ->
           checkSigma noHint result piResultTy''
       return $ PairE piEffs' body'
-  coreLamExpr piAppExpl ab
+  let (expls', bs') = unzipAttrs explBs
+  coreLamExpr piAppExpl expls' $ Abs bs' body'
 
 checkLamBinders
   :: (EmitsInf o, SinkableE e, HoistableE e, SubstE AtomSubstVal e, RenameE e)
-  => Nest (WithExpl CBinder) o any
-  -> Nest (WithExpl UOptAnnBinder) i i'
+  => [Explicitness] -> Nest CBinder o any
+  -> Nest UOptAnnBinder i i'
   -> (forall o'. (EmitsInf o', DExt o o') => [CAtomVar o'] -> InfererM i' o' (e o'))
   -> InfererM i o (Abs (Nest (WithExpl CBinder)) e o)
-checkLamBinders Empty Empty cont = getDistinct >>= \Distinct -> Abs Empty <$> cont []
-checkLamBinders (Nest (WithExpl piExpl (piB:>piAnn)) piBs) lamBs cont = do
+checkLamBinders [] Empty Empty cont = getDistinct >>= \Distinct -> Abs Empty <$> cont []
+checkLamBinders (piExpl:piExpls) (Nest (piB:>piAnn) piBs) lamBs cont = do
   prependAbs <$> case piExpl of
     Inferred _ _ ->
-      buildAbsInf (getNameHint piB) piExpl piAnn \v -> do
+      buildAbsInfWithExpl (getNameHint piB) piExpl piAnn \v -> do
         Abs piBs' UnitE <- applyRename (piB@>atomVarName v) $ Abs piBs UnitE
-        checkLamBinders piBs' lamBs \vs ->
+        checkLamBinders piExpls piBs' lamBs \vs ->
           cont (sink v:vs)
     Explicit -> case lamBs of
-      Nest (WithExpl Explicit (UAnnBinder lamB ann cs)) lamBsRest -> do
+      Nest (UAnnBinder lamB ann cs) lamBsRest -> do
         case ann of
           UAnn lamAnn -> checkUType lamAnn >>= constrainTypesEq piAnn
           UNoAnn -> return ()
-        buildAbsInf (getNameHint lamB) Explicit piAnn \v -> do
+        buildAbsInfWithExpl (getNameHint lamB) Explicit piAnn \v -> do
           concatAbs <$> withConstraintBinders cs v do
             Abs piBs' UnitE <- applyRename (piB@>sink (atomVarName v)) $ Abs piBs UnitE
-            extendRenamer (lamB@>sink (atomVarName v)) $ checkLamBinders piBs' lamBsRest \vs ->
+            extendRenamer (lamB@>sink (atomVarName v)) $ checkLamBinders piExpls piBs' lamBsRest \vs ->
               cont (sink v:vs)
-      Nest (WithExpl (Inferred _ _) _) _ ->
-        -- TODO(dougalm): I don't think this case is reachable, but if it is
-        -- then we can check for it in `checkULam` and fall back to `inferULam`.
-        error "shouldn't be able to check lambda terms with implicit binders"
       Empty -> error "zip error"
-checkLamBinders _ _ _ = error "zip error"
+checkLamBinders _ _ _ _ = error "zip error"
 
-checkInstanceParams :: EmitsInf o => RolePiBinders o any -> [UExpr i] -> InfererM i o [CAtom o]
-checkInstanceParams bsTop paramsTop = do
-  checkArity (fmapNest (\(RolePiBinder _ b) -> b) bsTop) paramsTop
+checkInstanceParams :: EmitsInf o => [Explicitness] -> Nest CBinder o any -> [UExpr i] -> InfererM i o [CAtom o]
+checkInstanceParams expls bsTop paramsTop = do
+  checkArity expls paramsTop
   go bsTop paramsTop
  where
-  go :: EmitsInf o => Nest RolePiBinder o any -> [UExpr i] -> InfererM i o [CAtom o]
+  go :: EmitsInf o => Nest CBinder o any -> [UExpr i] -> InfererM i o [CAtom o]
   go Empty [] = return []
-  go (Nest (RolePiBinder _ (WithExpl _ (b:>ty))) bs) (x:xs) = do
+  go (Nest (b:>ty) bs) (x:xs) = do
     x' <- checkUParam ty x
     Abs bs' UnitE <- applySubst (b@>SubstVal x') $ Abs bs UnitE
     (x':) <$> go bs' xs
@@ -1927,7 +1957,7 @@ checkInstanceBody
   :: EmitsInf o => ClassName o -> [CAtom o]
   -> [UMethodDef i] -> InfererM i o (InstanceBody o)
 checkInstanceBody className params methods = do
-  ClassDef _ methodNames _ paramBs scBs methodTys <- lookupClassDef className
+  ClassDef _ methodNames _ _ paramBs scBs methodTys <- lookupClassDef className
   Abs scBs' methodTys' <- applySubst (paramBs @@> (SubstVal <$> params)) $ Abs scBs $ ListE methodTys
   superclassTys <- superclassDictTys scBs'
   superclassDicts <- mapM (flip trySynthTerm Full) superclassTys
@@ -1952,7 +1982,7 @@ checkMethodDef className methodTys (WithSrcE src m) = addSrcContext src do
   UMethodDef ~(InternalName _ sourceName v) rhs <- return m
   MethodBinding className' i <- renameM v >>= lookupEnv
   when (className /= className') do
-    ClassBinding (ClassDef classSourceName _ _ _ _ _) <- lookupEnv className
+    ClassBinding (ClassDef classSourceName _ _ _ _ _ _) <- lookupEnv className
     throw TypeErr $ pprint sourceName ++ " is not a method of " ++ pprint classSourceName
   (i,) <$> Lam <$> checkULam rhs (methodTys !! i)
 
@@ -2008,12 +2038,12 @@ checkCasePat :: EmitsBoth o
 checkCasePat (WithSrcB pos pat) scrutineeTy cont = addSrcContext pos $ case pat of
   UPatCon ~(InternalName _ _ conName) ps -> do
     (dataDefName, con) <- renameM conName >>= lookupDataCon
-    TyConDef sourceName paramBs (ADTCons cons) <- lookupTyCon dataDefName
+    TyConDef sourceName roleExpls paramBs (ADTCons cons) <- lookupTyCon dataDefName
     DataConDef _ _ repTy idxs <- return $ cons !! con
     when (length idxs /= nestLength ps) $ throw TypeErr $
       "Unexpected number of pattern binders. Expected " ++ show (length idxs)
                                              ++ " got " ++ show (nestLength ps)
-    (params, repTy') <- inferParams sourceName (Abs paramBs repTy)
+    (params, repTy') <- inferParams sourceName roleExpls (Abs paramBs repTy)
     constrainTypesEq scrutineeTy $ TypeCon sourceName dataDefName params
     buildAltInf repTy' \arg -> do
       args <- forM idxs \projs -> do
@@ -2023,22 +2053,23 @@ checkCasePat (WithSrcB pos pat) scrutineeTy cont = addSrcContext pos $ case pat
   _ -> throw TypeErr $ "Case patterns must start with a data constructor or variant pattern"
 
 inferParams :: (EmitsBoth o, HasNamesE e, SinkableE e, SubstE AtomSubstVal e)
-            => SourceName -> Abs RolePiBinders e o -> InfererM i o (TyConParams o, e o)
-inferParams sourceName (Abs paramBs bodyTop) = do
-  (params, e') <- go (Abs paramBs bodyTop)
-  let expls = nestToList (\(RolePiBinder _ (WithExpl expl _)) -> expl) paramBs
+            => SourceName -> [RoleExpl] -> Abs (Nest CBinder) e o -> InfererM i o (TyConParams o, e o)
+inferParams sourceName roleExpls (Abs paramBs bodyTop) = do
+  let expls = snd <$> roleExpls
+  (params, e') <- go expls (Abs paramBs bodyTop)
   return (TyConParams expls params, e')
  where
   go :: (EmitsBoth o, HasNamesE e, SinkableE e, SubstE AtomSubstVal e)
-     => Abs (Nest RolePiBinder) e o -> InfererM i o ([CAtom o], e o)
-  go (Abs Empty body) = return ([], body)
-  go (Abs (Nest (RolePiBinder _ (WithExpl expl (b:>ty))) bs) body) = do
+     => [Explicitness] -> Abs (Nest CBinder) e o -> InfererM i o ([CAtom o], e o)
+  go [] (Abs Empty body) = return ([], body)
+  go (expl:expls) (Abs (Nest (b:>ty) bs) body) = do
     x <- case expl of
       Explicit -> Var <$> freshInferenceName (TypeInstantiationInfVar sourceName) ty
       Inferred argName infMech -> getImplicitArg (sourceName, fromMaybe "_" argName) infMech ty
     rest <- applySubst (b@>SubstVal x) $ Abs bs body
-    (params, body') <- go rest
+    (params, body') <- go expls rest
     return (x:params, body')
+  go _ _ = error "zip error"
 
 bindLetPats :: EmitsBoth o
             => Nest UPat i i' -> [CAtomVar o] -> InfererM i' o a -> InfererM i o a
@@ -2069,13 +2100,13 @@ bindLetPat (WithSrcB pos pat) v cont = addSrcContext pos $ case pat of
         cont
   UPatCon ~(InternalName _ _ conName) ps -> do
     (dataDefName, _) <- lookupDataCon =<< renameM conName
-    TyConDef sourceName paramBs cons <- lookupTyCon dataDefName
+    TyConDef sourceName roleExpls paramBs cons <- lookupTyCon dataDefName
     case cons of
       ADTCons [DataConDef _ _ _ idxss] -> do
         when (length idxss /= nestLength ps) $ throw TypeErr $
           "Unexpected number of pattern binders. Expected " ++ show (length idxss)
                                                  ++ " got " ++ show (nestLength ps)
-        (params, UnitE) <- inferParams sourceName (Abs paramBs UnitE)
+        (params, UnitE) <- inferParams sourceName roleExpls (Abs paramBs UnitE)
         constrainVarTy v $ TypeCon sourceName dataDefName params
         x <- cheapNormalize =<< zonk (Var v)
         xs <- forM idxss \idxs -> normalizeNaryProj idxs x >>= emit . Atom
@@ -2140,7 +2171,7 @@ inferTabCon hint xs reqTy = do
           withFreshBinder noHint finTy \b' ->  do
             elemTy' <- applyRename (b@>binderName b') elemTy
             dTy <- DictTy <$> dataDictType elemTy'
-            return $ Pi $ CorePiType ImplicitApp (UnaryNest (WithExpl (Inferred Nothing Unify) b')) (EffTy Pure dTy)
+            return $ Pi $ CorePiType ImplicitApp [Inferred Nothing Unify] (UnaryNest b') (EffTy Pure dTy)
       liftM Var $ emitHinted hint $ TabCon (dataDictHole dTy) tabTy xs'
 
 -- Bool flag is just to tweak the reported error message
@@ -2494,19 +2525,19 @@ unifyEq e1 e2 = guard =<< alphaEq e1 e2
 {-# INLINE unifyEq #-}
 
 instance Unifiable CorePiType where
-  unifyZonked (CorePiType appExpl1 bsTop1 effTy1)
-              (CorePiType appExpl2 bsTop2 effTy2) = do
+  unifyZonked (CorePiType appExpl1 expls1 bsTop1 effTy1)
+              (CorePiType appExpl2 expls2 bsTop2 effTy2) = do
     unless (appExpl1 == appExpl2) empty
+    unless (expls1 == expls2) empty
     go (Abs bsTop1 effTy1) (Abs bsTop2 effTy2)
    where
     go :: EmitsInf n
-       => Abs (Nest (WithExpl CBinder)) (EffTy CoreIR) n
-       -> Abs (Nest (WithExpl CBinder)) (EffTy CoreIR) n
+       => Abs (Nest CBinder) (EffTy CoreIR) n
+       -> Abs (Nest CBinder) (EffTy CoreIR) n
        -> SolverM n ()
     go (Abs Empty (EffTy e1 t1)) (Abs Empty (EffTy e2 t2)) = unify t1 t2 >> unify e1 e2
-    go (Abs (Nest (WithExpl expl1 (b1:>t1)) bs1) rest1)
-       (Abs (Nest (WithExpl expl2 (b2:>t2)) bs2) rest2) = do
-      unless (expl1 == expl2) empty
+    go (Abs (Nest (b1:>t1) bs1) rest1)
+       (Abs (Nest (b2:>t2) bs2) rest2) = do
       unify t1 t2
       v <- freshSkolemName t1
       ab1 <- zonk =<< applySubst (b1@>SubstVal (Var v)) (Abs bs1 rest1)
@@ -2585,13 +2616,9 @@ synthTopE block = do
 {-# SCC synthTopE #-}
 
 synthTyConDef :: (EnvReader m, Fallible1 m) => TyConDef n -> m n (TyConDef n)
-synthTyConDef (TyConDef sn rbs body) = (liftExcept =<<) $ liftDictSynthTraverserM do
-  let bs = fmapNest (\(RolePiBinder _ b) -> b) rbs
-  let roles = nestToList (\(RolePiBinder role _) -> role) rbs
-  dsTraverseExplBinders bs \bs' -> do
-    body' <- dsTraverse body
-    let rbs' = zipWithNest bs' roles \b role -> RolePiBinder role b
-    return $ TyConDef sn rbs' body'
+synthTyConDef (TyConDef sn roleExpls bs body) = (liftExcept =<<) $ liftDictSynthTraverserM do
+  dsTraverseExplBinders (snd <$> roleExpls) bs \bs' ->
+    TyConDef sn roleExpls bs' <$> dsTraverse body
 {-# SCC synthTyConDef #-}
 
 -- Given a simplified dict (an Atom of type `DictTy _` in the
@@ -2624,8 +2651,8 @@ generalizeDictRec dict = do
   DictCon _ dict' <- cheapNormalize dict
   mkDictAtom =<< case dict' of
     InstanceDict instanceName args -> do
-      InstanceDef _ bs _ _ <- lookupInstanceDef instanceName
-      args' <- generalizeInstanceArgs bs args
+      InstanceDef _ roleExpls bs _ _ <- lookupInstanceDef instanceName
+      args' <- generalizeInstanceArgs roleExpls bs args
       return $ InstanceDict instanceName args'
     IxFin _ -> IxFin <$> Var <$> freshInferenceName MiscInfVar NatTy
     InstantiatedGiven _ _ -> notSimplifiedDict
@@ -2633,9 +2660,9 @@ generalizeDictRec dict = do
     DataData ty           -> DataData <$> TyVar <$> freshInferenceName MiscInfVar ty
     where notSimplifiedDict = error $ "Not a simplified dict: " ++ pprint dict
 
-generalizeInstanceArgs :: EmitsInf n => RolePiBinders n l -> [CAtom n] -> SolverM n [CAtom n]
-generalizeInstanceArgs Empty [] = return []
-generalizeInstanceArgs (Nest (RolePiBinder role (WithExpl _ (b:>ty))) bs) (arg:args) = do
+generalizeInstanceArgs :: EmitsInf n => [RoleExpl] -> Nest CBinder n l -> [CAtom n] -> SolverM n [CAtom n]
+generalizeInstanceArgs [] Empty [] = return []
+generalizeInstanceArgs ((role,_):expls) (Nest (b:>ty) bs) (arg:args) = do
   arg' <- case role of
     -- XXX: for `TypeParam` we can just emit a fresh inference name rather than
     -- traversing the whole type like we do in `Generalize.hs`. The reason is
@@ -2646,21 +2673,21 @@ generalizeInstanceArgs (Nest (RolePiBinder role (WithExpl _ (b:>ty))) bs) (arg:a
     DictParam -> generalizeDictAndUnify ty arg
     DataParam -> Var <$> freshInferenceName MiscInfVar ty
   Abs bs' UnitE <- applySubst (b@>SubstVal arg') (Abs bs UnitE)
-  args' <- generalizeInstanceArgs bs' args
+  args' <- generalizeInstanceArgs expls bs' args
   return $ arg':args'
-generalizeInstanceArgs _ _ = error "zip error"
+generalizeInstanceArgs _ _ _ = error "zip error"
 
 synthInstanceDefAndAddSynthCandidate
   :: (Mut n, TopBuilder m, EnvReader m,  Fallible1 m) => InstanceDef n -> m n (InstanceName n)
-synthInstanceDefAndAddSynthCandidate def@(InstanceDef className bs params (InstanceBody superclasses _)) = do
-  let emptyDef = InstanceDef className bs params $ InstanceBody superclasses []
+synthInstanceDefAndAddSynthCandidate def@(InstanceDef className expls bs params (InstanceBody superclasses _)) = do
+  let emptyDef = InstanceDef className expls bs params $ InstanceBody superclasses []
   instanceName <- emitInstanceDef emptyDef
   addInstanceSynthCandidate className instanceName
   synthInstanceDefRec instanceName def
   return instanceName
 
 emitInstanceDef :: (Mut n, TopBuilder m) => InstanceDef n -> m n (Name InstanceNameC n)
-emitInstanceDef instanceDef@(InstanceDef className _ _ _) = do
+emitInstanceDef instanceDef@(InstanceDef className _ _ _ _) = do
   ty <- getInstanceType instanceDef
   emitBinding (getNameHint className) $ InstanceBinding instanceDef ty
 
@@ -2672,46 +2699,47 @@ pattern InstanceDefAbsBody :: [CAtom n] -> [CAtom n] -> [CAtom n] -> [CAtom n]
 pattern InstanceDefAbsBody params superclasses doneMethods todoMethods =
   ListE params `PairE` (ListE superclasses) `PairE` (ListE doneMethods) `PairE` (ListE todoMethods)
 
-type InstanceDefAbsT = Abs (Nest RolePiBinder) InstanceDefAbsBodyT
+type InstanceDefAbsT n = ([RoleExpl], Abs (Nest CBinder) InstanceDefAbsBodyT n)
 
-pattern InstanceDefAbs :: Nest RolePiBinder h n -> [CAtom n] -> [CAtom n] -> [CAtom n] -> [CAtom n]
+pattern InstanceDefAbs :: [RoleExpl] -> Nest CBinder h n -> [CAtom n] -> [CAtom n] -> [CAtom n] -> [CAtom n]
                        -> InstanceDefAbsT h
-pattern InstanceDefAbs bs params superclasses doneMethods todoMethods =
-  Abs bs (InstanceDefAbsBody params superclasses doneMethods todoMethods)
+pattern InstanceDefAbs expls bs params superclasses doneMethods todoMethods =
+  (expls, Abs bs (InstanceDefAbsBody params superclasses doneMethods todoMethods))
 
 synthInstanceDefRec
   :: (Mut n, TopBuilder m, EnvReader m,  Fallible1 m) => InstanceName n -> InstanceDef n -> m n ()
-synthInstanceDefRec instanceName (InstanceDef className bs params (InstanceBody superclasses methods)) = do
-  let ab = InstanceDefAbs bs params superclasses [] methods
+synthInstanceDefRec instanceName def = do
+  InstanceDef className roleExplsTop bs params (InstanceBody superclasses methods) <- return def
+  let ab = InstanceDefAbs roleExplsTop bs params superclasses [] methods
   recur ab className instanceName
   where
     recur :: (Mut n, TopBuilder m, EnvReader m, Fallible1 m)
           => InstanceDefAbsT n -> ClassName n -> InstanceName n -> m n ()
-    recur (InstanceDefAbs _ _ _ _ []) _ _ = return ()
-    recur ab cname iname = do
-      (def, ab') <- liftExceptEnvReaderM $ refreshAbs ab
+    recur (InstanceDefAbs _ _ _ _ _ []) _ _ = return ()
+    recur (roleExpls, ab) cname iname = do
+      (def', ab') <- liftExceptEnvReaderM $ refreshAbs ab
         \bs' (InstanceDefAbsBody ps scs doneMethods (m:ms)) -> do
           EnvReaderT $ ReaderT \(Distinct, env) -> do
-            let env' = extendSynthCandidatess bs' env
+            let env' = extendSynthCandidatess (snd<$>roleExpls) bs' env
             flip runReaderT (Distinct, env') $ runEnvReaderT' do
               m' <- synthTopE m
               let doneMethods' = doneMethods ++ [m']
-              let ab' = InstanceDefAbs bs' ps scs doneMethods' ms
-              let def = InstanceDef cname bs' ps $ InstanceBody scs doneMethods'
-              return (def, ab')
-      updateTopEnv $ UpdateInstanceDef iname def
+              let ab' = InstanceDefAbs roleExpls bs' ps scs doneMethods' ms
+              let def' = InstanceDef cname roleExpls bs' ps $ InstanceBody scs doneMethods'
+              return (def', ab')
+      updateTopEnv $ UpdateInstanceDef iname def'
       recur ab' cname iname
 
 synthInstanceDef
   :: (EnvReader m, Fallible1 m) => InstanceDef n -> m n (InstanceDef n)
-synthInstanceDef (InstanceDef className bs params body) = do
+synthInstanceDef (InstanceDef className expls bs params body) = do
   liftExceptEnvReaderM $ refreshAbs (Abs bs (ListE params `PairE` body))
     \bs' (ListE params' `PairE` InstanceBody superclasses methods) -> do
        EnvReaderT $ ReaderT \(Distinct, env) -> do
-         let env' = extendSynthCandidatess bs' env
+         let env' = extendSynthCandidatess (snd<$>expls) bs' env
          flip runReaderT (Distinct, env') $ runEnvReaderT' do
            methods' <- mapM synthTopE methods
-           return $ InstanceDef className bs' params' $ InstanceBody superclasses methods'
+           return $ InstanceDef className expls bs' params' $ InstanceBody superclasses methods'
 
 -- main entrypoint to dictionary synthesizer
 trySynthTerm :: (Fallible1 m, EnvReader m) => CType n -> RequiredMethodAccess -> m n (SynthAtom n)
@@ -2728,7 +2756,7 @@ trySynthTerm ty reqMethodAccess = do
 {-# SCC trySynthTerm #-}
 
 type SynthAtom = CAtom
-type SynthPiType = Abs (Nest (WithExpl CBinder)) DictType
+type SynthPiType n = ([Explicitness], Abs (Nest CBinder) DictType n)
 data SynthType n =
    SynthDictType (DictType n)
  | SynthPiType (SynthPiType n)
@@ -2781,7 +2809,7 @@ getSynthType x = ignoreExcept $ typeAsSynthType (getType x)
 typeAsSynthType :: CType n -> Except (SynthType n)
 typeAsSynthType = \case
   DictTy dictTy -> return $ SynthDictType dictTy
-  Pi (CorePiType ImplicitApp bs (EffTy Pure (DictTy d))) -> return $ SynthPiType (Abs bs d)
+  Pi (CorePiType ImplicitApp expls bs (EffTy Pure (DictTy d))) -> return $ SynthPiType (expls, Abs bs d)
   ty -> Failure $ Errs [Err TypeErr mempty $ "Can't synthesize terms of type: " ++ pprint ty]
 {-# SCC typeAsSynthType #-}
 
@@ -2827,11 +2855,11 @@ getSuperclassClosurePure env givens newGivens =
 
 synthTerm :: SynthType n -> RequiredMethodAccess -> SyntherM n (SynthAtom n)
 synthTerm targetTy reqMethodAccess = confuseGHC >>= \_ -> case targetTy of
-  SynthPiType ab -> do
-    ab' <- withGivenBinders ab \bs targetTy' -> do
+  SynthPiType (expls, ab) -> do
+    ab' <- withGivenBinders expls ab \bs targetTy' -> do
       Abs bs <$> synthTerm (SynthDictType targetTy') reqMethodAccess
     Abs bs synthExpr <- return ab'
-    liftM Lam $ coreLamExpr ImplicitApp $ Abs bs $ PairE Pure (WithoutDecls synthExpr)
+    liftM Lam $ coreLamExpr ImplicitApp expls $ Abs bs $ PairE Pure (WithoutDecls synthExpr)
   SynthDictType dictTy -> case dictTy of
     DictType "Ix" _ [Type (NewtypeTyCon (Fin n))] -> return $ DictCon (DictTy dictTy) $ IxFin n
     DictType "Data" _ [Type t] -> do
@@ -2848,21 +2876,29 @@ synthTerm targetTy reqMethodAccess = confuseGHC >>= \_ -> case targetTy of
         _ -> return dict
 {-# SCC synthTerm #-}
 
+coreLamExpr :: EnvReader m => AppExplicitness
+            -> [Explicitness] -> Abs (Nest CBinder) (PairE (EffectRow CoreIR) CBlock) n
+            -> m n (CoreLamExpr n)
+coreLamExpr appExpl expls ab = liftEnvReaderM do
+  refreshAbs ab \bs' (PairE effs' body') -> do
+    EffTy _ resultTy <- blockEffTy body'
+    return $ CoreLamExpr (CorePiType appExpl expls bs' (EffTy effs' resultTy)) (LamExpr bs' body')
+
 withGivenBinders
-  :: (SinkableE e, RenameE e) => Abs (Nest (WithExpl CBinder)) e n
-  -> (forall l. DExt n l => Nest (WithExpl CBinder) n l -> e l -> SyntherM l a)
+  :: (SinkableE e, RenameE 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 (Abs bsTop e) contTop =
-  runSubstReaderT idSubst $ go bsTop \bsTop' -> do
+withGivenBinders explsTop (Abs bsTop e) contTop =
+  runSubstReaderT idSubst $ go explsTop bsTop \bsTop' -> do
     e' <- renameM e
     liftSubstReaderT $ contTop bsTop' e'
  where
-   go :: Nest (WithExpl CBinder) i i'
-      -> (forall o'. DExt o o' => Nest (WithExpl CBinder) o o' -> SubstReaderT Name SyntherM i' o' a)
+   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 bs cont = case bs of
-     Empty -> getDistinct >>= \Distinct -> cont Empty
-     Nest (WithExpl expl b) rest -> do
+   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
@@ -2871,13 +2907,14 @@ withGivenBinders (Abs bsTop e) contTop =
          s <- getSubst
          liftSubstReaderT $ extendGivens givens $
            runSubstReaderT (s <>> b@>binderName b') $
-             go rest \rest' -> cont (Nest (WithExpl expl b') rest')
+             go explsRest rest \rest' -> cont (Nest b' rest')
+     _ -> error "zip error"
 
 isMethodAccessAllowedBy :: EnvReader m =>  RequiredMethodAccess -> InstanceName n -> m n Bool
 isMethodAccessAllowedBy access instanceName = do
-  InstanceDef className _ _ (InstanceBody _ methods) <- lookupInstanceDef instanceName
+  InstanceDef className _ _ _ (InstanceBody _ methods) <- lookupInstanceDef instanceName
   let numInstanceMethods = length methods
-  ClassDef _ _ _ _ _ methodTys <- lookupClassDef className
+  ClassDef _ _ _ _ _ _ methodTys <- lookupClassDef className
   let numClassMethods = length methodTys
   case access of
     Full                  -> return $ numClassMethods == numInstanceMethods
@@ -2899,34 +2936,35 @@ synthDictFromInstance :: DictType n -> SyntherM n (SynthAtom n)
 synthDictFromInstance targetTy@(DictType _ targetClass _) = do
   instances <- getInstanceDicts targetClass
   asum $ instances <&> \candidate -> do
-    CorePiType _ bs (EffTy _ (DictTy candidateTy)) <- lookupInstanceTy candidate
-    args <- instantiateSynthArgs targetTy $ Abs bs candidateTy
+    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 (Abs bsTop resultTyTop) = do
+instantiateSynthArgs targetTop (explsTop, Abs bsTop resultTyTop) = do
   ListE args <- (liftExceptAlt =<<) $ liftSolverM $ solveLocal do
-    args <- runSubstReaderT idSubst $ go (sink targetTop) (sink $ Abs bsTop resultTyTop)
+    args <- runSubstReaderT idSubst $ go (sink targetTop) explsTop (sink $ Abs bsTop resultTyTop)
     zonk $ ListE args
   forM args \case
     DictHole _ argTy req -> liftExceptAlt (typeAsSynthType argTy) >>= flip synthTerm req
     arg -> return arg
  where
    go :: EmitsInf o
-      => DictType o -> Abs (Nest (WithExpl CBinder)) DictType i
+      => DictType o -> [Explicitness] -> Abs (Nest CBinder) DictType i
       -> SubstReaderT AtomSubstVal SolverM i o [CAtom o]
-   go target (Abs bs proposed) = case bs of
-     Empty -> do
+   go target allExpls (Abs bs proposed) = case (allExpls, bs) of
+     ([], Empty) -> do
        proposed' <- substM proposed
        liftSubstReaderT $ unify target proposed'
        return []
-     Nest (WithExpl expl b) rest -> do
+     (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 (Abs rest proposed)
+       liftM (arg:) $ extendSubst (b@>SubstVal arg) $ go target expls (Abs rest proposed)
+     _ -> error "zip error"
 
 synthDictForData :: forall n. DictType n -> SyntherM n (SynthAtom n)
 synthDictForData dictTy@(DictType "Data" dName [Type ty]) = case ty of
@@ -3010,12 +3048,10 @@ instance DictSynthTraversable CAtom where
       case ans of
         Failure errs -> put (LiftE errs) >> renameM atom
         Success d    -> return d
-    Lam (CoreLamExpr piTy@(CorePiType _ bsPi _) (LamExpr bsLam (Abs decls result))) -> do
+    Lam (CoreLamExpr piTy@(CorePiType _ expls _ _) (LamExpr bsLam (Abs decls result))) -> do
       Pi piTy' <- dsTraverse $ Pi piTy
-      let (expls, _) = unzipExpls bsPi
-      lam' <- dsTraverseExplBinders (zipExpls expls bsLam) \bsLamExpl' -> do
+      lam' <- dsTraverseExplBinders expls bsLam \bsLam' -> do
         visitDeclsNoEmits decls \decls' -> do
-          let (_, bsLam') = unzipExpls bsLamExpl'
           LamExpr bsLam' <$> Abs decls' <$> dsTraverse result
       return $ Lam $ CoreLamExpr piTy' lam'
     Var _          -> renameM atom
@@ -3025,9 +3061,9 @@ instance DictSynthTraversable CAtom where
 
 instance DictSynthTraversable CType where
   dsTraverse ty = case ty of
-    Pi (CorePiType appExpl bs (EffTy effs resultTy)) -> Pi <$>
-      dsTraverseExplBinders bs \bs' -> do
-        CorePiType appExpl bs' <$> (EffTy <$> renameM effs <*> dsTraverse resultTy)
+    Pi (CorePiType appExpl expls bs (EffTy effs resultTy)) -> Pi <$>
+      dsTraverseExplBinders expls bs \bs' -> do
+        CorePiType appExpl expls bs' <$> (EffTy <$> renameM effs <*> dsTraverse resultTy)
     TyVar _          -> renameM ty
     ProjectEltTy _ _ _ -> renameM ty
     _ -> visitTypePartial ty
@@ -3035,16 +3071,17 @@ instance DictSynthTraversable CType where
 instance DictSynthTraversable DataConDefs where dsTraverse = visitGeneric
 
 dsTraverseExplBinders
-  :: Nest (WithExpl CBinder) i i'
-  -> (forall o'. DExt o o' => Nest (WithExpl CBinder) o o' -> DictSynthTraverserM i' o' a)
+  :: [Explicitness] -> Nest CBinder i i'
+  -> (forall o'. DExt o o' => Nest CBinder o o' -> DictSynthTraverserM i' o' a)
   -> DictSynthTraverserM i o a
-dsTraverseExplBinders Empty cont = getDistinct >>= \Distinct -> cont Empty
-dsTraverseExplBinders (Nest (WithExpl expl b) bs) cont = do
+dsTraverseExplBinders [] Empty cont = getDistinct >>= \Distinct -> cont Empty
+dsTraverseExplBinders (expl:expls) (Nest b bs) cont = do
   ty <- dsTraverse $ binderType b
   withFreshBinder (getNameHint b) ty \b' -> do
     let v = binderName b'
     extendSynthCandidatesDict expl v $ extendRenamer (b@>v) do
-      dsTraverseExplBinders bs \bs' -> cont $ Nest (WithExpl expl b') bs'
+      dsTraverseExplBinders expls bs \bs' -> cont $ Nest b' bs'
+dsTraverseExplBinders _ _ _ = error "zip error"
 
 extendSynthCandidatesDict :: Explicitness -> CAtomName n -> DictSynthTraverserM i n a -> DictSynthTraverserM i n a
 extendSynthCandidatesDict c v cont = DictSynthTraverserM do
@@ -3063,6 +3100,9 @@ extendSynthCandidatesDict c v cont = DictSynthTraverserM do
 -- the needs of inference, like adding `SubstE AtomSubstVal e` constraints in
 -- various places.
 
+type WithExpl     = WithAttrB Explicitness
+type WithRoleExpl = WithAttrB RoleExpl
+
 buildBlockInf
   :: EmitsInf n
   => (forall l. (EmitsBoth l, DExt n l) => InfererM i l (CAtom l))
@@ -3096,10 +3136,8 @@ buildTabPiInf
   -> (forall l. (EmitsInf l, Ext n l) => CAtomVar l -> InfererM i l (CType l))
   -> InfererM i n (TabPiType CoreIR n)
 buildTabPiInf hint (IxType t d) body = do
-  Abs (WithExpl _ (b:>_)) resultTy <-
-    buildAbsInf hint Explicit t \v ->
-      withoutEffects $ body v
-  return $ TabPiType d (b:>t) resultTy
+  Abs b resultTy <- buildAbsInf hint Explicit t \v -> withoutEffects $ body v
+  return $ TabPiType d b resultTy
 
 buildDepPairTyInf
   :: EmitsInf n
@@ -3108,7 +3146,7 @@ buildDepPairTyInf
   -> InfererM i n (DepPairType CoreIR n)
 buildDepPairTyInf hint expl ty body = do
   Abs b resultTy <- buildAbsInf hint Explicit ty body
-  return $ DepPairType expl (withoutExpl b) resultTy
+  return $ DepPairType expl b resultTy
 
 buildAltInf
   :: EmitsInf n
@@ -3116,11 +3154,10 @@ buildAltInf
   -> (forall l. (EmitsBoth l, Ext n l) => CAtomVar l -> InfererM i l (CAtom l))
   -> InfererM i n (Alt CoreIR n)
 buildAltInf ty body = do
-  Abs b body' <- buildAbsInf noHint Explicit ty \v ->
+  buildAbsInf noHint Explicit ty \v ->
     buildBlockInf do
       Distinct <- getDistinct
       body $ sink v
-  return $ Abs (withoutExpl b) body'
 
 -- === EmitsInf predicate ===
 
@@ -3190,11 +3227,11 @@ instance BindsEnv InfOutFrag where
   toEnvFrag (InfOutFrag frag _ _) = toEnvFrag frag
 
 instance GenericE SynthType where
-  type RepE SynthType = EitherE2 DictType (Abs (Nest (WithExpl CBinder)) DictType)
+  type RepE SynthType = EitherE2 DictType (PairE (LiftE [Explicitness]) (Abs (Nest CBinder) DictType))
   fromE (SynthDictType d) = Case0 d
-  fromE (SynthPiType   t) = Case1 t
+  fromE (SynthPiType   (expl, t)) = Case1 (PairE (LiftE expl) t)
   toE (Case0 d) = SynthDictType d
-  toE (Case1 t) = SynthPiType   t
+  toE (Case1 (PairE (LiftE expl) t)) = SynthPiType (expl, t)
   toE _ = error "impossible"
 
 instance AlphaEqE       SynthType
diff --git a/src/lib/Name.hs b/src/lib/Name.hs
index ddb01ab8d..68d1ad2f8 100644
--- a/src/lib/Name.hs
+++ b/src/lib/Name.hs
@@ -521,6 +521,20 @@ data PairB (b1::B) (b2::B) (n::S) (l::S) where
   PairB :: b1 n l' -> b2 l' l -> PairB b1 b2 n l
 deriving instance (ShowB b1, ShowB b2) => Show (PairB b1 b2 n l)
 
+data WithAttrB (a:: *) (b::B) (n::S) (l::S) =
+  WithAttrB {getAttr :: a , withoutAttr :: b n l }
+  deriving (Show, Generic)
+
+unzipAttrs :: Nest (WithAttrB a b) n l -> ([a], Nest b n l)
+unzipAttrs Empty = ([], Empty)
+unzipAttrs (Nest (WithAttrB a b) rest) = (a:as, Nest b bs)
+  where (as, bs) = unzipAttrs rest
+
+zipAttrs :: [a] -> Nest b n l -> Nest (WithAttrB a b) n l
+zipAttrs [] Empty = Empty
+zipAttrs (a:as) (Nest b bs) = Nest (WithAttrB a b) (zipAttrs as bs)
+zipAttrs _ _ = error "zip error"
+
 data EitherB (b1::B) (b2::B) (n::S) (l::S) =
    LeftB  (b1 n l)
  | RightB (b2 n l)
@@ -655,7 +669,7 @@ forNest :: Nest b  i i'
         -> Nest b' i i'
 forNest n f = fmapNest f n
 
-zipWithNest :: Nest b  n l -> [a]
+zipWithNest :: Nest b n l -> [a]
             -> (forall n1 n2. b n1 n2 -> a -> b' n1 n2)
             -> Nest b' n l
 zipWithNest Empty [] _ = Empty
@@ -3195,6 +3209,35 @@ instance Monad HoistExcept where
   HoistSuccess x >>= f = f x
   {-# INLINE (>>=) #-}
 
+instance (Store a, Store (b n l)) => Store (WithAttrB a b n l)
+
+instance (Eq a, AlphaEqB b) => AlphaEqB (WithAttrB a b) where
+  withAlphaEqB (WithAttrB a1 b1) (WithAttrB a2 b2) cont = do
+    unless (a1 == a2) zipErr
+    withAlphaEqB b1 b2 cont
+
+instance (Hashable a, AlphaHashableB b) => AlphaHashableB (WithAttrB a b) where
+  hashWithSaltB env salt (WithAttrB expl b) = do
+    let h = hashWithSalt salt expl
+    hashWithSaltB env h b
+
+instance BindsNames b => ProvesExt  (WithAttrB a b) where
+instance BindsNames b => BindsNames (WithAttrB a b) where
+  toScopeFrag (WithAttrB _ b) = toScopeFrag b
+
+instance (SinkableB b) => SinkableB (WithAttrB a b) where
+  sinkingProofB fresh (WithAttrB a b) cont =
+    sinkingProofB fresh b \fresh' b' ->
+      cont fresh' (WithAttrB a b')
+
+instance (BindsNames b, RenameB b) => RenameB (WithAttrB a b) where
+  renameB env (WithAttrB a b) cont =
+      renameB env b \env' b' ->
+        cont env' $ WithAttrB a b'
+
+instance HoistableB b => HoistableB (WithAttrB a b) where
+  freeVarsB (WithAttrB _ b) = freeVarsB b
+
 -- === extra data structures ===
 
 -- A map from names in some scope to values that do not contain names.  This is
diff --git a/src/lib/PPrint.hs b/src/lib/PPrint.hs
index c68ea0390..23bc7ea60 100644
--- a/src/lib/PPrint.hs
+++ b/src/lib/PPrint.hs
@@ -296,26 +296,26 @@ forStr Fwd = "for"
 forStr Rev = "rof"
 
 instance Pretty (CorePiType n) where
-  pretty (CorePiType appExpl bs (EffTy eff resultTy)) =
-    prettyBindersWithExpl bs <+> p appExpl <> prettyEff <> p resultTy
+  pretty (CorePiType appExpl expls bs (EffTy eff resultTy)) =
+    prettyBindersWithExpl expls bs <+> p appExpl <> prettyEff <> p resultTy
     where
       prettyEff = case eff of
         Pure -> space
         _    -> space <> pretty eff <> space
 
 prettyBindersWithExpl :: forall b n l ann. PrettyB b
-  => Nest (WithExpl b) n l -> Doc ann
-prettyBindersWithExpl bs = do
-  let groups = groupByExpl $ fromNest bs
+  => [Explicitness] -> Nest b n l -> Doc ann
+prettyBindersWithExpl expls bs = do
+  let groups = groupByExpl $ zip expls (fromNest bs)
   let groups' = case groups of [] -> [(Explicit, [])]
                                _  -> groups
   mconcat [withExplParens expl $ commaSep bsGroup | (expl, bsGroup) <- groups']
 
-groupByExpl :: [WithExpl b UnsafeS UnsafeS] -> [(Explicitness, [b UnsafeS UnsafeS])]
+groupByExpl :: [(Explicitness, b UnsafeS UnsafeS)] -> [(Explicitness, [b UnsafeS UnsafeS])]
 groupByExpl [] = []
-groupByExpl (WithExpl expl b:bs) = do
-  let (matches, rest) = span (\(WithExpl expl' _) -> expl == expl') bs
-  let matches' = map withoutExpl matches
+groupByExpl ((expl, b):bs) = do
+  let (matches, rest) = span (\(expl', _) -> expl == expl') bs
+  let matches' = map snd matches
   (expl, b:matches') : groupByExpl rest
 
 withExplParens :: Explicitness -> Doc ann -> Doc ann
@@ -431,36 +431,29 @@ instance Pretty (TyConParams n) where
   pretty (TyConParams _ _) = undefined
 
 instance Pretty (TyConDef n) where
-  pretty (TyConDef name bs cons) =
-    "data" <+> p name <+> (p $ map (\(RolePiBinder _ b) -> b) $ fromNest bs) <> pretty cons
+  pretty (TyConDef name _ bs cons) = "data" <+> p name <+> p bs <> pretty cons
 
 instance Pretty (DataConDefs n) where
   pretty = undefined
 
-instance Pretty (RolePiBinder n l) where
-  pretty (RolePiBinder _ b) = pretty b
-
 instance Pretty (DataConDef n) where
   pretty (DataConDef name _ repTy _) =
     p name <+> ":" <+> p repTy
 
 instance Pretty (ClassDef n) where
-  pretty (ClassDef classSourceName methodNames _ params superclasses methodTys) =
+  pretty (ClassDef classSourceName methodNames _ _ params superclasses methodTys) =
     "Class:" <+> pretty classSourceName <+> pretty methodNames
     <> indented (
-         line <> "parameter binders:" <+> prettyRolePiBinders params <>
+         line <> "parameter binders:" <+> pretty params <>
          line <> "superclasses:" <+> pretty superclasses <>
          line <> "methods:" <+> pretty methodTys)
 
 instance Pretty ParamRole where
   pretty r = p (show r)
 
-prettyRolePiBinders :: RolePiBinders n l -> Doc ann
-prettyRolePiBinders = undefined
-
 instance Pretty (InstanceDef n) where
-  pretty (InstanceDef className bs params _) =
-    "Instance" <+> p className <+> prettyRolePiBinders bs <+> p params
+  pretty (InstanceDef className _ bs params _) =
+    "Instance" <+> p className <+> pretty bs <+> p params
 
 deriving instance (forall c n. Pretty (v c n)) => Pretty (RecSubst v o)
 
@@ -629,14 +622,11 @@ instance Pretty FieldName' where
 instance Pretty (UAlt n) where
   pretty (UAlt pat body) = p pat <+> "->" <+> p body
 
-instance PrettyB b => Pretty (WithExpl b n l) where
-  pretty (WithExpl _ b) = pretty b
-
 instance Pretty (UTopDecl n l) where
-  pretty (UDataDefDecl (UDataDef nm bs dataCons) bTyCon bDataCons) =
+  pretty (UDataDefDecl (UDataDef nm (_, bs) dataCons) bTyCon bDataCons) =
     "data" <+> p bTyCon <+> p nm <+> spaced (fromNest bs) <+> "where" <> nest 2
        (prettyLines (zip (toList $ fromNest bDataCons) dataCons))
-  pretty (UStructDecl bTyCon (UStructDef nm bs fields defs)) =
+  pretty (UStructDecl bTyCon (UStructDef nm (_, bs) fields defs)) =
     "struct" <+> p bTyCon <+> p nm <+> spaced (fromNest bs) <+> "where" <> nest 2
        (prettyLines fields <> prettyLines defs)
   pretty (UInterface params methodTys interfaceName methodNames) =
diff --git a/src/lib/QueryType.hs b/src/lib/QueryType.hs
index eaad95cba..f5952402b 100644
--- a/src/lib/QueryType.hs
+++ b/src/lib/QueryType.hs
@@ -73,7 +73,7 @@ blockEff :: (EnvReader m, IRRep r) => Block r n -> m n (EffectRow r n)
 blockEff b = blockEffTy b <&> \(EffTy eff _) -> eff
 
 typeOfApp  :: (IRRep r, EnvReader m) => Type r n -> [Atom r n] -> m n (Type r n)
-typeOfApp (Pi (CorePiType _ bs (EffTy _ resultTy))) xs = do
+typeOfApp (Pi (CorePiType _ _ bs (EffTy _ resultTy))) xs = do
   let subst = bs @@> fmap SubstVal xs
   applySubst subst resultTy
 typeOfApp _ _ = error "expected a pi type"
@@ -93,14 +93,14 @@ typeOfApplyMethod d i args = do
 typeOfDictExpr :: EnvReader m => DictExpr n -> m n (CType n)
 typeOfDictExpr e = liftM ignoreExcept $ liftEnvReaderT $ case e of
   InstanceDict instanceName args -> do
-    InstanceDef className bs params _ <- lookupInstanceDef instanceName
-    ClassDef sourceName _ _ _ _ _ <- lookupClassDef className
+    InstanceDef className _ bs params _ <- lookupInstanceDef instanceName
+    ClassDef sourceName _ _ _ _ _ _ <- lookupClassDef className
     ListE params' <- applySubst (bs @@> map SubstVal args) $ ListE params
     return $ DictTy $ DictType sourceName className params'
   InstantiatedGiven given args -> typeOfApp (getType given) args
   SuperclassProj d i -> do
     DictTy (DictType _ className params) <- return $ getType d
-    ClassDef _ _ _ bs superclasses _ <- lookupClassDef className
+    ClassDef _ _ _ _ bs superclasses _ <- lookupClassDef className
     applySubst (bs @@> map SubstVal params) $
       getSuperclassType REmpty superclasses i
   IxFin n -> liftM DictTy $ ixDictType $ NewtypeTyCon $ Fin n
@@ -131,20 +131,21 @@ typeOfProjRef (TC (RefType h s)) p = do
 typeOfProjRef _ _ = error "expected a reference"
 
 appEffTy  :: (IRRep r, EnvReader m) => Type r n -> [Atom r n] -> m n (EffTy r n)
-appEffTy (Pi (CorePiType _ bs effTy)) xs = do
+appEffTy (Pi (CorePiType _ _ bs effTy)) xs = do
   let subst = bs @@> fmap SubstVal xs
   applySubst subst effTy
 appEffTy t _ = error $ "expected a pi type, got: " ++ pprint t
 
 partialAppType  :: (IRRep r, EnvReader m) => Type r n -> [Atom r n] -> m n (Type r n)
-partialAppType (Pi (CorePiType expl bs effTy)) xs = do
+partialAppType (Pi (CorePiType appExpl expls bs effTy)) xs = do
+  (_, expls2) <- return $ splitAt (length xs) expls
   PairB bs1 bs2 <- return $ splitNestAt (length xs) bs
   let subst = bs1 @@> fmap SubstVal xs
-  applySubst subst $ Pi $ CorePiType expl bs2 effTy
+  applySubst subst $ Pi $ CorePiType appExpl expls2 bs2 effTy
 partialAppType _ _ = error "expected a pi type"
 
 appEffects :: (EnvReader m, IRRep r) => Type r n -> [Atom r n] -> m n (EffectRow r n)
-appEffects (Pi (CorePiType _ bs (EffTy effs _))) xs = do
+appEffects (Pi (CorePiType _ _ bs (EffTy effs _))) xs = do
   let subst = bs @@> fmap SubstVal xs
   applySubst subst effs
 appEffects _ _ = error "expected a pi type"
@@ -198,7 +199,7 @@ deleteEff eff (EffectRow effs t) = EffectRow (effs `eSetDifference` eSetSingleto
 
 getMethodIndex :: EnvReader m => ClassName n -> SourceName -> m n Int
 getMethodIndex className methodSourceName = do
-  ClassDef _ methodNames _ _ _ _ <- lookupClassDef className
+  ClassDef _ methodNames _ _ _ _ _ <- lookupClassDef className
   case elemIndex methodSourceName methodNames of
     Nothing -> error $ methodSourceName ++ " is not a method of " ++ pprint className
     Just i -> return i
@@ -211,9 +212,8 @@ getUVarType = \case
   UDataConVar v -> getDataConNameType v
   UPunVar     v -> getStructDataConType v
   UClassVar v -> do
-    ClassDef _ _ _ bs _ _ <- lookupClassDef v
-    let bs' = fmapNest (\(RolePiBinder _ b) -> b) bs
-    return $ Pi $ CorePiType ExplicitApp bs' $ EffTy Pure TyKind
+    ClassDef _ _ _ roleExpls bs _ _ <- lookupClassDef v
+    return $ Pi $ CorePiType ExplicitApp (map snd roleExpls) bs $ EffTy Pure TyKind
   UMethodVar  v -> getMethodNameType v
   UEffectVar   _ -> error "not implemented"
   UEffectOpVar _ -> error "not implemented"
@@ -221,23 +221,22 @@ getUVarType = \case
 getMethodNameType :: EnvReader m => MethodName n -> m n (CType n)
 getMethodNameType v = liftEnvReaderM $ lookupEnv v >>= \case
   MethodBinding className i -> do
-    ClassDef _ _ paramNames paramBs scBinders methodTys <- lookupClassDef className
-    let paramBs' = zipWithNest paramBs paramNames \(RolePiBinder _ (WithExpl _ b)) paramName ->
-          WithExpl (Inferred paramName Unify) b
-    refreshAbs (Abs paramBs' $ Abs scBinders (methodTys !! i)) \paramBs'' (Abs scBinders' piTy) -> do
-      let params = Var <$> nestToAtomVars (fmapNest withoutExpl paramBs'')
+    ClassDef _ _ paramNames _ paramBs scBinders methodTys <- lookupClassDef className
+    refreshAbs (Abs paramBs $ Abs scBinders (methodTys !! i)) \paramBs' (Abs scBinders' piTy) -> do
+      let params = Var <$> nestToAtomVars paramBs'
       dictTy <- DictTy <$> dictType (sink className) params
       withFreshBinder noHint dictTy \dictB -> do
         scDicts <- getSuperclassDicts (Var $ binderVar dictB)
         piTy' <- applySubst (scBinders'@@>(SubstVal<$>scDicts)) piTy
-        CorePiType appExpl methodBs effTy <- return piTy'
-        let dictBs = UnaryNest $ WithExpl (Inferred Nothing (Synth $ Partial $ succ i)) dictB
-        return $ Pi $ CorePiType appExpl (paramBs'' >>> dictBs >>> methodBs) effTy
+        CorePiType appExpl methodExpls methodBs effTy <- return piTy'
+        let paramExpls = paramNames <&> \name -> Inferred name Unify
+        let expls = paramExpls <> [Inferred Nothing (Synth $ Partial $ succ i)] <> methodExpls
+        return $ Pi $ CorePiType appExpl expls (paramBs' >>> UnaryNest dictB >>> methodBs) effTy
 
 getMethodType :: EnvReader m => Dict n -> Int -> m n (CorePiType n)
 getMethodType dict i = do
   ~(DictTy (DictType _ className params)) <- return $ getType dict
-  ClassDef _ _ _ paramBs classBs methodTys <- lookupClassDef className
+  ClassDef _ _ _ _ paramBs classBs methodTys <- lookupClassDef className
   let methodTy = methodTys !! i
   superclassDicts <- getSuperclassDicts dict
   let subst = (    paramBs @@> map SubstVal params
@@ -245,60 +244,56 @@ getMethodType dict i = do
   applySubst subst methodTy
 {-# INLINE getMethodType #-}
 
-
 getTyConNameType :: EnvReader m => TyConName n -> m n (Type CoreIR n)
 getTyConNameType v = do
-  TyConDef _ bs _ <- lookupTyCon v
+  TyConDef _ expls bs _ <- lookupTyCon v
   case bs of
     Empty -> return TyKind
-    _ -> do
-      let bs' = fmapNest (\(RolePiBinder _ b) -> b) bs
-      return $ Pi $ CorePiType ExplicitApp bs' $ EffTy Pure TyKind
+    _ -> return $ Pi $ CorePiType ExplicitApp (snd <$> expls) bs $ EffTy Pure TyKind
 
 getDataConNameType :: EnvReader m => DataConName n -> m n (Type CoreIR n)
 getDataConNameType dataCon = liftEnvReaderM do
   (tyCon, i) <- lookupDataCon dataCon
   lookupTyCon tyCon >>= \case
-    tyConDef@(TyConDef tcSn paramBs ~(ADTCons dataCons)) ->
-      buildDataConType tyConDef \paramBs' paramVs params -> do
+    tyConDef@(TyConDef tcSn _ paramBs ~(ADTCons dataCons)) ->
+      buildDataConType tyConDef \expls paramBs' paramVs params -> do
         DataConDef _ ab _ _ <- applyRename (paramBs @@> paramVs) (dataCons !! i)
         refreshAbs ab \dataBs UnitE -> do
           let appExpl = case dataBs of Empty -> ImplicitApp
                                        _     -> ExplicitApp
           let resultTy = NewtypeTyCon $ UserADTType tcSn (sink tyCon) (sink params)
-          let dataBs' = fmapNest (WithExpl Explicit) dataBs
-          return $ Pi $ CorePiType appExpl (paramBs' >>> dataBs') (EffTy Pure resultTy)
+          let dataExpls = nestToList (const $ Explicit) dataBs
+          return $ Pi $ CorePiType appExpl (expls <> dataExpls) (paramBs' >>> dataBs) (EffTy Pure resultTy)
 
 getStructDataConType :: EnvReader m => TyConName n -> m n (CType n)
 getStructDataConType tyCon = liftEnvReaderM do
-  tyConDef@(TyConDef tcSn paramBs ~(StructFields fields)) <- lookupTyCon tyCon
-  buildDataConType tyConDef \paramBs' paramVs params -> do
+  tyConDef@(TyConDef tcSn _ paramBs ~(StructFields fields)) <- lookupTyCon tyCon
+  buildDataConType tyConDef \expls paramBs' paramVs params -> do
     fieldTys <- forM fields \(_, t) -> applyRename (paramBs @@> paramVs) t
     let resultTy = NewtypeTyCon $ UserADTType tcSn (sink tyCon) params
     Abs dataBs resultTy' <- return $ typesAsBinderNest fieldTys resultTy
-    let dataBs' = fmapNest (WithExpl Explicit) dataBs
-    return $ Pi $ CorePiType ExplicitApp (paramBs' >>> dataBs') (EffTy Pure resultTy')
+    let dataExpls = nestToList (const Explicit) dataBs
+    return $ Pi $ CorePiType ExplicitApp (expls <> dataExpls) (paramBs' >>> dataBs) (EffTy Pure resultTy')
 
 buildDataConType
   :: (EnvReader m, EnvExtender m)
   => TyConDef n
-  -> (forall l. DExt n l => Nest (WithExpl CBinder) n l -> [CAtomName l] -> TyConParams l -> m l a)
+  -> (forall l. DExt n l => [Explicitness] -> Nest CBinder n l -> [CAtomName l] -> TyConParams l -> m l a)
   -> m n a
-buildDataConType (TyConDef _ bs _) cont = do
-  bs' <- return $ forNest bs \(RolePiBinder _ (WithExpl expl b)) -> case expl of
-    Explicit -> WithExpl (Inferred Nothing Unify) b
-    _        -> WithExpl expl b
-  refreshAbs (Abs bs' UnitE) \bs'' UnitE -> do
-    let expls = nestToList (\(RolePiBinder _ b) -> getExpl b) bs
-    let vs = nestToNames bs''
+buildDataConType (TyConDef _ roleExpls bs _) cont = do
+  let expls = snd <$> roleExpls
+  expls' <- forM expls \case
+    Explicit -> return $ Inferred Nothing Unify
+    expl     -> return $ expl
+  refreshAbs (Abs bs UnitE) \bs' UnitE -> do
+    let vs = nestToNames bs'
     vs' <- mapM toAtomVar vs
-    cont bs'' vs $ TyConParams expls (Var <$> vs')
+    cont expls' bs' vs $ TyConParams expls (Var <$> vs')
 
 makeTyConParams :: EnvReader m => TyConName n -> [CAtom n] -> m n (TyConParams n)
 makeTyConParams tc params = do
-  TyConDef _ paramBs _ <- lookupTyCon tc
-  let expls = nestToList (\(RolePiBinder _ b) -> getExpl b) paramBs
-  return $ TyConParams expls params
+  TyConDef _ expls _ _ <- lookupTyCon tc
+  return $ TyConParams (map snd expls) params
 
 getDataClassName :: (Fallible1 m, EnvReader m) => m n (ClassName n)
 getDataClassName = lookupSourceMap "Data" >>= \case
@@ -319,7 +314,7 @@ getIxClassName = lookupSourceMap "Ix" >>= \case
 
 dictType :: EnvReader m => ClassName n -> [CAtom n] -> m n (DictType n)
 dictType className params = do
-  ClassDef sourceName _ _ _ _ _ <- lookupClassDef className
+  ClassDef sourceName _ _ _ _ _ _ <- lookupClassDef className
   return $ DictType sourceName className params
 
 ixDictType :: (Fallible1 m, EnvReader m) => CType n -> m n (DictType n)
@@ -374,7 +369,7 @@ getSuperclassDicts dict = do
 
 getSuperclassTys :: EnvReader m => DictType n -> m n [CType n]
 getSuperclassTys (DictType _ className params) = do
-  ClassDef _ _ _ bs superclasses _ <- lookupClassDef className
+  ClassDef _ _ _ _ bs superclasses _ <- lookupClassDef className
   forM [0 .. nestLength superclasses - 1] \i -> do
     applySubst (bs @@> map SubstVal params) $
       getSuperclassType REmpty superclasses i
diff --git a/src/lib/QueryTypePure.hs b/src/lib/QueryTypePure.hs
index 3bda0d8fd..2501cbf8f 100644
--- a/src/lib/QueryTypePure.hs
+++ b/src/lib/QueryTypePure.hs
@@ -221,8 +221,8 @@ typesAsBinderNest types body = toConstBinderNest types body
 nonDepPiType :: [CType n] -> EffectRow CoreIR n -> CType n -> CorePiType n
 nonDepPiType argTys eff resultTy = case typesAsBinderNest argTys (PairE eff resultTy) of
   Abs bs (PairE eff' resultTy') -> do
-    let bs' = fmapNest (WithExpl Explicit) bs
-    CorePiType ExplicitApp bs' $ EffTy eff' resultTy'
+    let expls = nestToList (const Explicit) bs
+    CorePiType ExplicitApp expls bs $ EffTy eff' resultTy'
 
 nonDepTabPiType :: IRRep r => IxType r n -> Type r n -> TabPiType r n
 nonDepTabPiType (IxType t d) resultTy =
@@ -230,7 +230,7 @@ nonDepTabPiType (IxType t d) resultTy =
     Abs b resultTy' -> TabPiType d (b:>t) resultTy'
 
 corePiTypeToPiType :: CorePiType n -> PiType CoreIR n
-corePiTypeToPiType (CorePiType _ bs effTy) = PiType (fmapNest withoutExpl bs) effTy
+corePiTypeToPiType (CorePiType _ _ bs effTy) = PiType bs effTy
 
 coreLamToTopLam :: CoreLamExpr n -> TopLam CoreIR n
 coreLamToTopLam (CoreLamExpr ty f) = TopLam False (corePiTypeToPiType ty) f
diff --git a/src/lib/RuntimePrint.hs b/src/lib/RuntimePrint.hs
index d1b17c792..3255773ad 100644
--- a/src/lib/RuntimePrint.hs
+++ b/src/lib/RuntimePrint.hs
@@ -169,8 +169,9 @@ withBuffer cont = do
       body <- buildBlock do
         cont $ sink $ Var $ binderVar b
         return UnitVal
-      let piBinders = BinaryNest (WithExpl (Inferred Nothing Unify) h) (WithExpl Explicit b)
-      let piTy = CorePiType ExplicitApp piBinders $ EffTy eff UnitTy
+      let binders = BinaryNest h b
+      let expls = [Inferred Nothing Unify, Explicit]
+      let piTy = CorePiType ExplicitApp expls binders $ EffTy eff UnitTy
       let lam = LamExpr (BinaryNest h b) body
       return $ Lam $ CoreLamExpr piTy lam
   applyPreludeFunction "with_stack_internal" [lam]
diff --git a/src/lib/Simplify.hs b/src/lib/Simplify.hs
index 2e820ee71..c151937b6 100644
--- a/src/lib/Simplify.hs
+++ b/src/lib/Simplify.hs
@@ -618,8 +618,8 @@ simplifyDictMethod absDict@(Abs bs dict) method = do
 ixMethodType :: IxMethod -> AbsDict n -> EnvReaderM n (PiType CoreIR n)
 ixMethodType method absDict = do
   refreshAbs absDict \extraArgBs dict -> do
-    CorePiType _ methodArgs (EffTy _ resultTy) <- getMethodType dict (fromEnum method)
-    let allBs = extraArgBs >>> fmapNest withoutExpl methodArgs
+    CorePiType _ _ methodArgs (EffTy _ resultTy) <- getMethodType dict (fromEnum method)
+    let allBs = extraArgBs >>> methodArgs
     return $ PiType allBs (EffTy Pure resultTy)
 
 -- TODO: do we even need this, or is it just a glorified `SubstM`?
@@ -788,7 +788,7 @@ applyDictMethod resultTy d i methodArgs = do
   cheapNormalize d >>= \case
     DictCon _ (InstanceDict instanceName instanceArgs) -> dropSubst do
       instanceArgs' <- mapM simplifyAtom instanceArgs
-      InstanceDef _ bsInstance _ body <- lookupInstanceDef instanceName
+      InstanceDef _ _ bsInstance _ body <- lookupInstanceDef instanceName
       let InstanceBody _ methods = body
       let method = methods !! i
       extendSubst (bsInstance @@> (SubstVal <$> instanceArgs')) do
@@ -921,7 +921,7 @@ preludeNothingVal ty = do
 preludeMaybeNewtypeCon :: EnvReader m => CType n -> m n (NewtypeCon n)
 preludeMaybeNewtypeCon ty = do
   ~(Just (UTyConVar tyConName)) <- lookupSourceMap "Maybe"
-  TyConDef sn _ _ <- lookupTyCon tyConName
+  TyConDef sn _ _ _ <- lookupTyCon tyConName
   let params = TyConParams [Explicit] [Type ty]
   return $ UserADTData sn tyConName params
 
@@ -997,7 +997,7 @@ simplifyCustomLinearization (Abs runtimeBs staticArgs) actives rule = do
           -- a custom linearization defined for a function on ADTs will
           -- not work.
           fLin' <- sinkM fLin
-          Pi (CorePiType _ bs _) <- return $ getType fLin'
+          Pi (CorePiType _ _ bs _) <- return $ getType fLin'
           let tangentCoreTys = fromNonDepNest bs
           tangentArgs' <- zipWithM liftSimpAtom tangentCoreTys tangentArgs
           resultTyTangent <- typeOfApp (getType fLin') tangentArgs'
diff --git a/src/lib/SourceRename.hs b/src/lib/SourceRename.hs
index 45fafc01e..3ee3b13b1 100644
--- a/src/lib/SourceRename.hs
+++ b/src/lib/SourceRename.hs
@@ -180,9 +180,9 @@ instance SourceRenamableE UExpr' where
     UVar v -> UVar <$> sourceRenameE v
     ULit l -> return $ ULit l
     ULam lam -> ULam <$> sourceRenameE lam
-    UPi (UPiExpr pats appExpl eff body) ->
+    UPi (UPiExpr (attrs, pats) appExpl eff body) ->
       sourceRenameB pats \pats' ->
-        UPi <$> (UPiExpr pats' <$> pure appExpl <*> sourceRenameE eff <*> sourceRenameE body)
+        UPi <$> (UPiExpr (attrs, pats') <$> pure appExpl <*> sourceRenameE eff <*> sourceRenameE body)
     UApp f xs ys -> UApp <$> sourceRenameE f
        <*> forM xs sourceRenameE
        <*> forM ys (\(name, y) -> (name,) <$> sourceRenameE y)
@@ -245,20 +245,20 @@ instance SourceRenamableB UTopDecl where
       sourceRenameUBinder UPunVar tyConName \tyConName' -> do
         structDef' <- sourceRenameE structDef
         cont $ UStructDecl tyConName' structDef'
-    UInterface paramBs methodTys className methodNames -> do
+    UInterface (attrs, paramBs) methodTys className methodNames -> do
       Abs paramBs' (ListE methodTys') <-
         sourceRenameB paramBs \paramBs' -> do
           methodTys' <- mapM sourceRenameE methodTys
           return $ Abs paramBs' $ ListE methodTys'
       sourceRenameUBinder UClassVar className \className' ->
         sourceRenameUBinderNest UMethodVar methodNames \methodNames' ->
-          cont $ UInterface paramBs' methodTys' className' methodNames'
-    UInstance className conditions params methodDefs instanceName expl -> do
+          cont $ UInterface (attrs, paramBs') methodTys' className' methodNames'
+    UInstance className (roleExpls, conditions) params methodDefs instanceName expl -> do
       className' <- sourceRenameE className
       Abs conditions' (PairE (ListE params') (ListE methodDefs')) <-
         sourceRenameE $ Abs conditions (PairE (ListE params) $ ListE methodDefs)
       sourceRenameB instanceName \instanceName' ->
-        cont $ UInstance className' conditions' params' methodDefs' instanceName' expl
+        cont $ UInstance className' (roleExpls, conditions') params' methodDefs' instanceName' expl
     UEffectDecl opTypes effName opNames -> do
       opTypes' <- mapM (\(UEffectOpType p ty) -> (UEffectOpType p) <$> sourceRenameE ty) opTypes
       sourceRenameUBinder UEffectVar effName \effName' ->
@@ -277,8 +277,8 @@ instance SourceRenamableB UDecl' where
     UPass -> cont UPass
 
 instance SourceRenamableE ULamExpr where
-  sourceRenameE (ULamExpr args expl effs resultTy body) =
-    sourceRenameB args \args' -> ULamExpr args'
+  sourceRenameE (ULamExpr (expls, args) expl effs resultTy body) =
+    sourceRenameB args \args' -> ULamExpr (expls, args')
       <$> pure expl
       <*> mapM sourceRenameE effs
       <*> mapM sourceRenameE resultTy
@@ -304,9 +304,6 @@ instance (SourceRenamableB b1, SourceRenamableB b2) => SourceRenamableB (PairB b
       sourceRenameB b2 \b2' ->
         cont $ PairB b1' b2'
 
-instance SourceRenamableB b => SourceRenamableB (WithExpl b) where
-  sourceRenameB (WithExpl x b) cont = sourceRenameB b \b' -> cont $ WithExpl x b'
-
 sourceRenameUBinderNest
   :: (Color c, Renamer m, Distinct o)
   => (forall l. Name c l -> UVar l)
@@ -339,15 +336,15 @@ sourceRenameUBinder asUVar ubinder cont = case ubinder of
   UIgnore -> cont UIgnore
 
 instance SourceRenamableE UDataDef where
-  sourceRenameE (UDataDef tyConName paramBs dataCons) = do
+  sourceRenameE (UDataDef tyConName (expls, paramBs) dataCons) = do
     sourceRenameB paramBs \paramBs' -> do
       dataCons' <- forM dataCons \(dataConName, argBs) -> do
         argBs' <- sourceRenameE argBs
         return (dataConName, argBs')
-      return $ UDataDef tyConName paramBs' dataCons'
+      return $ UDataDef tyConName (expls, paramBs') dataCons'
 
 instance SourceRenamableE UStructDef where
-  sourceRenameE (UStructDef tyConName paramBs fields methods) = do
+  sourceRenameE (UStructDef tyConName (expls, paramBs) fields methods) = do
     sourceRenameB paramBs \paramBs' -> do
       fields' <- forM fields \(fieldName, ty) -> do
         ty' <- sourceRenameE ty
@@ -355,7 +352,7 @@ instance SourceRenamableE UStructDef where
       methods' <- forM methods \(ann, methodName, lam) -> do
         lam' <- sourceRenameE lam
         return (ann, methodName, lam')
-      return $ UStructDef tyConName paramBs' fields' methods'
+      return $ UStructDef tyConName (expls, paramBs') fields' methods'
 
 instance SourceRenamableE UDataDefTrail where
   sourceRenameE (UDataDefTrail args) = sourceRenameB args \args' ->
diff --git a/src/lib/Subst.hs b/src/lib/Subst.hs
index 5e29db46a..5b13ef624 100644
--- a/src/lib/Subst.hs
+++ b/src/lib/Subst.hs
@@ -18,7 +18,6 @@ import Control.Monad.State.Strict
 import Name
 import IRVariants
 import Types.Core
-import Types.Primitives
 import Core
 import qualified RawName as R
 import Err
@@ -444,20 +443,16 @@ instance (BindsNames b, SubstB v b, SinkableV v)
 instance FromName v => SubstE v UnitE where
   substE _ UnitE = UnitE
 
+instance SubstB v b => SubstB v (WithAttrB a b) where
+  substB env (WithAttrB x b) cont =
+    substB env b \env' b' -> cont env' $ WithAttrB x b'
+
 instance (Traversable f, SubstE v e) => SubstE v (ComposeE f e) where
   substE env (ComposeE xs) = ComposeE $ fmap (substE env) xs
 
 instance (SubstE v e1, SubstE v e2) => SubstE v (PairE e1 e2) where
   substE env (PairE x y) = PairE (substE env x) (substE env y)
 
-instance SubstB v b => SubstB v (WithExpl b) where
-  substB env (WithExpl x b) cont =
-    substB env b \env' b' -> cont env' $ WithExpl x b'
-
-instance (FromName v, SubstB v CBinder) => SubstB v RolePiBinder where
-  substB env (RolePiBinder role b) cont =
-    substB env b \env' b' -> cont env' $ RolePiBinder role b'
-
 instance (SubstE v e1, SubstE v e2) => SubstE v (EitherE e1 e2) where
   substE env (LeftE  x) = LeftE  $ substE env x
   substE env (RightE x) = RightE $ substE env x
diff --git a/src/lib/TopLevel.hs b/src/lib/TopLevel.hs
index 9b08665ec..fdcafcc51 100644
--- a/src/lib/TopLevel.hs
+++ b/src/lib/TopLevel.hs
@@ -937,8 +937,8 @@ instance Generic TopStateEx where
 
 getLinearizationType :: SymbolicZeros -> CType n -> EnvReaderT Except n (Int, Int, CType n)
 getLinearizationType zeros = \case
-  Pi (CorePiType ExplicitApp bs (EffTy Pure resultTy)) -> do
-    (numIs, numEs) <- getNumImplicits $ fst $ unzipExpls bs
+  Pi (CorePiType ExplicitApp expls bs (EffTy Pure resultTy)) -> do
+    (numIs, numEs) <- getNumImplicits expls
     refreshAbs (Abs bs resultTy) \bs' resultTy' -> do
       PairB _ bsE <- return $ splitNestAt numIs bs'
       let explicitArgTys = nestToList (\b -> sink $ binderType b) bsE
@@ -951,7 +951,7 @@ getLinearizationType zeros = \case
         Just rtt -> return rtt
         Nothing  -> throw TypeErr $ "No tangent type for: " ++ pprint resultTy'
       let tanFunTy = Pi $ nonDepPiType argTanTys Pure resultTanTy
-      let fullTy = CorePiType ExplicitApp bs' $ EffTy Pure (PairTy resultTy' tanFunTy)
+      let fullTy = CorePiType ExplicitApp expls bs' $ EffTy Pure (PairTy resultTy' tanFunTy)
       return (numIs, numEs, Pi fullTy)
   _ -> throw TypeErr $ "Can't define a custom linearization for implicit or impure functions"
   where
diff --git a/src/lib/Types/Core.hs b/src/lib/Types/Core.hs
index 9f22018b8..9e9062d3f 100644
--- a/src/lib/Types/Core.hs
+++ b/src/lib/Types/Core.hs
@@ -151,7 +151,8 @@ data TyConDef n where
   -- binder name is in UExpr and Env
   TyConDef
     :: SourceName
-    -> RolePiBinders n l
+    -> [RoleExpl]
+    -> Nest CBinder n l
     ->   DataConDefs l
     -> TyConDef n
 
@@ -213,10 +214,8 @@ data TabPiType (r::IR) (n::S) where
 data PiType (r::IR) (n::S) where
   PiType :: Nest (Binder r) n l -> EffTy r l -> PiType r n
 
-type CoreBinders = Nest (WithExpl CBinder)
-
 data CorePiType (n::S) where
-  CorePiType :: AppExplicitness -> CoreBinders n l -> EffTy CoreIR l -> CorePiType n
+  CorePiType :: AppExplicitness -> [Explicitness] -> Nest CBinder n l -> EffTy CoreIR l -> CorePiType n
 
 data DepPairType (r::IR) (n::S) where
   DepPairType :: DepPairExplicitness -> Binder r n l -> Type r l -> DepPairType r n
@@ -443,16 +442,15 @@ isSumCon = \case
 
 -- === type classes ===
 
-data RolePiBinder (n::S) (l::S) = RolePiBinder ParamRole (WithExpl CBinder n l)
-     deriving (Show, Generic)
-type RolePiBinders = Nest RolePiBinder
+type RoleExpl = (ParamRole, Explicitness)
 
 data ClassDef (n::S) where
   ClassDef
     :: SourceName            -- name of class
     -> [SourceName]          -- method source names
     -> [Maybe SourceName]    -- parameter source names
-    -> RolePiBinders n1 n2   -- parameters
+    -> [RoleExpl]            -- parameter info
+    -> Nest CBinder n1 n2   -- parameters
     ->   Nest CBinder n2 n3  -- superclasses
     ->   [CorePiType n3]     -- method types
     -> ClassDef n1
@@ -460,7 +458,8 @@ data ClassDef (n::S) where
 data InstanceDef (n::S) where
   InstanceDef
     :: ClassName n1
-    -> RolePiBinders n1 n2   -- parameters (types and dictionaries)
+    -> [RoleExpl]           -- parameter info
+    -> Nest CBinder n1 n2   -- parameters (types and dictionaries)
     ->   [CAtom n2]          -- class parameters
     ->   InstanceBody n2
     -> InstanceDef n1
@@ -921,10 +920,6 @@ instance IRRep r => BindsOneAtomName r (BinderP (AtomNameC r) (Type r)) where
   binderType (_ :> ty) = ty
   binderVar (b:>t) = AtomVar (binderName b) (sink t)
 
-instance BindsOneAtomName CoreIR b => BindsOneAtomName CoreIR (WithExpl b) where
-  binderType (WithExpl _ b) = binderType b
-  binderVar  (WithExpl _ b) = binderVar b
-
 toBinderNest :: BindsOneAtomName r b => Nest b n l -> Nest (Binder r) n l
 toBinderNest Empty = Empty
 toBinderNest (Nest b bs) = Nest (asNameBinder b :> binderType b) (toBinderNest bs)
@@ -1183,10 +1178,10 @@ instance AlphaEqE       DataConDefs
 instance AlphaHashableE DataConDefs
 
 instance GenericE TyConDef where
-  type RepE TyConDef = PairE (LiftE SourceName) (Abs RolePiBinders DataConDefs)
-  fromE (TyConDef sourceName bs cons) = PairE (LiftE sourceName) (Abs bs cons)
+  type RepE TyConDef = PairE (LiftE (SourceName, [RoleExpl])) (Abs (Nest CBinder) DataConDefs)
+  fromE (TyConDef sourceName expls bs cons) = PairE (LiftE (sourceName, expls)) (Abs bs cons)
   {-# INLINE fromE #-}
-  toE   (PairE (LiftE sourceName) (Abs bs cons)) = TyConDef sourceName bs cons
+  toE   (PairE (LiftE (sourceName, expls)) (Abs bs cons)) = TyConDef sourceName expls bs cons
   {-# INLINE toE #-}
 
 deriving instance Show (TyConDef n)
@@ -1198,7 +1193,7 @@ instance AlphaEqE TyConDef
 instance AlphaHashableE TyConDef
 
 instance HasNameHint (TyConDef n) where
-  getNameHint (TyConDef v _ _) = getNameHint v
+  getNameHint (TyConDef v _ _ _) = getNameHint v
 
 instance GenericE DataConDef where
   type RepE DataConDef = (LiftE (SourceName, [[Projection]]))
@@ -1834,39 +1829,15 @@ instance (IRRep r, AlphaEqE       ann) => AlphaEqB       (NonDepNest r ann)
 instance (IRRep r, AlphaHashableE ann) => AlphaHashableB (NonDepNest r ann)
 deriving instance (Show (ann n)) => IRRep r => Show (NonDepNest r ann n l)
 
-instance GenericB RolePiBinder where
-  type RepB RolePiBinder = PairB (LiftB (LiftE ParamRole)) (WithExpl CBinder)
-  fromB (RolePiBinder role b) = PairB (LiftB (LiftE role)) b
-  toB   (PairB (LiftB (LiftE role)) b) = RolePiBinder role b
-
-instance BindsAtMostOneName RolePiBinder (AtomNameC CoreIR) where
-  RolePiBinder _ b @> x = b @> x
-  {-# INLINE (@>) #-}
-
-instance BindsOneName RolePiBinder (AtomNameC CoreIR) where
-  binderName (RolePiBinder _ b) = binderName b
-
-instance BindsOneAtomName CoreIR RolePiBinder where
-  binderType (RolePiBinder _ b) = binderType b
-  binderVar  (RolePiBinder _ b) = binderVar  b
-
-instance ProvesExt   RolePiBinder
-instance BindsNames  RolePiBinder
-instance SinkableB   RolePiBinder
-instance HoistableB  RolePiBinder
-instance RenameB     RolePiBinder
-instance AlphaEqB RolePiBinder
-instance AlphaHashableB RolePiBinder
-
 instance GenericE ClassDef where
   type RepE ClassDef =
-    LiftE (SourceName, [SourceName], [Maybe SourceName])
-     `PairE` Abs RolePiBinders (Abs (Nest CBinder) (ListE CorePiType))
-  fromE (ClassDef name names paramNames b scs tys) =
-    LiftE (name, names, paramNames) `PairE` Abs b (Abs scs (ListE tys))
+    LiftE (SourceName, [SourceName], [Maybe SourceName], [RoleExpl])
+     `PairE` Abs (Nest CBinder) (Abs (Nest CBinder) (ListE CorePiType))
+  fromE (ClassDef name names paramNames roleExpls b scs tys) =
+    LiftE (name, names, paramNames, roleExpls) `PairE` Abs b (Abs scs (ListE tys))
   {-# INLINE fromE #-}
-  toE (LiftE (name, names, paramNames) `PairE` Abs b (Abs scs (ListE tys))) =
-    ClassDef name names paramNames b scs tys
+  toE (LiftE (name, names, paramNames, roleExpls) `PairE` Abs b (Abs scs (ListE tys))) =
+    ClassDef name names paramNames roleExpls b scs tys
   {-# INLINE toE #-}
 
 instance SinkableE ClassDef
@@ -1879,11 +1850,11 @@ deriving via WrapE ClassDef n instance Generic (ClassDef n)
 
 instance GenericE InstanceDef where
   type RepE InstanceDef =
-    ClassName `PairE` Abs RolePiBinders (ListE CAtom `PairE` InstanceBody)
-  fromE (InstanceDef name bs params body) =
-    name `PairE` Abs bs (ListE params `PairE` body)
-  toE (name `PairE` Abs bs (ListE params `PairE` body)) =
-    InstanceDef name bs params body
+    ClassName `PairE` LiftE [RoleExpl] `PairE` Abs (Nest CBinder) (ListE CAtom `PairE` InstanceBody)
+  fromE (InstanceDef name expls bs params body) =
+    name `PairE` LiftE expls `PairE` Abs bs (ListE params `PairE` body)
+  toE (name `PairE` LiftE expls `PairE` Abs bs (ListE params `PairE` body)) =
+    InstanceDef name expls bs params body
 
 instance SinkableE InstanceDef
 instance HoistableE  InstanceDef
@@ -2015,10 +1986,10 @@ deriving instance Show (CoreLamExpr n)
 deriving via WrapE CoreLamExpr n instance Generic (CoreLamExpr n)
 
 instance GenericE CorePiType where
-  type RepE CorePiType = LiftE AppExplicitness `PairE` Abs CoreBinders (EffTy CoreIR)
-  fromE (CorePiType ex b effTy) = LiftE ex `PairE` Abs b effTy
+  type RepE CorePiType = LiftE (AppExplicitness, [Explicitness]) `PairE` Abs (Nest CBinder) (EffTy CoreIR)
+  fromE (CorePiType ex exs b effTy) = LiftE (ex, exs) `PairE` Abs b effTy
   {-# INLINE fromE #-}
-  toE   (LiftE ex `PairE` Abs b effTy) = CorePiType ex b effTy
+  toE   (LiftE (ex, exs) `PairE` Abs b effTy) = CorePiType ex exs b effTy
   {-# INLINE toE #-}
 
 instance SinkableE      CorePiType
@@ -2766,7 +2737,6 @@ instance Store (DictType n)
 instance Store (DictExpr n)
 instance Store (EffectDef n)
 instance Store (EffectOpDef n)
-instance Store (RolePiBinder n l)
 instance Store (EffectOpType n)
 instance Store (EffectOpIdx)
 instance Store (SynthCandidates n)
diff --git a/src/lib/Types/Primitives.hs b/src/lib/Types/Primitives.hs
index a9230a3ed..002a6d09a 100644
--- a/src/lib/Types/Primitives.hs
+++ b/src/lib/Types/Primitives.hs
@@ -22,9 +22,7 @@ module Types.Primitives (
   module Types.Primitives, UnOp (..), BinOp (..),
   CmpOp (..), Projection (..)) where
 
-import Name
 import qualified Data.ByteString       as BS
-import Control.Monad
 import Data.Int
 import Data.Word
 import Data.Hashable
@@ -35,7 +33,6 @@ import Foreign.Ptr
 import GHC.Generics (Generic (..))
 
 import Occurrence
-import Util (zipErr)
 import Types.OpNames (UnOp (..), BinOp (..), CmpOp (..), Projection (..))
 
 type SourceName = String
@@ -58,23 +55,6 @@ data Explicitness =
 data AppExplicitness = ExplicitApp | ImplicitApp  deriving (Show, Generic, Eq)
 data DepPairExplicitness = ExplicitDepPair | ImplicitDepPair  deriving (Show, Generic, Eq)
 
-data WithExpl (b::B) (n::S) (l::S) =
-  WithExpl { getExpl :: Explicitness , withoutExpl :: b n l }
-  deriving (Show, Generic)
-
-unzipExpls :: Nest (WithExpl b) n l -> ([Explicitness], Nest b n l)
-unzipExpls Empty = ([], Empty)
-unzipExpls (Nest (WithExpl expl b) rest) = (expl:expls, Nest b bs)
-  where (expls, bs) = unzipExpls rest
-
-zipExpls :: [Explicitness] -> Nest b n l -> Nest (WithExpl b) n l
-zipExpls [] Empty = Empty
-zipExpls (expl:expls) (Nest b bs) = Nest (WithExpl expl b) (zipExpls expls bs)
-zipExpls _ _ = error "zip error"
-
-addExpls :: Explicitness -> Nest b n l -> Nest (WithExpl b) n l
-addExpls expl bs = fmapNest (\b -> WithExpl expl b) bs
-
 data RequiredMethodAccess = Full | Partial Int deriving (Show, Eq, Ord, Generic)
 
 data LetAnn =
@@ -225,40 +205,3 @@ instance Hashable AppExplicitness
 instance Hashable DepPairExplicitness
 instance Hashable InferenceMechanism
 instance Hashable RequiredMethodAccess
-
-instance Store (b n l) => Store (WithExpl b n l)
-
-instance (Color c, BindsOneName b c) => BindsOneName (WithExpl b) c where
-  binderName (WithExpl _ b) = binderName b
-  asNameBinder (WithExpl _ b) = asNameBinder b
-
-instance (Color c, BindsAtMostOneName b c) => BindsAtMostOneName (WithExpl b) c where
-  WithExpl _ b @> x = b @> x
-  {-# INLINE (@>) #-}
-
-instance AlphaEqB b => AlphaEqB (WithExpl b) where
-  withAlphaEqB (WithExpl a1 b1) (WithExpl a2 b2) cont = do
-    unless (a1 == a2) zipErr
-    withAlphaEqB b1 b2 cont
-
-instance AlphaHashableB b => AlphaHashableB (WithExpl b) where
-  hashWithSaltB env salt (WithExpl expl b) = do
-    let h = hashWithSalt salt expl
-    hashWithSaltB env h b
-
-instance BindsNames b => ProvesExt  (WithExpl b) where
-instance BindsNames b => BindsNames (WithExpl b) where
-  toScopeFrag (WithExpl _ b) = toScopeFrag b
-
-instance (SinkableB b) => SinkableB (WithExpl b) where
-  sinkingProofB fresh (WithExpl a b) cont =
-    sinkingProofB fresh b \fresh' b' ->
-      cont fresh' (WithExpl a b')
-
-instance (BindsNames b, RenameB b) => RenameB (WithExpl b) where
-  renameB env (WithExpl a b) cont =
-      renameB env b \env' b' ->
-        cont env' $ WithExpl a b'
-
-instance HoistableB b => HoistableB (WithExpl b) where
-  freeVarsB (WithExpl _ b) = freeVarsB b
diff --git a/src/lib/Types/Source.hs b/src/lib/Types/Source.hs
index a27b02268..0c361236d 100644
--- a/src/lib/Types/Source.hs
+++ b/src/lib/Types/Source.hs
@@ -274,9 +274,12 @@ data FieldName' =
  | FieldNum  Int
   deriving (Show, Eq, Ord)
 
+type UAnnExplBinders req n l = ([Explicitness], Nest (UAnnBinder req) n l)
+type UOptAnnExplBinders n l = UAnnExplBinders AnnOptional n l
+
 data ULamExpr (n::S) where
   ULamExpr
-    :: Nest (WithExpl UOptAnnBinder) n l  -- args
+    :: UOptAnnExplBinders n l  -- args
     -> AppExplicitness
     -> Maybe (UEffectRow l)               -- optional effect
     -> Maybe (UType l)                    -- optional result type
@@ -284,7 +287,7 @@ data ULamExpr (n::S) where
     -> ULamExpr n
 
 data UPiExpr (n::S) where
-  UPiExpr :: Nest (WithExpl UOptAnnBinder) n l -> AppExplicitness -> UEffectRow l -> UType l -> UPiExpr n
+  UPiExpr :: UOptAnnExplBinders n l -> AppExplicitness -> UEffectRow l -> UType l -> UPiExpr n
 
 data UTabPiExpr (n::S) where
   UTabPiExpr :: UOptAnnBinder n l -> UType l -> UTabPiExpr n
@@ -297,14 +300,14 @@ type UConDef (n::S) (l::S) = (SourceName, Nest UReqAnnBinder n l)
 data UDataDef (n::S) where
   UDataDef
     :: SourceName  -- source name for pretty printing
-    -> Nest (WithExpl UOptAnnBinder) n l
+    -> UOptAnnExplBinders n l
     -> [(SourceName, UDataDefTrail l)] -- data constructor types
     -> UDataDef n
 
 data UStructDef (n::S) where
   UStructDef
     :: SourceName    -- source name for pretty printing
-    -> Nest (WithExpl UOptAnnBinder) n l
+    -> UOptAnnExplBinders n l
     -> [(SourceName, UType l)]                    -- named payloads
     -> [(LetAnn, SourceName, Abs UAtomBinder ULamExpr l)] -- named methods (initial binder is for `self`)
     -> UStructDef n
@@ -324,14 +327,14 @@ data UTopDecl (n::S) (l::S) where
     -> UStructDef l                        -- actual definition
     -> UTopDecl n l
   UInterface
-    :: Nest (WithExpl UOptAnnBinder) n p   -- parameter binders
+    :: UOptAnnExplBinders n p   -- parameter binders
     ->   [UType p]                         -- method types
     -> UBinder ClassNameC n l'             -- class name
     ->   Nest (UBinder MethodNameC) l' l   -- method names
     -> UTopDecl n l
   UInstance
     :: SourceNameOr (Name ClassNameC) n  -- class name
-    -> Nest (WithExpl UOptAnnBinder) n l'
+    -> UOptAnnExplBinders n l'
     ->   [UExpr l']                      -- class parameters
     ->   [UMethodDef l']                 -- method definitions
     -- Maybe we should make a separate color (namespace) for instance names?
@@ -346,7 +349,7 @@ data UTopDecl (n::S) (l::S) where
   UHandlerDecl
     :: SourceNameOr (Name EffectNameC) n  -- effect name
     -> UAtomBinder n b                    -- body type argument
-    -> Nest (WithExpl UOptAnnBinder) b l' -- type args
+    -> UOptAnnExplBinders b l'            -- type args
     ->   UEffectRow l'                    -- returning effect
     ->   UType l'                         -- returning type
     ->   [UEffectOpDef l']                -- operation definitions