WIP

src/lib/Inference.hs

@@ -414,12 +414,23 @@ data RequiredTy (e::E) (n::S) =
 checkSigma :: Emits o
            => NameHint -> UExpr i -> CType o -> InfererM i o (CAtom o)
 checkSigma hint expr sTy = confuseGHC >>= \_ -> case sTy of
-  Pi piTy@(CorePiType _ expls _ _) ->
+  Pi piTy@(CorePiType _ expls piBs resultEffTy) ->
     if all (== Explicit) expls
       then fallback
       else case expr of
         WithSrcE src (ULam lam) -> addSrcContext src $ Lam <$> checkULam lam piTy
-        _ -> undefined
+        _ -> withFreshBindersInf expls (EmptyAbs piBs) \bs -> do
+          let vs = bindersVars bs
+          let args = zip expls (Var <$> vs)
+          EffTy effs' resultTy' <- applyRename (piBs@@>(atomVarName <$> vs)) resultEffTy
+          explicits <- return $ catMaybes $ args <&> \case
+            (Explicit, arg) -> Just arg
+            _ -> Nothing
+          withAllowedEffects effs' do
+            body <- buildBlockInf do
+              expr' <- inferWithoutInstantiation expr >>= zonk
+              dropSubst $ checkOrInferApp expr' (sink <$> explicits) [] (Check $ sink resultTy')
+            return $ Lam $ CoreLamExpr piTy $ LamExpr bs body
   DepPairTy depPairTy -> case depPairTy of
     DepPairType ImplicitDepPair (_ :> lhsTy) _ -> do
       -- TODO: check for the case that we're given some of the implicit dependent pair args explicitly
@@ -1280,9 +1291,9 @@ withUBinders :: Nest UAnnBinder i i' -> InfererCPSB2 (Nest (WithExpl CBinder)) i
 withUBinders bs cont = do
   Abs bs' UnitE <- inferUBinders bs \_ -> return UnitE
   let (expls, bs'') = unzipAttrs bs'
-  withFreshBindersInf expls (EmptyAbs bs'') \bs'' -> do
-    extendSubst (bs@@> (atomVarName <$> bindersVars bs'')) $
-      cont $ zipAttrs expls bs''
+  withFreshBindersInf expls (EmptyAbs bs'') \bs''' -> do
+    extendSubst (bs@@> (atomVarName <$> bindersVars bs''')) $
+      cont $ zipAttrs expls bs'''
 
 inferUBinders
   :: Zonkable e => Nest UAnnBinder i i'
@@ -1634,11 +1645,14 @@ inferTabCon hint xs reqTy = do
         dataDict <- trySynthTerm dTy Full
         liftM Var $ emitHinted hint $ TabCon (Just $ WhenIRE dataDict) tabTy xs'
 
-addEffects :: Emits o => EffectRow CoreIR o -> InfererM i o ()
+addEffects :: EffectRow CoreIR o -> InfererM i o ()
+addEffects Pure = return ()
 addEffects eff = do
+  effsAllowed <- (infEffects <$> getInfState) >>= zonk
   eff' <- zonk eff
-  effAllowed <- (infEffects <$> getInfState) >>= zonk
-  checkExtends effAllowed eff'
+  case checkExtends effsAllowed eff' of
+    Success () -> return ()
+    Failure _  -> constrainEq (Eff effsAllowed) (Eff eff')
 
 getIxDict :: CType o -> InfererM i o (IxDict CoreIR o)
 getIxDict t = do