diff --git a/src/Agda2Hs/Compile.hs b/src/Agda2Hs/Compile.hs
index f76cc499..afa4a794 100644
--- a/src/Agda2Hs/Compile.hs
+++ b/src/Agda2Hs/Compile.hs
@@ -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)
 
diff --git a/src/Agda2Hs/Compile/Data.hs b/src/Agda2Hs/Compile/Data.hs
index 5f710c49..89f23aa0 100644
--- a/src/Agda2Hs/Compile/Data.hs
+++ b/src/Agda2Hs/Compile/Data.hs
@@ -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
 
@@ -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
@@ -64,7 +75,7 @@ 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
@@ -72,11 +83,12 @@ compileConstructor params c = do
   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 []
@@ -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)
diff --git a/src/Agda2Hs/Compile/Record.hs b/src/Agda2Hs/Compile/Record.hs
index fd9193b3..5956ce53 100644
--- a/src/Agda2Hs/Compile/Record.hs
+++ b/src/Agda2Hs/Compile/Record.hs
@@ -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
diff --git a/src/Agda2Hs/Compile/Type.hs b/src/Agda2Hs/Compile/Type.hs
index 74d2dcde..3df2620c 100644
--- a/src/Agda2Hs/Compile/Type.hs
+++ b/src/Agda2Hs/Compile/Type.hs
@@ -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
 
@@ -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 []
@@ -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
@@ -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
diff --git a/src/Agda2Hs/Compile/Types.hs b/src/Agda2Hs/Compile/Types.hs
index 84be1b82..e540106b 100644
--- a/src/Agda2Hs/Compile/Types.hs
+++ b/src/Agda2Hs/Compile/Types.hs
@@ -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.
diff --git a/src/Agda2Hs/Compile/Utils.hs b/src/Agda2Hs/Compile/Utils.hs
index b228d0be..6d57eaf9 100644
--- a/src/Agda2Hs/Compile/Utils.hs
+++ b/src/Agda2Hs/Compile/Utils.hs
@@ -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
 
@@ -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
diff --git a/src/Agda2Hs/Pragma.hs b/src/Agda2Hs/Pragma.hs
index 1f6a5822..5d9e7b23 100644
--- a/src/Agda2Hs/Pragma.hs
+++ b/src/Agda2Hs/Pragma.hs
@@ -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)
@@ -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
@@ -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 []
diff --git a/test/AllTests.agda b/test/AllTests.agda
index bc786d2b..abc23f3b 100644
--- a/test/AllTests.agda
+++ b/test/AllTests.agda
@@ -1,4 +1,4 @@
-{-# OPTIONS --prop #-}
+{-# OPTIONS --prop --polarity #-}
 module AllTests where
 
 import AllCubicalTests
@@ -106,6 +106,7 @@ import Issue306
 import RelevantDotPattern1
 import RelevantDotPattern2
 import RelevantDotPattern3
+import GadtSyntax
 
 {-# FOREIGN AGDA2HS
 import Issue14
@@ -209,4 +210,5 @@ import Issue306
 import RelevantDotPattern1
 import RelevantDotPattern2
 import RelevantDotPattern3
+import GadtSyntax
 #-}
diff --git a/test/GadtSyntax.agda b/test/GadtSyntax.agda
new file mode 100644
index 00000000..a8d2cbf3
--- /dev/null
+++ b/test/GadtSyntax.agda
@@ -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 #-}
diff --git a/test/GadtSyntax.hs b/test/GadtSyntax.hs
new file mode 100644
index 00000000..c87c8722
--- /dev/null
+++ b/test/GadtSyntax.hs
@@ -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)
+
diff --git a/test/NonUniformNesting.agda b/test/NonUniformNesting.agda
new file mode 100644
index 00000000..c33d28ba
--- /dev/null
+++ b/test/NonUniformNesting.agda
@@ -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
diff --git a/test/golden/AllTests.hs b/test/golden/AllTests.hs
index 8c90d4aa..5d95fc9e 100644
--- a/test/golden/AllTests.hs
+++ b/test/golden/AllTests.hs
@@ -101,4 +101,5 @@ import Issue306
 import RelevantDotPattern1
 import RelevantDotPattern2
 import RelevantDotPattern3
+import GadtSyntax
 
diff --git a/test/golden/GadtSyntax.hs b/test/golden/GadtSyntax.hs
new file mode 100644
index 00000000..878fa75a
--- /dev/null
+++ b/test/golden/GadtSyntax.hs
@@ -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
+