Skip to content

[ #242 ] Implement GADT syntax #453

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
jespercockx wants to merge 2 commits into
base: master
Choose a base branch
from
Open

[ #242 ] Implement GADT syntax #453

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
f862cbc
[ #242 ] Implement GADT syntax
jespercockx Nov 28, 2025
ac27870
Silly experiments with GADTs
jespercockx Feb 3, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
9 changes: 5 additions & 4 deletions src/Agda2Hs/Compile.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -126,15 +126,16 @@ compile genv tlm _ def =
(CompileToPragma s , Function{}) -> [] <$ checkCompileToFunctionPragma def s

(ClassPragma ms , Record{} ) -> pure <$> compileRecord (ToClass ms) def
(NewTypePragma ds , Record{} ) -> pure <$> compileRecord (ToRecord True ds) def
(NewTypePragma ds , Datatype{}) -> compileData True ds def
(DefaultPragma ds , Datatype{}) -> compileData False ds def
(NewTypePragma ds , Record{} ) -> pure <$> compileRecord (ToRecord ToNewType ds) def
(NewTypePragma ds , Datatype{}) -> compileData ToNewType ds def
(GadtPragma ds , Datatype{}) -> compileData ToGadt ds def
(DefaultPragma ds , Datatype{}) -> compileData ToData ds def
(DerivePragma s , _ ) | isInstance -> pure <$> compileInstance (ToDerivation s) def
(DefaultPragma _ , Axiom{} ) | isInstance -> pure <$> compileInstance (ToDerivation Nothing) def
(DefaultPragma _ , _ ) | isInstance -> pure <$> compileInstance ToDefinition def
(DefaultPragma _ , Axiom{} ) -> compilePostulate def
(DefaultPragma _ , Function{}) -> compileFun True def
(DefaultPragma ds , Record{} ) -> pure <$> compileRecord (ToRecord False ds) def
(DefaultPragma ds , Record{} ) -> pure <$> compileRecord (ToRecord ToData ds) def

_ -> agda2hsErrorM $ text "Don't know how to compile" <+> prettyTCM (defName def)

Expand Down
41 changes: 27 additions & 14 deletions src/Agda2Hs/Compile/Data.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -13,12 +13,13 @@ import Agda.TypeChecking.Telescope

import Agda.Utils.Maybe
import Agda.Utils.Monad
import Agda.Utils.Singleton
import Agda.Utils.Impossible ( __IMPOSSIBLE__ )

import Agda2Hs.AgdaUtils

import Agda2Hs.Compile.Name
import Agda2Hs.Compile.Type ( compileDomType, compileTeleBinds, compileDom, DomOutput(..) )
import Agda2Hs.Compile.Type ( compileType, compileDomType, compileTeleBinds, compileDom, DomOutput(..) )
import Agda2Hs.Compile.Types
import Agda2Hs.Compile.Utils

Expand All @@ -34,26 +35,36 @@ checkNewtype name cs = do
(Hs.QualConDecl () _ _ (Hs.ConDecl () cName types):_) -> checkNewtypeCon cName types
_ -> __IMPOSSIBLE__

compileData :: AsNewType -> [Hs.Deriving ()] -> Definition -> C [Hs.Decl ()]
compileData newtyp ds def = do
compileData :: DataTarget -> [Hs.Deriving ()] -> Definition -> C [Hs.Decl ()]
compileData target ds def = do
let d = hsName $ prettyShow $ qnameName $ defName def
checkValidTypeName d
let Datatype{dataPars = n, dataIxs = numIxs, dataCons = cs} = theDef def
TelV tel t <- telViewUpTo n (defType def)
TelV tel t <- telView {-UpTo n-} (defType def)
reportSDoc "agda2hs.data" 10 $ text "Datatype telescope:" <+> prettyTCM tel
allIndicesErased t
let params = teleArgs tel
--allIndicesErased t
let params = take n $ teleArgs tel
binds <- compileTeleBinds False tel -- TODO: add kind annotations?
addContext tel $ do
-- TODO: filter out erased constructors
cs <- mapM (compileConstructor params) cs
let hd = foldl (Hs.DHApp ()) (Hs.DHead () d) binds
let htarget = toDataTarget target

let target = if newtyp then Hs.NewType () else Hs.DataType ()
when (target == ToNewType) (checkNewtype d $ map fst cs)

when newtyp (checkNewtype d cs)
return . singleton $ case target of
ToGadt -> Hs.GDataDecl () htarget Nothing hd Nothing (map (uncurry conToGadtCon) cs) ds
_ -> Hs.DataDecl () htarget Nothing hd (map fst cs) ds

return [Hs.DataDecl () target Nothing hd cs ds]
where
conToGadtCon :: Hs.QualConDecl () -> Hs.Type () -> Hs.GadtDecl ()
conToGadtCon (Hs.QualConDecl _ tys ctx con) rt = case con of
Hs.ConDecl () c ts ->
Hs.GadtDecl () c tys ctx Nothing $
foldr (Hs.TyFun ()) rt ts
Hs.InfixConDecl{} -> __IMPOSSIBLE__
Hs.RecDecl{} -> __IMPOSSIBLE__

allIndicesErased :: Type -> C ()
allIndicesErased t = reduce (unEl t) >>= \case
Expand All @@ -64,19 +75,20 @@ allIndicesErased t = reduce (unEl t) >>= \case
DomForall{} -> agda2hsError "Not supported: indexed datatypes"
_ -> return ()

compileConstructor :: [Arg Term] -> QName -> C (Hs.QualConDecl ())
compileConstructor :: [Arg Term] -> QName -> C (Hs.QualConDecl (), Hs.Type ())
compileConstructor params c = do
reportSDoc "agda2hs.data.con" 15 $ text "compileConstructor" <+> prettyTCM c
reportSDoc "agda2hs.data.con" 20 $ text " params = " <+> prettyTCM params
ty <- defType <$> getConstInfo c
reportSDoc "agda2hs.data.con" 30 $ text " ty (before piApply) = " <+> prettyTCM ty
ty <- ty `piApplyM` params
reportSDoc "agda2hs.data.con" 20 $ text " ty = " <+> prettyTCM ty
TelV tel _ <- telView ty
TelV tel ret <- telView ty
let conName = hsName $ prettyShow $ qnameName c
checkValidConName conName
args <- compileConstructorArgs tel
return $ Hs.QualConDecl () Nothing Nothing $ Hs.ConDecl () conName args
hret <- addContext tel $ compileType $ unEl ret
return (Hs.QualConDecl () Nothing Nothing $ Hs.ConDecl () conName args, hret)

compileConstructorArgs :: Telescope -> C [Hs.Type ()]
compileConstructorArgs EmptyTel = return []
Expand Down Expand Up @@ -132,12 +144,13 @@ checkCompileToDataPragma def s = noCheckNames $ do
unless (length rcons == length dcons) $ fail
"they have a different number of constructors"
forM_ (zip dcons rcons) $ \(c1, c2) -> do
Hs.QualConDecl _ _ _ (Hs.ConDecl _ hsC1 args1) <-
(Hs.QualConDecl _ _ _ (Hs.ConDecl _ hsC1 args1) , rt1) <-
addContext dtel $ compileConstructor (teleArgs dtel) c1
-- rename parameters of r to match those of d
rtel' <- renameParameters dtel rtel
Hs.QualConDecl _ _ _ (Hs.ConDecl _ hsC2 args2) <-
(Hs.QualConDecl _ _ _ (Hs.ConDecl _ hsC2 args2) , rt2) <-
addContext rtel' $ compileConstructor (teleArgs rtel') c2
-- TODO: check that rt1 and rt2 are equal?
unless (hsC1 == hsC2) $ fail $
"name of constructor" <+> text (Hs.pp hsC1) <+>
"does not match" <+> text (Hs.pp hsC2)
Expand Down
6 changes: 3 additions & 3 deletions src/Agda2Hs/Compile/Record.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -114,14 +114,14 @@ compileRecord target def = do
assts -> Just (Hs.CxTuple () assts)
defaultDecls <- compileMinRecords def ms
return $ Hs.ClassDecl () context hd [] (Just (classDecls ++ map (Hs.ClsDecl ()) defaultDecls))
ToRecord newtyp ds -> do
ToRecord dtarget ds -> do
checkValidConName cName
when (theEtaEquality recEtaEquality' == YesEta) $ agda2hsErrorM $
"Agda records compiled to Haskell should have eta-equality disabled." <+>
"Add no-eta-equality to the definition of" <+> (text (pp rName) <> ".")
(constraints, fieldDecls) <- compileRecFields fieldDecl recFields fieldTel
when newtyp $ checkNewtypeCon cName fieldDecls
let target = if newtyp then Hs.NewType () else Hs.DataType ()
when (dtarget == ToNewType) $ checkNewtypeCon cName fieldDecls
let target = toDataTarget dtarget
compileDataRecord constraints fieldDecls target hd ds

where
Expand Down
18 changes: 14 additions & 4 deletions src/Agda2Hs/Compile/Type.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -145,6 +145,12 @@ compileType t = do
, y == x0 -> return f
| otherwise -> agda2hsErrorM $ text "Not supported: type-level lambda" <+> prettyTCM t

Con ch ci es | Just args <- allApplyElims es -> do
c <- compileQName (conName ch)
ty <- defType <$> getConstInfo (conName ch)
vs <- compileTypeArgs ty args
return $ tApp (Hs.TyCon () c) vs

_ -> fail
where fail = agda2hsErrorM $ text "Bad Haskell type:" <?> prettyTCM t

Expand All @@ -164,7 +170,8 @@ compileTypeArgs ty (x:xs) = do
DOInstance -> fail "Type-level instance argument not supported"
DOType -> do
(:) <$> compileType (unArg x) <*> rest
DOTerm -> fail "Type-level term argument not supported"
DOTerm -> (:) <$> compileType (unArg x) <*> rest
--fail "Type-level term argument not supported"

compileTel :: Telescope -> C [Hs.Type ()]
compileTel EmptyTel = return []
Expand Down Expand Up @@ -263,7 +270,10 @@ compileTeleBinds kinded = go
ha <- compileKeptTeleBind kinded (hsName $ absName tel) (unDom a)
(ha:) <$> underAbstraction a tel go
DOInstance -> agda2hsError "Constraint in type parameter not supported"
DOTerm -> agda2hsError "Term variable in type parameter not supported"
DOTerm -> do
ha <- compileKeptTeleBind kinded (hsName $ absName tel) (unDom a)
(ha:) <$> underAbstraction a tel go
--agda2hsError "Term variable in type parameter not supported"

compileKeptTeleBind :: Bool -> Hs.Name () -> Type -> C (Hs.TyVarBind ())
compileKeptTeleBind kinded x t = do
Expand All @@ -279,8 +289,8 @@ compileKind t = case unEl t of
Pi a b -> compileDom a >>= \case
DODropped -> underAbstraction a b compileKind
DOType -> Hs.TyFun () <$> compileKind (unDom a) <*> underAbstraction a b compileKind
DOTerm -> err
DOTerm -> Hs.TyFun () <$> compileKind (unDom a) <*> underAbstraction a b compileKind
DOInstance -> err
_ -> err
a -> compileType a
where
err = agda2hsErrorM $ text "Not a valid Haskell kind: " <+> prettyTCM t
11 changes: 8 additions & 3 deletions src/Agda2Hs/Compile/Types.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -210,12 +210,17 @@ data CompiledDom
| DomDropped
-- ^ To nothing (e.g. erased proofs)

-- | Whether a datatype/record should be compiled as a @newtype@ haskell definition.
type AsNewType = Bool
-- | Whether a datatype/record should be compiled as a @newtype@ haskell definition,
-- a gadt-style datatype, or a regular datatype.
data DataTarget
= ToNewType
| ToGadt
| ToData
deriving (Eq)

-- | Compilation target for an Agda record definition.
data RecordTarget
= ToRecord AsNewType [Hs.Deriving ()]
= ToRecord DataTarget [Hs.Deriving ()]
| ToClass [String]

-- | Compilation target for an Agda instance declaration.
Expand Down
6 changes: 6 additions & 0 deletions src/Agda2Hs/Compile/Utils.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -106,6 +106,11 @@ infixr 0 /\, \/
f /\ g = \x -> f x && g x
f \/ g = \x -> f x || g x

toDataTarget :: DataTarget -> Hs.DataOrNew ()
toDataTarget ToNewType = Hs.NewType ()
toDataTarget ToData = Hs.DataType ()
toDataTarget ToGadt = Hs.DataType ()

showTCM :: PrettyTCM a => a -> C String
showTCM x = liftTCM $ show <$> prettyTCM x

Expand Down Expand Up @@ -200,6 +205,7 @@ hasCompilePragma q = processPragma q <&> \case
TransparentPragma{} -> True
CompileToPragma{} -> True
NewTypePragma{} -> True
GadtPragma{} -> True
DerivePragma{} -> True

-- Exploits the fact that the name of the record type and the name of the record module are the
Expand Down
6 changes: 6 additions & 0 deletions src/Agda2Hs/Pragma.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -56,6 +56,7 @@ data ParsedPragma
| TransparentPragma
| NewTypePragma [Hs.Deriving ()]
| TuplePragma Hs.Boxed
| GadtPragma [Hs.Deriving ()]
| CompileToPragma String
| DerivePragma (Maybe (Hs.DerivStrategy ()))
deriving (Eq, Show)
Expand All @@ -72,6 +73,9 @@ parseStrategy _ = Nothing
newtypePragma :: String
newtypePragma = "newtype"

gadtPragma :: String
gadtPragma = "gadt"

processDeriving :: Range -> String -> ([Hs.Deriving ()] -> ParsedPragma) -> C ParsedPragma
processDeriving r d pragma = do
-- parse a deriving clause for a datatype by tacking it onto a
Expand All @@ -95,10 +99,12 @@ processPragma qn = liftTCM (getUniqueCompilerPragma pragmaName qn) >>= \case
| s == "transparent" -> return TransparentPragma
| s == "tuple" -> return $ TuplePragma Hs.Boxed
| s == "unboxed-tuple" -> return $ TuplePragma Hs.Unboxed
| s == "gadt" -> return $ GadtPragma []
| "to" `isPrefixOf` s -> return $ CompileToPragma (drop 3 s)
| s == newtypePragma -> return $ NewTypePragma []
| s == derivePragma -> return $ DerivePragma Nothing
| derivePragma `isPrefixOf` s -> return $ DerivePragma (parseStrategy (drop (length derivePragma + 1) s))
| "deriving" `isPrefixOf` s -> processDeriving r s DefaultPragma
| (newtypePragma ++ " deriving") `isPrefixOf` s -> processDeriving r (drop (length newtypePragma + 1) s) NewTypePragma
| (gadtPragma ++ " deriving") `isPrefixOf` s -> processDeriving r (drop (length gadtPragma + 1) s) GadtPragma
_ -> return $ DefaultPragma []
4 changes: 3 additions & 1 deletion test/AllTests.agda
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
{-# OPTIONS --prop #-}
{-# OPTIONS --prop --polarity #-}
module AllTests where

import AllCubicalTests
Expand Down Expand Up @@ -106,6 +106,7 @@ import Issue306
import RelevantDotPattern1
import RelevantDotPattern2
import RelevantDotPattern3
import GadtSyntax

{-# FOREIGN AGDA2HS
import Issue14
Expand Down Expand Up @@ -209,4 +210,5 @@ import Issue306
import RelevantDotPattern1
import RelevantDotPattern2
import RelevantDotPattern3
import GadtSyntax
#-}
26 changes: 26 additions & 0 deletions test/GadtSyntax.agda
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,26 @@
{-# OPTIONS --polarity #-}

open import Haskell.Prelude

data Bol : Set where Tru Fls : Bol

{-# COMPILE AGDA2HS Bol gadt #-}

data Free (f : @++ Set → Set) (a : Set) : Set where
Return : a → Free f a
Roll : f (Free f a) → Free f a

{-# COMPILE AGDA2HS Free gadt #-}

data Na : Set where
Ze : Na
Su : Na → Na
{-# COMPILE AGDA2HS Na #-}

variable n : Na

data Vec (a : Set) : (n : Na) → Set where
Nil : Vec a Ze
Cons : (x : a) (xs : Vec a n) → Vec a (Su n)

{-# COMPILE AGDA2HS Vec gadt #-}
17 changes: 17 additions & 0 deletions test/GadtSyntax.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,17 @@
module GadtSyntax where

data Bol where
Tru :: Bol
Fls :: Bol

data Free f a where
Return :: a -> Free f a
Roll :: f (Free f a) -> Free f a

data Na = Ze
| Su Na

data Vec a n where
Nil :: Vec a Ze
Cons :: a -> Vec a n -> Vec a (Su n)

40 changes: 40 additions & 0 deletions test/NonUniformNesting.agda
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,40 @@

open import Agda.Builtin.Nat

variable
A B C D : Set
k l m n : Nat

record _×_ (A B : Set) : Set where
constructor _,_
field
fst : A
snd : B
open _×_

data PList (A : Set) : Nat → Set where
[] : PList A zero
_∷_ : A → PList (A × A) n → PList A (suc n)

data RoseTree (A : Set) : Nat → Set where
leaf : A → RoseTree A zero
node : PList (RoseTree A m) n → RoseTree A (suc m)

_***_ : (A → B) → (C → D) → A × C → B × D
(f *** g) (x , y) = f x , g y

map : (A → B) → PList A n → PList B n
map f [] = []
map f (x ∷ xs) = f x ∷ map (f *** f) xs

unzip : {A B : Set} → PList (A × B) n → PList A n × PList B n
unzip zs = map fst zs , map snd zs

sum : RoseTree Nat m → Nat
suml : PList (RoseTree Nat m) n → Nat

sum (leaf x) = x
sum (node x) = suml x

suml [] = 0
suml (x ∷ xs) = sum x + let (xs , ys) = unzip xs in suml xs + suml ys
1 change: 1 addition & 0 deletions test/golden/AllTests.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -101,4 +101,5 @@ import Issue306
import RelevantDotPattern1
import RelevantDotPattern2
import RelevantDotPattern3
import GadtSyntax

10 changes: 10 additions & 0 deletions test/golden/GadtSyntax.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,10 @@
module GadtSyntax where

data Bol where
Tru :: Bol
Fls :: Bol

data Free f a where
Return :: a -> Free f a
Roll :: f (Free f a) -> Free f a