diff --git a/src/Language/Inch/Check.lhs b/src/Language/Inch/Check.lhs
index 500ab9a..9324802 100644
--- a/src/Language/Inch/Check.lhs
+++ b/src/Language/Inch/Check.lhs
@@ -67,9 +67,12 @@ Set this to True in order to verify the context regularly:
 > goodTy :: Context -> Type k -> Bool
 > goodTy = goodFV
 
+> goodTopDecl :: Context -> TopDeclaration () -> Bool
+> goodTopDecl g (DataDecl _ _ cs _)  = all (\ (_ ::: t) -> goodTy g t) cs
+> goodTopDecl g (Decl d)             = goodDecl g d
+
 > goodDecl :: Context -> Declaration () -> Bool
 > goodDecl g (SigDecl _ t)        = goodTy g t
-> goodDecl g (DataDecl _ _ cs _)  = all (\ (_ ::: t) -> goodTy g t) cs
 > goodDecl _ (FunDecl _ _)        = True
 
 
diff --git a/src/Language/Inch/Erase.lhs b/src/Language/Inch/Erase.lhs
index be841b4..3433c45 100644
--- a/src/Language/Inch/Erase.lhs
+++ b/src/Language/Inch/Erase.lhs
@@ -159,16 +159,19 @@
 >     (ps',  g) <- erasePatList ps
 >     return (p' :! ps', f . g)
 
-> eraseDecl :: Declaration () -> Contextual (Declaration ())
-> eraseDecl (DataDecl s k cs ds) =
+> eraseTopDecl :: TopDeclaration () -> Contextual (TopDeclaration ())
+> eraseTopDecl (DataDecl s k cs ds) =
 >     case eraseKind k of
 >         Just (Ex k') -> do
 >             cs' <- traverse eraseCon cs
 >             return $ DataDecl s k' cs' ds
->         Nothing -> error $ "eraseType: failed to erase kind " ++ show k
+>         Nothing -> error $ "eraseTopDecl: failed to erase kind " ++ show k
+> eraseTopDecl (Decl d) = Decl <$> eraseDecl d
+
+> eraseDecl :: Declaration () -> Contextual (Declaration ())
 > eraseDecl (FunDecl x ps) =
 >     FunDecl x <$> traverse eraseAlt ps
 > eraseDecl (SigDecl x ty) = SigDecl x <$> eraseToSet ty
 
 > eraseModule :: Module () -> Contextual (Module ())
-> eraseModule (Mod mh is ds) = Mod mh is <$> traverse eraseDecl ds
+> eraseModule (Mod mh is ds) = Mod mh is <$> traverse eraseTopDecl ds
diff --git a/src/Language/Inch/File.lhs b/src/Language/Inch/File.lhs
index 9e5dc5e..5747f7d 100644
--- a/src/Language/Inch/File.lhs
+++ b/src/Language/Inch/File.lhs
@@ -41,18 +41,18 @@
 > getInterface :: Module () -> String
 > getInterface = renderMe . map fog . filter dataOrSigDecl . modDecls
 >   where
->     dataOrSigDecl (SigDecl _ _)       = True
->     dataOrSigDecl (DataDecl _ _ _ _)  = True
->     dataOrSigDecl (FunDecl _ _)       = False
+>     dataOrSigDecl (DataDecl _ _ _ _)    = True
+>     dataOrSigDecl (Decl (SigDecl _ _))  = True
+>     dataOrSigDecl (Decl (FunDecl _ _))  = False
 
 
-> readImport :: FilePath -> Import -> IO [SDeclaration ()]
+> readImport :: FilePath -> Import -> IO [STopDeclaration ()]
 > readImport dir im = do
 >     s <- catch (readFile (combine dir inchFile)) $ \ (_ :: IOException) ->
 >              catch (readFile =<< getDataFileName inchFile) $ \ (_ :: IOException) ->
 >                  hPutStrLn stderr ("Could not load " ++ inchFile) >> return ""
 >     case parseInterface inchFile s of
->         Right ds  -> return $ filter (included . declName) ds
+>         Right ds  -> return $ filter (included . topDeclName) ds
 >         Left err  -> putStrLn ("interface parse error:\n" ++ show err) >> exitFailure
 >   where
 >     inchFile = importName im ++ ".inch"
@@ -61,7 +61,7 @@
 >         Imp ys        -> x `elem` ys
 >         ImpHiding ys  -> x `notElem` ys
 
-> readImports :: FilePath -> [Import] -> IO [SDeclaration ()]
+> readImports :: FilePath -> [Import] -> IO [STopDeclaration ()]
 > readImports dir is = fmap join (mapM (readImport dir) is')
 >   where
 >     is' = if any (("Prelude" ==) . importName) is then is
diff --git a/src/Language/Inch/Parser.lhs b/src/Language/Inch/Parser.lhs
index d715808..08c37f1 100644
--- a/src/Language/Inch/Parser.lhs
+++ b/src/Language/Inch/Parser.lhs
@@ -284,7 +284,7 @@ Terms
 
 Interface files
 
-> interface = many (dataDecl <|> sigDecl)
+> interface = many (dataDecl <|> Decl <$> sigDecl)
 
 
 Modules
@@ -316,12 +316,28 @@ Modules
 > moduleName = join . intersperse "." <$> identLike False "module name" `sepBy` dot
 
 
-> topdecls  = associate <$> many (dataDecl <|> sigDecl <|> funDecl)
-> decls     = associate <$> many (sigDecl <|> funDecl)
+> topdecls  = associateTop <$> many (dataDecl
+>                                    <|> (Decl <$> (sigDecl <|> funDecl)))
+>  where
+>     associateTop :: [STopDeclaration ()] -> [STopDeclaration ()]
+>     associateTop = map joinFun . groupBy sameFun
+>
+>     sameFun (Decl (FunDecl x _)) (Decl (FunDecl y _))  = x == y
+>     sameFun _             _                            = False
+> 
+>     joinFun :: [STopDeclaration ()] -> STopDeclaration ()
+>     joinFun [d] = d
+>     joinFun fs@(Decl (FunDecl x _) : _) = Decl (FunDecl x (join (map altsOf fs)))
+>     joinFun _ = error "joinFun: impossible"
+>
+>     altsOf (Decl (FunDecl _ as)) = as
+>     altsOf _ = error "altsOf: impossible"
 
-> associate :: [SDeclaration ()] -> [SDeclaration ()]
-> associate = map joinFun . groupBy sameFun
+> decls     = associate <$> many (sigDecl <|> funDecl)
 >   where
+>     associate :: [SDeclaration ()] -> [SDeclaration ()]
+>     associate = map joinFun . groupBy sameFun
+>
 >     sameFun (FunDecl x _) (FunDecl y _)  = x == y
 >     sameFun _             _              = False
 > 
@@ -329,10 +345,12 @@ Modules
 >     joinFun [d] = d
 >     joinFun fs@(FunDecl x _ : _) = FunDecl x (join (map altsOf fs))
 >     joinFun _ = error "joinFun: impossible"
-
+>
 >     altsOf (FunDecl _ as) = as
 >     altsOf _ = error "altsOf: impossible"
 
+
+
 > dataDecl = I.lineFold $ do
 >     try (reserved "data")
 >     s <- tyConName
diff --git a/src/Language/Inch/PrettyPrinter.lhs b/src/Language/Inch/PrettyPrinter.lhs
index c9a307b..293b067 100644
--- a/src/Language/Inch/PrettyPrinter.lhs
+++ b/src/Language/Inch/PrettyPrinter.lhs
@@ -54,7 +54,7 @@
 > instance Pretty String where
 >     pretty s _ = text s
 
-> instance Pretty [SDeclaration ()] where
+> instance Pretty [STopDeclaration ()] where
 >     pretty ds _ = vcat (map prettyHigh ds)
 
 > instance Pretty SKind where
@@ -192,7 +192,7 @@
 >     pretty (ImpHiding xs)  _ = text "hiding" <+> parens (hsep (punctuate (text ",") (map text xs)))
 
 
-> instance Pretty (SDeclaration a) where
+> instance Pretty (STopDeclaration a) where
 >     pretty (DataDecl n k cs ds) _ = hang (text "data" <+> text n
 >         <+> (if k /= SKSet then text "::" <+> prettyHigh k else empty)
 >         <+> text "where") 2 $
@@ -201,6 +201,9 @@
 >         derivingClause []  = empty
 >         derivingClause xs  = text "deriving" <+>
 >                                parens (hsep (punctuate  (text ",") (map text xs)))
+>     pretty (Decl d) s = pretty d s
+
+> instance Pretty (SDeclaration a) where
 >     pretty (FunDecl n ps) _ = vcat (map ((text n <+>) . prettyHigh) ps)
 >     pretty (SigDecl n ty) _ = text n <+> text "::" <+> prettyHigh ty
 
diff --git a/src/Language/Inch/ProgramCheck.lhs b/src/Language/Inch/ProgramCheck.lhs
index ac81a07..b40b3de 100644
--- a/src/Language/Inch/ProgramCheck.lhs
+++ b/src/Language/Inch/ProgramCheck.lhs
@@ -29,35 +29,39 @@
 >         B0  -> return ()
 >         _   -> traceContext "assertContextEmpty" >> erk "context is not empty"
 
-> checkModule :: SModule () -> [SDeclaration ()] -> Contextual (Module ())
+> checkModule :: SModule () -> [STopDeclaration ()] -> Contextual (Module ())
 > checkModule (Mod mh is ds) xs = do
 >     mapM_ makeTyCon xs
->     mapM_ (makeBinding True) xs
->     mapM_ checkDecl xs
+>     mapM_ (makeTopBinding True) xs
+>     mapM_ checkTopDecl xs
 >     mapM_ makeTyCon ds
->     mapM_ (makeBinding False) ds
->     ds' <- concat <$> traverse checkDecl ds
+>     mapM_ (makeTopBinding False) ds
+>     ds' <- concat <$> traverse checkTopDecl ds
 >     return $ Mod mh is ds'
 >   where
->     makeTyCon :: SDeclaration () -> Contextual ()
+>     makeTyCon :: STopDeclaration () -> Contextual ()
 >     makeTyCon (DataDecl t k _ _) = inLocation (text $ "in data type " ++ t) $
 >         case kindKind k of
 >           Ex k' -> do
 >             unless (targetsSet k') $ errKindTarget k
 >             insertTyCon t (Ex k')
->     makeTyCon _ = return ()
+>     makeTyCon (Decl _) = return ()
 
-> checkDecl :: SDeclaration () -> Contextual [Declaration ()]
-> checkDecl (DataDecl t k cs ds) = inLocation (text $ "in data type " ++ t) $ 
+> makeTopBinding :: Bool -> STopDeclaration () -> Contextual ()
+> makeTopBinding _ (DataDecl _ _ _ _)  = return ()
+> makeTopBinding b (Decl d) = makeBinding b d
+
+> checkTopDecl :: STopDeclaration () -> Contextual [TopDeclaration ()]
+> checkTopDecl (DataDecl t k cs ds) = inLocation (text $ "in data type " ++ t) $ 
 >   unEx (kindKind k) $ \ k' -> do
 >     cs'    <- traverse (checkConstructor t) cs
 >     return [DataDecl t k' cs' ds]
 > checkDecl d = do
 >   assertContextEmpty 
->   ds <- checkInferFunDecl d
+>   ds <- checkInferDecl d
 >   assertContextEmpty
->   unless (all (goodDecl B0) ds) $ erk $ unlines ("checkDecl: bad declaration" : map (renderMe . fog) ds)
->   return ds
+>   unless (all (goodDecl B0) ds) $ erk $ unlines ("checkTopDecl: bad declaration" : map (renderMe . fog) ds)
+>   return $ map Decl ds
 
 > checkConstructor :: TyConName -> SConstructor -> Contextual Constructor
 > checkConstructor t (c ::: ty) = inLocation (text $ "in constructor " ++ c) $ do
diff --git a/src/Language/Inch/Syntax.lhs b/src/Language/Inch/Syntax.lhs
index e01d5e5..53c8756 100644
--- a/src/Language/Inch/Syntax.lhs
+++ b/src/Language/Inch/Syntax.lhs
@@ -53,24 +53,26 @@
 
 > type Con s        = TmConName ::: ATy s () KSet
 
-> type Term             = Tm OK
 > type Module           = Mod OK
+> type Term             = Tm OK
 > type Constructor      = Con OK
 > type Alternative      = Alt OK
 > type CaseAlternative  = CaseAlt OK
 > type PatternList      = PatList OK
 > type Pattern          = Pat OK
+> type TopDeclaration   = TopDecl OK
 > type Declaration      = Decl OK
 > type Guard            = Grd OK
 > type GuardTerms       = GrdTms OK
 
-> type STerm             = Tm RAW
 > type SModule           = Mod RAW
+> type STerm             = Tm RAW
 > type SConstructor      = Con RAW
 > type SAlternative      = Alt RAW
 > type SCaseAlternative  = CaseAlt RAW
 > type SPatternList      = PatList RAW
 > type SPattern          = Pat RAW
+> type STopDeclaration   = TopDecl RAW
 > type SDeclaration      = Decl RAW
 > type SGuard            = Grd RAW
 > type SGuardTerms       = GrdTms RAW
@@ -150,7 +152,7 @@
 
 > data Mod s a = Mod { modName :: Maybe (String, [String])
 >                    , modImports :: [Import]
->                    , modDecls :: [Decl s a]
+>                    , modDecls :: [TopDecl s a]
 >                    }
 
 > deriving instance Show (Mod RAW a)
@@ -172,6 +174,7 @@
 >   deriving (Eq, Show)
 
 
+
 > data Tm s a where
 >     TmVar    :: TmName                    -> Tm s a
 >     TmCon    :: TmConName                 -> Tm s a
@@ -251,9 +254,47 @@
 > tmBinOp t m n = TmBinOp t `TmApp` m `TmApp` n
 
 
-> data Decl s a where
+
+
+> data TopDecl s a where
 >     DataDecl  :: TyConName -> AKind s k -> [TmConName ::: ATy s a KSet] ->
->                      [String] -> Decl s a
+>                      [String] -> TopDecl s a
+>     Decl      :: Decl s a -> TopDecl s a
+
+> deriving instance Show (TopDecl RAW a)
+> deriving instance Show (TopDecl OK a)
+
+> instance Eq (TopDecl RAW a) where
+>     DataDecl x k cs ds == DataDecl x' k' cs' ds' = x == x' && k == k' && cs == cs' && ds == ds'
+>     Decl d == Decl d' = d == d'
+>     _ == _ = False
+
+> instance TravTypes TopDecl where
+
+>     travTypes g (DataDecl x k cs ds) =
+>         DataDecl x k <$> traverse (\ (y ::: t) -> (y :::) <$> g t) cs <*> pure ds
+>     travTypes g (Decl d) = Decl <$> travTypes g d
+
+>     fogTypes g (DataDecl x k cs ds) = DataDecl x (fogKind k)
+>         (map (\ (y ::: t) -> y ::: fogTy' g [] t) cs)
+>         ds
+>     fogTypes g (Decl d)  = Decl (fogTypes g d)
+
+>     renameTypes g (DataDecl x k cs ds) = DataDecl x k
+>         (map (\ (y ::: t) -> y ::: renameTy g t) cs)
+>         ds
+>     renameTypes g (Decl d)  = Decl (renameTypes g d)
+
+> instance a ~ b => FV (TopDecl OK a) b where
+>     fvFoldMap f (DataDecl _ _ cs _)  = fvFoldMap f (map (\ (_ ::: t) -> t) cs)
+>     fvFoldMap f (Decl d)             = fvFoldMap f d
+
+> topDeclName :: TopDecl s a -> String
+> topDeclName (DataDecl x _ _ _)  = x
+> topDeclName (Decl d)            = declName d
+
+
+> data Decl s a where
 >     FunDecl   :: TmName -> [Alt s a] -> Decl s a
 >     SigDecl   :: TmName -> ATy s a KSet -> Decl s a
 
@@ -262,32 +303,21 @@
 > deriving instance Eq (Decl RAW a)
 
 > instance TravTypes Decl where
-
->     travTypes g (DataDecl x k cs ds) =
->         DataDecl x k <$> traverse (\ (y ::: t) -> (y :::) <$> g t) cs <*> pure ds
 >     travTypes g (FunDecl x ps) =
 >         FunDecl x <$> traverse (travTypes g) ps
 >     travTypes g (SigDecl x ty) = SigDecl x <$> g ty
 
->     fogTypes g (DataDecl x k cs ds) = DataDecl x (fogKind k)
->         (map (\ (y ::: t) -> y ::: fogTy' g [] t) cs)
->         ds
 >     fogTypes g (FunDecl x ps)  = FunDecl x (map (fogTypes g) ps)
 >     fogTypes g (SigDecl x ty)  = SigDecl x (fogTy' g [] ty)
 
->     renameTypes g (DataDecl x k cs ds) = DataDecl x k
->         (map (\ (y ::: t) -> y ::: renameTy g t) cs)
->         ds
 >     renameTypes g (FunDecl x ps)  = FunDecl x (map (renameTypes g) ps)
 >     renameTypes g (SigDecl x ty)  = SigDecl x (renameTy g ty) 
 
 > instance a ~ b => FV (Decl OK a) b where
->     fvFoldMap f (DataDecl _ _ cs _)  = fvFoldMap f (map (\ (_ ::: t) -> t) cs)
 >     fvFoldMap f (FunDecl _ as)       = fvFoldMap f as
 >     fvFoldMap f (SigDecl _ t)        = fvFoldMap f t
 
 > declName :: Decl s a -> String
-> declName (DataDecl x _ _ _)  = x
 > declName (FunDecl x _)       = x
 > declName (SigDecl x _)       = x
 
diff --git a/src/Language/Inch/TypeCheck.lhs b/src/Language/Inch/TypeCheck.lhs
index 597d094..5a7ca61 100644
--- a/src/Language/Inch/TypeCheck.lhs
+++ b/src/Language/Inch/TypeCheck.lhs
@@ -380,7 +380,7 @@ status.
 > checkLocalDecls ds =
 >     withLayerExtract False False (LetBindings Map.empty) letBindings $ do
 >         mapM_ (makeBinding False) ds
->         Data.List.concat <$> traverse checkInferFunDecl ds  
+>         Data.List.concat <$> traverse checkInferDecl ds  
 
 > makeBinding :: Bool -> SDeclaration () -> Contextual ()
 > makeBinding defd (SigDecl x ty) = inLocation (text $ "in binding " ++ x) $ do
@@ -390,12 +390,11 @@ status.
 >         KSet  -> insertBinding x (Just ty', defd)
 >         _     -> errKindNotSet (fogKind k)
 > makeBinding _ (FunDecl _ _)       = return ()
-> makeBinding _ (DataDecl _ _ _ _)  = return ()
 
-> checkInferFunDecl :: SDeclaration () -> Contextual [Declaration ()]
-> checkInferFunDecl (FunDecl s []) =
+> checkInferDecl :: SDeclaration () -> Contextual [Declaration ()]
+> checkInferDecl (FunDecl s []) =
 >   inLocation (text $ "in declaration of " ++ s) $ erk $ "No alternative"
-> checkInferFunDecl (FunDecl s (p:ps)) = do
+> checkInferDecl (FunDecl s (p:ps)) = do
 >     when (not (null ps) && isVarAlt p) $ errDuplicateTmVar s
 >     mty <- optional $ lookupBinding s
 >     case mty of
@@ -405,10 +404,9 @@ status.
 >             (fd, ty) <- inferFunDecl s (p:ps)
 >             updateBinding s (Just ty, True)
 >             return [SigDecl s ty, fd]
-> checkInferFunDecl (SigDecl x _) = do
+> checkInferDecl (SigDecl x _) = do
 >     _ ::: ty <- fst <$> lookupBinding x
 >     return [SigDecl x ty]
-> checkInferFunDecl (DataDecl _ _ _ _) = error "checkInferFunDecl: that's a data declaration"
 
 > inferFunDecl :: String -> [SAlternative ()] -> Contextual (Declaration (), Type KSet)
 > inferFunDecl s pats =
diff --git a/tests/Main.lhs b/tests/Main.lhs
index e3182c1..d37cb04 100644
--- a/tests/Main.lhs
+++ b/tests/Main.lhs
@@ -77,7 +77,7 @@
 >                                    ++ s' ++ "\n" ++ show err
 >     Left err -> Left $ "Initial parse:\n" ++ s ++ "\n" ++ show err
 
-> parseCheck :: [SDeclaration ()] -> (String, Bool) -> Either String String
+> parseCheck :: [STopDeclaration ()] -> (String, Bool) -> Either String String
 > parseCheck ds (s, b) = case parseModule "parseCheck" s of
 >     Right md   -> case evalStateT (checkModule md ds) initialState of
 >         Right md'
@@ -92,7 +92,7 @@
 >                             ++ renderMe md ++ "\n" ++ renderMe err ++ "\n"
 >     Left err  -> Left $ "Parse error:\n" ++ s ++ "\n" ++ show err ++ "\n"
 
-> eraseCheck :: [SDeclaration ()] -> String -> Either String String
+> eraseCheck :: [STopDeclaration ()] -> String -> Either String String
 > eraseCheck ds s = case parseModule "eraseCheck" s of
 >     Right md   -> case runStateT (checkModule md ds) initialState of
 >         Right (md', st) -> case evalStateT (eraseModule md') st of