On the Agda mailing list, Conor McBride asked:
is there any way to get hold of operations like a putative
trustFromJust :: Maybe x -> x
which doesn't actually check for Just and Goes Wrong (in Milner's sense) if fed Nothing?
Agda might prove Maybe a == Just1 a, and the intermediate constructor for the sum type could be eliminated.
I can think of approaches using unsafeCoerce# or unpackClosure#, but does anyone else have thoughts?
import GHC.Prim
trustFromJust :: Maybe x -> x
trustFromJust x = y
where Just1 y = unsafeCoerce# x
data Just1 a = Just1 a
though this segfaults (single constructor types can avoid some of the closure overhead). The core looks ok though:
main2 =
case (Data.Maybe.Just @ Type.Integer main3)
`cast`
(CoUnsafe
(Data.Maybe.Maybe Type.Integer)
(Just1 Type.Integer)
:: Data.Maybe.Maybe Type.Integer
~
Just1 Type.Integer)
of _ { Just1 y_aeb ->
$wshowsPrec 0 y_aeb ([] @ Char)