diff --git a/haskus-utils-types.cabal b/haskus-utils-types.cabal
--- a/haskus-utils-types.cabal
+++ b/haskus-utils-types.cabal
@@ -1,13 +1,13 @@
 name:                haskus-utils-types
-version:             1.4.1
+version:             1.5
 synopsis:            Haskus types utility modules
 license:             BSD3
 license-file:        LICENSE
 author:              Sylvain Henry
 maintainer:          sylvain@haskus.fr
-homepage:            http://www.haskus.org
-copyright:           Sylvain Henry 2018
-category:            System
+homepage:            https://www.haskus.org
+copyright:           Sylvain Henry 2020
+category:            Type
 build-type:          Simple
 cabal-version:       1.20
 
@@ -33,9 +33,8 @@
   other-modules:
 
   build-depends:       
-         base                      >= 4.9 && < 5
+         base >= 4.9 && < 5
 
-  build-tools: 
   ghc-options:          -Wall
   default-language:     Haskell2010
   hs-source-dirs:       src/lib
@@ -48,5 +47,5 @@
    default-language:    Haskell2010
 
    build-depends:
-         base
-      ,  doctest                 >= 0.16
+         base >= 4.9 && < 5
+      ,  doctest >= 0.16
diff --git a/src/lib/Haskus/Utils/Types.hs b/src/lib/Haskus/Utils/Types.hs
--- a/src/lib/Haskus/Utils/Types.hs
+++ b/src/lib/Haskus/Utils/Types.hs
@@ -1,6 +1,7 @@
 -- | Type-level utils
 module Haskus.Utils.Types
    ( module X
+   , Type
    )
 where
 
@@ -11,3 +12,4 @@
 import Haskus.Utils.Types.List       as X
 import Haskus.Utils.Types.Proxy      as X
 import Haskus.Utils.Types.Constraint as X
+import Data.Kind (Type)
diff --git a/src/lib/Haskus/Utils/Types/Bool.hs b/src/lib/Haskus/Utils/Types/Bool.hs
--- a/src/lib/Haskus/Utils/Types/Bool.hs
+++ b/src/lib/Haskus/Utils/Types/Bool.hs
@@ -51,11 +51,11 @@
    boolValue :: Bool
 
 instance KnownBool 'True where
-   {-# INLINE boolValue #-}
+   {-# INLINABLE boolValue #-}
    boolValue = True
 
 instance KnownBool 'False where
-   {-# INLINE boolValue #-}
+   {-# INLINABLE boolValue #-}
    boolValue = False
 
 
diff --git a/src/lib/Haskus/Utils/Types/List.hs b/src/lib/Haskus/Utils/Types/List.hs
--- a/src/lib/Haskus/Utils/Types/List.hs
+++ b/src/lib/Haskus/Utils/Types/List.hs
@@ -25,6 +25,7 @@
    , NubHead
    -- * Sublist
    , Head
+   , Last
    , Tail
    , Init
    , Take
@@ -122,6 +123,11 @@
 type family Head (xs :: [k]) :: k where
    Head (x ': xs) = x
 
+-- | Last of a list
+type family Last (xs :: [k]) :: k where
+   Last '[x]      = x
+   Last (x ': xs) = Last xs
+
 -- | Concat two type lists
 type family Concat (xs :: [k]) (ys :: [k]) :: [k] where
    Concat '[] '[]      = '[]
@@ -202,33 +208,32 @@
 
 -- | Check that a type is member of a type list
 type family CheckMember (a :: k) (l :: [k]) :: Constraint where
-   CheckMember a l = CheckMember' l a l
+   CheckMember a l = CheckMember' (MaybeIndexOf a l) a l
 
 -- | Helper for CheckMember
-type family CheckMember' (i :: [k]) (a :: k) (l :: [k]) :: Constraint where
-   CheckMember' i a (a ': l) = ()
-   CheckMember' i a (b ': l) = CheckMember' i a l
-   CheckMember' i a '[]      = TypeError ( 'Text "`"
-                                     ':<>: 'ShowType a
-                                     ':<>: 'Text "'"
-                                     ':<>: 'Text " is not a member of "
-                                     ':<>: 'ShowType i)
+type family CheckMember' (i :: Nat) (a :: k) (l :: [k]) :: Constraint where
+   CheckMember' 0 a l = TypeError ( 'Text "`"
+                              ':<>: 'ShowType a
+                              ':<>: 'Text "'"
+                              ':<>: 'Text " is not a member of "
+                              ':<>: 'ShowType l)
+   CheckMember' _ _ _ = ()
 
 
 -- | Check that a list is a subset of another
 type family CheckMembers (l1 :: [k]) (l2 :: [k]) :: Constraint where
-   CheckMembers l1 l1 = ()
-   CheckMembers l1 l2 = CheckMembers' l2 '[] l1 l2
+   CheckMembers '[]       l1 = ()
+   CheckMembers (x ': xs) l2 = CheckMembers' (MaybeIndexOf x l2) x xs (x ': xs) l2
 
 -- | Helper for CheckMembers
-type family CheckMembers' (i :: [k]) (e :: [k]) (l1 :: [k]) (l2 :: [k]) :: Constraint where
-   CheckMembers' i e '[] '[] = TypeError (   'ShowType e
-                                       ':$$: 'Text "is not a subset of"
-                                       ':$$: 'ShowType i)
-   CheckMembers' i e '[] l2  = ()
-   CheckMembers' i e (l ': ls) '[]       = CheckMembers' i (l ': e) ls i
-   CheckMembers' i e (x ': xs) (x ': ys) = CheckMembers' i e xs i
-   CheckMembers' i e (x ': xs) (y ': ys) = CheckMembers' i e (x ': xs) ys
+type family CheckMembers' (i :: Nat) (x :: k) (xs :: [k]) (l1 :: [k]) (l2 :: [k]) :: Constraint where
+   CheckMembers' 0 x _ l1 l2 = TypeError (     'ShowType l1
+                                         ':$$: 'Text "is not a subset of"
+                                         ':$$: 'ShowType l2
+                                         ':$$: 'ShowType x
+                                         ':<>: 'Text " is missing from the latter.")
+   CheckMembers' _ _ '[] _ _ = ()
+   CheckMembers' _ _ (x ': xs) l1 l2 = CheckMembers' (MaybeIndexOf x l2) x xs l1 l2
 
 -- | Get list indexes
 type family Indexes (l :: [k]) :: [Nat] where
@@ -270,13 +275,15 @@
    NubHead (x ': xs) = x ': Remove x xs
 
 -- | Get the first index of a type
-type family IndexOf (a :: k) (l :: [k]) :: Nat where
-   IndexOf x xs = IndexOf' x xs xs
+type IndexOf (x :: k) (xs :: [k]) = IndexOf' (MaybeIndexOf x xs) x xs
 
 -- | Get the first index of a type
-type family IndexOf' (a :: k) (l :: [k]) (l2 :: [k]) :: Nat where
-   IndexOf' x (x ': xs) l2 = 0
-   IndexOf' y (x ': xs) l2 = 1 + IndexOf' y xs l2
+type family IndexOf' (i :: Nat) (a :: k) (l :: [k]) :: Nat where
+   IndexOf' 0 x l = TypeError ( 'ShowType x
+                          ':<>: 'Text " not found in list:"
+                          ':$$: 'Text " "
+                          ':<>: 'ShowType l )
+   IndexOf' i _ _ = i - 1
 
 -- | Get all the indexes of a type
 type family IndexesOf (a :: k) (l :: [k]) :: [Nat] where
@@ -295,14 +302,22 @@
 -- | Helper for MaybeIndexOf
 type family MaybeIndexOf' (n :: Nat) (a :: k) (l :: [k]) where
    MaybeIndexOf' n x '[]       = 0
-   MaybeIndexOf' n x (x ': xs) = 1 + n
+   MaybeIndexOf' n x (x ': xs) = n + 1
    MaybeIndexOf' n x (y ': xs) = MaybeIndexOf' (n+1) x xs
 
 -- | Indexed access into the list
-type family Index (n :: Nat) (l :: [k]) :: k where
-   Index 0 (x ': xs) = x
-   Index n (x ': xs) = Index (n-1) xs
+type Index (n :: Nat) (l :: [k]) = Index' n l l
 
+-- | Indexed access into the list
+type family Index' (n :: Nat) (l :: [k]) (l2 :: [k]) = (r :: k) where
+   Index' 0 (x ': _ ) _  = x
+   Index' n (_ ': xs) l2 = Index' (n-1) xs l2
+   Index' n '[]       l2 = TypeError ( 'Text "Index "
+                                ':<>: 'ShowType n
+                                ':<>: 'Text " out of bounds for list:"
+                                ':$$: 'Text " "
+                                ':<>: 'ShowType l2 )
+
 -- | List membership test
 type family Elem (t :: b) (f :: b) (x :: k) (xs :: [k]) :: b where
    Elem t f x '[]       = f
@@ -348,9 +363,12 @@
 --------------------------------------
 
 -- | Constraint: x member of xs
-type Member x xs =
-   ( x ~ Index (IndexOf x xs) xs
-   , KnownNat (IndexOf x xs)
+type family Member x xs :: Constraint where
+   Member x xs = MemberAtIndex (IndexOf x xs) x xs
+   
+type MemberAtIndex i x xs =
+   ( x ~ Index i xs
+   , KnownNat i
    )
 
 -- | Constraint: all the xs are members of ys