[Agda] Does Agda2 have fast arrays?

[Don Stewart]

andreas.abel:
>>>
>>> Meanwhile, 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?
>>>
>>
>> The best way would be to generate the core for this (e.g. after the
>> "FillInCaseDefault" pass.
>>
>>    %module main:A
>>      main:A.trustFromJust :: %forall t . (base:DataziMaybe.Maybe t) -> 
>> t =
>>        \ @ t (x::(base:DataziMaybe.Maybe t)) ->
>>            %case t x %of
>>               base:DataziMaybe.Just (y::t) -> y};
>
> I think what Conor meant is that the the y is projected out directly,  
> without a case statement verifying that the tag "Just" is present.
>
> Is this compiled like Conor would expect?
>
>> But GHC doesn't accept .hcr input at the moment.
>>
>> Another way might be to use unpackClosure# (e.g. like the vacuum  
>> library does , to render the heap).
>>
>> Yet another would be to write a  -fdisable-fill-in-case-default that  
>> turns off that bit of code.
>

Ah, that's a different situation. You want to ignore the tag and jump
straight to the field of the closure. That could be done manually via
the unpackClosure# hacking, but really needs modifying the code
generator, or writing one...

-- Don