Unsafe coerce and more efficient Agda code (-ftrust-me-im-agda)

Question

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)

Answer 1

Since this is a research question, we've got a few possible ways forward, but they all come down to:

• Play tricks reversing the tag bits of Maybe