Handle Inferred terms in getDepsTerm
commit2c906858d4d8a46c8ed272e4ab14a2ed5b3fdb01
authorNiklas Larsson <niklas@mm.st>
dateThu 19 Jul 2018, 21:41 (8 years ago)
parentf16b5c0
src/Idris/Erasure.hs+3
@@ -572,6 +572,9 @@ buildDepMap ci used externs ctx startNames
572572 getDepsTerm vs bs cd (Proj t (-1)) = getDepsTerm vs bs cd t -- naturals, (S n) -> n
573573 getDepsTerm vs bs cd (Proj t i) = error $ "cannot[1] analyse projection !" ++ show i ++ " of " ++ show t
574574
575+ -- inferred term
576+ getDepsTerm vs bs cd (Inferred t) = getDepsTerm vs bs cd t
577+
575578 -- the easy cases
576579 getDepsTerm vs bs cd (Constant _) = M.empty
577580 getDepsTerm vs bs cd (TType _) = M.empty