Features

By default, all of the following Agda examples are implicitly prefixed (if necessary) with the following snippet.

open import Haskell.Prelude

Data & Type Declarations

Types

Creating a type synonym using the type keyword requires only a simple declaration in Agda.

Agda:

Entry = Int × List String

{-# COMPILE AGDA2HS Entry #-}

Haskell:

type Entry = (Int, [String])

Datatypes

Standard data type declarations have a simple equivalent in Agda.

Agda:

data Nat : Set where
    Zero : Nat 
    Suc : Nat → Nat

{-# COMPILE AGDA2HS Nat #-}

Haskell:

data Nat = Zero | Suc Nat

You can also use polymorphic types in the data declarations.

Agda:

data Tree (a : Set) : Set where
    Leaf   : a → Tree a
    Branch : a → Tree a → Tree a → Tree a
    
{-# COMPILE AGDA2HS Tree #-}

Haskell:

data Tree a = Leaf a
            | Branch a (Tree a) (Tree a)

UNSUPPORTED: term-indexed datatypes

Records

Data definitions with fields are represented by records on the Agda side.

Agda:

record Citation : Set where
    field
        id     : Int
        author : String
        title  : String
        url    : String
        year   : Int
open Citation public

{-# COMPILE AGDA2HS Citation #-}

Haskell:

data Citation = Citation{id :: Int, author :: String,
                         title :: String, url :: String, year :: Int}

Newtypes

Data declaration using the newtype keyword can be created by adding a newtype annotation to the compile pragma.

Agda:

-- data newtype
data Indexed (a : Set) : Set where
    MkIndexed : Int × a → Indexed a

{-# COMPILE AGDA2HS Indexed newtype #-}

-- data newtype with deriving
data Pair (a b : Set) : Set where
    MkPair : a × b → Pair a b

{-# COMPILE AGDA2HS Pair newtype deriving ( Show, Eq ) #-}

-- record newtype
record Identity (a : Set) : Set where
    constructor MkIdentity
    field
        runIdentity : a
open Identity public

{-# COMPILE AGDA2HS Identity newtype #-}

-- record newtype with erased proof
record Equal (a : Set) : Set where
    constructor MkEqual
    field
        pair : a × a
        @0 proof : (fst pair) ≡ (snd pair)
open Equal public

{-# COMPILE AGDA2HS Equal newtype #-}

Haskell:

-- data newtype
newtype Indexed a = MkIndexed (Int, a)

-- data newtype with deriving
newtype Pair a b = MkPair (a, b)
                     deriving (Show, Eq)

-- record newtype
newtype Identity a = MkIdentity{runIdentity :: a}

-- record newtype with erased proof
newtype Equal a = MkEqual{pair :: (a, a)}

Unfortunately, Agda does not allow the constructor name to be the same as the data/record name. However, it is possible to achieve this with Agda2HS if you do not explicitly add a constructor name to a record definition (this requires the use of record { ... } syntax on the Agda side):

record Duo (a : Set) : Set where
    field
        duo : a × a
open Duo public

{-# COMPILE AGDA2HS Duo newtype #-}

createDuo : a → a → Duo a
createDuo a b = record { duo = a , b }

{-# COMPILE AGDA2HS createDuo #-}

newtype Duo a = Duo{duo :: (a, a)}

createDuo :: a -> a -> Duo a
createDuo a b = Duo (a, b)

Pattern Matching on Datatype Values

Agda:

{-# FOREIGN AGDA2HS {-# LANGUAGE LambdaCase #-} #-}

negate : Bool → Bool
negate True = False
negate False = True

negate' : Bool → Bool
negate' x = case x of λ where
    True → False
    False → True

negate'' : Bool → Bool
negate'' = λ where
    True -> False
    False -> True

{-# LANGUAGE LambdaCase #-}

negate :: Bool -> Bool
negate True = False
negate False = True

negate' :: Bool -> Bool
negate' x = case x of 
    True -> False
    False -> True

negate'' :: Bool -> Bool
negate'' = \case
    True -> False
    False -> True

Flow Control

Agda2HS provides native support for the Haskell if_then_else_ and case_of_ constructs.

Agda:

ifThenElse : Int → String
ifThenElse n = if n >= 10 then "big" else "small"
{-# COMPILE AGDA2HS ifThenElse #-}

mhead : List a → Maybe a
mhead xs = case xs of λ where
  []      → Nothing
  (x ∷ _) → Just x
{-# COMPILE AGDA2HS mhead #-}

Haskell:

ifThenElse :: Int -> String
ifThenElse n = if n >= 10 then "big" else "small"

mhead :: [a] -> Maybe a
mhead xs
  = case xs of
        [] -> Nothing
        x : _ -> Just x

It is NOT possible to partially apply these two constructs. This means that you must explicitly write λ x → if x then 2 else 3 instead of if_then 2 else 3. (This copies the impossibility of the second implementation in Haskell.)

Flow Witnesses

While in Haskell such a thing is never necessary, in Agda there are cases when it is useful for a branch to contain a “witness” (proof) of the condition on which it split (i.e. the true branch of if x < 2 then ... else ... knows that x < 2 = True).

The type signatures of both if_then_else_ and case_of_ on the Agda side contain instances of these proofs which can be used to work with e.g. intrinsic verification.

This allows for the following Agda code to type check:

data Range : Set where
    MkRange : (low high : Int)
            → {{ @0 h : ((low <= high) ≡ True) }}
            → Range

{-# COMPILE AGDA2HS Range #-}

createRange : Int → Int → Maybe Range
createRange low high = if low <= high then Just (MkRange low high) else Nothing

{-# COMPILE AGDA2HS createRange #-}

createRangeCase : Int → Int → Maybe Range
createRangeCase low high = 
    case low <= high of λ where
        True → Just (MkRange low high)
        False → Nothing

{-# COMPILE AGDA2HS createRangeCase #-}

and compile to this simplified Haskell code:

data Range = MkRange Int Int

createRange :: Int -> Int -> Maybe Range
createRange low high
  = if low <= high then Just (MkRange low high) else Nothing

createRangeCase :: Int -> Int -> Maybe Range
createRangeCase low high
  = case low <= high of
        True -> Just (MkRange low high)
        False -> Nothing

Explicit type singatures

Haskell’s :: syntax for explicit type signatures can be achieved using the the function in Haskell.Prim.

Agda:

five : Nat
five = the (Nat -> Nat) id 5
{-# COMPILE AGDA2HS five #-}

Haskell:

five :: Natural
five = (id :: Natural -> Natural) 5

0-Quantity Parameters

Parameters can be annotated with a quantity of either 0 or ω (the default quantity is ω if no quantity is explicitly annotated). Parameters annotated with 0 are irrelevant to evaluation, so they are irrelevant to the compiled Haskell program, and so agda2hs erases them.

Agda:

data GhostInt : Set where
    MakeGhostInt : @0 Int → GhostInt

-- fails
fromGhostInt : GhostInt -> Int
fromGhostInt (MakeGhostInt i) = i

-- passes
addGhostInts : GhostInt -> GhostInt -> GhostInt
addGhostInts (MakeGhostInt i) (MakeGhostInt j) = MakeGhostInt (i + j)

Haskell:

data GhostInt = MakeGhostInt

addGhostInts :: GhostInt -> GhostInt -> GhostInt
addGhostInts MakeGhostInt MakeGhostInt = MakeGhostInt

Coinduction

Agda:

data Stream (a : Set) (@0 i : Size) : Set where
    Nil : Stream a i
    Cons : a → Thunk (Stream a) i → Stream a i
{-# COMPILE AGDA2HS Stream #-}

repeat {a} {i} : a → Stream a i
repeat x = Cons x λ where .force → repeat x
{-# COMPILE AGDA2HS repeat #-}

Haskell:

data Stream a = Nil | Cons a (Stream a)

repeat :: a -> Stream a
repeat x = Cons x (repeat x)

Type Classes

To construct an instance of a type class, you can simply do the following:

Agda:

record Circle : Set where
    constructor MkCircle
    field
        radius : Int
open Circle public

{-# COMPILE AGDA2HS Circle newtype #-}

instance
  iCircleEq : Eq Circle
  iCircleEq ._==_ (MkCircle r1) (MkCircle r2) = r1 == r2

{-# COMPILE AGDA2HS iCircleEq #-}

Haskell:

newtype Circle = MkCircle{radius :: Int}

instance Eq Circle where
    MkCircle r1 == MkCircle r2 = r1 == r2

In some cases (especially when writing proofs), it might be necessary to use the properties (laws) that a type class instance should uphold. In this case, you can also implement the IsLawful instance for the data type and use it’s (erased) properties.

Agda:

record Equal (a : Set) : Set where
    constructor MkEqual
    field
        pair : a × a
        @0 proof : fst pair ≡ snd pair
open Equal public

{-# COMPILE AGDA2HS Equal newtype #-}

constructEqual : ⦃ iEqA : Eq a ⦄ → @0 ⦃ IsLawfulEq a ⦄ → (c : a) → (d : a) → Maybe (Equal a)
constructEqual a b = 
  if a == b then
    (λ ⦃ h ⦄ → Just (MkEqual (a , b) (equality a b h)))
  else Nothing

{-# COMPILE AGDA2HS constructEqual #-}

instance
  iLawfulCircleEq : IsLawfulEq Circle
  iLawfulCircleEq .isEquality (MkCircle r1) (MkCircle r2)
    with r1 == r2 in eq
  ... | True  = ofY (cong MkCircle (equality r1 r2 eq))
  ... | False = ofN λ ceq → (nequality r1 r2 eq) (cong radius ceq)

constructEqualCircle : (c : Circle) → (d : Circle) → Maybe (Equal Circle)
constructEqualCircle c d = constructEqual c d

{-# COMPILE AGDA2HS constructEqualCircle #-}

Haskell:

newtype Equal a = MkEqual{pair :: (a, a)}

constructEqual :: Eq a => a -> a -> Maybe (Equal a)
constructEqual a b
  = if a == b then Just (MkEqual (a, b)) else Nothing

constructEqualCircle :: Circle -> Circle -> Maybe (Equal Circle)
constructEqualCircle c d = constructEqual c d

Constrained Typeclass Instance

Agda:

record Class1 (a : Set) : Set where
    field
        field1 : a
{-# COMPILE AGDA2HS Class1 class #-}

record Class2 (a : Set) : Set where
    field
        field2 : a
{-# COMPILE AGDA2HS Class2 class #-}

class1-implies-class2 (a : Set) : Class1 a → Class2 a
class1-implies-class2 _ class1 = record { field2 = class1.field1 }
{-# COMPILE AGDA2HS class1-implies-class2 #-}

Haskell:

class Class1 a where
    field1 :: a

class Class2 where
    field2 :: a

instance Class1 a => Class2 a where
    field2 = field1

Constrained Typeclass

Agda:

record Class1 (a : Set) : Set where
    field
        field1 : a
{-# COMPILE AGDA2HS Class1 class #-}

record Class2 (a : Set) : Set where
    field
        overlap ⦃ super ⦄ : ClassA b
        field2 : a
{-# COMPILE AGDA2HS Class2 class #-}

Haskell:

class Class1 a where
    field1 :: a 

class Class1 a => Class2 a where
    field2 :: a 

Default Typeclass Field Implementations

Agda:

record Ord (a : Set) : Set where
  field
    _<_ _>_ : a → a → Bool

record Ord₁ (a : Set) : Set where
  field
    _<_ : a → a → Bool

  _>_ : a → a → Bool
  x > y = y < x

record Ord₂ (a : Set) : Set where
  field
    _>_ : a → a → Bool

  _<_ : a → a → Bool
  _<_ = flip _>_

open Ord ⦃ ... ⦄

{-# COMPILE AGDA2HS Ord class Ord₁ Ord₂ #-}

instance 
    Ord₁-Bool : Ord₁ Bool
    Ord₁-Bool .Ord₁._<_ False b = b
    Ord₁-Bool .Ord₁._<_ True _ = False

instance
   Ord₂-Bool : Ord₂ Bool
   Ord₂-Bool .Ord₂.

Haskell:

class Ord a where
    (<) :: a -> a -> Bool
    (>) :: a -> a -> Bool
    {-# MINIMAL (<) | (>) #-}
    (<) = flip (>)
    x > y = y < x

Copatterns in Type Class Instances

Agda copatterns are not supported by agda2hs in full generality. They can be used to define fields of typeclass instances, for example:

Agda:

record HasId (a : Set)  : Set where
    field id : a → a
{-# COMPILE AGDA2HS HasId class #-}

instance
    UnitHasId : HasId
    UnitHasId .id x = x
{-# COMPILE AGDA2HS UnitHasId #-}

class HasId a where
    id :: a -> a

instance HasId () where
    id x = x

Deriving Type Class Instances

If the derived instance is not needed on the Agda side and needs to only be generated in Haskell, the deriving clause can simply be added to the compilation pragma (this also works with the newtype pragma):

data Planet : Set where
  Mercury : Planet
  Venus   : Planet
  Earth   : Planet
  Mars    : Planet
  Jupiter : Planet
  Saturn  : Planet
  Uranus  : Planet
  Neptune : Planet
  Pluto   : Planet

{-# COMPILE AGDA2HS Planet deriving ( Read ) #-}

Haskell:

data Planet = Mercury
            | Venus
            | Earth
            | Mars
            | Jupiter
            | Saturn
            | Uranus
            | Neptune
            | Pluto
                deriving (Read)

It is also possible to include a standalone deriving clause which makes the instance available on the Agda side by

• adding the derive pragma to an implemented instance,

• or postulating the instance.

Agda:

instance
  iPlanetEq : Eq Planet
  iPlanetEq ._==_ Mercury Mercury = True
  iPlanetEq ._==_ Venus   Venus   = True
  iPlanetEq ._==_ Earth   Earth   = True
  iPlanetEq ._==_ Mars    Mars    = True
  iPlanetEq ._==_ Jupiter Jupiter = True
  iPlanetEq ._==_ Saturn  Saturn  = True
  iPlanetEq ._==_ Uranus  Uranus  = True
  iPlanetEq ._==_ Neptune Neptune = True
  iPlanetEq ._==_ Pluto   Pluto   = True
  iPlanetEq ._==_ _       _       = False

{-# COMPILE AGDA2HS iPlanetEq derive #-}

postulate instance iPlanetOrd : Ord Planet

{-# COMPILE AGDA2HS iPlanetOrd #-}

Haskell:

deriving instance Eq Planet

deriving instance Ord Planet

This is also possible with more complicated instance definitions, such as in the example below.

Agda:

data Optional (a : Set) : Set where
  Of    : a → Optional a
  Empty : Optional a

{-# COMPILE AGDA2HS Optional #-}

postulate instance iOptionalEq : ⦃ Eq a ⦄ → Eq (Optional a)

{-# COMPILE AGDA2HS iOptionalEq #-}

Haskell:

data Optional a = Of a
                | Empty

deriving instance (Eq a) => Eq (Optional a)

Or even with deriving strategies, by specifying them within the derive pragma (Agda2HS will also automatically set the language flags):

Agda:

postulate instance iPlanetShow : Show Planet

{-# COMPILE AGDA2HS iPlanetShow derive stock #-}

record Clazz (a : Set) : Set where
  field
    foo : a → Int
    bar : a → Bool

open Clazz ⦃...⦄ public

{-# COMPILE AGDA2HS Clazz class #-}

postulate instance iPlanetClazz : Clazz Planet

{-# COMPILE AGDA2HS iPlanetClazz derive anyclass #-}

data Duo (a b : Set) : Set where
  MkDuo : (a × b) → Duo a b

{-# COMPILE AGDA2HS Duo newtype #-}

postulate instance iDuoEq : ⦃ Eq a ⦄ → ⦃ Eq b ⦄ → Eq (Duo a b)

{-# COMPILE AGDA2HS iDuoEq derive newtype #-}

Haskell:

{-# LANGUAGE StandaloneDeriving, DerivingStrategies,
  DeriveAnyClass, GeneralizedNewtypeDeriving #-}

deriving stock instance Show Planet

class Clazz a where
    foo :: a -> Int
    bar :: a -> Bool

deriving anyclass instance Clazz Planet

newtype Duo a b = MkDuo (a, b)

deriving newtype instance (Eq a, Eq b) => Eq (Duo a b)

Partial Application

Agda:

add1 : Nat → Nat
add1 = 1 +_
{-# COMPILE AGDA2HS add1 #-}

Haskell:

add1 :: Nat -> Nat 
add1 = (1 +)

Mutual Recursion

Mutually Recursive Functions

Agda

mutual
    even : Nat → Bool
    even Zero = True
    even (Suc n) = odd n

    odd : Nat → Bool
    odd Zero = False
    odd (Suc n) = even n

Haskell

even :: Nat -> Bool
even Zero = True
even (Suc n) = odd n

odd :: Nat -> Bool
odd Zero = False
odd (Suc n) = even n 

Mutually Recursive Datatype and Function

Agda

mutual

  data Map (k : Set) (a : Set) : Set where
    Bin : (sz : Nat) → (kx : k) → (x : a)
          → (l : Map k a) → (r : Map k a)
          → {{@0 szVal : sz ≡ (size l) + (size r) + 1}}
          → Map k a
    Tip : Map k a
  {-# COMPILE AGDA2HS Map #-}

  size : {k a : Set} → Map k a → Nat
  size Tip = 0
  size (Bin sz _ _ _ _) = sz
  {-# COMPILE AGDA2HS size #-}

Haskell

data Map k a = Bin Natural k a (Map k a) (Map k a)
             | Tip

size :: Map k a -> Natural
size Tip = 0
size (Bin sz _ _ _ _) = sz

Implicit Record Field

Agda

record ImplicitField (a : Set) : Set where
    field
        aField : a
        @0 {anImplicitField} : a
open ImplicitField public
{-# COMPILE AGDA2HS ImplicitField class #-}

Haskell

class ImplicitField a where
    aField :: a

Haskell Language Extensions

Required haskell language extensions will be automatically inferred and enabled.

A Haskell language extension can also be enabled manually as follows:

Agda

{-# FOREIGN AGDA2HS {-# LANGUAGE LambdaCase #-} #-}

Haskell

{-# LANGUAGE LambdaCase #-}

Imports

Agda supports import statements anywhere in a file, but all generated Haskell imports will be placed at the top of the file.

Agda

open import M1 -- imports datatype `A` with constructor `mkA`

a : A
a = mkA
{-# COMPILE AGDA2HS a #-}

open import M2 -- imports datatype `B` with constructor `mkB`

b : B
b = mkB
{-# COMPILE AGDA2HS b #-}

Haskell

import M1 (A(mkA))
import M2 (B(mkB))

a :: A
a = mkA

b :: B
b = bar

Note that on the Haskell side all imports are explicit, i.e. indicate the imported identifiers.

Imports can be qualified, but not hidden (although one can still do this manually using FOREIGN).

Agda

import MyModule as M -- imports type X and function foo

test : M.X -> M.X
test = M.foo
{-# COMPILE AGDA2HS test #-}

Haskell

import qualified MyModule as M (X, foo)

test :: M.X -> M.X
test = M.foo

Other supported features include

• qualifying the Haskell prelude,

• automatically inserting necessary packages for built-in types

• sharing a qualifier across different modules to make a common namespace

Agda

import Haskell.Prelude as Pre

_+_ : Pre.Nat → Pre.Nat → Pre.Nat
x + y = x
{-# COMPILE AGDA2HS _+_ #-}

test : Pre.Nat
test = 0 Pre.+ 1 + 0
{-# COMPILE AGDA2HS test #-}

Haskell

import Numeric.Natural (Natural)
import qualified Prelude as Pre ((+))

(+) :: Natural -> Natural -> Natural
x + y = x

test :: Natural
test = (Pre.+) 0 (1 + 0)

An important difference is that multiple qualifications of the same module will be absorbed in a single qualifier, specifically the lexicographically smallest one based on each character’s ASCII value, independent of the order the imports appear in the source file:

Agda

import MyModule as C

testC = C.foo
{-# COMPILE AGDA2HS testC #-}

import MyModule as A

testA = A.foo
{-# COMPILE AGDA2HS testA #-}

testB = B.foo
import MyModule as B
{-# COMPILE AGDA2HS testB #-}

Haskell

import qualified MyModule as A (foo)

testC = A.foo
testA = A.foo
testB = A.foo

Rewrite rules and Prelude imports

Rewrite rules

User-defined rewrite rules can be defined through a YAML configuration file. It is enabled with the --config option.

This feature is particularly useful if you have a project depending on a large library which is not agda2hs-compatible (e.g the standard library). In this case, you might not want to rewrite the entire library, but may still rely on it for proofs.

User-defined rewrite rules can help translating the library functions to ones available in the Haskell Prelude, or even to those written by yourself. In the latter case, place a Haskell file (e.g. Base.hs) next to your .agda files that contains your custom definitions and provide this custom module in the importing clauses of the config file.

To an extent, this compromises the mathematically proven correctness of your project. But if you trust that your (or Prelude’s) functions are equivalent to the original ones, this might not be a problem. You can also prove the equivalence of the two definitions to be safe.

For example, let’s suppose we want to compile the following file:

open import Data.Nat as ℕ
open import Data.Integer as ℤ
open import Data.Rational.Unnormalised as ℚ

double : ℚᵘ → ℚᵘ
double p = (+ 2 / 1) ℚ.* p
{-# COMPILE AGDA2HS double #-}

-- this will use denominator-1 and suc from BaseExample.hs
twoDenoms : ℚᵘ → ℕ
twoDenoms p = 2 ℕ.* (ℕ.suc (ℚᵘ.denominator-1 p))
{-# COMPILE AGDA2HS twoDenoms #-}

By default, the output would be this:

module Example where

import Data.Rational.Unnormalised.Base (ℚᵘ(denominator-1), (/))
import qualified Data.Rational.Unnormalised.Base as ℚ ((*))
import Numeric.Natural (Natural)
import qualified Prelude as ℕ ((*))

double :: ℚᵘ -> ℚᵘ
double p = (ℚ.*) (pos 2 / 1) p

twoDenoms :: ℚᵘ -> Natural
twoDenoms p = (ℕ.*) 2 (suc (denominator-1 p))

Here, agda2hs doesn’t know where to find these definitions; so it simply leaves them as they are.

Run this again with the following config file:

rewrites:
  - from: "Agda.Builtin.Nat.Nat.suc"
    to: "suc"
    importing: "BaseExample"
  - from: "Agda.Builtin.Nat._*_"
    to: "_*_"
    importing: "Prelude"
  - from: "Agda.Builtin.Int.Int.pos"
    to: "toInteger"
    importing: "Prelude"
  - from: "Data.Rational.Unnormalised.Base.ℚᵘ"
    to: "Rational"
    importing: "Data.Ratio"
  - from: "Data.Rational.Unnormalised.Base._*_"
    to: "_*_"
    importing: "Prelude"
  - from: "Data.Rational.Unnormalised.Base._/_"
    to: "_%_"
    importing: "Data.Ratio"
  - from: "Data.Rational.Unnormalised.Base.ℚᵘ.denominator-1"
    to: "denominatorMinus1"
    importing: "BaseExample"

The names are a bit difficult to find. It helps if you run agda2hs with a verbosity level of 26 and check the logs (specifically the parts beginning with compiling name).

The output is now this:

module Example where

import BaseExample (denominatorMinus1, suc)
import Data.Ratio (Rational, (%))
import Numeric.Natural (Natural)
import Prelude (toInteger, (*))

double :: Rational -> Rational
double p = toInteger 2 % 1 * p

twoDenoms :: Rational -> Natural
twoDenoms p = 2 * suc (denominatorMinus1 p)

With a manually written BaseExample.hs file like this, GHCi accepts it:

module BaseExample where

import Numeric.Natural
import Data.Ratio

suc :: Natural -> Natural
suc = (1 +)

denominatorMinus1 :: Rational -> Natural
denominatorMinus1 = fromIntegral . denominator

See also rewrite-rules-example.yaml in the root of the repository.

Handling of Prelude

By default, agda2hs handles Prelude like other modules: it collects all the identifiers it finds we use from Prelude, and adds them to Prelude’s import list.

A different behaviour can be specified in a YAML configuration file. The format is the following:

# First, we specify how to handle Prelude.
prelude:
  implicit: true
  hiding:           # if implicit is true
    - seq

  #using:           # if implicit is false
  #  - +
  #  - Num

# Then the rules themselves.
rewrites:

  # The rational type.
  - from: "Data.Rational.Unnormalised.Base.ℚᵘ"
    to: "Rational"
    importing: "Data.Ratio"

  # ...

If implicit is true, then everything gets imported from Prelude, except for those that are specified in the hiding list. This can cause clashes if you reuse names from Prelude, hence the opportunity for a hiding list. If there is no such list, then everything gets imported.

If implicit is false, Prelude gets imported explicitly, and only those identifiers that are specified in the using list. If there is no such list, agda2hs reverts to the default behaviour (it tries to collect imports by itself).

Known issues

• Rewrite rules only work for things you do use, not for those that you only define. This causes a problem with class instances: if you choose the default behaviour, then write an instance of the Num class and define signum but do not use it, it will not get into Prelude’s import list, and so GHC will complain.

• You cannot change to a version with arguments of different modality without getting useless code. So if you rewrite a function to a version which has some of its parameters erased, the parameters remain there; probably because rewriting happens only after compiling the type signature.

Emacs mode

Since there is a full Agda typechecker in the agda2hs binary, you can readily use the Emacs mode of a pre-existing Agda installation by changing the binary that agda-mode uses to the path to agda2hs binary.

• First, check the version of the Agda typechecker in the agda2hs binary by calling agda2hs --version.

• Install this version of Agda.

• Run agda-mode setup.

• In Emacs, set the agda2-program-name variable to agda2hs (use M-x customize-variable). Alternatively, you can also set it in your ~/.emacs file by hand.

• With C-c C-x C-c, you will now be able call the agda2hs backend from inside Emacs; all the other built-in backends still remain available.

Known issues

• Now, the output can only be written next to the .agda files; there is no option to collect these under a separate directory.

• The --config option is not yet supported in Emacs mode.