diff --git a/poly-rec.cabal b/poly-rec.cabal
--- a/poly-rec.cabal
+++ b/poly-rec.cabal
@@ -2,7 +2,7 @@
 -- documentation, see http://haskell.org/cabal/users-guide/
 
 name:                poly-rec
-version:             0.6.0.0
+version:             0.7.0.0
 synopsis:            Polykinded extensible records
 description:         Extensible records/row polymorphism for Haskell. Fields are polykinded,
                      to statically check rich structures. This library was initially conceived
@@ -11,7 +11,7 @@
 license-file:        LICENSE
 author:              Juan García-Garland
 maintainer:          jpgarcia@fing.edu.uy
-copyright:           2020, Juan García-Garland, Marcos Viera, Alberto Pardo
+copyright:           2020-2022, Juan García-Garland, Marcos Viera, Alberto Pardo
 category:            Data
 build-type:          Simple
 extra-source-files:  CHANGELOG.md
@@ -25,6 +25,6 @@
   -- other-modules:
   -- other-extensions:
   build-depends:       requirements >= 0.6.0.0 && < 0.7,
-                       base >=4.11 && <4.15
+                       base >=4.11 && <4.18
   hs-source-dirs:      src
   default-language:    Haskell2010
diff --git a/src/Data/GenRec.hs b/src/Data/GenRec.hs
--- a/src/Data/GenRec.hs
+++ b/src/Data/GenRec.hs
@@ -86,9 +86,13 @@
     (.=.),
     (#),
     (.*.),
+
+    OrdType,
     Cmp,
     ShowRec,
     ShowField,
+    ShowLabel,
+    
     OpLookup(OpLookup),
     lookup,
     OpExtend(OpExtend),
@@ -103,6 +107,8 @@
 import Data.Proxy
 import Data.GenRec.Label
 import Data.Type.Require
+import Data.Type.Bool
+
 import Prelude hiding (lookup)
 
 import GHC.TypeLits
@@ -171,18 +177,24 @@
 
 -- | comparisson of Labels, this family is polykinded, each record-like
 -- structure must implement this family for its labels
-type family Cmp (a :: k) (b :: k) :: Ordering
+--type family Cmp (a :: k) (b :: k) :: Ordering
 
 -- | Instance for Symbols
-type instance Cmp (a :: Symbol) (b :: Symbol) = CmpSymbol a b
+--type instance Cmp (a :: Symbol) (b :: Symbol) = CmpSymbol a b
 
+class OrdType k where
+  type Cmp (a :: k) (b :: k) :: Ordering
 
+instance OrdType Symbol where
+  type Cmp a b = CmpSymbol a b
+
 -- | Function to show the name of records (Record, Mapping, etc):
 type family ShowRec c :: Symbol
 
 -- | Function to show the field of the record ("field named", "children", "tag:", etc)
 type family ShowField c :: Symbol
 
+type family ShowLabel (l :: k) :: Symbol
 
 -- * Operations
 
@@ -215,7 +227,7 @@
 instance
   Require (OpError (Text "field not Found on " :<>: Text (ShowRec c)
                      :$$: Text "looking up the " :<>: Text (ShowField c)
-                           :<>: Text " " :<>: ShowTE l
+                           :<>: Text " " :<>: Text (ShowLabel l)
                           )) ctx
   =>
   Require (OpLookup c l ( '[] :: [(k,k')])) ctx where
@@ -252,9 +264,9 @@
   req ctx (OpLookup' Proxy l (ConsRec _ r)) = ()
 
 -- | Pretty lookup
-(#) :: RequireR (OpLookup c l r) '[] v =>
+(#) :: forall c l r ctx v. RequireR (OpLookupCall c l r) ctx v =>
   Rec c r -> Label l -> v
-r # l = req (Proxy @ '[]) (OpLookup l r)
+r # l = req (Proxy @ctx) (OpLookupCall l r)
 
 
 -- ** update
@@ -402,7 +414,7 @@
   (Require (OpError (Text "cannot extend " :<>: Text (ShowRec c)
                      -- :<>: Text " because the label (" :<>: ShowT l
                      -- :<>: Text ") already exists"
-                    :$$: Text "colision in " :<>: Text (ShowField c)
+                    :$$: Text "collision in " :<>: Text (ShowField c)
                      :<>: Text " ":<>: ShowTE l)) ctx)
   =>
   Require (OpExtend' 'EQ c l v ( '(l, v') ': r)) ctx where
@@ -414,3 +426,28 @@
 infixr 2 .*.
 (TagField c l v :: TagField c l v) .*. (r :: Rec c r) =
   req emptyCtx (OpExtend @l @c @v @r l v r)
+
+
+
+type family LabelSetF (r :: [(k, k')]) :: Bool where
+  LabelSetF '[] = True
+  LabelSetF '[ '(l, v)] = True
+  LabelSetF ( '(l, v) ': '(l',v') ': r) =
+    Cmp l l' == LT && LabelSetF ( '(l',v') ': r)
+
+
+data OpLookupCall
+  (c :: Type)
+  (l  :: k)
+  (r  :: [(k, k')]) :: Type where
+  OpLookupCall :: Label l -> Rec c r -> OpLookupCall c l r
+
+
+instance
+  Require (OpLookup c l r) ( ShowType r ': ctx)
+  =>
+  Require (OpLookupCall c l r) ctx where
+  type ReqR (OpLookupCall c l r) =
+    ReqR (OpLookup c l r)
+  req ctx (OpLookupCall l r) =
+   req (Proxy @ (ShowType r ': ctx)) (OpLookup l r)
diff --git a/src/Data/GenRec/RecInstances/Record.hs b/src/Data/GenRec/RecInstances/Record.hs
--- a/src/Data/GenRec/RecInstances/Record.hs
+++ b/src/Data/GenRec/RecInstances/Record.hs
@@ -111,6 +111,40 @@
     let ('{':shr) = show r
     in '{' : show lv ++ ", " ++ shr
 
-v1 = (Label @"boolean" .==. True) .**. emptyRecord
-v2 = (Label @"integer" .==. 3) .**. v1
-v3 = (Label @"text" .==. "wa") .**. v2
+
+r =        (Label @"integer" .==. (3 :: Integer))
+     .**.  (Label @"boolean" .==. True)
+     .**.  emptyRecord
+
+
+data Mat
+type Matrix = Rec Mat :: [(Nat, [(Symbol, Type)])] -> Type
+
+type instance  WrapField Mat  (r :: [(Symbol, Type)]) = Record r
+
+-- | Type level show utilities
+type instance ShowRec Mat         = "Matrix"
+type instance ShowField Mat       = "record named "
+
+type TaggedRecord (l :: Nat) (r :: [(Symbol, Type)]) = TagField Mat l r
+pattern TaggedRecord :: forall l r. Record r -> TaggedRecord l r
+pattern TaggedRecord r = TagField Label Label r
+
+
+instance OrdType Nat where
+  type Cmp (m :: Nat) (n :: Nat) = CmpNat m n
+
+
+--m = TaggedRecord @1 r .*. TaggedRecord @2 emptyRecord .*. EmptyRec 
+
+--m = (TagField @Mat (l::Nat) (r :: [(Symbol, Type)]))
+
+m = let tf = (TagField :: forall l r . -- (l::Nat) (r :: [(Symbol, Type)]).
+               Label Mat -> Label l -> Record r -> TagField Mat l r)
+    in      tf Label (Label @1) r
+       .*.  tf Label (Label @2) emptyRecord
+       .*.  EmptyRec
+
+-- m' =        TagField @Mat (Label @Mat) (Label @1) r
+--        .*.  TagField (Label @Mat) (Label @2) (EmptyRec :: Record ('[] :: [(Symbol, Type)]))
+--        .*.  EmptyRec