Brian W Bush

Unary operators

2

Running `agda2hs` on code like ```agda +++_ : Nat → Nat +++_ x = 2 * x {-# COMPILE AGDA2HS +++_ #-} usage : Nat usage = +++ 5 ```...

If an Agda module only contains typeclass instances (i.e., orphans), then `agda2hs` code in other modules do not have an `import` statement generated for the module with the instances. Here...

Postulates are not exported

1

If a type is postulated, but aliased via the `COMPILE` pragma, it is not exported for other modules to use. In the example below, `ByteString` is not accessible from Haskell...

`agda2hs` fails unless `agda` or `agda2hs` is run first

2

The first execution of `agda2hs` fails for [this code](https://github.com/input-output-hk/peras-design/tree/56a57bb1475b60c76904909ead532cc0967a84de/src): ```console $ find -type f -name \*.agdai -delete $ agda2hs --local-interfaces --library-file=$AGDA_LIBS --compile-dir=peras-hs/src src/Peras/QCD/Node/Specification.agda agda2hs --local-interfaces --library-file=$AGDA_LIBS --compile-dir=peras-hs/src src/Peras/QCD/Node/Specification.agda Checking Peras.QCD.Node.Specification...

Code like ```agda instance iMaybeHashable : ⦃ i : Hashable a ⦄ → Hashable (Maybe a) iMaybeHashable {{_}} .hash Nothing = MakeHash ∘ hashBytes $ hash iUnitHashable tt iMaybeHashable {{i}}...

Definition of `Functor` is inconsistent with `base-4.18.1.0` etc.

1

The `agda2hs` prelude puts `void` as a member of the typeclass, but the latest GHC base libraries do not. Compare `void` in https://github.com/agda/agda2hs/blob/7b3e48a35448acff9bb5823ca22623eafb000d15/lib/Haskell/Prim/Functor.agda#L15-L24 and to it's top-level placement in https://github.com/ghc/ghc/blob/f3225ed4b3f3c4309f9342c5e40643eeb0cc45da/libraries/base/Data/Functor.hs#L210-L211...

Newtype constructor erroneously removed

2

Agda ```agda record Hash (a : Set) : Set where constructor MakeHash field hashBytes : ByteString open Hash public {-# COMPILE AGDA2HS Hash newtype deriving (Generic, Show) #-} instance iMaybeHashable...

The docker compose file for the Marlowe Starter Kit does not include an image with the `marlowe-oracle` executable. Neither does it expose the ports required to use `marlowe-oracle` externally. See...