diff --git a/DrHylo.cabal b/DrHylo.cabal
--- a/DrHylo.cabal
+++ b/DrHylo.cabal
@@ -1,5 +1,5 @@
 Name:            DrHylo
-Version:         0.0.1
+Version:         0.0.2
 License:         BSD3
 License-file:    LICENSE
 Author:          Alcino Cunha <alcino@di.uminho.pt>, Hugo Pacheco <hpacheco@di.uminho.pt>
@@ -23,7 +23,7 @@
 
 Library
   Hs-Source-Dirs: lib
-  Build-Depends:        base >= 4, pointless-haskell, mtl, haskell-src-exts >= 0.4.4, syb
+  Build-Depends:        base >= 4, pointless-haskell, mtl, haskell-src-exts == 0.4.4.1, syb
   exposed-modules:
        Language.Pointwise.Matching,
        Language.Pointwise.Parser,
diff --git a/Sample.hs b/Sample.hs
--- a/Sample.hs
+++ b/Sample.hs
@@ -48,7 +48,7 @@
 cat []    l = l
 cat (h:t) l = h:(cat t l)
 
-data Tree a = Leaf | Node a (Tree a) (Tree a)
+data Tree a = Leaf | Node a (Tree a) (Tree a) deriving Show
 
 inorder :: Tree a -> [a]
 inorder Leaf = []
diff --git a/src/DrHylo.hs b/src/DrHylo.hs
--- a/src/DrHylo.hs
+++ b/src/DrHylo.hs
@@ -86,28 +86,31 @@
          getVar (TyVar v) = [v]
          getVar _ = []
 
-observableTypeSig :: Decl -> Decl
-observableTypeSig (TypeSig loc names t) = TypeSig loc names (aux t)
+addTypeSig :: Decl -> Decl
+addTypeSig (TypeSig loc names t) = TypeSig loc names (aux t)
    where
-   aux (TyForall mb ctx (TyFun a b)) = TyForall mb (ctx++obs a b) (TyFun a b)
-   aux (TyFun a b) = TyForall Nothing (obs a b) (TyFun a b)
+   aux (TyForall mb ctx (TyFun a b)) = TyForall mb (ctx++inst typeable a b++inst observable a b) (TyFun a b)
+   aux (TyFun a b) = TyForall Nothing (inst typeable a b++inst observable a b) (TyFun a b)
    vars a b = nub $ intersect (getTypeVars a) (getTypeVars b)
-   obs a b = map mkObservableIns (vars a b)
+   inst cl a b = map (mkInsVar cl) (vars a b)
 
-mkObservableIns :: Name -> Asst
-mkObservableIns n = ClassA (UnQual (Ident "Observable")) [TyVar n]
+mkInsVar :: Name -> Name -> Asst
+mkInsVar cl n = ClassA (UnQual cl) [TyVar n]
 
-addObservableIns :: String -> [Decl] -> [Decl]
-addObservableIns n [] = []
-addObservableIns n (d:ds) = if (isTypeSig n d) then observableTypeSig d : ds else d : addObservableIns n ds
+addTypeableObservableIns :: String -> [Decl] -> [Decl]
+addTypeableObservableIns n [] = []
+addTypeableObservableIns n (d:ds) | isTypeSig n d = addTypeSig d : addTypeableObservableIns n ds
+                          | otherwise = d : addTypeableObservableIns n ds
 
 -- From Pointwise to Point-free (or not)
 
 pwpfModule :: [Flag] -> [(String,Pw.Term)] -> Module -> Module
-pwpfModule f c (Module loc name warnings exports imports decls) = Module loc name warnings exports imports decls''
+pwpfModule f c (Module loc name pragmas warnings exports imports decls) = Module loc name pragmas' warnings exports imports decls''
    where
    (decls',obs) = (id >< catMaybes) $ unzip $ map aux decls
-   decls'' = foldr addObservableIns decls' obs
+   decls'' = if (obrequired f) then foldr addTypeableObservableIns decls' obs else decls'
+   pragmaNames = if (obrequired f) then ["TypeFamilies,","DeriveDataTypeable"] else ["TypeFamilies"]
+   pragmas' = LanguagePragma loc (map Ident pragmaNames) : pragmas
    aux d = case pwpfDecl f c d 
       of Just (d',mb) -> (d',mb)
          Nothing -> (d,Nothing)
@@ -150,12 +153,12 @@
 getImportName (ImportDecl _ (ModuleName n) _ _ _ _) = n
 
 handleImports :: Bool -> Module -> Module
-handleImports b (Module loc name warnings exports imports decls) =
-    let aux True  = ["Generics.Pointless.Combinators", "Generics.Pointless.Functors", "Generics.Pointless.RecursionPatterns", "Debug.Observe","Generics.Pointless.Observe.Functors", "Generics.Pointless.Observe.RecursionPatterns"]
+handleImports b (Module loc name pragmas warnings exports imports decls) =
+    let aux True  = ["Generics.Pointless.Combinators", "Generics.Pointless.Functors", "Generics.Pointless.RecursionPatterns", "Data.Typeable", "Debug.Observe", "Generics.Pointless.Observe.Functors", "Generics.Pointless.Observe.RecursionPatterns"]
         aux False = ["Generics.Pointless.Combinators", "Generics.Pointless.Functors", "Generics.Pointless.RecursionPatterns"]
 	aux' = aux b \\ (map getImportName imports) 
 	imports' = imports++(map mkImportDecl aux')
-    in Module loc name warnings exports imports' decls
+    in Module loc name pragmas warnings exports imports' decls
 
 
 -- Main
@@ -170,7 +173,7 @@
 	  hsModule <- parse source
 	  hsModule0 <- return (casificate hsModule)
 	  hsModule1 <- return (functorOfInst ob hsModule0)
-	  hsModule2 <- return (pwpfModule flags (getCtx hsModule0) hsModule1)
+	  hsModule2 <- return (pwpfModule flags (getCtx hsModule1) hsModule1)
           hPutStrLn ohandle (prettyPrint (handleImports ob hsModule2))
           hClose ihandle
           hClose ohandle
diff --git a/src/FunctorOf.hs b/src/FunctorOf.hs
--- a/src/FunctorOf.hs
+++ b/src/FunctorOf.hs
@@ -3,6 +3,8 @@
  , functorOfInst
  , getSeed
  , hsPat2Exp
+ , typeable
+ , observable
  ) where
 
 import Data.Map hiding (map) 
@@ -25,7 +27,7 @@
 type Ctx = [(String,Term)]
 
 getCtx :: Module -> Ctx
-getCtx (Module _ _ _ _ _ decls)
+getCtx (Module _ _ _ _ _ _ decls)
   = concat $ catMaybes $ map getCtxDecl decls
 
 getCtxDecl :: Decl -> Maybe Ctx
@@ -48,18 +50,20 @@
 
 {- Calculation of the instances of FunctorOf, when possible. -}
 
-type St = StateT (String,Int) Maybe
+type St = StateT ((String,Int),[Type]) Maybe
 
 conDecl :: QualConDecl -> ConDecl
 conDecl (QualConDecl _ _ _ con) = con
 
 functorOfInst :: Bool -> Module -> Module
-functorOfInst ob (Module a b c d i decls)
+functorOfInst ob (Module a b c d e i decls)
   = let seed = "v" --getSeed decls
         newDecls = concat $ catMaybes $
-                   map (\x -> evalStateT (getInstances ob x) (seed,0)) decls
-    in Module a b c d i (decls ++ newDecls)
+                   map (\x -> evalStateT (getInstances ob x) ((seed,0),[])) decls
+    in Module a b c d e i (newDecls)
 
+addConst t = modify (\(s,l) -> (s,t:l))
+
 g :: Type -> QualConDecl -> St Type
 g arg = gCon arg . conDecl
 
@@ -79,8 +83,8 @@
 i arg (TyTuple _ lType)       = mapM (ii arg) lType >>= return . foldr1 timesType
 i arg (TyApp hsType1 hsType2) = i arg hsType2 >>= return . appType hsType1
 -- fail "TyApp not yet supported" --g :@: h
-i arg t@(TyVar hsName)        = return $ TyApp (TyCon $ UnQual $ Ident "Const") t
-i arg t@(TyCon hsQName)       = return $ TyApp (TyCon $ UnQual $ Ident "Const") t
+i arg t@(TyVar hsName)        = addConst t >> (return $ TyApp (TyCon $ UnQual $ Ident "Const") t)
+i arg t@(TyCon hsQName)       = addConst t >> (return $ TyApp (TyCon $ UnQual $ Ident "Const") t)
 
 ii :: Type -> Type -> St Type
 ii arg typ | typ == arg = return $ TyCon $ UnQual $ Ident "Id"
@@ -143,25 +147,30 @@
 mkDataName :: Decl -> Type
 mkDataName (DataDecl _ _ _ hsName lName _ _) = foldl TyApp (TyCon $ UnQual hsName) . map TyVar $ lName
 
-getDataDeclFunctor :: Type -> [QualConDecl] -> St Type
-getDataDeclFunctor arg lConDecl = do
+getDataDeclFunctor :: Type -> [QualConDecl] -> St (Type,[Type])
+getDataDeclFunctor arg lConDecl = withStateT (\((s,n),_) -> ((s,n),[])) $ do
    l1 <- mapM (g arg) lConDecl
    let functor = foldr1 plusType l1
-   return functor
+   (_,consts) <- get
+   return (functor,consts)
 
+deriveTypeable :: Decl -> Decl
+deriveTypeable (DataDecl loc dn ctx hsName lName lConDecl derive) =
+   DataDecl loc dn ctx hsName lName lConDecl (nub $ UnQual typeable : derive)
+
 getInstances :: Bool      -- ^ Observable or not
              -> Decl      -- ^ Data types
              -> St [Decl] -- ^ Instances for functor representation
 getInstances ob d@(DataDecl loc _ [] hsName lName lConDecl _) = do
      let arg = mkDataName d
-     functor <- getDataDeclFunctor arg lConDecl
+     (functor,consts) <- getDataDeclFunctor arg lConDecl
      l <- genInOut arg lConDecl
      let innOut = [InsDecl (FunBind (map inMatch l)), InsDecl (FunBind (map outMatch l))]
      let pfTInst = TypeInsDecl loc (TyApp pfType arg) functor
      let muInst = InstDecl loc [] mu [arg] innOut
-     let observableInst = getObservableInst loc arg
-     if ob then return [pfTInst,muInst,observableInst]
-           else return [pfTInst,muInst]
+     let observableInst = getObservableInst loc (nub consts) arg
+     if ob then return [deriveTypeable d,pfTInst,muInst,observableInst]
+           else return [d,pfTInst,muInst]
   where
     match str (a,b) = Exts.Match mkLoc (Ident str) [a]
                         (UnGuardedRhs $ hsPat2Exp b) (BDecls [])
@@ -171,14 +180,15 @@
 
 getInstances _ (DataDecl _ _ _ _ _ _ _ ) =
                  fail "type context not treated"
-getInstances _ _ = fail "not a data declaration"
+getInstances _ d = return [d]
 
 -- types
 opType op a b = TyApp (TyApp (TyVar $ Symbol op) a ) b
 plusType  = opType ":+:"
 timesType = opType ":*:"
 appType   = opType ":@:"
-constNil  = TyApp (TyCon $ UnQual $ Ident "Const") (TyCon $ UnQual $ Ident "One")
+constNil  = TyApp (TyCon $ UnQual $ Ident "Const") nil
+nil = TyCon $ UnQual $ Ident "One"
 mu = UnQual $ Ident "Mu"
 pfType = TyCon $ UnQual $ Ident "PF"
 
@@ -192,14 +202,22 @@
 unRec (a,b) = replicate (length a) b
 
 getFreshVar = do
-   (seed,n) <- gets id
-   modify (\_->(seed,n+1))
+   ((seed,n),l) <- gets id
+   modify (\_->((seed,n+1),l))
    return $ Ident $ seed ++ show (n+1)
 
-getObservableInst :: SrcLoc -> Type -> Decl
-getObservableInst loc a = InstDecl loc [ClassA (UnQual (Ident "FunctorO")) [TyApp (TyCon (UnQual (Ident "PF"))) a]] (UnQual (Ident "Observable")) [a] [InsDecl (FunBind [Exts.Match loc (Ident "observer") [PVar (Ident "x")] (UnGuardedRhs (App (App (Exts.Var (UnQual (Ident "send"))) (Lit (String ""))) (Paren (InfixApp (InfixApp (App (App (App (Exts.Var (UnQual (Ident "omap"))) (Paren (ExpTypeSig loc (Exts.Var (UnQual (Ident "_L"))) a))) (Exts.Var (UnQual (Ident "thk")))) (Paren (App (Exts.Var (UnQual (Ident "out"))) (Exts.Var (UnQual (Ident "x")))))) (QVarOp (UnQual (Symbol ">>="))) (Exts.Var (UnQual (Ident "return")))) (QVarOp (UnQual (Symbol "."))) (Exts.Var (UnQual (Ident "inn"))))))) (BDecls [PatBind loc (PVar (Ident "thk")) (UnGuardedRhs (ExpTypeSig loc (Exts.Var (UnQual (Ident "thunk"))) (TyFun a (TyApp (TyCon (UnQual (Ident "ObserverM"))) a)))) (BDecls [])])])]
+getObservableInst :: SrcLoc -> [Type] -> Type -> Decl
+getObservableInst loc cts a = InstDecl loc ctx (UnQual (Ident "Observable")) [a] [InsDecl (FunBind [Exts.Match loc (Ident "observer") [PVar (Ident "x")] (UnGuardedRhs (App (App (Exts.Var (UnQual (Ident "send"))) (Lit (String ""))) (Paren (InfixApp (InfixApp (App (App (App (Exts.Var (UnQual (Ident "omap"))) (Paren (ExpTypeSig loc (Exts.Var (UnQual (Ident "_L"))) a))) (Exts.Var (UnQual (Ident "thk")))) (Paren (App (Exts.Var (UnQual (Ident "out"))) (Exts.Var (UnQual (Ident "x")))))) (QVarOp (UnQual (Symbol ">>="))) (Exts.Var (UnQual (Ident "return")))) (QVarOp (UnQual (Symbol "."))) (Exts.Var (UnQual (Ident "inn"))))))) (BDecls [PatBind loc (PVar (Ident "thk")) (UnGuardedRhs (ExpTypeSig loc (Exts.Var (UnQual (Ident "thunk"))) thunkSig )) (BDecls [])])])]
+   where ctx = foldr (\c b -> mkIns typeable c : mkIns observable c : b) [] cts
+         thunkSig = TyForall Nothing ctx $ TyFun a (TyApp (TyCon (UnQual (Ident "ObserverM"))) a)
 
+typeable :: Name
+typeable = Ident "Typeable"
+observable :: Name
+observable = Ident "Observable"
 
+mkIns :: Name -> Type -> Asst
+mkIns cl t = ClassA (UnQual cl) [t]
 
 ---- auxiliary functions
 swap (a,b) = (b,a)
diff --git a/src/Matching.hs b/src/Matching.hs
--- a/src/Matching.hs
+++ b/src/Matching.hs
@@ -9,10 +9,10 @@
    f x y = e2 /      \                 (x,y) -> e2
 -}
 casificate :: Module -> Module
-casificate (Module a b c d i decls) =
+casificate (Module a b c d e i decls) =
   let seed = "v"
       newDecls = evalState (mapM cas_decl decls) seed
-  in Module a b c d i newDecls
+  in Module a b c d e i newDecls
 
 
 type ST a = State String a