GADTs

[jmchapman]

Add support for GADTs

[kindaro]

For example, say I want to have abstract syntax à la Emil Axelsson (2012). This construction needs generalized algebraic types for storing arity information on the type level. But indexed types must be erased by agda2hs, so what looks like a generalized algebraic type in Agda will become a plain sum type in Haskell. This then would allow me to construct in Haskell values that would have been illegal in Agda and should be illegal if I were writing abstract syntax in Haskell with generalized algebraic types to begin with.

For example, the following translation of Emil's NUM to Agda:

data NUM : (@0 a : Signature) → Set₁ where
  Num : Int → NUM (Full Int)
  Add : NUM (Argument Int :→ Argument Int :→ Full Int)
  Mul : NUM (Argument Int :→ Argument Int :→ Full Int)
{-# COMPILE AGDA2HS NUM #-}

— Loses all the arity data when compiled to Haskell with agda2hs:

data NUM = Num Int
         | Add
         | Mul

Instead, it would be fantastic if it would become something like this:

data NUM (a :: Signature) where
  Num :: Int -> NUM (Full Int)
  Add :: NUM (Argument Int :→ Argument Int :→ Full Int)
  Mul :: NUM (Argument Int :→ Argument Int :→ Full Int)

Is this realistic?

[jespercockx]

Currently, we do not allow forced patterns in non-erased positions due to https://github.com/agda/agda2hs/issues/142, but this would be too strict when we support GADTs. So in order to support GADTs we need a different fix for that issue.