diff --git a/AspectAG.cabal b/AspectAG.cabal
--- a/AspectAG.cabal
+++ b/AspectAG.cabal
@@ -10,7 +10,7 @@
 -- PVP summary:      +-+------- breaking API changes
 --                   | | +----- non-breaking API additions
 --                   | | | +--- code changes with no API change
-version:             0.5.0.0
+version:             0.6.0.0
 
 -- A short (one-line) description of the package.
 synopsis:            Strongly typed Attribute Grammars implemented using type-level programming.
@@ -36,9 +36,6 @@
 -- patches.
 maintainer:          jpgarcia@fing.edu.uy
 
--- A copyright notice.
--- copyright:
-
 category:            Language
 
 build-type:          Simple
@@ -46,12 +43,7 @@
 -- Extra files to be distributed with the package, such as examples or a
 -- README.
 extra-source-files:  ChangeLog.md,
-                     LICENSE,
-                     examples/ExprExt.hs,
-                     examples/Expr.hs,
-                     examples/List.hs,
-                     examples/RepminTHExt.lhs,
-                     examples/RepminTH.lhs
+                     LICENSE
 
 
 
@@ -68,11 +60,9 @@
   exposed-modules:     Language.Grammars.AspectAG,
                        Language.Grammars.AspectAG.TH,
                        Language.Grammars.AspectAG.HList,
-                       Language.Grammars.AspectAG.TPrelude,
-                       Language.Grammars.AspectAG.GenRecord,
-                       Language.Grammars.AspectAG.RecordInstances,
-                       Language.Grammars.AspectAG.Require
-  -- LANGUAGE extensions used by modules in this package.
+                       Language.Grammars.AspectAG.RecordInstances
+
+-- LANGUAGE extensions used by modules in this package.
   other-extensions:    TypeInType,
                        TypeFamilies,
                        FlexibleContexts,
@@ -97,17 +87,17 @@
                        InstanceSigs
 
   -- Other library packages from which modules are imported.
-  build-depends:       base >=4.11 && <4.13,
+  build-depends:       base >=4.11 && <4.15,
                        tagged >=0.8,
                        containers >= 0.5,
                        template-haskell >= 2.13,
-                       th-strict-compat >= 0.1,
                        mtl >= 2.0,
-                       ghc-prim >= 0.5
+                       requirements >=0.6 && <0.7,
+                       poly-rec >=0.6 && <0.7
  
 
   -- Directories containing source files.
-  hs-source-dirs:      src, examples
+  hs-source-dirs:      src
 
   -- Base language which the package is written in.
   default-language:    Haskell2010
diff --git a/examples/Expr.hs b/examples/Expr.hs
deleted file mode 100644
--- a/examples/Expr.hs
+++ /dev/null
@@ -1,95 +0,0 @@
-{-# LANGUAGE TypeOperators #-}
-
-{-# LANGUAGE
-             TypeFamilies,
-             FlexibleContexts,
-             ScopedTypeVariables,
-             NoMonomorphismRestriction,
-             ImplicitParams,
-             ExtendedDefaultRules,
-             UnicodeSyntax,
-             DataKinds,
-             TypeApplications,
-             PartialTypeSignatures,
-             AllowAmbiguousTypes
-#-}
-
-
-module Expr where
-
-import System.Exit (exitFailure)
-import Language.Grammars.AspectAG
-import Control.Monad
-import Control.Applicative
-import Data.Proxy
-import GHC.TypeLits
-import Data.Map
-import Data.Maybe
-import Debug.Trace
-import Language.Grammars.AspectAG.TH
-
-type Nt_Expr = 'NT "Expr"
-expr = Label @ Nt_Expr
-
-type P_Add = 'Prd "p_Add" Nt_Expr
-add = Label @ P_Add
-
-type P_Val = 'Prd "p_Val" Nt_Expr
-val = Label @ P_Val
-
-type P_Var = 'Prd "p_Var" Nt_Expr
-var = Label @ P_Var
-
-
-leftAdd   = Label @ ('Chi "leftAdd"   P_Add ('Left Nt_Expr))
-rightAdd  = Label @ ('Chi "rightAdd"  P_Add ('Left Nt_Expr))
-ival      = Label @ ('Chi "ival"      P_Val ('Right ('T Int)))
-vname     = Label @ ('Chi "vname"     P_Var ('Right ('T String)))
-
-eval = Label @ ('Att "eval" Int)
-env  = Label @ ('Att "env"  (Map String Int))
-
-add_eval  =  syndefM eval add  $ (+) <$> at leftAdd eval <*> at rightAdd eval
-val_eval  =  syndefM eval val  $ ter ival
-var_eval  =  syndefM eval var  $ slookup <$> ter vname <*> at lhs env
-
-slookup nm = fromJust . Data.Map.lookup nm
-
-aspEval   =  traceAspect (Proxy @ ('Text "eval"))
-          $  add_eval .+: val_eval .+: var_eval .+: emptyAspect
-
-
-add_leftAdd_env  = inhdefM env add leftAdd  $ at lhs env
-add_rightAdd_env = inhdefM env add rightAdd $ at lhs env
--- val_ival_env = inhdefM env val ival $ at lhs env
-
-aspEnv  =  traceAspect (Proxy @ ('Text "env"))
-        $  add_leftAdd_env .+: add_rightAdd_env .+: emptyAspect 
-
-
-asp = aspEval .:+: aspEnv
-
-
-data Expr = Val Int
-          | Var String
-          | Add Expr Expr
-       deriving Show
-
-
-
-sem_Expr asp (Add l r) = knitAspect add asp
-                           $  leftAdd  .=. sem_Expr asp l
-                          .*. rightAdd .=. sem_Expr asp r
-                          .*.  EmptyRec
-sem_Expr asp (Val i)   = knitAspect val asp$
-                          ival  .=. sem_Lit i .*. EmptyRec
-sem_Expr asp (Var v)   = knitAspect var asp$
-                          vname .=. sem_Lit v .*. EmptyRec
-
-evalExpr e m = sem_Expr asp e (env =. m .*. emptyAtt) #. eval
-
-
-exampleExpr =  Add (Val (-9)) (Add (Var "x") (Val 2))
-exampleEval =  evalExpr exampleExpr (insert "x" 5 Data.Map.empty)
-
-
diff --git a/examples/ExprExt.hs b/examples/ExprExt.hs
deleted file mode 100644
--- a/examples/ExprExt.hs
+++ /dev/null
@@ -1,184 +0,0 @@
-{-# LANGUAGE TypeOperators #-}
-
-{-# LANGUAGE
-             TypeFamilies,
-             FlexibleContexts,
-             ScopedTypeVariables,
-             NoMonomorphismRestriction,
-             ImplicitParams,
-             ExtendedDefaultRules,
-             UnicodeSyntax,
-             DataKinds,
-             TypeApplications,
-             PartialTypeSignatures,
-             AllowAmbiguousTypes
-#-}
-
-module ExprExt where
-
-import Language.Grammars.AspectAG
-import Control.Monad
-import Control.Applicative
-import Data.Proxy
-import GHC.TypeLits
-import Data.Map
-import Data.Maybe
-import Expr
-
-
-type P_Let = 'Prd "p_Let" Nt_Expr
-elet = Label @ P_Let
-
-
-exprLet   = Label @ ('Chi "exprLet"   P_Let ('Left Nt_Expr))
-bodyLet   = Label @ ('Chi "bodyLet"   P_Let ('Left Nt_Expr))
-vlet      = Label @ ('Chi "vlet"      P_Let ('Right ('T String)))
-
-
-aspEval2  = traceAspect (Proxy @ ('Text "eval2"))
-          $ syndefM eval elet (at bodyLet eval) .+: aspEval
-
-
-aspEnv2   =   traceAspect (Proxy @ ('Text "env2"))
-          $   inhdefM env elet exprLet (at lhs env)
-         .+:  inhdefM env elet bodyLet (insert  <$> ter vlet
-                                                <*> at exprLet eval
-                                                <*> at lhs env)
-         .+:  aspEnv
-
-
-asp2 = aspEval2 .:+: aspEnv2
-
-data Expr' = Val' Int
-           | Var' String
-           | Add' Expr' Expr'
-           | Let String Expr' Expr'
-       deriving Show
-
-sem_Expr' asp (Add' l r) = knitAspect add asp
-                           $  leftAdd  .=. sem_Expr' asp l
-                          .*. rightAdd .=. sem_Expr' asp r
-                          .*.  EmptyRec
-sem_Expr' asp (Val' i)   = knitAspect val asp
-                          $ ival  .=. sem_Lit i .*. EmptyRec
-sem_Expr' asp (Var' v)   = knitAspect var asp
-                          $ vname .=. sem_Lit v .*. EmptyRec
-
-sem_Expr' asp (Let v e b) = knitAspect elet asp
-                           $   vlet     .=. sem_Lit v
-                          .*.  exprLet  .=. sem_Expr' asp e
-                          .*.  bodyLet  .=. sem_Expr' asp b
-                          .*.  EmptyRec
-
-evalExpr' e m = sem_Expr' asp2 e (env =. m .*. emptyAtt) #. eval 
-
-exampleExpr' =  Add' (Val' (-9))
-                     (Add' (Var' "x") (Let "x" (Val' 2)
-                                               (Var' "x")))
-exampleEval' =  evalExpr' exampleExpr'
-                          (insert "x" 5 Data.Map.empty)
-
-val_eval'  =  synmodM eval val  $ abs <$> ter ival
-
-
-type P_Abs = 'Prd "p_Abs" Nt_Expr
-eabs = Label @ P_Abs
-type P_App = 'Prd "p_App" Nt_Expr
-eapp = Label @ P_App
-
-tAbs   = Label @ ('Chi "tAbs"   P_Abs ('Left Nt_Expr))
-xAbs   = Label @ ('Chi "xAbs"   P_Abs ('Right ('T String)))
-
-tApp   = Label @ ('Chi "tApp"   P_App ('Left Nt_Expr))
-uApp   = Label @ ('Chi "uApp"   P_App ('Left Nt_Expr))
-
-
-
-appStack = Label @ ('Att "appStack" [Int])
-
-app_eval      = syndefM eval eapp $ at tApp eval
-app_env_t     = inhdefM env eapp tApp $ at lhs env
-app_env_u     = inhdefM env eapp uApp $ at lhs env
-app_appStk_t  = inhdefM appStack eapp tApp
-  $ do u      <- at uApp eval
-       oldStk <- at lhs appStack
-       return (u:oldStk)
-app_appStk_u = inhdefM appStack eapp uApp $ pure []
-
-abs_eval = syndefM eval eabs $ at tAbs eval
-abs_env = inhdefM env eabs tAbs
-  $ do x      <- ter xAbs
-       envi   <- at lhs env
-       st  <- at lhs appStack
-       case st of
-        -- [] -> return envi
-         (s:_) -> return (insert x s envi)
-abs_appStk_t = inhdefM appStack eabs tAbs
-  $ tail <$> at lhs appStack
-
-add_appStk_l  = inhdefM appStack add leftAdd  $ pure []
-add_appStk_r  = inhdefM appStack add rightAdd $ pure []
-
-let_appStk_r = inhdefM appStack elet bodyLet $ pure []
-let_appStk_l = inhdefM appStack elet exprLet $ pure []
-
-(.:+.) = flip (.+:)
-
-aspLam = asp2 .:+. app_env_t .:+. app_env_u .:+. abs_env .:+. app_eval .:+. abs_eval
-  .:+. abs_appStk_t .:+. app_appStk_t .:+. app_appStk_u
-  .:+. let_appStk_l .:+. let_appStk_r .:+. add_appStk_r .:+. add_appStk_l
-
-evalExpr'' e = sem_Expr'' aspLam e ( (appStack =. []) .*. (env =. (Data.Map.empty :: Map String Int )) .*. emptyAtt) #. eval
-
-
-data Expr'' = Val'' Int
-            | Var'' String
-            | Add'' Expr'' Expr''
-            | Let'' String Expr'' Expr''
-            | App Expr'' Expr''
-            | Abs String Expr''
-
-sem_Expr'' asp (Add'' l r) = knitAspect add asp
-                           $  leftAdd  .=. sem_Expr'' asp l
-                          .*. rightAdd .=. sem_Expr'' asp r
-                          .*.  EmptyRec
-sem_Expr'' asp (Val'' i)   = knitAspect val asp
-                         $ ival  .=. sem_Lit i .*. EmptyRec
-sem_Expr'' asp (Var'' v)   = knitAspect var asp
-                         $ vname .=. sem_Lit v .*. EmptyRec
-
-sem_Expr'' asp (Let'' v e b) = knitAspect elet asp
-                          $   vlet     .=. sem_Lit v
-                         .*.  exprLet  .=. sem_Expr'' asp e
-                         .*.  bodyLet  .=. sem_Expr'' asp b
-                         .*.  EmptyRec
-sem_Expr'' asp (Abs x t) = knitAspect eabs asp
-                          $   xAbs   .=. sem_Lit x
-                         .*.  tAbs   .=. sem_Expr'' asp t
-                         .*.  EmptyRec
-sem_Expr'' asp (App t u) = knitAspect eapp asp
-                          $   uApp   .=. sem_Expr'' asp u
-                         .*.  tApp   .=. sem_Expr'' asp t
-                         .*.  EmptyRec
-
-
---evalExpr'' e = sem_Expr'' asp_All e (emptyAtt) #. eval
-
-
-fun = Abs "x" (Var'' "x" `Add''` Val'' 4)
-
-ex1 = fun `App` Val'' 89
-
-f $$ x = App f x
-
-instance Num Expr'' where
-  fromInteger = Val'' . fromIntegral
-
-lam = Abs
-leti = Let''
-v = Var''
-
-
-f = (lam ("x") ((v "x") `Add''` (5 :: Expr'')))
-g = (lam ("y") ((v "y") `Add''` (4::Expr'')))
-
diff --git a/examples/List.hs b/examples/List.hs
deleted file mode 100644
--- a/examples/List.hs
+++ /dev/null
@@ -1,128 +0,0 @@
-{-# LANGUAGE TypeOperators #-}
-
-{-# LANGUAGE
-             TypeFamilies,
-             FlexibleContexts,
-             ScopedTypeVariables,
-             NoMonomorphismRestriction,
-             ImplicitParams,
-             ExtendedDefaultRules,
-             UnicodeSyntax,
-             DataKinds,
-             TypeApplications,
-             PartialTypeSignatures,
-             AllowAmbiguousTypes,
-             RankNTypes,
-             ScopedTypeVariables
-#-}
-
-
-module List where
-
-import Prelude hiding (head, tail, sum, all, length, null, last)
-
-import Language.Grammars.AspectAG
-import Control.Monad
-import Control.Applicative
-import Data.Proxy
-import GHC.TypeLits
-
-type Nt_List = 'NT "List"
-list = Label @ Nt_List
-
-type P_Cons = 'Prd "Cons" Nt_List
-cons = Label @ P_Cons
-
-
-type P_Nil = 'Prd "Nil" Nt_List
-nil = Label @ P_Nil
-
-head :: forall a . Label ('Chi "head" P_Cons ('Right ('T a)))
-head   = Label
-
-tail   = Label @ ('Chi "tail"   P_Cons ('Left Nt_List))
-nilCh :: Label ('Chi "nilCh"  P_Nil  ('Right ('T ())))
-nilCh = Label
-
-
-  -- data List a = Cons a (List a) | Nil () deriving Show
-
-sem_List (proxy :: Proxy a) asp (x:xs)
-  = knitAspect cons asp
-  $    head @ a .=. sem_Lit @ a x
- .*.   tail  .=. sem_List proxy asp xs
- .*.   EmptyRec
-sem_List (_ :: Proxy a) asp []
-  = knitAspect nil asp
-  $ nilCh  .=. sem_Lit () .*. EmptyRec
-
-scata :: forall b . Label ('Att "cata" b)
-scata = Label
-
-asp_cata (Proxy :: Proxy a) f e
-  =   (syndefM (scata @ a) cons $ f <$> ter head <*> at tail (scata @ a))
-  .+: (syndefM (scata @ a) nil $ pure e)
-  .+: emptyAspect
-
-sum :: [Integer] -> Integer
-sum xs
-  = sem_List (Proxy @ Integer)
-    (asp_cata (Proxy @ Integer) (+) 0) xs emptyAtt #. (scata @ Integer)
-
-all xs
-  = sem_List (Proxy @ Bool)
-    (asp_cata (Proxy @ Bool) (&&) True) xs emptyAtt #. (scata @ Bool)
-
-
-cata :: (a -> b -> b) -> b -> [a] -> b
-cata (f :: a -> b -> b) e xs
-  = sem_List (Proxy @ a) (asp_cata (Proxy @ b) f e) xs emptyAtt #. (scata @ b)
-
-
-tyApp :: (forall a. Label ('Att "cata" a)) -> Proxy a
-      -> (Label ('Att "cata" a))
-tyApp poly (Proxy :: Proxy a) = poly @ a
-
-slen = Label @ ('Att "slen" Integer)
-
-asp_slen
-  =   syndefM slen cons ((1+) <$> at tail slen)
-  .+: syndefM slen nil (pure 0) .+: emptyAspect
-
-length xs
-  = sem_List (proxyFrom xs) asp_slen xs emptyAtt #. slen
-
-sempty = Label @ ('Att "sempty" Bool)
-asp_sempty
-  = syndefM sempty cons (pure False) .+: syndefM sempty nil (pure True) .+: emptyAspect
-
-null xs = sem_List (proxyFrom xs) asp_sempty xs emptyAtt #. sempty
-
-sid :: forall a . Label ('Att "sid" [a]) ; sid = Label
-
-asp_sid
-  = \(Proxy :: Proxy a)
-    ->   syndefM (sid @ a) cons ((:) <$> ter head <*> at tail sid)
-     .+: syndefM (sid @ a) nil (pure []) .+: emptyAspect
-
-idList (xs :: [a])
-  = sem_List (proxyFrom xs) (asp_sid (proxyFrom xs)) xs emptyAtt #. (sid @ a) -- TODO
--- Si queremos evitar anotar tipos, los atributos polimorficos pueden tomar un proxy como
--- parametro, y usar proxyFrom
-
-
-
-slast :: forall a . Label ('Att "slast" a); slast = Label
-asp_slast (Proxy :: Proxy a)
-  = syndefM (slast @ a) cons (
-    do isLast <- at tail sempty
-       case isLast of
-         True  -> ter head
-         False -> at tail slast
-    )
-   .+: syndefM (slast @ a) nil (error "Exception: empty list")
-   .+: emptyAspect
-
-last (xs :: [a])
-  = sem_List (proxyFrom xs) (asp_slast (proxyFrom xs) .:+: asp_sempty)
-    xs emptyAtt #. slast @ a
diff --git a/examples/RepminTH.lhs b/examples/RepminTH.lhs
deleted file mode 100644
--- a/examples/RepminTH.lhs
+++ /dev/null
@@ -1,117 +0,0 @@
-
-
-
-
-To use AspectAG in a module, some extensions must be enabled,
-otherwise type errors we won't have readable type errors.
-
-
-> {-# LANGUAGE TemplateHaskell #-}
-> {-# LANGUAGE FlexibleContexts  #-}
-> {-# LANGUAGE GADTs #-}
-> {-# LANGUAGE TypeFamilies #-}
-
-> {-# LANGUAGE AllowAmbiguousTypes #-}
-> {-# LANGUAGE NoMonomorphismRestriction #-}
-> {-# LANGUAGE DataKinds #-}
-
-> {-# LANGUAGE FlexibleInstances #-}
-> {-# LANGUAGE MultiParamTypeClasses #-}
-> {-# LANGUAGE TypeApplications #-}
-
-
-> module RepminTH where
-
-> import Language.Grammars.AspectAG
-> import Language.Grammars.AspectAG.TH
-
-
-To add a nonterminal we can use the TH function |addNont|:
-
-> $(addNont "Root")
-> $(addNont "Tree")
-
-The produce the following code:
-
-< type Nt_Root = NT "Root"
-< nt_Root = Label :: Label Nt_Root
-
-< type Nt_Tree = NT "Tree"
-< nt_Tree = Label :: Label (Nt_Tree)
-
-
-After, we generate productions:
-
-
-> $(addProd "Leaf" ''Nt_Tree [("val", Ter ''Int)])
-> $(addProd "Node" ''Nt_Tree [("l", NonTer ''Nt_Tree),("r", NonTer ''Nt_Tree)])
-> $(addProd "Root" ''Nt_Root [("tree",NonTer ''Nt_Tree)])
-
-
-Semantic functions and a datatype by hand (for now)
-
-> data Root = Root Tree deriving Show
-> data Tree = Leaf Int | Node Tree Tree deriving Show
-
-
-> sem_Root asp (Root t)
->  = knitAspect p_Root asp $ ch_tree .=. sem_Tree asp t .*. EmptyRec
-
-> sem_Tree asp (Leaf i)
->  = knitAspect p_Leaf asp $ ch_val .=. sem_Lit i .*. EmptyRec
-> sem_Tree asp (Node l r)
->  = knitAspect p_Node asp
->  $   ch_l .=. sem_Tree asp l
->  .*. ch_r .=. sem_Tree asp r
->  .*. EmptyRec
-
-
-> $(attLabels [("sres", ''Tree), ("smin", ''Int), ("ival", ''Int)])
-
-> asp_smin
->  =   syn smin p_Node (min @ Int <$> at ch_l smin <*> at ch_r smin)
->  .+: syn smin p_Leaf (ter ch_val)
->  .+: emptyAspect
-
-> asp_sres
->  =    syn sres p_Node (Node <$> at ch_l sres <*> at ch_r sres)
->  .+:  syn sres p_Leaf (Leaf <$> at lhs ival)
->  .+:  syn sres p_Root (at ch_tree sres)
->  .+:  emptyAspect
-
-> asp_ival
->  =    inh ival p_Root ch_tree (at ch_tree smin)
->  .+:  inh ival p_Node ch_l (at lhs ival)
->  .+:  inh ival p_Node ch_r (at lhs ival)
->  .+:  emptyAspect
-
-> asp_repmin
->   = asp_smin .:+: asp_sres .:+: asp_ival
-
-> repmin t
->   = sem_Root asp_repmin (Root t)
->          emptyAtt #. sres
-
-
-Another way to build  semantic functions:
-
-> semRoot_Root asp tree
->  = knitAspect p_Root asp
->  $ ch_tree .=. tree .*. EmptyRec
-
-> semTree_Node asp l r
->  = knitAspect p_Node asp
->  $    ch_l .=. l
->  .*.  ch_r .=. r
->  .*.  EmptyRec
-
-> semTree_Leaf asp i
->  = knitAspect p_Leaf asp
->  $ ch_val .=. i .*. EmptyRec
-
-> semR asp (Root t)    = semRoot_Root asp (semT asp t)
-> semT asp (Node l r)  = semTree_Node asp (semT asp l) (semT asp r)
-> semT asp (Leaf i)    = semTree_Leaf asp (sem_Lit i)
-
-
-> repmin' t = semR asp_repmin (Root t) emptyAtt #. sres
diff --git a/examples/RepminTHExt.lhs b/examples/RepminTHExt.lhs
deleted file mode 100644
--- a/examples/RepminTHExt.lhs
+++ /dev/null
@@ -1,69 +0,0 @@
-> {-# LANGUAGE DataKinds #-}
-> {-# LANGUAGE TemplateHaskell #-}
-> {-# LANGUAGE FlexibleContexts  #-}
-> {-# LANGUAGE GADTs #-}
-> {-# LANGUAGE TypeFamilies #-}
-
-> {-# LANGUAGE AllowAmbiguousTypes #-}
-> {-# LANGUAGE NoMonomorphismRestriction #-}
-
-
-> {-# LANGUAGE TypeApplications #-}
-
-
-> module RepminTHExt where
-
-> import Language.Grammars.AspectAG
-> import Language.Grammars.AspectAG.TH
-
-> import RepminTH hiding (Tree, semT, Leaf)
-
-Extending the grammar: New production, a ternary node
-
-> $(addProd "Node3" ''Nt_Tree [("l3", NonTer ''Nt_Tree),
->                              ("c3", NonTer ''Nt_Tree),
->                              ("r3", NonTer ''Nt_Tree)])
-
-A support datatype
-
-> data Tree3
->   = Node2 Tree3 Tree3
->   | Node3 Tree3 Tree3 Tree3
->   | Leaf Int
-
-semantic function for the new production
-
-> semTree_Node3 asp l c r
->   =   knitAspect p_Node3 asp
->  $    ch_l3 .=. l
->  .*.  ch_c3 .=. c
->  .*.  ch_r3 .=. r
->  .*.  EmptyRec
-
-> semT asp (Node2 l r)
->   = semTree_Node asp (semT asp l) (semT asp r)
-> semT asp (Node3 l c r)
->   = semTree_Node3 asp (semT asp l) (semT asp c) (semT asp r)
-> semT asp (Leaf i)
->   = semTree_Leaf asp (sem_Lit i)
-
-> asp_repmin3
->  =    syn sres p_Node3 (do x <- at ch_l3 sres
->                            y <- at ch_c3 sres
->                            z <- at ch_r3 sres
->                            return (Node x (Node y z)))
->  .+: syn smin p_Node3 (min3  <$> at ch_l3 smin
->                              <*> at ch_c3 smin
->                              <*> at ch_r3 smin)
->  .+: inh ival p_Node3 ch_l3 (at lhs ival)
->  .+: inh ival p_Node3 ch_c3 (at lhs ival)
->  .+: inh ival p_Node3 ch_r3 (at lhs ival)
->  .+: asp_repmin
->  where min3 a b c = a `min` b `min` c
-
--- TODO: invert arg order
-
-
-> repmin'' t = semR3 asp_repmin3 (Root3 t) emptyAtt #. sres
-> data Root3 = Root3 Tree3
-> semR3 asp (Root3 t) = semRoot_Root asp (semT asp t)
diff --git a/src/Language/Grammars/AspectAG.hs b/src/Language/Grammars/AspectAG.hs
--- a/src/Language/Grammars/AspectAG.hs
+++ b/src/Language/Grammars/AspectAG.hs
@@ -1,12 +1,11 @@
 {-|
 Module      : Language.Grammars.AspectAG
 Description : Main module, First-class attribute grammars
-Copyright   : (c) Juan García Garland, Marcos Viera, 2019
+Copyright   : (c) Juan García-Garland, Marcos Viera, 2019, 2020
 License     : GPL
 Maintainer  : jpgarcia@fing.edu.uy
 Stability   : experimental
 Portability : POSIX
-
 -}
 
 {-# LANGUAGE PolyKinds                 #-}
@@ -30,29 +29,73 @@
 {-# LANGUAGE PartialTypeSignatures     #-}
 {-# LANGUAGE IncoherentInstances       #-}
 {-# LANGUAGE AllowAmbiguousTypes       #-}
+{-# LANGUAGE UnicodeSyntax             #-}
 
-module Language.Grammars.AspectAG (
-              module Language.Grammars.AspectAG,
-              module Language.Grammars.AspectAG.HList,
-              module Language.Grammars.AspectAG.GenRecord,
-              module Language.Grammars.AspectAG.RecordInstances,
-              module Language.Grammars.AspectAG.TPrelude
-            ) where
+module Language.Grammars.AspectAG
+  (
 
+    -- * Rules
+    Rule, CRule(..),
+    
+    -- ** Defining Rules
+    syndef, syndefM, syn,
+    
+    synmod, synmodM,
 
-import Language.Grammars.AspectAG.HList
-import Data.Kind
-import Language.Grammars.AspectAG.TPrelude
-import Data.Proxy
 
+    inh, inhdef, inhdefM,
 
+    inhmod, inhmodM, 
+
+    emptyRule,
+    emptyRuleAtPrd,
+    ext,
+    
+    -- * Aspects 
+    -- ** Building Aspects.
+    
+    emptyAspect,
+    singAsp,
+    extAspect,
+    comAspect,
+    (.+:),(◃),
+    (.:+.),(▹),
+    (.:+:),(⋈),
+    
+    
+    CAspect(..),
+    Label(Label), Prod(..), T(..), NT(..), Child(..), Att(..),
+    (.#), (#.), (=.), (.=), (.*), (*.),
+    emptyAtt,
+    ter,
+    at, lhs,
+    sem_Lit,
+    knitAspect,
+    traceAspect,
+    traceRule,
+    copyAtChi,
+    use,
+    emptyAspectC,
+    emptyAspectForProds,
+    module Data.GenRec,
+    module Language.Grammars.AspectAG.HList
+  )
+  where
+
+
+import Language.Grammars.AspectAG.HList
 import Language.Grammars.AspectAG.RecordInstances
-import Language.Grammars.AspectAG.Require
-import Language.Grammars.AspectAG.GenRecord
+
+import Data.Type.Require hiding (emptyCtx)
+
+import Data.GenRec
+import Data.GenRec.Label
+
+import Data.Kind
+import Data.Proxy
 import GHC.TypeLits
 
 import Data.Maybe
-import GHC.Types
 import Data.Type.Equality
 import Control.Monad.Reader
 
@@ -68,7 +111,8 @@
 -- * Families and Rules
 
 -- | In each node of the grammar, the "Fam" contains a single attribution
--- for the parent, and a collection (Record) of attributions for the children:
+-- for the parent, and a collection (Record) of attributions for
+-- the children:
 data Fam (prd :: Prod)
          (c :: [(Child, [(Att, Type)])])
          (p :: [(Att, Type)]) :: Type
@@ -76,18 +120,20 @@
   Fam :: ChAttsRec prd c -> Attribution p -> Fam prd c p
 
 
--- | Getters
+-- | getter
 chi :: Fam prd c p -> ChAttsRec prd c
 chi (Fam c p) = c
 
+-- | getter
 par :: Fam prd c p -> Attribution p
 par (Fam c p) = p
 
+-- | getter (extracts a 'Label')
 prd :: Fam prd c p -> Label prd
 prd (Fam c p) = Label
 
--- | Rules are a function from the input family to the output family.
--- They are indexed by a production.
+-- | Rules are a function from the input family to the output family,
+-- with an extra arity to make them composable.  They are indexed by a production.
 type Rule
   (prd  :: Prod)
   (sc   :: [(Child, [(Att, Type)])])
@@ -98,27 +144,36 @@
   (sp'  :: [(Att,       Type)])
   = Fam prd sc ip -> Fam prd ic sp -> Fam prd ic' sp'
 
--- | Rules with context.
+-- | Rules with context (used to print domain specific type errors).
 newtype CRule (ctx :: [ErrorMessage]) prd sc ip ic sp ic' sp'
   = CRule { mkRule :: (Proxy ctx -> Rule prd sc ip ic sp ic' sp')}
 
+emptyRule =
+  CRule $ \Proxy -> \fam inp -> inp
 
--- * Aspects
+emptyRuleAtPrd :: Label prd -> CRule ctx prd sc ip ic' sp' ic' sp'
+emptyRuleAtPrd Label = emptyRule
 
--- | Context tagged aspects.
+-- | Aspects, tagged with context. 'Aspect' is a record instance having
+-- productions as labels, containing 'Rule's as fields.
 newtype CAspect (ctx :: [ErrorMessage]) (asp :: [(Prod, Type)] )
   = CAspect { mkAspect :: Proxy ctx -> Aspect asp}
 
--- | Empty Aspect.
+-- | Recall that Aspects are mappings from productions to rules. They
+-- have a record-like interface to build them. This is the constructor
+-- for the empty Aspect.
 emptyAspect :: CAspect ctx '[]
 emptyAspect  = CAspect $ const EmptyRec
 
-
--- | combination of Aspects
+-- | combination of two Aspects. It merges them. When both aspects
+-- have rules for a given production, in the resulting Aspect the rule
+-- at that field is the combination of the rules for the arguments
+-- (with 'ext').
 comAspect ::
- ( Require (OpComAsp al ar) ctx
- , ReqR (OpComAsp al ar) ~ Aspect asp)
- =>  CAspect ctx al -> CAspect ctx ar -> CAspect ctx asp
+  ( Require (OpComAsp al ar) ctx
+  , ReqR (OpComAsp al ar) ~ Aspect asp
+  )
+  =>  CAspect ctx al -> CAspect ctx ar -> CAspect ctx asp
 comAspect al ar
   = CAspect $ \ctx -> req ctx (OpComAsp (mkAspect al ctx) (mkAspect ar ctx))
 
@@ -147,10 +202,11 @@
   mapCtxRec :: (Proxy ctx -> Proxy ctx')
             -> Aspect r -> Aspect (ResMapCtx r ctx ctx')
 
-instance ( MapCtxAsp r ctx ctx' 
-         , ResMapCtx r ctx ctx' ~ r'
-         , LabelSetF ('(l, CRule ctx prd sc ip ic sp ic' sp') : r')
-         ~ True) =>
+instance
+  ( MapCtxAsp r ctx ctx' 
+  , ResMapCtx r ctx ctx' ~ r'
+  )
+  =>
   MapCtxAsp ( '(l, CRule ctx' prd sc ip ic sp ic' sp') ': r) ctx ctx' where
   type ResMapCtx ( '(l, CRule ctx' prd sc ip ic sp ic' sp') ': r) ctx ctx'
      =  '(l, CRule ctx prd sc ip ic sp ic' sp') ':  ResMapCtx r ctx ctx'
@@ -163,108 +219,190 @@
      =  '[]
   mapCtxRec _ EmptyRec = EmptyRec
 
+
+-- | The "cons" for 'CAspect's. It adds a 'Rule' `rule`
+-- to a 'CAspect'. If there is no rule for that production in the
+-- argument it is a record extension. If the production is there, the
+-- rules are combined.
 extAspect
-  :: RequireR (OpComRA ctx prd sc ip ic sp ic' sp' a) ctx (Aspect asp)
-  => CRule ctx prd sc ip ic sp ic' sp'
+  :: ExtAspect ctx prd sc ip ic sp ic' sp' a asp =>
+     CRule ctx prd sc ip ic sp ic' sp'
      -> CAspect ctx a -> CAspect ctx asp
 extAspect rule (CAspect fasp)
   = CAspect $ \ctx -> req ctx (OpComRA rule (fasp ctx))
 
+type ExtAspect ctx prd sc ip ic sp ic' sp' a asp
+  = (Require
+        (OpComRA ctx prd (CRule ctx prd sc ip ic sp ic' sp') a) ctx,
+      ReqR (OpComRA ctx prd (CRule ctx prd sc ip ic sp ic' sp') a)
+      ~ Rec PrdReco asp) 
+
+-- | An operator, alias for 'extAspect'. It combines a rule with an
+-- aspect, to build a bigger one.
 (.+:) = extAspect
 infixr 3 .+:
 
+-- | Unicode version of 'extAspect' or '.+:' (\\triangleleft)
+(◃) = extAspect
+infixr 3 ◃
+
+-- | The other way, combines an aspect with a rule. It is a `flip`ped
+-- 'extAspect'.
 (.:+.) = flip extAspect
 infixl 3 .:+.
 
+-- | Unicode operator for '.:+.' or `flip extAspect`.
+(▹) = flip extAspect
+infixl 3 ▹
+
+
+-- | Operator for 'comAspect'. It takes two 'CAspect's to build the
+-- combination of both.
 (.:+:) = comAspect
 infixr 4 .:+:
 
-data OpComAsp  (al :: [(Prod, Type)])
-               (ar :: [(Prod, Type)]) where
-  OpComAsp :: Aspect al -> Aspect ar -> OpComAsp al ar
+-- | Unicode operator for 'comAspect' or '.:+:'. (\\bowtie)
+(⋈) = comAspect
+infixr 4 ⋈
 
-instance Require (OpComAsp al '[]) ctx where
-  type ReqR (OpComAsp al '[]) = Aspect al
-  req ctx (OpComAsp al _) = al
+ext' ::  CRule ctx prd sc ip ic sp ic' sp'
+     ->  CRule ctx prd sc ip a b ic sp
+     ->  CRule ctx prd sc ip a b ic' sp'
+(CRule f) `ext'` (CRule g)
+ = CRule $ \ctx input -> f ctx input . g ctx input
 
-instance
-  ( RequireR (OpComAsp al ar) ctx  (Aspect ar')
-  , Require  (OpComRA ctx prd sc ip ic sp ic' sp' ar') ctx
-  )
-  => Require (OpComAsp al
-       ( '(prd, CRule ctx prd sc ip ic sp ic' sp') ': ar)) ctx where
-  type ReqR (OpComAsp al
-       ( '(prd, CRule ctx prd sc ip ic sp ic' sp') ': ar))
-    = ReqR (OpComRA ctx prd sc ip ic sp ic' sp'
-            (UnWrap (ReqR (OpComAsp al ar))))
-  req ctx (OpComAsp al (ConsRec prdrule ar))
-   = req ctx (OpComRA (untagField prdrule)
-                      (req ctx (OpComAsp al ar)))
 
+-- | Given two rules for a given (the same) production, it combines
+-- them. Note that the production equality is visible in the context,
+-- not sintactically. This is a use of the 'Require' pattern.
+ext ::  RequireEq prd prd' (Text "ext":ctx) 
+     => CRule ctx prd sc ip ic sp ic' sp'
+     -> CRule ctx prd' sc ip a b ic sp
+     -> CRule ctx prd sc ip a b ic' sp'
+ext = ext'
 
-data OpComRA  (ctx  :: [ErrorMessage])
-              (prd  :: Prod)
-              (sc   :: [(Child, [(Att, Type)])])
-              (ip   :: [(Att, Type)])
-              (ic   :: [(Child, [(Att, Type)])])
-              (sp   :: [(Att, Type)])
-              (ic'  :: [(Child, [(Att, Type)])])
-              (sp'  :: [(Att, Type)])
-              (a     :: [(Prod, Type)])  where
+-- | Singleton Aspect. Wraps a rule to build an Aspect from it.
+singAsp r
+  = r .+: emptyAspect
+
+infixr 6 .+.
+(.+.) = ext
+
+-- | combine a rule with an aspect (wrapper)
+data OpComRA (ctx  :: [ErrorMessage])
+             (prd  :: Prod)
+             (rule :: Type) -- TODO : doc this
+             (a    :: [(Prod, Type)]) where
   OpComRA :: CRule ctx prd sc ip ic sp ic' sp'
-          -> Aspect a -> OpComRA ctx prd sc ip ic sp ic' sp' a
+          -> Aspect a -> OpComRA ctx prd (CRule ctx prd sc ip ic sp ic' sp') a
 
-data OpComRA' (b :: Bool)
+-- | combine a rule with an aspect (inner)
+data OpComRA' (cmp  :: Ordering)
               (ctx  :: [ErrorMessage])
               (prd  :: Prod)
-              (sc   :: [(Child, [(Att, Type)])])
-              (ip   :: [(Att, Type)])
-              (ic   :: [(Child, [(Att, Type)])])
-              (sp   :: [(Att, Type)])
-              (ic'  :: [(Child, [(Att, Type)])])
-              (sp'  :: [(Att, Type)])
-              (a     :: [(Prod, Type)])  where
-  OpComRA' :: Proxy b -> CRule ctx prd sc ip ic sp ic' sp'
-          -> Aspect a -> OpComRA' b ctx  prd sc ip ic sp ic' sp' a
+              (rule :: Type) -- TODO : doc this
+              (a    :: [(Prod, Type)]) where
+  OpComRA' :: Proxy cmp
+           -> CRule ctx prd sc ip ic sp ic' sp'
+           -> Aspect a
+           -> OpComRA' cmp ctx prd (CRule ctx prd sc ip ic sp ic' sp') a
 
+cRuleToTagField :: (CRule ctx prd sc ip ic sp ic' sp')
+                -> TagField PrdReco prd (CRule ctx prd sc ip ic sp ic' sp')
+cRuleToTagField =
+  TagField Label Label
 
 instance
- (Require (OpComRA' (HasLabel prd a) ctx prd sc ip ic sp ic' sp' a) ctx)
-  => Require (OpComRA ctx prd sc ip ic sp ic' sp' a) ctx where
-  type ReqR (OpComRA ctx prd sc ip ic sp ic' sp' a)
-     = ReqR (OpComRA' (HasLabel prd a) ctx prd sc ip ic sp ic' sp' a)
-  req ctx (OpComRA rule a)
-     = req ctx (OpComRA' (Proxy @ (HasLabel prd a)) rule a)
+  Require (OpComRA ctx prd (CRule ctx prd sc ip ic sp ic' sp') '[]) ctx where
+  type ReqR (OpComRA ctx prd (CRule ctx prd sc ip ic sp ic' sp') '[]) =
+    Aspect '[ '(prd, CRule ctx prd sc ip ic sp ic' sp')]
+  req ctx (OpComRA rule EmptyRec) =
+    ConsRec (cRuleToTagField rule) EmptyRec
 
 instance
-  (Require (OpExtend PrdReco prd (CRule ctx prd sc ip ic sp ic' sp') a)) ctx
-  => Require (OpComRA' 'False ctx prd sc ip ic sp ic' sp' a) ctx where
-  type ReqR (OpComRA' 'False ctx prd sc ip ic sp ic' sp' a)
-    = ReqR (OpExtend PrdReco prd (CRule ctx prd sc ip ic sp ic' sp') a)
-  req ctx (OpComRA' _ (rule :: CRule ctx prd sc ip ic sp ic' sp') asp)
-    = req ctx (OpExtend (Label @ prd) rule asp)
+  Require (OpComRA' (Cmp prd prd') ctx prd rule ( '(prd', rule') ': asp )) ctx
+  =>
+  Require (OpComRA ctx prd rule ( '(prd', rule') ': asp )) ctx where
+  type ReqR (OpComRA ctx prd rule ( '(prd', rule') ': asp )) =
+    ReqR (OpComRA' (Cmp prd prd') ctx prd rule ( '(prd', rule') ': asp ))
+  req ctx (OpComRA rule asp) =
+    req ctx (OpComRA' (Proxy @ (Cmp prd prd')) rule asp)
 
 instance
- ( Require (OpUpdate PrdReco prd (CRule ctx prd sc ip ic sp ic'' sp'') a) ctx
- , RequireR (OpLookup PrdReco prd a) ctx (CRule ctx prd sc ip ic sp ic' sp') 
- , (IC (ReqR (OpLookup PrdReco prd a))) ~ ic
- , (SP (ReqR (OpLookup PrdReco prd a))) ~ sp
- ) =>
-  Require (OpComRA' 'True ctx prd sc ip ic' sp' ic'' sp'' a) ctx where
-  type ReqR (OpComRA' 'True ctx prd sc ip ic' sp' ic'' sp'' a)
-    = ReqR (OpUpdate PrdReco prd
-           (CRule ctx prd sc ip
+  ( Require (OpUpdate PrdReco prd (CRule ctx prd sc ip ic sp ic'' sp'') a) ctx
+  , Require (OpLookup PrdReco prd a) ctx
+  , ReqR (OpLookup PrdReco prd a) ~ CRule ctx prd sc ip ic sp ic' sp'
+  , (IC (ReqR (OpLookup PrdReco prd a))) ~ ic
+  , (SP (ReqR (OpLookup PrdReco prd a))) ~ sp
+  ) =>
+  Require
+   (OpComRA' 'EQ ctx prd (CRule ctx prd sc ip ic' sp' ic'' sp'') a) ctx where
+  type ReqR (OpComRA' 'EQ ctx prd (CRule ctx prd sc ip ic' sp' ic'' sp'') a) =
+    ReqR (OpUpdate PrdReco prd
+            (CRule ctx prd sc ip
              (IC (ReqR (OpLookup PrdReco prd a)))
              (SP (ReqR (OpLookup PrdReco prd a)))
             ic'' sp'') a)
-  req ctx (OpComRA' _ rule asp)
-    = let prd     = Label @ prd
-          oldRule = req ctx (OpLookup prd asp)
-          newRule = rule `ext` oldRule
-      in  req ctx (OpUpdate prd newRule asp)
+  req ctx (OpComRA' _ crule asp) =
+    let prd     = Label @ prd
+        oldRule = req ctx (OpLookup prd asp)
+        newRule = crule `ext` oldRule
+    in  req ctx (OpUpdate prd newRule asp)
 
+instance
+  ( Require (OpComRA ctx prd rule asp) ctx
+  -- , ReqR (OpComRA ctx prd rule asp) ~ Rec
+  --                           PrdReco
+  --                           (UnWrap
+  --                              (ReqR (OpComRA ctx prd (CRule ctx prd sc ip ic sp ic' sp') asp)))
+  , ReqR (OpComRA ctx prd rule asp) ~ Aspect a0
+  )
+  =>
+  Require (OpComRA' 'GT ctx prd rule ( '(prd' , rule') ': asp)) ctx where
+  type ReqR (OpComRA' 'GT ctx prd rule ( '(prd' , rule') ': asp)) =
+    Aspect ( '(prd' , rule') ': UnWrap (ReqR (OpComRA ctx prd rule asp)))
+  req ctx (OpComRA' _ crule (ConsRec crule' asp)) =
+    ConsRec crule' $ req ctx (OpComRA crule asp)
 
+instance 
+  Require (OpComRA' 'LT ctx prd rule ( '(prd' , rule') ': asp)) ctx where
+  type ReqR (OpComRA' 'LT ctx prd rule ( '(prd' , rule') ': asp)) =
+    Aspect ( '(prd, rule) ': '(prd' , rule') ': asp)
+  req ctx (OpComRA' _ crule asp) =
+    ConsRec (TagField Label Label crule) asp
 
+
+
+
+data OpComAsp  (al :: [(Prod, Type)])
+               (ar :: [(Prod, Type)]) where
+  OpComAsp :: Aspect al -> Aspect ar -> OpComAsp al ar
+
+instance
+  Require (OpComAsp '[] ar) ctx where
+  type ReqR (OpComAsp '[] ar) = Aspect ar
+  req ctx (OpComAsp _ ar) = ar
+
+instance
+ ( (ReqR (OpComRA ctx prd (CRule ctx prd sc ip ic sp ic' sp') ar))
+   ~ (Rec PrdReco
+    (UnWrap
+      (ReqR (OpComRA ctx prd (CRule ctx prd sc ip ic sp ic' sp') ar))))
+ , ReqR (OpComRA ctx prd (CRule ctx prd sc ip ic sp ic' sp') ar)
+   ~ Rec PrdReco ar0
+ , (Require (OpComAsp al ar0) ctx)
+ , (Require
+     (OpComRA ctx prd (CRule ctx prd sc ip ic sp ic' sp') ar) ctx)
+ ) =>
+  Require (OpComAsp
+           ('(prd, CRule ctx prd sc ip ic sp ic' sp') ': al) ar) ctx where
+  type ReqR (OpComAsp ('(prd, CRule ctx prd sc ip ic sp ic' sp') ': al) ar) =
+    ReqR (OpComAsp al
+      (UnWrap (ReqR
+                (OpComRA ctx prd (CRule ctx prd sc ip ic sp ic' sp') ar))))
+  req ctx (OpComAsp (ConsRec (TagField _ _ rul) al) ar)
+    = req ctx (OpComAsp al (req ctx (OpComRA rul ar)))
+
 type family IC (rule :: Type) where
   IC (Rule prd sc ip ic sp ic' sp') = ic
   IC (CRule ctx prd sc ip ic sp ic' sp') = ic
@@ -272,38 +410,64 @@
   SP (Rule prd sc ip ic sp ic' sp') = sp
   SP (CRule ctx prd sc ip ic sp ic' sp') = sp
 
-syndef
-  :: ( RequireEq t t' ctx'
+
+type family Syndef t t' ctx ctx' att sp sp' prd :: Constraint where
+  Syndef t t' ctx ctx' att sp sp' prd =
+     ( RequireEq t t' ctx'
      , RequireR (OpExtend AttReco ('Att att t) t sp) ctx (Attribution sp')
      , ctx'
          ~ ((Text "syndef("
-             :<>: ShowT ('Att att t) :<>: Text ", "
-             :<>: ShowT prd :<>: Text ")") ': ctx)
+             :<>: ShowTE ('Att att t) :<>: Text ", "
+             :<>: ShowTE prd :<>: Text ")") ': ctx)
      )
-     => Label ('Att att t)
-     -> Label prd
-     -> (Proxy ctx' -> Fam prd sc ip -> t')
-     -> CRule ctx prd sc ip ic sp ic sp'
+
+-- | The function 'syndef' adds the definition of a synthesized
+--   attribute.  It takes an attribute label 'att' representing the
+--   name of the new attribute; a production label 'prd' representing
+--   the production where the rule is defined; a value 't'' to be
+--   assigned to this attribute, given a context and an input
+--   family. It updates the output constructed thus far.
+syndef
+  :: Syndef t t' ctx ctx' att sp sp' prd
+  => forall sc ip ic . Label ('Att att t)
+  -> Label prd
+  -> (Proxy ctx' -> Fam prd sc ip -> t')
+  -> CRule ctx prd sc ip ic sp ic sp'
 syndef att prd f
   = CRule $ \ctx inp (Fam ic sp)
    ->  Fam ic $ req ctx (OpExtend att (f Proxy inp) sp)
 
-
+-- | As 'syndef', the function 'syndefM' adds the definition of a
+--   synthesized attribute.  It takes an attribute label 'att'
+--   representing the name of the new attribute; a production label
+--   'prd' representing the production where the rule is defined; a
+--   value 't'' to be assigned to this attribute, given a context and
+--   an input family. It updates the output constructed thus far. This
+--   function captures the monadic behaviour of the family
+--   updating. For instance, the following definition specifies a rule
+--   for an attribute `att_size :: Label (Att "size" Int)` at the
+--   prduction `p_cons :: Label (Prd "cons" (NT "List"))`. The value
+--   is computed from the very same attribute value at a child
+--   `ch_tail :: Chi "tail" (Prd "cons" (NT "List") (Left NT))`
+--
+-- @
+-- foo = syndefM att_size p_cons $ do sizeatchi <- at ch_tail att_size
+--                                    return (sizeatchi + 1)
+-- @
 syndefM
-  :: ( RequireEq t t' ctx'
-     , RequireR (OpExtend AttReco ('Att att t) t sp) ctx (Attribution sp')
-     , ctx'
-         ~ ((Text "syndef("
-             :<>: ShowT ('Att att t) :<>: Text ", "
-             :<>: ShowT prd :<>: Text ")") ': ctx)
-     )
-     => Label ('Att att t)
-     -> Label prd
-     -> Reader (Proxy ctx', Fam prd sc ip) t'
-     -> CRule ctx prd sc ip ic sp ic sp'
+  :: Syndef t t' ctx ctx' att sp sp' prd
+  => Label ('Att att t)
+  -> Label prd
+  -> Reader (Proxy ctx', Fam prd sc ip) t'
+  -> CRule ctx prd sc ip ic sp ic sp'
 syndefM att prd = syndef att prd . def
 
+
+-- | This is simply an alias for 'syndefM'
 syn = syndefM
+
+
+-- | This is simply an alias for 'inhdefM'
 inh = inhdefM
 
 
@@ -312,8 +476,8 @@
   => Label ('Att att t)
      -> Label prd
      -> (Proxy
-           ((('Text "synmod(" ':<>: ShowT ('Att att t)) :<>: Text ", "
-                              ':<>: ShowT prd :<>: Text ")")
+           ((('Text "synmod(" ':<>: ShowTE ('Att att t)) :<>: Text ", "
+                              ':<>: ShowTE prd :<>: Text ")")
               : ctx)
          -> Fam prd sc ip -> t)
      -> CRule ctx prd sc ip ic' r ic' sp'
@@ -326,8 +490,8 @@
   :: RequireR (OpUpdate AttReco ('Att att t) t r) ctx (Attribution sp')
   => Label ('Att att t)
      -> Label prd
-     -> Reader ( Proxy ((('Text "synmod(" ':<>: ShowT ('Att att t)) :<>: Text ", "
-                                          ':<>: ShowT prd :<>: Text ")")
+     -> Reader ( Proxy ((('Text "synmod(" ':<>: ShowTE ('Att att t)) :<>: Text ", "
+                                          ':<>: ShowTE prd :<>: Text ")")
                        : ctx)
                , Fam prd sc ip)
                t
@@ -335,28 +499,33 @@
 synmodM att prd = synmod att prd . def
 
 
+type family Inhdef t t' ctx ctx' att r v2 prd nt chi ntch ic ic' n where
+  Inhdef t t' ctx ctx' att r v2 prd nt chi ntch ic ic' n =
+    ( RequireEq t t' ctx'
+    , RequireR  (OpExtend AttReco ('Att att t) t r) ctx (Attribution v2)
+    , RequireR (OpUpdate (ChiReco ('Prd prd nt))
+                 ('Chi chi ('Prd prd nt) ntch) v2 ic) ctx
+                 (ChAttsRec ('Prd prd nt) ic')
+    , RequireR (OpLookup (ChiReco ('Prd prd nt))
+                 ('Chi chi ('Prd prd nt) ntch) ic) ctx
+                 (Attribution r)
+    , RequireEq ntch ('Left n) ctx'
+    , ctx' ~ ((Text "inhdef("
+                :<>: ShowTE ('Att att t)  :<>: Text ", "
+                :<>: ShowTE ('Prd prd nt) :<>: Text ", "
+                :<>: ShowTE ('Chi chi ('Prd prd nt) ntch) :<>: Text ")")
+                ': ctx)
+    )
+  
 
 inhdef
-  :: ( RequireEq t t' ctx'
-     , RequireR  (OpExtend AttReco ('Att att t) t r) ctx (Attribution v2)
-     , RequireR (OpUpdate (ChiReco ('Prd prd nt))
-                ('Chi chi ('Prd prd nt) ntch) v2 ic) ctx
-                (ChAttsRec ('Prd prd nt) ic')
-     , RequireR (OpLookup (ChiReco ('Prd prd nt))
-                ('Chi chi ('Prd prd nt) ntch) ic) ctx
-                (Attribution r)
-     , RequireEq ntch ('Left n) ctx'
-     , ctx' ~ ((Text "inhdef("
-                :<>: ShowT ('Att att t)  :<>: Text ", "
-                :<>: ShowT ('Prd prd nt) :<>: Text ", "
-                :<>: ShowT ('Chi chi ('Prd prd nt) ntch) :<>: Text ")")
-                ': ctx))
+  :: Inhdef t t' ctx ctx' att r v2 prd nt chi ntch ic ic' n
      =>
      Label ('Att att t)
      -> Label ('Prd prd nt)
      -> Label ('Chi chi ('Prd prd nt) ntch)
      -> (Proxy ctx' -> Fam ('Prd prd nt) sc ip -> t')
-     -> CRule ctx ('Prd prd nt) sc ip ic sp ic' sp
+     -> forall sp . CRule ctx ('Prd prd nt) sc ip ic sp ic' sp
 inhdef  att prd chi f
   = CRule $ \ctx inp (Fam ic sp)
        -> let ic'   = req ctx (OpUpdate chi catts' ic)
@@ -367,27 +536,13 @@
 
 
 inhdefM
-  :: ( RequireEq t t' ctx'
-     -- , RequireR  (OpExtend AttReco ('Att att t) t r) ctx (Attribution v2)
-     , RequireR  (OpExtend' (LabelSetF ('( 'Att att t, t) : r)) AttReco ('Att att t) t r) ctx (Attribution v2)
-     , RequireR (OpUpdate (ChiReco ('Prd prd nt))
-                ('Chi chi ('Prd prd nt) ntch) v2 ic) ctx
-                (ChAttsRec ('Prd prd nt) ic')
-     , RequireR (OpLookup (ChiReco ('Prd prd nt))
-                ('Chi chi ('Prd prd nt) ntch) ic) ctx
-                (Attribution r)
-     , RequireEq ntch ('Left n) ctx'
-     , ctx' ~ ((Text "inhdef("
-                :<>: ShowT ('Att att t')  :<>: Text ", "
-                :<>: ShowT ('Prd prd nt) :<>: Text ", "
-                :<>: ShowT ('Chi chi ('Prd prd nt) ntch) :<>: Text ")")
-                ': ctx))
-     =>
-     Label ('Att att t)
-     -> Label ('Prd prd nt)
-     -> Label ('Chi chi ('Prd prd nt) ntch)
-     -> Reader (Proxy ctx', Fam ('Prd prd nt) sc ip) t'
-     -> CRule ctx ('Prd prd nt) sc ip ic sp ic' sp 
+  :: Inhdef t t' ctx ctx' att r v2 prd nt chi ntch ic ic' n
+  =>
+  Label ('Att att t)
+  -> Label ('Prd prd nt)
+  -> Label ('Chi chi ('Prd prd nt) ntch)
+  -> Reader (Proxy ctx', Fam ('Prd prd nt) sc ip) t'
+  -> CRule ctx ('Prd prd nt) sc ip ic sp ic' sp
 inhdefM att prd chi = inhdef att prd chi . def
 
 
@@ -405,9 +560,9 @@
                 (Attribution r)
      , RequireEq ntch ('Left n) ctx'
      , ctx' ~ ((Text "inhmod("
-                :<>: ShowT ('Att att t)  :<>: Text ", "
-                :<>: ShowT ('Prd prd nt) :<>: Text ", "
-                :<>: ShowT ('Chi chi ('Prd prd nt) ntch) :<>: Text ")")
+                :<>: ShowTE ('Att att t)  :<>: Text ", "
+                :<>: ShowTE ('Prd prd nt) :<>: Text ", "
+                :<>: ShowTE ('Chi chi ('Prd prd nt) ntch) :<>: Text ")")
                 ': ctx))
      =>
      Label ('Att att t)
@@ -435,9 +590,9 @@
                 (Attribution r)
      , RequireEq ntch ('Left n) ctx'
      , ctx' ~ ((Text "inhmod("
-                :<>: ShowT ('Att att t)  :<>: Text ", "
-                :<>: ShowT ('Prd prd nt) :<>: Text ", "
-                :<>: ShowT ('Chi chi ('Prd prd nt) ntch) :<>: Text ")")
+                :<>: ShowTE ('Att att t)  :<>: Text ", "
+                :<>: ShowTE ('Prd prd nt) :<>: Text ", "
+                :<>: ShowTE ('Chi chi ('Prd prd nt) ntch) :<>: Text ")")
                 ': ctx))
      =>
      Label ('Att att t)
@@ -447,23 +602,6 @@
      -> CRule ctx ('Prd prd nt) sc ip ic sp ic' sp
 inhmodM att prd chi = inhmod att prd chi . def
 
-ext' ::  CRule ctx prd sc ip ic sp ic' sp'
-     ->  CRule ctx prd sc ip a b ic sp
-     ->  CRule ctx prd sc ip a b ic' sp'
-(CRule f) `ext'` (CRule g)
- = CRule $ \ctx input -> f ctx input . g ctx input
-
-ext ::  RequireEq prd prd' (Text "ext":ctx) 
-     => CRule ctx prd sc ip ic sp ic' sp'
-     -> CRule ctx prd' sc ip a b ic sp
-     -> CRule ctx prd sc ip a b ic' sp'
-ext = ext'
-
-
-infixr 6 .+.
-(.+.) = ext
-
-
 data Lhs
 lhs :: Label Lhs
 lhs = Label
@@ -533,8 +671,8 @@
 
 instance ( lch ~ 'Chi l prd nt
          , Kn fc prd
-         , LabelSet ('(lch, sch) : SCh fc)
-         , LabelSet ('(lch, ich) : ICh fc)
+         -- , LabelSet ('(lch, sch) : SCh fc)
+         -- , LabelSet ('(lch, ich) : ICh fc)
          ) =>
   Kn ( '(lch , Attribution ich -> Attribution sch) ': fc) prd where
   type ICh ( '(lch , Attribution ich -> Attribution sch) ': fc)
@@ -542,28 +680,29 @@
   type SCh ( '(lch , Attribution ich -> Attribution sch) ': fc)
     = '(lch , sch) ': SCh fc
   kn ((ConsRec (TagField _ lch fch) (fcr :: Record fc)))
-   = \((ConsCh pich icr) :: ChAttsRec prd ( '(lch, ich) ': ICh fc))
+   = \((ConsRec pich icr) :: ChAttsRec prd ( '(lch, ich) ': ICh fc))
    -> let scr = kn fcr icr
           ich = unTaggedChAttr pich
-      in ConsCh (TaggedChAttr lch
+      in ConsRec (TaggedChAttr lch
                (fch ich)) scr
 
 
 
 emptyCtx = Proxy @ '[]
 
-knit' :: ( Kn fc prd
-        , Empties fc prd)
- => CRule '[] prd (SCh fc) ip (EmptiesR fc) '[] (ICh fc) sp
+knit'
+  :: ( Kn fc prd
+     , Empties fc prd)
+  => CRule '[] prd (SCh fc) ip (EmptiesR fc) '[] (ICh fc) sp
   -> Record fc -> Attribution ip -> Attribution sp
 knit' (rule :: CRule '[] prd (SCh fc) ip
               (EmptiesR fc) '[] (ICh fc) sp)
-              (fc :: Record fc) ip
-  = let (Fam ic sp) = mkRule rule emptyCtx
-                       (Fam sc ip) (Fam ec emptyAtt)
-        sc          = kn fc ic
-        ec          = empties fc
-    in  sp
+              (fc :: Record fc) ip =
+  let (Fam ic sp) = mkRule rule emptyCtx
+                    (Fam sc ip) (Fam ec emptyAtt)
+      sc          = kn fc ic
+      ec          = empties fc
+  in  sp
 
 
 class Empties (fc :: [(Child,Type)]) (prd :: Prod) where
@@ -574,16 +713,19 @@
   type EmptiesR '[] = '[]
   empties _ = emptyCh
 
-instance ( Empties fcr prd
-         , chi ~ 'Chi ch prd nt
-         , LabelSet ( '(chi, '[]) ': EmptiesR fcr))
- => Empties ( '(chi, Attribution e -> Attribution a) ': fcr) prd where
-  type EmptiesR ( '(chi, Attribution e -> Attribution a) ': fcr)
-    = '(chi, '[]) ': EmptiesR fcr
-  empties (ConsRec pch fcr)
-    = let lch = labelTChAtt pch
-      in  (lch .= emptyAtt) .* (empties fcr)
+instance
+  ( Empties fcr prd
+  , chi ~ 'Chi ch prd nt
+  )
+  =>
+  Empties ( '(chi, Attribution e -> Attribution a) ': fcr) prd where
+  type EmptiesR ( '(chi, Attribution e -> Attribution a) ': fcr) =
+    '(chi, '[]) ': EmptiesR fcr
+  empties (ConsRec (TagField labelc
+                   (labelch :: Label chi) fch) r) =
+    ConsRec (TagField (Label @(ChiReco prd)) labelch emptyAtt) $ empties r
 
+
 knit (ctx  :: Proxy ctx)
      (rule :: CRule ctx prd (SCh fc) ip (EmptiesR fc) '[] (ICh fc) sp)
      (fc   :: Record fc)
@@ -597,10 +739,10 @@
 
 knitAspect (prd :: Label prd) asp fc ip
   = let ctx  = Proxy @ '[]
-        ctx' = Proxy @ '[Text "knit" :<>: ShowT prd]
+        ctx' = Proxy @ '[Text "knit" :<>: ShowTE prd]
     in  knit ctx (req ctx' (OpLookup prd ((mkAspect asp) ctx))) fc ip
 
-
+-- | use
 class Use (att :: Att) (prd :: Prod) (nts :: [NT]) (a :: Type) sc
  where
   usechi :: Label att -> Label prd -> KList nts -> (a -> a -> a) -> ChAttsRec prd sc
@@ -616,40 +758,144 @@
 instance Use prd att nts a '[] where
   usechi _ _ _ _ _ = Nothing
 
-instance( HMember' nt nts
-        , HMemberRes' nt nts ~ mnts
-        , Use' mnts att prd nts a ( '( 'Chi ch prd ('Left nt), attr) ': cs))
-  => Use att prd nts a ( '( 'Chi ch prd ('Left nt), attr) ': cs) where
+instance
+  ( HMember' nt nts
+  , HMemberRes' nt nts ~ mnts
+  , Use' mnts att prd nts a ( '( 'Chi ch prd ('Left nt), attr) ': cs))
+  =>
+  Use att prd nts a ( '( 'Chi ch prd ('Left nt), attr) ': cs) where
   usechi att prd nts op ch
     = usechi' (Proxy @ mnts) att prd nts op ch
 
-instance ( LabelSet ( '( 'Chi ch prd ('Left nt), attr) : cs)
-         , Use att prd nts a cs)
-  => Use' False att prd nts a ( '( 'Chi ch prd ('Left nt), attr) ': cs)
- where
-  usechi' _ att prd nts op (ConsCh _ cs) = usechi att prd nts op cs
+instance
+  Use att prd nts a cs
+  =>
+  Use att prd nts a ( '( 'Chi ch prd ('Right t), attr) ': cs) where
+  usechi att prd nts op (ConsRec _ ch)
+    = usechi att prd nts op ch
 
-instance ( Require (OpLookup AttReco att attr)
-           '[('Text "looking up attribute " ':<>: ShowT att)
-              ':$$: ('Text "on " ':<>: ShowT attr)]
-         , ReqR (OpLookup AttReco att attr) ~ a
-         , Use att prd nts a cs
-         , LabelSet ( '( 'Chi ch prd ('Left nt), attr) : cs)
-         , WrapField (ChiReco prd) attr ~ Attribution attr)  --ayudín
-  => Use' True att prd nts a ( '( 'Chi ch prd ('Left nt), attr) : cs) where
-  usechi' _ att prd nts op (ConsCh lattr scr)
-    = let attr = unTaggedChAttr lattr
-          val  = attr #. att
-      in  Just $ maybe val (op val) $ usechi att prd nts op scr
 
+instance
+  Use att prd nts a cs
+  =>
+  Use' False att prd nts a ( '( 'Chi ch prd ('Left nt), attr) ': cs) where
+  usechi' _ att prd nts op (ConsRec _ cs) = usechi att prd nts op cs
+
+instance
+  ( Require (OpLookup AttReco att attr)
+            '[('Text "looking up attribute " ':<>: ShowTE att)
+              ':$$: ('Text "on " ':<>: ShowTE attr)]
+  , ReqR (OpLookup AttReco att attr) ~ a
+  , Use att prd nts a cs
+  , WrapField (ChiReco prd) attr ~ Attribution attr)  --ayudín
+  =>
+  Use' True att prd nts a ( '( 'Chi ch prd ('Left nt), attr) : cs) where
+  usechi' _ att prd nts op (ConsRec lattr scr) =
+    let attr = unTaggedChAttr lattr
+        val  = attr #. att
+    in  Just $ maybe val (op val) $ usechi att prd nts op scr
+
+
+-- | Defines a rule to compute an attribute 'att' in the production
+-- 'prd', by applying an operator to the values of 'att' in each non
+-- terminal in the list 'nts'.
+
+use
+  :: UseC att prd nts t' sp sc sp' ctx
+  => Label ('Att att t')
+  -> Label prd
+  -> KList nts
+  -> (t' -> t' -> t')
+  -> t'
+  -> forall ip ic' . CRule ctx prd sc ip ic' sp ic' sp'
 use att prd nts op unit
-  = singAsp $ syndef att prd $ \_ fam -> maybe unit id (usechi att prd nts op $ chi fam)
+  = syndef att prd
+  $ \_ fam -> maybe unit id (usechi att prd nts op $ chi fam)
 
-singAsp r = r .+: emptyAspect
 
+type UseC att prd nts t' sp sc sp' ctx =
+  ( Require (OpExtend  AttReco ('Att att t') t' sp) ctx
+  ,  Use ('Att att t') prd nts t' sc
+  ,  ReqR (OpExtend AttReco ('Att att t') t' sp)
+     ~ Rec AttReco sp'
+  )
 
-tyAppAtt :: (forall b. Label ('Att name b)) -> Proxy a -> Label ('Att name a)
-att `tyAppAtt` Proxy = att
+class EmptyAspectSameShape (es1 :: [k]) (es2 :: [m])
 
-tyAppChi :: (forall b. Label ('Chi name prd b)) -> Proxy a -> Label ('Chi name prd a)
-att `tyAppChi` Proxy = att
+instance (es2 ~ '[]) => EmptyAspectSameShape '[] es2
+instance (EmptyAspectSameShape xs ys, es2 ~ ( '(y1,y2,y3,y4) ': ys))
+  => EmptyAspectSameShape (x ': xs) es2
+
+
+-- require KLIST de prods?, NO, eso está en el kind!
+class
+  EmptyAspectSameShape prds polyArgs
+  =>
+  EmptyAspect (prds :: [Prod])
+              (polyArgs :: [([(Child, [(Att, Type)])], [(Att, Type)],
+                             [(Child, [(Att, Type)])], [(Att, Type)] )])
+              ctx where
+  type EmptyAspectR prds polyArgs ctx :: [(Prod, Type)]
+  emptyAspectC :: KList prds -> Proxy polyArgs
+    -> CAspect ctx (EmptyAspectR prds polyArgs ctx)
+
+instance
+  EmptyAspect '[] '[] ctx where
+  type EmptyAspectR '[] '[] ctx = '[]
+  emptyAspectC _ _ = emptyAspect
+
+instance
+  ( EmptyAspect prds polys ctx
+  , ExtAspect ctx prd sc ip ic sp ic sp
+    (EmptyAspectR prds polys ctx)
+    (EmptyAspectR (prd ': prds) ( '(sc, ip, ic, sp) ': polys) ctx)
+  )
+  =>
+  EmptyAspect (prd ': prds) ( '(sc, ip, ic, sp) ': polys) ctx where
+  type EmptyAspectR (prd ': prds) ( '(sc, ip, ic, sp) ': polys) ctx =
+    UnWrap (ReqR (OpComRA '[] prd ((CRule '[] prd sc ip ic sp ic sp))
+                  (EmptyAspectR prds polys ctx)))
+  emptyAspectC (KCons prd prds) (p :: Proxy ( '(sc, ip, ic, sp) ': polys)) =
+    (emptyRule :: CRule ctx prd sc ip ic sp ic sp) 
+    .+: emptyAspectC @prds @polys prds (Proxy @ polys)
+
+emptyAspectForProds prdList = emptyAspectC prdList Proxy
+
+-- ** copy rules
+
+-- | a rule to copy one attribute `att` from the parent to the children `chi`
+
+copyAtChi att chi
+  = inh att (prdFromChi chi) chi (at lhs att)
+
+-- | to copy at many children
+class CopyAtChiList (att :: Att)
+                    (chi :: [Child])
+                    (polyArgs :: [([(Child, [(Att, Type)])], [(Att, Type)],
+                                   [(Child, [(Att, Type)])], [(Att, Type)],
+                                   [(Child, [(Att, Type)])], [(Att, Type)] )])
+                     ctx where
+  type CopyAtChiListR att chi polyArgs ctx :: [(Prod, Type)]
+  copyAtChiList :: Label att -> KList chi -> Proxy polyArgs
+                -> CAspect ctx (CopyAtChiListR att chi polyArgs ctx)
+
+instance CopyAtChiList att '[] '[] ctx where
+  type CopyAtChiListR att '[] '[] ctx = '[]
+  copyAtChiList _ _ _ = emptyAspect
+
+-- instance
+--   ( CopyAtChiList ('Att att t) chi polys ctx
+--   , prd ~ Prd p nt
+--   , tnt ~ Left nc
+--   )
+--   =>
+--   CopyAtChiList ('Att att t) (Chi ch prd tnt ': chi)
+--    ('(sc, ip, ic, sp, ic', sp') ': polys) ctx where
+--   type CopyAtChiListR ('Att att t) (Chi ch prd tnt ': chi)
+--    ('(sc, ip, ic, sp, ic', sp') ': polys) ctx =
+--     UnWrap (ReqR (OpComRA '[] prd ((CRule '[] prd sc ip ic sp ic' sp'))
+--                   (CopyAtChiListR ('Att att t) chi polys ctx)))
+--   copyAtChiList att (KCons chi chs :: KList ('Chi ch prd tnt ': chs) )
+--    (p :: Proxy ( '(sc, ip, ic, sp, ic', sp') ': polys))
+--     = copyAtChi att chi
+--     .+: copyAtChiList @('Att att t) @chs att chs (Proxy @polys)
diff --git a/src/Language/Grammars/AspectAG/GenRecord.hs b/src/Language/Grammars/AspectAG/GenRecord.hs
deleted file mode 100644
--- a/src/Language/Grammars/AspectAG/GenRecord.hs
+++ /dev/null
@@ -1,243 +0,0 @@
-{-|
-Module      : Language.Grammars.AspectAG.GenRecord
-Description : Record library, this will be eventually forked out
-              from AAG codebase and used as a standalone library, depending on it
-Copyright   : (c) Juan García Garland, Marcos Viera, 2019
-License     : GPL
-Maintainer  : jpgarcia@fing.edu.uy
-Stability   : experimental
-Portability : POSIX
--}
-
-{-# OPTIONS_GHC -fno-warn-missing-methods #-}
-
-{-# LANGUAGE DataKinds,
-             TypeOperators,
-             PolyKinds,
-             GADTs,
-             TypeInType,
-             RankNTypes,
-             StandaloneDeriving,
-             FlexibleInstances,
-             FlexibleContexts,
-             ConstraintKinds,
-             MultiParamTypeClasses,
-             FunctionalDependencies,
-             UndecidableInstances,
-             ScopedTypeVariables,
-             TypeFamilies,
-             InstanceSigs,
-             AllowAmbiguousTypes,
-             TypeApplications,
-             PatternSynonyms
-#-}
-
-module Language.Grammars.AspectAG.GenRecord where
-
-import Data.Kind
---import Data.Type.Equality hiding ((==))
-import Data.Proxy
-import Language.Grammars.AspectAG.TPrelude
-import Language.Grammars.AspectAG.Require
-
-import GHC.TypeLits
-
-
-type family a == b where
-  a == b = Equal a b
-
--- * Pretty constructors
-
-infixr 2 .*.
-(.*.) :: LabelSet ( '(l, v) ': r) =>
-    TagField c l v -> Rec c r -> Rec c ( '(l,v) ': r)
-(.*.) = ConsRec
-
--- * destructors
-
--- | A getter, also a predicate
--- class HasField (l :: k) (r :: [(k, k')]) field where
---   type LookupByLabel field l r :: Type
---   (#) :: REC field r -> Label l -> LookupByLabel field l v
-
-
-tailRec :: Rec c ( '(l,v) ': r) -> Rec c r
-tailRec (ConsRec _ t) = t
-
-data Rec (c :: k) (r :: [(k', k'')]) :: Type where
-  EmptyRec :: Rec c '[]
-  ConsRec  :: LabelSet ( '(l,v) ': r) =>
-              TagField c l v -> Rec c r -> Rec c ( '(l,v) ': r)
-
-data TagField (cat :: k) (l :: k') (v :: k'') where
-  TagField :: Label c -> Label l -> WrapField c v -> TagField c l v
-
-untagField :: TagField c l v -> WrapField c v
-untagField (TagField lc lv v) = v
-
-type family    WrapField (c :: k')  (v :: k) -- = ftype | ftype c -> v
-
-{-
-Node:
-We cannot encode the dependency {ftype, c} -> v since TypeFamilyDependencies
-does not support this general dependencies. So from (WrapField c v) we
-can't infer c.
-
--}
-
-
-data OpLookup (c :: Type)
-              (l  :: k)
-              (r  :: [(k, k')]) :: Type where
-  OpLookup :: Label l -> Rec c r -> OpLookup c l r
-
-data OpLookup' (b  :: Bool)
-               (c  :: Type)
-               (l  :: k)
-               (r  :: [(k, k')]) :: Type where
-  OpLookup' :: Proxy b -> Label l -> Rec c r -> OpLookup' b c l r
-
-
-
-
-instance (Require (OpLookup' (l == l') c l ( '(l', v) ': r)) ctx)
-  => Require (OpLookup c l ( '(l', v) ': r)) ctx where
-  type ReqR (OpLookup c l ( '(l', v) ': r))
-    = ReqR (OpLookup' (l == l') c l ( '(l', v) ': r))
-  req ctx (OpLookup l r) = req ctx (OpLookup' (Proxy @ (l == l')) l r)
-
-instance Require (OpLookup' 'True c l ( '(l, v) ': r)) ctx where
-  type ReqR (OpLookup' 'True c l ( '(l, v) ': r)) = WrapField c v
-  req Proxy (OpLookup' Proxy Label (ConsRec f _)) = untagField f
-
-instance (Require (OpLookup c l r) ctx)
-  => Require (OpLookup' False c l ( '(l', v) ': r)) ctx where
-  type ReqR (OpLookup' False c l ( '(l', v) ': r)) = ReqR (OpLookup c l r)
-  req ctx (OpLookup' Proxy l (ConsRec _ r)) = req ctx (OpLookup l r)
-
-
-
-
-instance
-  Require (OpError (Text "field not Found on " :<>: Text (ShowRec c)
-                     :$$: Text "looking up the " :<>: Text (ShowField c)
-                           :<>: ShowT l
-                          )) ctx
-  => Require (OpLookup c l ( '[] :: [(k,k')])) ctx where
-  type ReqR (OpLookup c l ('[] :: [(k,k')])  ) = ()
-  req = undefined
-
-type family ShowRec c :: Symbol
-type family ShowField c :: Symbol
-
-instance (Require (OpError (Text "field not Found on " :<>: Text (ShowRec c)
-                    :$$: Text "updating the " :<>: Text (ShowField c)
-                     :<>: ShowT l)) ctx)
-  => Require (OpUpdate c l v '[]) ctx where
-  type ReqR (OpUpdate c l v ('[] )  ) = Rec c '[]
-  req = undefined
-
--- | update
-data OpUpdate (c  :: Type)
-              (l  :: k)
-              (v  :: k')
-              (r  :: [(k, k')]) :: Type where
-  OpUpdate :: Label l -> WrapField c v -> Rec c r
-           -> OpUpdate c l v r
-
-data OpUpdate' (b  :: Bool)
-               (c  :: Type)
-               (l  :: k)
-               (v  :: k')
-               (r  :: [(k, k')]) :: Type where
-  OpUpdate' :: Proxy p -> Label l -> WrapField c v ->  Rec c r
-           -> OpUpdate' b c l v r
-
-
-instance (Require (OpUpdate' (l == l') c l v ( '(l', v') ': r) ) ctx )
-  => Require (OpUpdate c l v ( '(l', v') ': r) ) ctx where
-  type ReqR (OpUpdate c l v ( '(l', v') ': r) )
-    = ReqR (OpUpdate' (l == l') c l v ( '(l', v') ': r) )
-  req ctx (OpUpdate l f r)
-    = (req @(OpUpdate' (l == l') _ _ v _ ))
-       ctx (OpUpdate' (Proxy @(l == l')) l f r)
-
-
-instance ( LabelSet ( '(l, v) ': r)
-         , LabelSet ( '(l, v') ': r))
-  => Require (OpUpdate' 'True c l v ( '(l, v') ': r)) ctx where
-  type ReqR (OpUpdate' 'True c l v ( '(l, v') ': r))
-    = Rec c ( '(l, v) ': r)
-  req ctx (OpUpdate' proxy label field (ConsRec tgf r))
-    = ConsRec (TagField Label label field) r
-
-
-instance ( Require (OpUpdate c l v r) ctx
-         , UnWrap (ReqR (OpUpdate c l v r)) ~ r0
-         , LabelSet ( '(l', v') : r0)
-         , ReqR (OpUpdate c l v r) ~ Rec c r0)
-  => Require (OpUpdate' 'False c l v ( '(l',v') ': r)) ctx where
-  type ReqR (OpUpdate' 'False c l v ( '(l',v') ': r))
-    = Rec c ( '(l',v') ': (UnWrap (ReqR (OpUpdate c l v r))))
-  req ctx (OpUpdate' _ l f (ConsRec field r))
-    = ConsRec field $ (req @(OpUpdate _ _ v r)) ctx (OpUpdate l f r)
-
-
-
-type family UnWrap t :: [(k,k')]
-type instance UnWrap (Rec c r) = r
-
-
-
-
-data OpExtend (c :: Type)
-              (l  :: k)
-              (v  :: k')
-              (r  :: [(k, k')]) :: Type where
-  OpExtend :: Label l -> WrapField c v -> Rec c r
-           -> OpExtend c l v r
-
-data OpExtend' (b :: Bool)
-               (c :: Type)
-               (l  :: k)
-               (v  :: k')
-               (r  :: [(k, k')]) :: Type where
-  OpExtend' :: Proxy b -> Label l -> WrapField c v -> Rec c r
-           -> OpExtend' b c l v r
-
-
-instance (LabelSetF ( '(l, v) ': r) ~ 'True)
-  => Require (OpExtend' True  c l v r) ctx where
-  type ReqR (OpExtend' True c l v r) = Rec c ( '(l, v) ': r)
-  req ctx (OpExtend' _ l f r) = ConsRec (TagField (Label @c) l f) r
-
-
-instance ( LabelSetF ( '(l, v) ':  r) ~ b
-         , Require (OpExtend' b c l v r) ctx)
-  => Require (OpExtend c l v r) ctx where
-  type ReqR (OpExtend c l v r)
-    = ReqR (OpExtend' (LabelSetF ( '(l, v) ': r)) c l v r)
-  req ctx (OpExtend l v r)
-    = req @(OpExtend' (LabelSetF ( '(l, v) ': r)) _ _ v _ )
-      ctx (OpExtend' Proxy l v r) 
-
-instance Require (OpError (Text "Duplicated Labels on " :<>: Text (ShowRec c)
-                          :$$: Text "on the " :<>: Text (ShowField c)
-                           :<>: ShowT l
-                          )) ctx
-  => Require (OpExtend' False c l v (r :: [(k, k')])) ctx where
-  type ReqR (OpExtend' False c l v r) = Rec c (r :: [(k, k')])
-  req ctx (OpExtend' p l v r) = undefined
-
-
-
-data OpNonEmpty (c :: Type) (r :: [(k, k')]) where
-  OpNonEmpty :: Rec c r -> OpNonEmpty c r
-
-
-instance Require (OpNonEmpty c ( '(l, v) ': r)) ctx where {}
-
-instance (Require (OpError (Text "Empty " :<>: Text (ShowRec c)
-                          :$$: Text " Required to be nonempty "
-                          )) ctx)
-  => Require (OpNonEmpty c '[]) ctx where {}
diff --git a/src/Language/Grammars/AspectAG/HList.hs b/src/Language/Grammars/AspectAG/HList.hs
--- a/src/Language/Grammars/AspectAG/HList.hs
+++ b/src/Language/Grammars/AspectAG/HList.hs
@@ -26,7 +26,9 @@
 #-}
 
 module Language.Grammars.AspectAG.HList where
-import Language.Grammars.AspectAG.TPrelude
+
+import Data.Type.Bool
+import Data.GenRec.Label
 import Data.Proxy
 import Data.Type.Equality
 import Data.Kind
@@ -49,7 +51,7 @@
   hMember _ _ = Proxy
 
 instance HMember t (t' ': ts) where
-  type HMemberRes t (t' ': ts) = Or (t == t') (HMemberRes t ts)
+  type HMemberRes t (t' ': ts) = t == t' || HMemberRes t ts
   hMember _ _ = Proxy
 
 -- | HMember' is a test membership function.
@@ -63,7 +65,7 @@
   hMember' _ _ = Proxy
 
 instance HMember' t (t' ': ts) where
-  type HMemberRes' t (t' ': ts) = Or (t == t') (HMemberRes' t ts)
+  type HMemberRes' t (t' ': ts) = t == t' || HMemberRes' t ts
   hMember' _ _ = Proxy
 
 
@@ -81,3 +83,4 @@
 infixr 2 .:.
 (.:.) = KCons
 eL = KNil
+
diff --git a/src/Language/Grammars/AspectAG/RecordInstances.hs b/src/Language/Grammars/AspectAG/RecordInstances.hs
--- a/src/Language/Grammars/AspectAG/RecordInstances.hs
+++ b/src/Language/Grammars/AspectAG/RecordInstances.hs
@@ -19,41 +19,52 @@
              InstanceSigs,
              AllowAmbiguousTypes,
              TypeApplications,
-             PatternSynonyms
+             PatternSynonyms,
+             PartialTypeSignatures
 #-}
 
 module Language.Grammars.AspectAG.RecordInstances where
 
-import Language.Grammars.AspectAG.Require
-import Language.Grammars.AspectAG.GenRecord
-import Language.Grammars.AspectAG.TPrelude
+import Data.Type.Require
+import Data.GenRec
 import GHC.TypeLits
 import Data.Kind
 import Data.Proxy
 
-data Att   = Att Symbol Type               -- deriving Eq
-data Prod  = Prd Symbol NT                  --deriving Eq
-data Child = Chi Symbol Prod (Either NT T)  --deriving Eq
-data NT    = NT Symbol                      --deriving Eq
-data T     = T Type                        -- deriving Eq
+data Att   = Att Symbol Type                -- deriving Eq
+data Prod  = Prd Symbol NT                  -- deriving Eq
+data Child = Chi Symbol Prod (Either NT T)  -- deriving Eq
+data NT    = NT Symbol                      -- deriving Eq
+data T     = T Type                         -- deriving Eq
 
+prdFromChi :: Label (Chi nam prd tnt) -> Label prd
+prdFromChi _ = Label
 
 
+type instance Cmp ('Att a _) ('Att b _) =
+  CmpSymbol a b
 
-type instance  ShowT ('Att l t)   = Text  "Attribute " :<>: Text l
-                                                       :<>: Text ":"
-                                                       :<>: ShowT t 
-type instance  ShowT ('Prd l nt)  = ShowT nt :<>: Text "::Production "
-                                             :<>: Text l
-type instance  ShowT ('Chi l p s) = ShowT p :<>:  Text "::Child " :<>: Text l 
-                                            :<>:  Text ":" :<>: ShowT s
-type instance  ShowT ('Left l)    = ShowT l
-type instance  ShowT ('Right r)   = ShowT r
-type instance  ShowT ('NT l)      = Text "Non-Terminal " :<>: Text l
-type instance  ShowT ('T  l)      = Text "Terminal " :<>: ShowT l
+type instance Cmp ('Prd a _) ('Prd b _) =
+  CmpSymbol a b
 
+type instance Cmp ('Chi a _ _) ('Chi b _ _) =
+  CmpSymbol a b
 
 
+type instance  ShowTE ('Att l t)   = Text  "Attribute " :<>: Text l
+                                                        :<>: Text ":"
+                                                        :<>: ShowTE t 
+type instance  ShowTE ('Prd l nt)  = ShowTE nt :<>: Text "::Production "
+                                              :<>: Text l
+type instance  ShowTE ('Chi l p s) = ShowTE p :<>:  Text "::Child " :<>: Text l 
+                                            :<>:  Text ":" :<>: ShowTE s
+type instance  ShowTE ('Left l)    = ShowTE l
+type instance  ShowTE ('Right r)   = ShowTE r
+type instance  ShowTE ('NT l)      = Text "Non-Terminal " :<>: Text l
+type instance  ShowTE ('T  l)      = Text "Terminal " :<>: ShowTE l
+
+
+
 -- | * Records
 
 -- | datatype definition
@@ -70,15 +81,6 @@
 type instance ShowField Reco       = "field named "
 
 
-
--- | ** Pattern Synonyms
-pattern EmptyR :: Rec Reco '[]
-pattern EmptyR = EmptyRec :: Rec Reco '[]
-pattern ConsR :: (LabelSet ( '(l,v ) ': xs))
-  => Tagged l v -> Rec Reco xs -> Rec Reco ( '(l,v ) ': xs) 
-pattern ConsR lv r = ConsRec lv r
-
-
 type Tagged = TagField Reco
 pattern Tagged :: v -> Tagged l v
 pattern Tagged v = TagField Label Label v
@@ -86,37 +88,37 @@
 
 -- ** Constructors
 
--- | Pretty Constructor
-infixr 4 .=.
-(.=.) :: Label l -> v -> Tagged l v
-l .=. v = Tagged v
+-- -- | Pretty Constructor
+-- infixr 4 .=.
+-- (.=.) :: Label l -> v -> Tagged l v
+-- l .=. v = Tagged v
 
--- | For the empty Record
-emptyRecord :: Record '[]
-emptyRecord = EmptyR
+-- -- | For the empty Record
+-- emptyRecord :: Record '[]
+-- emptyRecord = EmptyRec
 
-unTagged :: Tagged l v -> v
-unTagged (TagField _ _ v) = v
+-- unTagged :: Tagged l v -> v
+-- unTagged (TagField _ _ v) = v
 
--- * Destructors
--- | Get a label
-label :: Tagged l v -> Label l
-label _ = Label
+-- -- * Destructors
+-- -- | Get a label
+-- label :: Tagged l v -> Label l
+-- label _ = Label
 
--- | Same, mnemonically defined
-labelTChAtt :: Tagged l v -> Label l
-labelTChAtt _ = Label
+-- -- | Same, mnemonically defined
+-- labelTChAtt :: Tagged l v -> Label l
+-- labelTChAtt _ = Label
 
 
--- | Show instance, used for debugging
-instance Show (Record '[]) where
-  show _ = "{}"
+-- -- | Show instance, used for debugging
+-- instance Show (Record '[]) where
+--   show _ = "{}"
 
-instance (Show v, Show (Record xs), (LabelSet ('(l, v) : xs))) =>
-         Show (Record ( '(l,v) ': xs ) ) where
-  show (ConsR lv xs) = let tail = show xs
-                       in "{" ++ show (unTagged lv)
-                          ++ "," ++ drop 1 tail
+-- instance (Show v, Show (Record xs)) =>
+--          Show (Record ( '(l,v) ': xs ) ) where
+--   show (ConsRec lv xs) = let tail = show xs
+--                          in "{" ++ show (unTagged lv)
+--                             ++ "," ++ drop 1 tail
 
 
 
@@ -137,11 +139,11 @@
 type instance ShowField AttReco       = "attribute named "
 
 -- | Pattern Synonyms
-pattern EmptyAtt :: Attribution '[]
-pattern EmptyAtt = EmptyRec
-pattern ConsAtt :: LabelSet ( '(att, val) ': atts) =>
-    Attribute att val -> Attribution atts -> Attribution ( '(att,val) ': atts)
-pattern ConsAtt att atts = ConsRec att atts
+-- pattern EmptyAtt :: Attribution '[]
+-- pattern EmptyAtt = EmptyRec
+-- pattern ConsAtt :: LabelSet ( '(att, val) ': atts) =>
+--     Attribute att val -> Attribution atts -> Attribution ( '(att,val) ': atts)
+-- pattern ConsAtt att atts = ConsRec att atts
 
 -- | Attribute
 
@@ -159,10 +161,9 @@
 
 -- | Extending
 infixr 2 *.
-(*.) :: LabelSet ('(att, val) : atts) =>
-    Attribute att val -> Attribution atts
-      -> Attribution ('(att, val) : atts)
-(*.) = ConsRec
+-- (*.) :: Attribute att val -> Attribution atts
+--       -> Attribution (ReqR (OpExtend AttReco att val atts) ctx)
+(l :: Attribute att val) *. (r :: Attribution atts) = l .*. r
 
 -- | Empty
 emptyAtt :: Attribution '[]
@@ -172,15 +173,15 @@
 infixl 7 #.
 
 (#.) ::
-  ( msg ~ '[Text "looking up attribute " :<>: ShowT l :$$:
-            Text "on " :<>: ShowT r
+  ( msg ~ '[Text "looking up attribute " :<>: ShowTE l :$$:
+            Text "on " :<>: ShowTE r
            ]
   , Require (OpLookup AttReco l r) msg
   )
   => Attribution r -> Label l -> ReqR (OpLookup AttReco l r)
 (attr :: Attribution r) #. (l :: Label l)
-  = let prctx = Proxy @ '[Text "looking up attribute " :<>: ShowT l :$$:
-                          Text "on " :<>: ShowT r
+  = let prctx = Proxy @ '[Text "looking up attribute " :<>: ShowTE l :$$:
+                          Text "on " :<>: ShowTE r
                          ]
     in req prctx (OpLookup @_ @(AttReco) l attr)
 
@@ -209,12 +210,12 @@
 
 -- |since now we implement ChAttsRec as a generic record, this allows us to
 --   recover pattern matching
-pattern EmptyCh :: ChAttsRec prd '[]
-pattern EmptyCh = EmptyRec
-pattern ConsCh :: (LabelSet ( '( 'Chi ch prd nt, v) ': xs)) =>
-  TaggedChAttr prd ( 'Chi ch prd nt) v -> ChAttsRec prd xs
-                         -> ChAttsRec prd ( '( 'Chi ch prd nt,v) ': xs)
-pattern ConsCh h t = ConsRec h t
+-- pattern EmptyCh :: ChAttsRec prd '[]
+-- pattern EmptyCh = EmptyRec
+-- pattern ConsCh :: (LabelSet ( '( 'Chi ch prd nt, v) ': xs)) =>
+--   TaggedChAttr prd ( 'Chi ch prd nt) v -> ChAttsRec prd xs
+--                          -> ChAttsRec prd ( '( 'Chi ch prd nt,v) ': xs)
+-- pattern ConsCh h t = ConsRec h t
 
 -- | Attributions tagged by a child
 type TaggedChAttr prd = TagField (ChiReco prd)
@@ -232,10 +233,8 @@
 
 -- | Pretty constructors
 infixr 2 .*
-(.*) :: LabelSet ('(ch, attrib) ':  attribs) =>
-  TaggedChAttr prd ch attrib -> ChAttsRec prd attribs
-    -> ChAttsRec prd ('(ch, attrib) ': attribs)
-(.*) = ConsRec
+(tch :: TaggedChAttr prd ch attrib) .* (chs :: ChAttsRec prd attribs) = tch .*. chs
+-- TODO: error instances if different prds are used?
 
 -- | empty
 emptyCh :: ChAttsRec prd '[]
@@ -251,17 +250,17 @@
 infixl 8 .#
 (.#) ::
   (  c ~ ('Chi ch prd nt)
-  ,  ctx ~ '[Text "looking up " :<>: ShowT c :$$:
-            Text "on " :<>: ShowT r :$$:
-            Text "producion: " :<>: ShowT prd
+  ,  ctx ~ '[Text "looking up " :<>: ShowTE c :$$:
+            Text "on " :<>: ShowTE r :$$:
+            Text "producion: " :<>: ShowTE prd
            ]
   , Require (OpLookup (ChiReco prd) c r) ctx
   ) =>
      Rec (ChiReco prd) r -> Label c -> ReqR (OpLookup (ChiReco prd) c r)
 (chi :: Rec (ChiReco prd) r) .# (l :: Label c)
-  = let prctx = Proxy @ '[Text "looking up " :<>: ShowT c :$$:
-                          Text "on " :<>: ShowT r :$$:
-                          Text "producion: " :<>: ShowT prd
+  = let prctx = Proxy @ '[Text "looking up " :<>: ShowTE c :$$:
+                          Text "on " :<>: ShowTE r :$$:
+                          Text "producion: " :<>: ShowTE prd
                          ]
     in req prctx (OpLookup @_ @(ChiReco prd) l chi)
 
@@ -275,5 +274,5 @@
   = rule
 
 type Aspect (asp :: [(Prod, Type)]) = Rec PrdReco asp
-type instance ShowRec PrdReco      = "Aspect"
-type instance ShowField PrdReco       = "production named "
+type instance ShowRec PrdReco       = "Aspect"
+type instance ShowField PrdReco     = "production named "
diff --git a/src/Language/Grammars/AspectAG/Require.hs b/src/Language/Grammars/AspectAG/Require.hs
deleted file mode 100644
--- a/src/Language/Grammars/AspectAG/Require.hs
+++ /dev/null
@@ -1,77 +0,0 @@
-{-# OPTIONS_GHC -fno-warn-missing-methods #-}
-{-# LANGUAGE DataKinds,
-             TypeOperators,
-             PolyKinds,
-             GADTs,
-             TypeInType,
-             RankNTypes,
-             StandaloneDeriving,
-             FlexibleInstances,
-             FlexibleContexts,
-             ConstraintKinds,
-             MultiParamTypeClasses,
-             FunctionalDependencies,
-             UndecidableInstances,
-             ScopedTypeVariables,
-             TypeFamilies,
-             InstanceSigs,
-             AllowAmbiguousTypes,
-             TypeApplications,
-             PatternSynonyms
-#-}
-
-module Language.Grammars.AspectAG.Require where
-
-import Data.Kind
-import Data.Proxy
-import GHC.TypeLits
-import Language.Grammars.AspectAG.TPrelude
-import Data.Type.Equality
-
-class Require (op   :: Type)
-              (ctx  :: [ErrorMessage])  where
-   type ReqR op :: Type
-   req :: Proxy ctx -> op -> ReqR op
-
-instance (TypeError (Text "Error: " :<>: m :$$:
-                     Text "trace: " :<>: ShowCTX ctx))
-  => Require (OpError m) ctx where {}
-
-data OpError (m :: ErrorMessage) where {}
-
-type family ShowCTX (ctx :: [ErrorMessage]) :: ErrorMessage where
-  ShowCTX '[] = Text ""
-  ShowCTX (m ': ms) = m :$$: ShowCTX ms
-
-
-type family ShowEM (m :: ErrorMessage) :: ErrorMessage
-
-type family ShowT (t :: k) :: ErrorMessage
-type instance ShowT (t :: Type) = ShowType t
-{-
-Abro esta familia para poder definirla de manera extensible, porque no sabemos
-en GenReord como se muestran los tipos para instancias concretas. El problema es
-que estaba definida con un pattern que capturaba todos los demas casos al final
-y en tf cerradas no se admite overlap. Entonces defino aca una instancia para el
-kind t (era a fin de cuentas lo que caia en el último pattern)
--}
-
-type RequireR (op :: Type ) (ctx:: [ErrorMessage]) (res :: Type)
-     = (Require op ctx, ReqR op ~ res)
-
-
-type RequireEq (t1 :: k )(t2 :: k) (ctx:: [ErrorMessage])
-    = (Require (OpEq t1 t2) ctx, t1 ~ t2)
-
-data OpEq t1 t2
-
-instance RequireEqRes t1 t2 ctx
-  => Require (OpEq t1 t2) ctx where
-  type ReqR (OpEq t1 t2) = ()
-  req = undefined
-
-type family RequireEqRes (t1 :: k) (t2 :: k)
-                     (ctx :: [ErrorMessage]) ::  Constraint where
-  RequireEqRes t1 t2 ctx = If (t1 `Equal` t2) (() :: Constraint)
-    (Require (OpError (Text "" :<>: ShowT t1 :<>: Text " /= " :<>: ShowT t2)) ctx)
-
diff --git a/src/Language/Grammars/AspectAG/TH.hs b/src/Language/Grammars/AspectAG/TH.hs
--- a/src/Language/Grammars/AspectAG/TH.hs
+++ b/src/Language/Grammars/AspectAG/TH.hs
@@ -40,10 +40,12 @@
 
 import Control.Monad
 
+import Data.GenRec.Label
+import Data.GenRec
 import Language.Grammars.AspectAG
+import Language.Grammars.AspectAG.RecordInstances
 import qualified Data.Kind as DK
 
-import qualified Language.Haskell.TH.Compat.Strict as Comp
 
 -- * Attribute labels
 
@@ -145,8 +147,8 @@
     : addInstance nt prd (map preProc xs)
     : [addChi chi (mkName ("P_" ++ prd)) sym | (chi, sym) <- xs]
     where preProc (n, Ter a)    = (mkName n, a)
-          preProc (n, NonTer a) = (mkName n, a) 
-
+          preProc (n, NonTer a) = (mkName n, a)
+          preProc (n, Poly)     = (mkName n, mkName "a")
 
 -- | class
 class Prods (lhs :: NT) (name :: Symbol) (rhs :: [(Symbol, Symbol)]) where {}
@@ -174,12 +176,6 @@
           -> appT (appT promotedConsT (appT (appT (promotedTupleT 2)
                                               (nameToSymbol n))
                                        (nameToSymbolBase t))) xs
-  -- where f = \x xs -> if isNTName x
-  --         then ((appT (appT promotedConsT
-  --                      ((appT [t| Left |]) (conT x))))) xs
-  --         else ((appT (appT promotedConsT
-  --                      ((appT [t| Right |])
-  --                       (appT [t| 'T |] (conT x)))))) xs
 
 nameToSymbol = litT . strTyLit . show
 nameToSymbolBase = litT . strTyLit . nameBase
@@ -188,7 +184,6 @@
 isNTName n
   = "Nt_" `isPrefixOf` nameBase n
 
-
 closeNT :: Name -> Q [Dec]
 closeNT nt
   = do decs <- getInstances
@@ -222,8 +217,6 @@
     : getTList ts
 getTList _ = []
 
-
-
 -- | keeps nt info
 getTListNT :: Type -> [(Name, Name)]
 getTListNT (SigT _ _) = []
@@ -253,7 +246,7 @@
 
 toSemRec :: [(Name, Name)] -> Exp
 toSemRec
-  = foldr mkChSem (VarE (mkName "emptyRecord"))
+  = foldr mkChSem (VarE (mkName "emptyGenRec"))
   where mkChSem (n,pos) xs
           | "Nt_" `isPrefixOf` nameBase pos =
           (AppE (AppE (VarE $ mkName ".*.")
@@ -280,4 +273,7 @@
      let clauses = map mkClause $ filter (isInstanceOf nt) decs
      return [FunD (mkName $ "sem_" ++ drop 3 (nameBase nt)) clauses ]
 
+mkSemFuncs :: [Name] -> Q [Dec]
+mkSemFuncs
+  = liftM concat . sequence . map (mkSemFunc)
 
diff --git a/src/Language/Grammars/AspectAG/TPrelude.hs b/src/Language/Grammars/AspectAG/TPrelude.hs
deleted file mode 100644
--- a/src/Language/Grammars/AspectAG/TPrelude.hs
+++ /dev/null
@@ -1,135 +0,0 @@
-{-|
-Module      : Language.Grammars.AspectAG.TPrelude
-Description : Some type level functions, needed for AspectAG
-Copyright   : (c) Juan García Garland, 2018 
-License     : LGPL
-Maintainer  : jpgarcia@fing.edu.uy
-Stability   : experimental
-Portability : POSIX
-
-
--}
-{-# LANGUAGE GADTs,
-             KindSignatures,
-             TypeOperators,
-             TypeFamilies,
-             MultiParamTypeClasses,
-             FlexibleInstances,
-             FlexibleContexts,
-             StandaloneDeriving,
-             UndecidableInstances,
-             FunctionalDependencies,
-             ConstraintKinds,
-             ScopedTypeVariables,
-             PolyKinds,
-             DataKinds
-#-}
-
-module Language.Grammars.AspectAG.TPrelude where
-import Data.Kind
-import Data.Type.Equality
-import GHC.TypeLits
-import Data.Proxy
-
-
-data Label l = Label
-sndLabel :: Label '(a,b) -> Label b
-sndLabel _ = undefined
-
-getProxy :: a -> Proxy a ; getProxy _ = Proxy
-getLabel :: a -> Label a ; getLabel _ = Label
-
-proxyFrom :: t a -> Proxy a
-proxyFrom _ = Proxy
-
-
--- | If construction, purely computed at type level
-type family If (cond:: Bool) (thn :: k) (els :: k) :: k where
-  If 'True  thn els = thn
-  If 'False thn els = els
-
--- | Or, purely computed at type level
-type family Or (l :: Bool)(r :: Bool) :: Bool where
-  Or False b = b
-  Or True b  = 'True
-
-
--- | And, purely computed at type level
-type family And (l :: Bool)(r :: Bool) :: Bool where
-  And False b = False
-  And True b  = b
-
--- | Not, purely computed at type level
-type family Not (l :: Bool) :: Bool where
-  Not False = True
-  Not True  = False
-
-
--- | LabelSet is a predicate over lists of pairs.
---We assume the list represent a (partial) mapping from k1 to k2.
---k1 is a label, k2 possibly a value.
---The first member of each pair must be unique, this is a predicate of
---well formedness
--- class LabelSet (l :: [(k1,k2)])
-
-type family LabelSetF (r :: [(k, k')]) :: Bool where
-  LabelSetF '[] = True
-  LabelSetF '[ '(l, v)] = True
-  LabelSetF ( '(l, v) ': '(l', v') ': r) = And3 (Not (l == l')) 
-                                                (LabelSetF ( '(l, v)   ': r) )
-                                                (LabelSetF ( '(l', v') ': r) )
-
-{-
-class LabelSet (r :: [(k, k')]) where {}
-instance LabelSetF r ~ True => LabelSet r
--}
-
-type LabelSet r = LabelSetF r ~ True
-
-type family And3 (a1 :: Bool) (a2 :: Bool) (a3 :: Bool) where
-  And3 True True True  = True
-  And3 _     _   _     = False
-
--- | Predicate of membership, for lists at type level
-type family HMemberT (e::k)(l ::[k]) :: Bool where
-  HMemberT k '[] = 'False
-  HMemberT k ( k' ': l) = If (k==k') 'True (HMemberT k l)
-
-
--- | Predicate of membership, for labels at type level
-type family HasLabelT (l::k) (lst :: [(k,Type)]) :: Bool where
-  HasLabelT l '[] = 'False
-  HasLabelT l ( '(k,v) ': tail) = If (l == k) 'True (HasLabelT l tail)
-
-
--- |This is used for type Equality
-class HEq (x :: k) (y :: k) (b :: Bool) | x y -> b
-type HEqK (x :: k1) (y :: k2) (b :: Bool) = HEq (Proxy x) (Proxy y) b
-instance ((Proxy x == Proxy y) ~ b) => HEq x y b
-
-type family HEqKF (a :: k)(b :: k) :: Bool
-type instance HEqKF a b = a == b
-
-
--- | heterogeneous equality at type level
-type family (a :: k1) === (b :: k2) where
-  a === b = (Proxy a) == (Proxy b)
-
-
-type family TPair (a :: k) b where
-  TPair a b = '(a, b)
-
-
-type family LabelsOf (r :: [(k, k')]) :: [k] where
-  LabelsOf '[] = '[]
-  LabelsOf ( '(k, ks) ': ls) = k ': LabelsOf ls
-
-type family HasLabel (l :: k) (r :: [(k, k')]) :: Bool where
-  HasLabel l '[] = False
-  HasLabel l ( '(l', v) ': r) = Or (l == l') (HasLabel l r)
-
-
-type family Equal (a:: k)(b :: k') :: Bool where
---  Equal (f a) (g b) = And (Equal f g) (Equal a b) 
-  Equal a a = True
-  Equal a b = False