The Maybe hack is incorrect

[ziman]

The Maybe hack means that Just x compiles to x and Nothing compiles to None. If there's a value v that compiles to None, such as Nothing, then Just v is indistinguishable from Nothing.

12:35 CET < Melvar> > :let foo : Maybe (Maybe a) -> Int; foo Nothing = 0; foo (Just Nothing) = 1; foo (Just (Just _)) = 2
12:35 CET < idris-bot> defined
12:36 CET < Melvar> ↑ Will or will not that function, compiled with idris-py, return 0 if given (Just Nothing)?
12:36 CET < ziman> yeah, it probably will
12:38 CET < ziman> I probably shouldn't abuse Maybe for that