diff --git a/changelog.md b/changelog.md
--- a/changelog.md
+++ b/changelog.md
@@ -1,3 +1,9 @@
+## [0.7] - UNRELEASED
+- listProductSequence, matchListProduct
+- sequenceComposeListType
+- mapAllFor
+- fix for GHC 9.10
+
 ## [0.6.2] - 2023-07-25
 - withAllConstraint, withSomeAllConstraint
 - listTypeToListM, listTypeForList, listTypeFind
diff --git a/src/Data/PeanoNat.hs b/src/Data/PeanoNat.hs
--- a/src/Data/PeanoNat.hs
+++ b/src/Data/PeanoNat.hs
@@ -43,4 +43,4 @@
 type ListLength :: forall k. [k] -> PeanoNat
 type family ListLength l where
     ListLength '[] = 'Zero
-    ListLength (a ': aa) = 'Succ (ListLength aa)
+    ListLength (_ ': aa) = 'Succ (ListLength aa)
diff --git a/src/Data/Type/Witness/General/HetConstraint.hs b/src/Data/Type/Witness/General/HetConstraint.hs
--- a/src/Data/Type/Witness/General/HetConstraint.hs
+++ b/src/Data/Type/Witness/General/HetConstraint.hs
@@ -3,6 +3,7 @@
 import Import
 
 type HetConstraintWitness :: forall k1. (k1 -> Constraint) -> forall k2. k2 -> Type
+type role HetConstraintWitness representational nominal
 data HetConstraintWitness c t where
     MkHetConstraintWitness
         :: forall k (c :: k -> Constraint) (t :: k). c t
diff --git a/src/Data/Type/Witness/General/Order.hs b/src/Data/Type/Witness/General/Order.hs
--- a/src/Data/Type/Witness/General/Order.hs
+++ b/src/Data/Type/Witness/General/Order.hs
@@ -2,6 +2,7 @@
 
 import Import
 
+type role WOrdering nominal nominal
 data WOrdering (a :: k) (b :: k) where
     WLT :: forall k (a :: k) (b :: k). WOrdering a b
     WEQ :: forall k (a :: k). WOrdering a a
diff --git a/src/Data/Type/Witness/General/TestHetEquality.hs b/src/Data/Type/Witness/General/TestHetEquality.hs
--- a/src/Data/Type/Witness/General/TestHetEquality.hs
+++ b/src/Data/Type/Witness/General/TestHetEquality.hs
@@ -20,6 +20,7 @@
 
 -- | Equivalent to ':~~:', but can be made an instance of 'TestHetEquality'
 type HetEqual :: forall ka. ka -> forall kb. kb -> Type
+type role HetEqual nominal nominal
 data HetEqual a b where
     HetRefl :: forall k (a :: k). HetEqual a a
 
diff --git a/src/Data/Type/Witness/Specific/All.hs b/src/Data/Type/Witness/Specific/All.hs
--- a/src/Data/Type/Witness/Specific/All.hs
+++ b/src/Data/Type/Witness/Specific/All.hs
@@ -5,11 +5,16 @@
 import Import
 
 type AllFor :: forall k. (k -> Type) -> (k -> Type) -> Type
+type role AllFor representational representational
 newtype AllFor f w = MkAllFor
     { unAllFor :: forall t. w t -> f t
     }
 
+mapAllFor :: (forall a. f1 a -> f2 a) -> AllFor f1 w -> AllFor f2 w
+mapAllFor ff (MkAllFor wtft) = MkAllFor $ ff . wtft
+
 type AllOf :: (Type -> Type) -> Type
+type role AllOf representational
 newtype AllOf w = MkAllOf
     { unAllOf :: forall t. w t -> t
     }
diff --git a/src/Data/Type/Witness/Specific/Either.hs b/src/Data/Type/Witness/Specific/Either.hs
--- a/src/Data/Type/Witness/Specific/Either.hs
+++ b/src/Data/Type/Witness/Specific/Either.hs
@@ -10,6 +10,7 @@
 import Import
 
 type EitherType :: forall k. (k -> Type) -> (k -> Type) -> (k -> Type)
+type role EitherType representational representational nominal
 data EitherType w1 w2 t
     = LeftType (w1 t)
     | RightType (w2 t)
@@ -71,7 +72,7 @@
 type ConsType a = EitherType (SingleType a)
 
 instance ListElementWitness lt => ListElementWitness (ConsType a lt) where
-    type WitnessTypeList (ConsType a lt) = a : (WitnessTypeList lt)
+    type WitnessTypeList (ConsType a lt) = a ': (WitnessTypeList lt)
     toListElementWitness (LeftType Refl) = FirstElementType
     toListElementWitness (RightType sel) = RestElementType $ toListElementWitness sel
     fromListElementWitness FirstElementType = LeftType Refl
diff --git a/src/Data/Type/Witness/Specific/Empty.hs b/src/Data/Type/Witness/Specific/Empty.hs
--- a/src/Data/Type/Witness/Specific/Empty.hs
+++ b/src/Data/Type/Witness/Specific/Empty.hs
@@ -9,9 +9,10 @@
 import Import
 
 type EmptyType :: forall k. k -> Type
+type role EmptyType phantom
 newtype EmptyType t =
     MkEmptyType Void
-    deriving (Eq, Countable, Searchable, Empty)
+    deriving newtype (Eq, Countable, Searchable, Empty)
 
 instance Finite (EmptyType t) where
     allValues = []
diff --git a/src/Data/Type/Witness/Specific/FiniteAllFor.hs b/src/Data/Type/Witness/Specific/FiniteAllFor.hs
--- a/src/Data/Type/Witness/Specific/FiniteAllFor.hs
+++ b/src/Data/Type/Witness/Specific/FiniteAllFor.hs
@@ -7,6 +7,7 @@
 import Import
 
 type FiniteAllFor :: forall k. (k -> Type) -> (k -> Type) -> Type
+type role FiniteAllFor representational representational
 data FiniteAllFor f w = MkFiniteAllFor
     { finiteDomain :: [Some w]
     , finiteGetAllFor :: forall t. w t -> f t
diff --git a/src/Data/Type/Witness/Specific/FixedList.hs b/src/Data/Type/Witness/Specific/FixedList.hs
--- a/src/Data/Type/Witness/Specific/FixedList.hs
+++ b/src/Data/Type/Witness/Specific/FixedList.hs
@@ -7,6 +7,7 @@
 import Import
 
 type FixedList :: PeanoNat -> Type -> Type
+type role FixedList nominal representational
 data FixedList n a where
     NilFixedList :: FixedList 'Zero a
     ConsFixedList :: a -> FixedList n a -> FixedList ('Succ n) a
diff --git a/src/Data/Type/Witness/Specific/List/Element.hs b/src/Data/Type/Witness/Specific/List/Element.hs
--- a/src/Data/Type/Witness/Specific/List/Element.hs
+++ b/src/Data/Type/Witness/Specific/List/Element.hs
@@ -8,9 +8,10 @@
 import Import
 
 type ListElementType :: forall k. [k] -> k -> Type
+type role ListElementType nominal nominal
 data ListElementType kk t where
-    FirstElementType :: ListElementType (t : tt) t
-    RestElementType :: ListElementType aa t -> ListElementType (a : aa) t
+    FirstElementType :: ListElementType (t ': tt) t
+    RestElementType :: ListElementType aa t -> ListElementType (a ': aa) t
 
 instance TestEquality (ListElementType tt) where
     testEquality FirstElementType FirstElementType = Just Refl
diff --git a/src/Data/Type/Witness/Specific/List/List.hs b/src/Data/Type/Witness/Specific/List/List.hs
--- a/src/Data/Type/Witness/Specific/List/List.hs
+++ b/src/Data/Type/Witness/Specific/List/List.hs
@@ -11,9 +11,10 @@
 -- | a witness type for lists of types
 -- The @w@ parameter is the witness type of the elements.
 type ListType :: (k -> Type) -> ([k] -> Type)
+type role ListType representational nominal
 data ListType w lt where
     NilListType :: ListType w '[]
-    ConsListType :: w a -> ListType w lt -> ListType w (a : lt)
+    ConsListType :: w a -> ListType w lt -> ListType w (a ': lt)
 
 instance Representative w => Representative (ListType w) where
     getRepWitness NilListType = Dict
@@ -24,7 +25,7 @@
 instance Representative w => Is (ListType w) '[] where
     representative = NilListType
 
-instance (Is w a, Is (ListType w) lt) => Is (ListType w) (a : lt) where
+instance (Is w a, Is (ListType w) lt) => Is (ListType w) (a ': lt) where
     representative = ConsListType representative representative
 
 instance TestEquality w => TestEquality (ListType w) where
@@ -111,3 +112,7 @@
     case f a of
         Just r -> Just r
         Nothing -> listTypeFind f aa
+
+sequenceComposeListType :: Applicative f => ListType (Compose f w) lt -> f (ListType w lt)
+sequenceComposeListType NilListType = pure NilListType
+sequenceComposeListType (ConsListType (Compose fwa) tt) = liftA2 ConsListType fwa $ sequenceComposeListType tt
diff --git a/src/Data/Type/Witness/Specific/List/Product.hs b/src/Data/Type/Witness/Specific/List/Product.hs
--- a/src/Data/Type/Witness/Specific/List/Product.hs
+++ b/src/Data/Type/Witness/Specific/List/Product.hs
@@ -1,16 +1,19 @@
+{-# OPTIONS -Wno-redundant-constraints #-}
+
 module Data.Type.Witness.Specific.List.Product where
 
 import Data.Type.Witness.General.Representative
 import Data.Type.Witness.General.WitnessConstraint
 import Data.Type.Witness.Specific.List.Element
 import Data.Type.Witness.Specific.List.List
+import Data.Type.Witness.Specific.Some
 import Import
 import Unsafe.Coerce
 
 type ListProduct :: [Type] -> Type
 type family ListProduct w = r | r -> w where
     ListProduct '[] = ()
-    ListProduct (t : tt) = (t, ListProduct tt)
+    ListProduct (t ': tt) = (t, ListProduct tt)
 
 -- | workaround for https://gitlab.haskell.org/ghc/ghc/issues/10833
 injectiveListProduct ::
@@ -61,7 +64,31 @@
 listProductModifyElement :: ListElementType list t -> (t -> t) -> ListProduct list -> ListProduct list
 listProductModifyElement n aa t = listProductPutElement n (aa (listProductGetElement n t)) t
 
+listProductSequence ::
+       forall f list. Applicative f
+    => ListType f list
+    -> f (ListProduct list)
+listProductSequence NilListType = pure ()
+listProductSequence (ConsListType t tt) = liftA2 (,) t $ listProductSequence tt
+
+pickListProduct :: TestEquality w => ListType w lta -> w b -> Maybe (ListProduct lta -> b)
+pickListProduct NilListType _ = Nothing
+pickListProduct (ConsListType wa _) wb
+    | Just Refl <- testEquality wa wb = Just fst
+pickListProduct (ConsListType _ la) wb = fmap (\f -> f . snd) $ pickListProduct la wb
+
+matchListProduct ::
+       TestEquality w => ListType w lta -> ListType w ltb -> Either (Some w) (ListProduct lta -> ListProduct ltb)
+matchListProduct _ NilListType = return $ \_ -> ()
+matchListProduct la (ConsListType wb lb) =
+    case pickListProduct la wb of
+        Nothing -> Left $ MkSome wb
+        Just f1 -> do
+            fr <- matchListProduct la lb
+            return $ \pa -> (f1 pa, fr pa)
+
 type ListProductType :: (Type -> Type) -> (Type -> Type)
+type role ListProductType representational nominal
 data ListProductType wit t where
     MkListProductType
         :: forall (wit :: Type -> Type) (lt :: [Type]). ListType wit lt -> ListProductType wit (ListProduct lt)
diff --git a/src/Data/Type/Witness/Specific/List/Sum.hs b/src/Data/Type/Witness/Specific/List/Sum.hs
--- a/src/Data/Type/Witness/Specific/List/Sum.hs
+++ b/src/Data/Type/Witness/Specific/List/Sum.hs
@@ -1,3 +1,5 @@
+{-# OPTIONS -Wno-redundant-constraints #-}
+
 module Data.Type.Witness.Specific.List.Sum where
 
 import Data.Type.Witness.General.Representative
@@ -9,7 +11,7 @@
 type ListSum :: [Type] -> Type
 type family ListSum w = r | r -> w where
     ListSum '[] = Void
-    ListSum (t : tt) = Either t (ListSum tt)
+    ListSum (t ': tt) = Either t (ListSum tt)
 
 -- | workaround for https://gitlab.haskell.org/ghc/ghc/issues/10833
 injectiveListSum ::
@@ -35,6 +37,7 @@
 mapListSum (ConsListType _wa wr) f (Right rest) = Right $ mapListSum wr f rest
 
 type ListSumType :: (Type -> Type) -> (Type -> Type)
+type role ListSumType representational nominal
 data ListSumType wit t where
     MkListSumType :: forall (wit :: Type -> Type) (lt :: [Type]). ListType wit lt -> ListSumType wit (ListSum lt)
 
diff --git a/src/Data/Type/Witness/Specific/Natural.hs b/src/Data/Type/Witness/Specific/Natural.hs
--- a/src/Data/Type/Witness/Specific/Natural.hs
+++ b/src/Data/Type/Witness/Specific/Natural.hs
@@ -30,6 +30,7 @@
 import Unsafe.Coerce
 
 type NaturalType :: Nat -> Type
+type role NaturalType nominal
 data NaturalType bn where
     MkNaturalType :: KnownNat bn => NaturalType bn
 
diff --git a/src/Data/Type/Witness/Specific/OrderedWitnessMap/For.hs b/src/Data/Type/Witness/Specific/OrderedWitnessMap/For.hs
--- a/src/Data/Type/Witness/Specific/OrderedWitnessMap/For.hs
+++ b/src/Data/Type/Witness/Specific/OrderedWitnessMap/For.hs
@@ -1,6 +1,6 @@
 module Data.Type.Witness.Specific.OrderedWitnessMap.For where
 
-import qualified Data.Map as Map
+import Data.Map qualified as Map
 import Data.Type.Witness.General.Order
 import Data.Type.Witness.Specific.Some
 import Import
@@ -8,9 +8,10 @@
 -- | A dictionary that is heterogenous up to its simple witness type @w@.
 -- Witnesses are the keys of the dictionary, and the values they witness are the values of the dictionary.
 type OrderedWitnessMapFor :: forall k. (k -> Type) -> (k -> Type) -> Type
+type role OrderedWitnessMapFor representational nominal
 newtype OrderedWitnessMapFor f w =
     MkOrderedWitnessMapFor (Map.Map (Some w) (SomeFor f w))
-    deriving (Semigroup, Monoid)
+    deriving newtype (Semigroup, Monoid)
 
 -- | An empty dictionary.
 emptyOrderedWitnessMapFor :: TestOrder w => OrderedWitnessMapFor f w
diff --git a/src/Data/Type/Witness/Specific/Pair.hs b/src/Data/Type/Witness/Specific/Pair.hs
--- a/src/Data/Type/Witness/Specific/Pair.hs
+++ b/src/Data/Type/Witness/Specific/Pair.hs
@@ -7,6 +7,7 @@
 
 -- | a witness for pairs of witnesses
 type PairType :: (k -> Type) -> (k -> Type) -> (k -> Type)
+type role PairType representational representational nominal
 data PairType w1 w2 t =
     MkPairType (w1 t)
                (w2 t)
diff --git a/src/Data/Type/Witness/Specific/PeanoNat.hs b/src/Data/Type/Witness/Specific/PeanoNat.hs
--- a/src/Data/Type/Witness/Specific/PeanoNat.hs
+++ b/src/Data/Type/Witness/Specific/PeanoNat.hs
@@ -7,6 +7,7 @@
 import Import
 
 type PeanoNatType :: PeanoNat -> Type
+type role PeanoNatType nominal
 data PeanoNatType t where
     ZeroType :: PeanoNatType 'Zero
     SuccType :: PeanoNatType t -> PeanoNatType ('Succ t)
@@ -49,6 +50,7 @@
     valueToWitness (Succ n) cont = valueToWitness n $ \t -> cont $ SuccType t
 
 type GreaterEqual :: PeanoNat -> PeanoNat -> Type
+type role GreaterEqual nominal nominal
 data GreaterEqual a b where
     ZeroGreaterEqual :: GreaterEqual a 'Zero
     SuccGreaterEqual :: GreaterEqual a b -> GreaterEqual ('Succ a) ('Succ b)
@@ -100,6 +102,7 @@
         Refl -> diff1GreaterEqual $ addPeanoNatTypeGE a b
 
 type Greater :: PeanoNat -> PeanoNat -> Type
+type role Greater nominal nominal
 data Greater a b where
     MkGreater :: GreaterEqual a b -> Greater ('Succ a) b
 
diff --git a/src/Data/Type/Witness/Specific/Some.hs b/src/Data/Type/Witness/Specific/Some.hs
--- a/src/Data/Type/Witness/Specific/Some.hs
+++ b/src/Data/Type/Witness/Specific/Some.hs
@@ -7,6 +7,7 @@
 
 -- | Any value with a witness to a parameter of its type.
 type SomeFor :: forall k. (k -> Type) -> (k -> Type) -> Type
+type role SomeFor representational representational
 data SomeFor f w =
     forall a. MkSomeFor (w a)
                         (f a)
@@ -50,7 +51,7 @@
     return a
 
 type Some :: forall k. (k -> Type) -> Type
-type Some = SomeFor (Const ())
+type Some @k = SomeFor @k (Const ())
 
 pattern MkSome :: w a -> Some w
 
diff --git a/src/Data/Type/Witness/Specific/Symbol.hs b/src/Data/Type/Witness/Specific/Symbol.hs
--- a/src/Data/Type/Witness/Specific/Symbol.hs
+++ b/src/Data/Type/Witness/Specific/Symbol.hs
@@ -12,6 +12,7 @@
 import Import
 
 type SymbolType :: Symbol -> Type
+type role SymbolType nominal
 data SymbolType symbol where
     MkSymbolType :: KnownSymbol symbol => SymbolType symbol
 
diff --git a/src/Data/Type/Witness/Specific/WitnessMap/For.hs b/src/Data/Type/Witness/Specific/WitnessMap/For.hs
--- a/src/Data/Type/Witness/Specific/WitnessMap/For.hs
+++ b/src/Data/Type/Witness/Specific/WitnessMap/For.hs
@@ -6,9 +6,10 @@
 -- | A dictionary that is heterogenous up to its simple witness type @w@.
 -- Witnesses are the keys of the dictionary, and the values they witness are the values of the dictionary.
 type WitnessMapFor :: forall k. (k -> Type) -> (k -> Type) -> Type
+type role WitnessMapFor representational representational
 newtype WitnessMapFor f w = MkWitnessMapFor
     { witnessMapForToList :: [SomeFor f w]
-    } deriving (Semigroup, Monoid)
+    } deriving newtype (Semigroup, Monoid)
 
 -- | An empty dictionary.
 emptyWitnessMapFor :: WitnessMapFor f w
diff --git a/witness.cabal b/witness.cabal
--- a/witness.cabal
+++ b/witness.cabal
@@ -1,25 +1,32 @@
 cabal-version: 2.2
 
--- This file has been generated from package.yaml by hpack version 0.35.2.
+-- This file has been generated from package.yaml by hpack version 0.37.0.
 --
 -- see: https://github.com/sol/hpack
 
 name:           witness
-version:        0.6.2
+version:        0.7
 synopsis:       values that witness types
 description:    A /witness/ is a value that witnesses some sort of constraint on some list of type variables. This library provides support for a wide variety of witness types. It also provides classes for /representatives/, which are values that represent types.
 category:       Data
-homepage:       https://github.com/AshleyYakeley/witness
+homepage:       https://github.com/AshleyYakeley/witness#readme
 bug-reports:    https://github.com/AshleyYakeley/witness/issues
 author:         Ashley Yakeley
 maintainer:     <ashley@semantic.org>
-copyright:      (c) 2017-2022 Ashley Yakeley
+copyright:      (c) 2017-2024 Ashley Yakeley
 license:        BSD-2-Clause
 license-file:   LICENSE
 build-type:     Simple
-extra-source-files:
+tested-with:
+    GHC == 9.8.4
+  , GHC == 9.10.1
+extra-doc-files:
     changelog.md
 
+source-repository head
+  type: git
+  location: https://github.com/AshleyYakeley/witness
+
 library
   exposed-modules:
       Data.Type.Witness.Apply
@@ -62,52 +69,33 @@
   default-extensions:
       AllowAmbiguousTypes
       Arrows
-      ConstraintKinds
       DataKinds
       DefaultSignatures
-      EmptyCase
-      EmptyDataDecls
-      ExistentialQuantification
-      FlexibleContexts
-      FlexibleInstances
-      ForeignFunctionInterface
+      DerivingStrategies
       FunctionalDependencies
-      GADTs
-      GeneralizedNewtypeDeriving
       ImplicitParams
       NoImplicitPrelude
-      InstanceSigs
-      KindSignatures
       LambdaCase
-      MultiParamTypeClasses
       OverloadedLabels
       OverloadedStrings
       PartialTypeSignatures
-      PatternGuards
       PatternSynonyms
-      PolyKinds
       QuantifiedConstraints
-      RankNTypes
       RecordWildCards
       RecursiveDo
-      ScopedTypeVariables
-      StandaloneDeriving
-      StandaloneKindSignatures
+      RoleAnnotations
       NoStarIsType
       TemplateHaskell
-      TypeApplications
+      TypeAbstractions
       TypeFamilies
       TypeFamilyDependencies
-      TypeInType
-      TypeOperators
-      TypeSynonymInstances
       UndecidableInstances
       UndecidableSuperClasses
       ViewPatterns
-  ghc-options: -Wall -Wincomplete-uni-patterns -Wincomplete-record-updates -Wcompat -Wnoncanonical-monad-instances
+  ghc-options: -Weverything -Wno-missing-import-lists -Wno-missing-export-lists -Wno-unsafe -Wno-missing-safe-haskell-mode -Wno-missing-kind-signatures -Wno-partial-type-signatures -Wno-monomorphism-restriction -Wno-missing-local-signatures -Wno-partial-fields -Wno-all-missed-specialisations -Wno-missed-specialisations
   build-depends:
-      base >=4.16 && <5
-    , constraints >=0.13
-    , containers >=0.4
+      base >=4.19 && <5
+    , constraints >=0.14
+    , containers >=0.6
     , countable >=1.2
-  default-language: Haskell2010
+  default-language: GHC2021