@@ -271,7 +271,14 @@ buildDepMap ci ctx mainName = addPostulates $ dfs S.empty M.empty [mainName]
271271 getDepsSC :: Name -> [Name] -> Vars -> SC -> Deps
272272 getDepsSC fn es vs ImpossibleCase = M.empty
273273 getDepsSC fn es vs (UnmatchedCase msg) = M.empty
274− getDepsSC fn es vs (ProjCase t alt) = error "ProjCase not supported"
274+
275+ -- for the purposes of erasure, we can disregard the projection
276+ getDepsSC fn es vs (ProjCase (Proj t i) alts) = getDepsSC fn es vs (ProjCase t alts) -- step
277+ getDepsSC fn es vs (ProjCase (P _ n _) alts) = getDepsSC fn es vs (Case n alts) -- base
278+
279+ -- other ProjCase's are not supported
280+ getDepsSC fn es vs (ProjCase t alts) = error $ "ProjCase not supported:\n" ++ show (ProjCase t alts)
281+
275282 getDepsSC fn es vs (STerm t) = getDepsTerm vs [] (S.singleton (fn, Result)) (etaExpand es t)
276283 getDepsSC fn es vs (Case n alts)
277284 -- we case-split on this variable, which marks it as used