{-# LANGUAGE AllowAmbiguousTypes #-} {-# LANGUAGE BangPatterns #-} {-# LANGUAGE ConstraintKinds #-} {-# LANGUAGE CPP #-} {-# LANGUAGE DataKinds #-} {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE GADTs #-} {-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE PolyKinds #-} {-# LANGUAGE RankNTypes #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE Trustworthy #-} {-# LANGUAGE TypeApplications #-} {-# LANGUAGE TypeFamilies #-} #if __GLASGOW_HASKELL__ >= 806 {-# LANGUAGE QuantifiedConstraints #-} #endif {-# LANGUAGE TypeOperators #-} {-# LANGUAGE UndecidableInstances #-} -- | Core vinyl definitions. The 'Rec' data type is defined here, but -- also of interest are definitions commonly used functions like -- 'rmap', 'rapply', and 'rtraverse'. -- -- The definitions in this module are written in terms of type classes -- so that the definitions may be specialized to each record type at -- which they are used. This usually helps with runtime performance, -- but can slow down compilation time. If you are experiencing poor -- compile times, you may wish to try the semantically equivalent -- definitions in the "Data.Vinyl.Recursive" module: they should -- produce the same results given the same inputs as functions defined -- in this module, but they will not be specialized to your record -- type. Instead, they treat the record as a list of fields, so will -- have performance linear in the size of the record. module Data.Vinyl.Core where import Data.Coerce (Coercible) #if __GLASGOW_HASKELL__ < 808 import Data.Monoid (Monoid) #endif #if __GLASGOW_HASKELL__ < 804 import Data.Semigroup (Semigroup(..)) #endif import Foreign.Ptr (castPtr, plusPtr) import Foreign.Storable (Storable(..)) import Data.Functor.Product (Product(Pair)) import Data.List (intercalate) import Data.Vinyl.Functor import Data.Vinyl.TypeLevel import Data.Type.Equality (TestEquality (..), (:~:) (..)) import Data.Type.Coercion (TestCoercion (..), Coercion (..)) import GHC.Generics import GHC.Types (Constraint, Type) import Unsafe.Coerce (unsafeCoerce) import Control.DeepSeq (NFData, rnf) #if __GLASGOW_HASKELL__ < 806 import Data.Constraint.Forall (Forall) #endif -- | A record is parameterized by a universe @u@, an interpretation @f@ and a -- list of rows @rs@. The labels or indices of the record are given by -- inhabitants of the kind @u@; the type of values at any label @r :: u@ is -- given by its interpretation @f r :: *@. data Rec :: (u -> *) -> [u] -> * where RNil :: Rec f '[] (:&) :: !(f r) -> !(Rec f rs) -> Rec f (r ': rs) infixr 7 :& infixr 5 <+> infixl 8 <<$>> infixl 8 <<*>> instance TestEquality f => TestEquality (Rec f) where testEquality :: Rec f a -> Rec f b -> Maybe (a :~: b) testEquality Rec f a RNil Rec f b RNil = (a :~: a) -> Maybe (a :~: a) forall a. a -> Maybe a Just a :~: a forall k (a :: k). a :~: a Refl testEquality (f r x :& Rec f rs xs) (f r y :& Rec f rs ys) = do r :~: r Refl <- f r -> f r -> Maybe (r :~: r) forall k (f :: k -> *) (a :: k) (b :: k). TestEquality f => f a -> f b -> Maybe (a :~: b) testEquality f r x f r y rs :~: rs Refl <- Rec f rs -> Rec f rs -> Maybe (rs :~: rs) forall k (f :: k -> *) (a :: k) (b :: k). TestEquality f => f a -> f b -> Maybe (a :~: b) testEquality Rec f rs xs Rec f rs ys (a :~: a) -> Maybe (a :~: a) forall a. a -> Maybe a Just a :~: a forall k (a :: k). a :~: a Refl testEquality Rec f a _ Rec f b _ = Maybe (a :~: b) forall a. Maybe a Nothing instance TestCoercion f => TestCoercion (Rec f) where testCoercion :: Rec f a -> Rec f b -> Maybe (Coercion a b) testCoercion Rec f a RNil Rec f b RNil = Coercion a b -> Maybe (Coercion a b) forall a. a -> Maybe a Just Coercion a b forall k (a :: k) (b :: k). Coercible a b => Coercion a b Coercion testCoercion (f r x :& Rec f rs xs) (f r y :& Rec f rs ys) = do Coercion r r Coercion <- f r -> f r -> Maybe (Coercion r r) forall k (f :: k -> *) (a :: k) (b :: k). TestCoercion f => f a -> f b -> Maybe (Coercion a b) testCoercion f r x f r y Coercion rs rs Coercion <- Rec f rs -> Rec f rs -> Maybe (Coercion rs rs) forall k (f :: k -> *) (a :: k) (b :: k). TestCoercion f => f a -> f b -> Maybe (Coercion a b) testCoercion Rec f rs xs Rec f rs ys Coercion a b -> Maybe (Coercion a b) forall a. a -> Maybe a Just Coercion a b forall k (a :: k) (b :: k). Coercible a b => Coercion a b Coercion testCoercion Rec f a _ Rec f b _ = Maybe (Coercion a b) forall a. Maybe a Nothing -- | Two records may be pasted together. rappend :: Rec f as -> Rec f bs -> Rec f (as ++ bs) rappend :: Rec f as -> Rec f bs -> Rec f (as ++ bs) rappend Rec f as RNil Rec f bs ys = Rec f bs Rec f (as ++ bs) ys rappend (f r x :& Rec f rs xs) Rec f bs ys = f r x f r -> Rec f (rs ++ bs) -> Rec f (r : (rs ++ bs)) forall a (f :: a -> *) (r :: a) (rs :: [a]). f r -> Rec f rs -> Rec f (r : rs) :& (Rec f rs xs Rec f rs -> Rec f bs -> Rec f (rs ++ bs) forall k (f :: k -> *) (as :: [k]) (bs :: [k]). Rec f as -> Rec f bs -> Rec f (as ++ bs) `rappend` Rec f bs ys) -- | A shorthand for 'rappend'. (<+>) :: Rec f as -> Rec f bs -> Rec f (as ++ bs) <+> :: Rec f as -> Rec f bs -> Rec f (as ++ bs) (<+>) = Rec f as -> Rec f bs -> Rec f (as ++ bs) forall k (f :: k -> *) (as :: [k]) (bs :: [k]). Rec f as -> Rec f bs -> Rec f (as ++ bs) rappend -- | Combine two records by combining their fields using the given -- function. The first argument is a binary operation for combining -- two values (e.g. '(<>)'), the second argument takes a record field -- into the type equipped with the desired operation, the third -- argument takes the combined value back to a result type. rcombine :: (RMap rs, RApply rs) => (forall a. m a -> m a -> m a) -> (forall a. f a -> m a) -> (forall a. m a -> g a) -> Rec f rs -> Rec f rs -> Rec g rs rcombine :: (forall (a :: u). m a -> m a -> m a) -> (forall (a :: u). f a -> m a) -> (forall (a :: u). m a -> g a) -> Rec f rs -> Rec f rs -> Rec g rs rcombine forall (a :: u). m a -> m a -> m a smash forall (a :: u). f a -> m a toM forall (a :: u). m a -> g a fromM Rec f rs x Rec f rs y = (forall (a :: u). m a -> g a) -> Rec m rs -> Rec g rs forall u (rs :: [u]) (f :: u -> *) (g :: u -> *). RMap rs => (forall (x :: u). f x -> g x) -> Rec f rs -> Rec g rs rmap forall (a :: u). m a -> g a fromM (Rec (Lift (->) m m) rs -> Rec m rs -> Rec m rs forall u (rs :: [u]) (f :: u -> *) (g :: u -> *). RApply rs => Rec (Lift (->) f g) rs -> Rec f rs -> Rec g rs rapply ((forall (x :: u). m x -> Lift (->) m m x) -> Rec m rs -> Rec (Lift (->) m m) rs forall u (rs :: [u]) (f :: u -> *) (g :: u -> *). RMap rs => (forall (x :: u). f x -> g x) -> Rec f rs -> Rec g rs rmap ((m x -> m x) -> Lift (->) m m x forall l l' k (op :: l -> l' -> *) (f :: k -> l) (g :: k -> l') (x :: k). op (f x) (g x) -> Lift op f g x Lift ((m x -> m x) -> Lift (->) m m x) -> (m x -> m x -> m x) -> m x -> Lift (->) m m x forall b c a. (b -> c) -> (a -> b) -> a -> c . m x -> m x -> m x forall (a :: u). m a -> m a -> m a smash) Rec m rs x') Rec m rs y') where x' :: Rec m rs x' = (forall (a :: u). f a -> m a) -> Rec f rs -> Rec m rs forall u (rs :: [u]) (f :: u -> *) (g :: u -> *). RMap rs => (forall (x :: u). f x -> g x) -> Rec f rs -> Rec g rs rmap forall (a :: u). f a -> m a toM Rec f rs x y' :: Rec m rs y' = (forall (a :: u). f a -> m a) -> Rec f rs -> Rec m rs forall u (rs :: [u]) (f :: u -> *) (g :: u -> *). RMap rs => (forall (x :: u). f x -> g x) -> Rec f rs -> Rec g rs rmap forall (a :: u). f a -> m a toM Rec f rs y -- | 'Rec' @_ rs@ with labels in kind @u@ gives rise to a functor @Hask^u -> -- Hask@; that is, a natural transformation between two interpretation functors -- @f,g@ may be used to transport a value from 'Rec' @f rs@ to 'Rec' @g rs@. class RMap rs where rmap :: (forall x. f x -> g x) -> Rec f rs -> Rec g rs instance RMap '[] where rmap :: (forall (x :: u). f x -> g x) -> Rec f '[] -> Rec g '[] rmap forall (x :: u). f x -> g x _ Rec f '[] RNil = Rec g '[] forall u (f :: u -> *). Rec f '[] RNil {-# INLINE rmap #-} instance RMap xs => RMap (x ': xs) where rmap :: (forall (x :: u). f x -> g x) -> Rec f (x : xs) -> Rec g (x : xs) rmap forall (x :: u). f x -> g x f (f r x :& Rec f rs xs) = f r -> g r forall (x :: u). f x -> g x f f r x g r -> Rec g rs -> Rec g (r : rs) forall a (f :: a -> *) (r :: a) (rs :: [a]). f r -> Rec f rs -> Rec f (r : rs) :& (forall (x :: u). f x -> g x) -> Rec f rs -> Rec g rs forall u (rs :: [u]) (f :: u -> *) (g :: u -> *). RMap rs => (forall (x :: u). f x -> g x) -> Rec f rs -> Rec g rs rmap forall (x :: u). f x -> g x f Rec f rs xs {-# INLINE rmap #-} -- | A shorthand for 'rmap'. (<<$>>) :: RMap rs => (forall x. f x -> g x) -> Rec f rs -> Rec g rs <<$>> :: (forall (x :: u). f x -> g x) -> Rec f rs -> Rec g rs (<<$>>) = (forall (x :: u). f x -> g x) -> Rec f rs -> Rec g rs forall u (rs :: [u]) (f :: u -> *) (g :: u -> *). RMap rs => (forall (x :: u). f x -> g x) -> Rec f rs -> Rec g rs rmap {-# INLINE (<<$>>) #-} -- | An inverted shorthand for 'rmap'. (<<&>>) :: RMap rs => Rec f rs -> (forall x. f x -> g x) -> Rec g rs Rec f rs xs <<&>> :: Rec f rs -> (forall (x :: u). f x -> g x) -> Rec g rs <<&>> forall (x :: u). f x -> g x f = (forall (x :: u). f x -> g x) -> Rec f rs -> Rec g rs forall u (rs :: [u]) (f :: u -> *) (g :: u -> *). RMap rs => (forall (x :: u). f x -> g x) -> Rec f rs -> Rec g rs rmap forall (x :: u). f x -> g x f Rec f rs xs {-# INLINE (<<&>>) #-} -- | A record of components @f r -> g r@ may be applied to a record of @f@ to -- get a record of @g@. class RApply rs where rapply :: Rec (Lift (->) f g) rs -> Rec f rs -> Rec g rs instance RApply '[] where rapply :: Rec (Lift (->) f g) '[] -> Rec f '[] -> Rec g '[] rapply Rec (Lift (->) f g) '[] _ Rec f '[] RNil = Rec g '[] forall u (f :: u -> *). Rec f '[] RNil {-# INLINE rapply #-} instance RApply xs => RApply (x ': xs) where rapply :: Rec (Lift (->) f g) (x : xs) -> Rec f (x : xs) -> Rec g (x : xs) rapply (Lift (->) f g r f :& Rec (Lift (->) f g) rs fs) (f r x :& Rec f rs xs) = Lift (->) f g r -> f r -> g x forall l l' (op :: l -> l' -> *) k (f :: k -> l) (g :: k -> l') (x :: k). Lift op f g x -> op (f x) (g x) getLift Lift (->) f g r f f r x g x -> Rec g rs -> Rec g (x : rs) forall a (f :: a -> *) (r :: a) (rs :: [a]). f r -> Rec f rs -> Rec f (r : rs) :& (Rec (Lift (->) f g) rs fs Rec (Lift (->) f g) rs -> Rec f rs -> Rec g rs forall u (rs :: [u]) (f :: u -> *) (g :: u -> *). RApply rs => Rec (Lift (->) f g) rs -> Rec f rs -> Rec g rs `rapply` Rec f rs Rec f rs xs) {-# INLINE rapply #-} -- | A shorthand for 'rapply'. (<<*>>) :: RApply rs => Rec (Lift (->) f g) rs -> Rec f rs -> Rec g rs <<*>> :: Rec (Lift (->) f g) rs -> Rec f rs -> Rec g rs (<<*>>) = Rec (Lift (->) f g) rs -> Rec f rs -> Rec g rs forall u (rs :: [u]) (f :: u -> *) (g :: u -> *). RApply rs => Rec (Lift (->) f g) rs -> Rec f rs -> Rec g rs rapply {-# INLINE (<<*>>) #-} -- | Given a section of some functor, records in that functor of any size are -- inhabited. class RecApplicative rs where rpure :: (forall x. f x) -> Rec f rs instance RecApplicative '[] where rpure :: (forall (x :: u). f x) -> Rec f '[] rpure forall (x :: u). f x _ = Rec f '[] forall u (f :: u -> *). Rec f '[] RNil {-# INLINE rpure #-} instance RecApplicative rs => RecApplicative (r ': rs) where rpure :: (forall (x :: u). f x) -> Rec f (r : rs) rpure forall (x :: u). f x s = f r forall (x :: u). f x s f r -> Rec f rs -> Rec f (r : rs) forall a (f :: a -> *) (r :: a) (rs :: [a]). f r -> Rec f rs -> Rec f (r : rs) :& (forall (x :: u). f x) -> Rec f rs forall u (rs :: [u]) (f :: u -> *). RecApplicative rs => (forall (x :: u). f x) -> Rec f rs rpure forall (x :: u). f x s {-# INLINE rpure #-} -- | A record may be traversed with respect to its interpretation functor. This -- can be used to yank (some or all) effects from the fields of the record to -- the outside of the record. rtraverse :: Applicative h => (forall x. f x -> h (g x)) -> Rec f rs -> h (Rec g rs) rtraverse :: (forall (x :: u). f x -> h (g x)) -> Rec f rs -> h (Rec g rs) rtraverse forall (x :: u). f x -> h (g x) _ Rec f rs RNil = Rec g '[] -> h (Rec g '[]) forall (f :: * -> *) a. Applicative f => a -> f a pure Rec g '[] forall u (f :: u -> *). Rec f '[] RNil rtraverse forall (x :: u). f x -> h (g x) f (f r x :& Rec f rs xs) = g r -> Rec g rs -> Rec g (r : rs) forall a (f :: a -> *) (r :: a) (rs :: [a]). f r -> Rec f rs -> Rec f (r : rs) (:&) (g r -> Rec g rs -> Rec g (r : rs)) -> h (g r) -> h (Rec g rs -> Rec g (r : rs)) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b <$> f r -> h (g r) forall (x :: u). f x -> h (g x) f f r x h (Rec g rs -> Rec g (r : rs)) -> h (Rec g rs) -> h (Rec g (r : rs)) forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b <*> (forall (x :: u). f x -> h (g x)) -> Rec f rs -> h (Rec g rs) forall u (h :: * -> *) (f :: u -> *) (g :: u -> *) (rs :: [u]). Applicative h => (forall (x :: u). f x -> h (g x)) -> Rec f rs -> h (Rec g rs) rtraverse forall (x :: u). f x -> h (g x) f Rec f rs xs {-# INLINABLE rtraverse #-} -- | While 'rtraverse' pulls the interpretation functor out of the -- record, 'rtraverseIn' pushes the interpretation functor in to each -- field type. This is particularly useful when you wish to discharge -- that interpretation on a per-field basis. For instance, rather than -- a @Rec IO '[a,b]@, you may wish to have a @Rec Identity '[IO a, IO -- b]@ so that you can evaluate a single field to obtain a value of -- type @Rec Identity '[a, IO b]@. rtraverseIn :: forall h f g rs. (forall a. f a -> g (ApplyToField h a)) -> Rec f rs -> Rec g (MapTyCon h rs) rtraverseIn :: (forall (a :: u). f a -> g (ApplyToField h a)) -> Rec f rs -> Rec g (MapTyCon h rs) rtraverseIn forall (a :: u). f a -> g (ApplyToField h a) _ Rec f rs RNil = Rec g (MapTyCon h rs) forall u (f :: u -> *). Rec f '[] RNil rtraverseIn forall (a :: u). f a -> g (ApplyToField h a) f (f r x :& Rec f rs xs) = f r -> g (ApplyToField h r) forall (a :: u). f a -> g (ApplyToField h a) f f r x g (ApplyToField h r) -> Rec g (MapTyCon h rs) -> Rec g (ApplyToField h r : MapTyCon h rs) forall a (f :: a -> *) (r :: a) (rs :: [a]). f r -> Rec f rs -> Rec f (r : rs) :& (forall (a :: u). f a -> g (ApplyToField h a)) -> Rec f rs -> Rec g (MapTyCon h rs) forall u (h :: * -> *) (f :: u -> *) (g :: u -> *) (rs :: [u]). (forall (a :: u). f a -> g (ApplyToField h a)) -> Rec f rs -> Rec g (MapTyCon h rs) rtraverseIn forall (a :: u). f a -> g (ApplyToField h a) f Rec f rs xs {-# INLINABLE rtraverseIn #-} -- | Push an outer layer of interpretation functor into each field. rsequenceIn :: forall f g (rs :: [Type]). (Traversable f, Applicative g) => Rec (f :. g) rs -> Rec g (MapTyCon f rs) rsequenceIn :: Rec (f :. g) rs -> Rec g (MapTyCon f rs) rsequenceIn = (forall a. (:.) f g a -> g (ApplyToField f a)) -> Rec (f :. g) rs -> Rec g (MapTyCon f rs) forall u (h :: * -> *) (f :: u -> *) (g :: u -> *) (rs :: [u]). (forall (a :: u). f a -> g (ApplyToField h a)) -> Rec f rs -> Rec g (MapTyCon h rs) rtraverseIn @f (f (g a) -> g (f a) forall (t :: * -> *) (f :: * -> *) a. (Traversable t, Applicative f) => t (f a) -> f (t a) sequenceA (f (g a) -> g (f a)) -> (Compose f g a -> f (g a)) -> Compose f g a -> g (f a) forall b c a. (b -> c) -> (a -> b) -> a -> c . Compose f g a -> f (g a) forall l (f :: l -> *) k (g :: k -> l) (x :: k). Compose f g x -> f (g x) getCompose) {-# INLINABLE rsequenceIn #-} -- | Given a natural transformation from the product of @f@ and @g@ to @h@, we -- have a natural transformation from the product of @'Rec' f@ and @'Rec' g@ to -- @'Rec' h@. You can also think about this operation as zipping two records -- with the same element types but different interpretations. rzipWith :: (RMap xs, RApply xs) => (forall x. f x -> g x -> h x) -> Rec f xs -> Rec g xs -> Rec h xs rzipWith :: (forall (x :: u). f x -> g x -> h x) -> Rec f xs -> Rec g xs -> Rec h xs rzipWith forall (x :: u). f x -> g x -> h x f = Rec (Lift (->) g h) xs -> Rec g xs -> Rec h xs forall u (rs :: [u]) (f :: u -> *) (g :: u -> *). RApply rs => Rec (Lift (->) f g) rs -> Rec f rs -> Rec g rs rapply (Rec (Lift (->) g h) xs -> Rec g xs -> Rec h xs) -> (Rec f xs -> Rec (Lift (->) g h) xs) -> Rec f xs -> Rec g xs -> Rec h xs forall b c a. (b -> c) -> (a -> b) -> a -> c . (forall (x :: u). f x -> Lift (->) g h x) -> Rec f xs -> Rec (Lift (->) g h) xs forall u (rs :: [u]) (f :: u -> *) (g :: u -> *). RMap rs => (forall (x :: u). f x -> g x) -> Rec f rs -> Rec g rs rmap ((g x -> h x) -> Lift (->) g h x forall l l' k (op :: l -> l' -> *) (f :: k -> l) (g :: k -> l') (x :: k). op (f x) (g x) -> Lift op f g x Lift ((g x -> h x) -> Lift (->) g h x) -> (f x -> g x -> h x) -> f x -> Lift (->) g h x forall b c a. (b -> c) -> (a -> b) -> a -> c . f x -> g x -> h x forall (x :: u). f x -> g x -> h x f) -- | Map each element of a record to a monoid and combine the results. class RFoldMap rs where rfoldMapAux :: Monoid m => (forall x. f x -> m) -> m -> Rec f rs -> m instance RFoldMap '[] where rfoldMapAux :: (forall (x :: u). f x -> m) -> m -> Rec f '[] -> m rfoldMapAux forall (x :: u). f x -> m _ m m Rec f '[] RNil = m m {-# INLINE rfoldMapAux #-} instance RFoldMap xs => RFoldMap (x ': xs) where rfoldMapAux :: (forall (x :: u). f x -> m) -> m -> Rec f (x : xs) -> m rfoldMapAux forall (x :: u). f x -> m f m m (f r r :& Rec f rs rs) = (forall (x :: u). f x -> m) -> m -> Rec f rs -> m forall u (rs :: [u]) m (f :: u -> *). (RFoldMap rs, Monoid m) => (forall (x :: u). f x -> m) -> m -> Rec f rs -> m rfoldMapAux forall (x :: u). f x -> m f (m -> m -> m forall a. Monoid a => a -> a -> a mappend m m (f r -> m forall (x :: u). f x -> m f f r r)) Rec f rs rs {-# INLINE rfoldMapAux #-} rfoldMap :: forall rs m f. (Monoid m, RFoldMap rs) => (forall x. f x -> m) -> Rec f rs -> m rfoldMap :: (forall (x :: u). f x -> m) -> Rec f rs -> m rfoldMap forall (x :: u). f x -> m f = (forall (x :: u). f x -> m) -> m -> Rec f rs -> m forall u (rs :: [u]) m (f :: u -> *). (RFoldMap rs, Monoid m) => (forall (x :: u). f x -> m) -> m -> Rec f rs -> m rfoldMapAux forall (x :: u). f x -> m f m forall a. Monoid a => a mempty {-# INLINE rfoldMap #-} -- | A record with uniform fields may be turned into a list. class RecordToList rs where recordToList :: Rec (Const a) rs -> [a] instance RecordToList '[] where recordToList :: Rec (Const a) '[] -> [a] recordToList Rec (Const a) '[] RNil = [] {-# INLINE recordToList #-} instance RecordToList xs => RecordToList (x ': xs) where recordToList :: Rec (Const a) (x : xs) -> [a] recordToList (Const a r x :& Rec (Const a) rs xs) = Const a r -> a forall a k (b :: k). Const a b -> a getConst Const a r x a -> [a] -> [a] forall a. a -> [a] -> [a] : Rec (Const a) rs -> [a] forall u (rs :: [u]) a. RecordToList rs => Rec (Const a) rs -> [a] recordToList Rec (Const a) rs xs {-# INLINE recordToList #-} -- | Wrap up a value with a capability given by its type data Dict c a where Dict :: c a => a -> Dict c a -- | Sometimes we may know something for /all/ fields of a record, but when -- you expect to be able to /each/ of the fields, you are then out of luck. -- Surely given @∀x:u.φ(x)@ we should be able to recover @x:u ⊢ φ(x)@! Sadly, -- the constraint solver is not quite smart enough to realize this and we must -- make it patently obvious by reifying the constraint pointwise with proof. class ReifyConstraint c f rs where reifyConstraint :: Rec f rs -> Rec (Dict c :. f) rs instance ReifyConstraint c f '[] where reifyConstraint :: Rec f '[] -> Rec (Dict c :. f) '[] reifyConstraint Rec f '[] RNil = Rec (Dict c :. f) '[] forall u (f :: u -> *). Rec f '[] RNil {-# INLINE reifyConstraint #-} instance (c (f x), ReifyConstraint c f xs) => ReifyConstraint c f (x ': xs) where reifyConstraint :: Rec f (x : xs) -> Rec (Dict c :. f) (x : xs) reifyConstraint (f r x :& Rec f rs xs) = Dict c (f r) -> Compose (Dict c) f r forall l k (f :: l -> *) (g :: k -> l) (x :: k). f (g x) -> Compose f g x Compose (f r -> Dict c (f r) forall (c :: * -> Constraint) a. c a => a -> Dict c a Dict f r x) Compose (Dict c) f r -> Rec (Dict c :. f) rs -> Rec (Dict c :. f) (r : rs) forall a (f :: a -> *) (r :: a) (rs :: [a]). f r -> Rec f rs -> Rec f (r : rs) :& Rec f rs -> Rec (Dict c :. f) rs forall u (c :: * -> Constraint) (f :: u -> *) (rs :: [u]). ReifyConstraint c f rs => Rec f rs -> Rec (Dict c :. f) rs reifyConstraint Rec f rs xs {-# INLINE reifyConstraint #-} -- | Build a record whose elements are derived solely from a -- constraint satisfied by each. class RPureConstrained c ts where rpureConstrained :: (forall a. c a => f a) -> Rec f ts instance RPureConstrained c '[] where rpureConstrained :: (forall (a :: u). c a => f a) -> Rec f '[] rpureConstrained forall (a :: u). c a => f a _ = Rec f '[] forall u (f :: u -> *). Rec f '[] RNil {-# INLINE rpureConstrained #-} instance (c x, RPureConstrained c xs) => RPureConstrained c (x ': xs) where rpureConstrained :: (forall (a :: a). c a => f a) -> Rec f (x : xs) rpureConstrained forall (a :: a). c a => f a f = f x forall (a :: a). c a => f a f f x -> Rec f xs -> Rec f (x : xs) forall a (f :: a -> *) (r :: a) (rs :: [a]). f r -> Rec f rs -> Rec f (r : rs) :& (forall (a :: a). c a => f a) -> Rec f xs forall u (c :: u -> Constraint) (ts :: [u]) (f :: u -> *). RPureConstrained c ts => (forall (a :: u). c a => f a) -> Rec f ts rpureConstrained @c @xs forall (a :: a). c a => f a f {-# INLINE rpureConstrained #-} -- | Capture a type class instance dictionary. See -- 'Data.Vinyl.Lens.getDict' for a way to obtain a 'DictOnly' value -- from an 'RPureConstrained' constraint. data DictOnly (c :: k -> Constraint) a where DictOnly :: forall c a. c a => DictOnly c a -- | A useful technique is to use 'rmap (Pair (DictOnly @MyClass))' on -- a 'Rec' to pair each field with a type class dictionary for -- @MyClass@. This helper can then be used to eliminate the original. withPairedDict :: (c a => f a -> r) -> Product (DictOnly c) f a -> r withPairedDict :: (c a => f a -> r) -> Product (DictOnly c) f a -> r withPairedDict c a => f a -> r f (Pair DictOnly c a DictOnly f a x) = c a => f a -> r f a -> r f f a x -- | Build a record whose elements are derived solely from a -- list of constraint constructors satisfied by each. class RPureConstraints cs ts where rpureConstraints :: (forall a. AllSatisfied cs a => f a) -> Rec f ts instance RPureConstraints cs '[] where rpureConstraints :: (forall (a :: u). AllSatisfied cs a => f a) -> Rec f '[] rpureConstraints forall (a :: u). AllSatisfied cs a => f a _ = Rec f '[] forall u (f :: u -> *). Rec f '[] RNil {-# INLINE rpureConstraints #-} instance (AllSatisfied cs t, RPureConstraints cs ts) => RPureConstraints cs (t ': ts) where rpureConstraints :: (forall (a :: u). AllSatisfied cs a => f a) -> Rec f (t : ts) rpureConstraints forall (a :: u). AllSatisfied cs a => f a f = f t forall (a :: u). AllSatisfied cs a => f a f f t -> Rec f ts -> Rec f (t : ts) forall a (f :: a -> *) (r :: a) (rs :: [a]). f r -> Rec f rs -> Rec f (r : rs) :& (forall (a :: u). AllSatisfied cs a => f a) -> Rec f ts forall k u (cs :: k) (ts :: [u]) (f :: u -> *). RPureConstraints cs ts => (forall (a :: u). AllSatisfied cs a => f a) -> Rec f ts rpureConstraints @cs @ts forall (a :: u). AllSatisfied cs a => f a f {-# INLINE rpureConstraints #-} -- | Records may be shown insofar as their points may be shown. -- 'reifyConstraint' is used to great effect here. instance (RMap rs, ReifyConstraint Show f rs, RecordToList rs) => Show (Rec f rs) where show :: Rec f rs -> String show Rec f rs xs = (\String str -> String "{" String -> ShowS forall a. Semigroup a => a -> a -> a <> String str String -> ShowS forall a. Semigroup a => a -> a -> a <> String "}") ShowS -> (Rec (Dict Show :. f) rs -> String) -> Rec (Dict Show :. f) rs -> String forall b c a. (b -> c) -> (a -> b) -> a -> c . String -> [String] -> String forall a. [a] -> [[a]] -> [a] intercalate String ", " ([String] -> String) -> (Rec (Dict Show :. f) rs -> [String]) -> Rec (Dict Show :. f) rs -> String forall b c a. (b -> c) -> (a -> b) -> a -> c . Rec (Const String) rs -> [String] forall u (rs :: [u]) a. RecordToList rs => Rec (Const a) rs -> [a] recordToList (Rec (Const String) rs -> [String]) -> (Rec (Dict Show :. f) rs -> Rec (Const String) rs) -> Rec (Dict Show :. f) rs -> [String] forall b c a. (b -> c) -> (a -> b) -> a -> c . (forall (x :: u). (:.) (Dict Show) f x -> Const String x) -> Rec (Dict Show :. f) rs -> Rec (Const String) rs forall u (rs :: [u]) (f :: u -> *) (g :: u -> *). RMap rs => (forall (x :: u). f x -> g x) -> Rec f rs -> Rec g rs rmap (\(Compose (Dict x)) -> String -> Const String x forall k a (b :: k). a -> Const a b Const (String -> Const String x) -> String -> Const String x forall a b. (a -> b) -> a -> b $ f x -> String forall a. Show a => a -> String show f x x) (Rec (Dict Show :. f) rs -> String) -> Rec (Dict Show :. f) rs -> String forall a b. (a -> b) -> a -> b $ Rec f rs -> Rec (Dict Show :. f) rs forall u (c :: * -> Constraint) (f :: u -> *) (rs :: [u]). ReifyConstraint c f rs => Rec f rs -> Rec (Dict c :. f) rs reifyConstraint @Show Rec f rs xs instance Semigroup (Rec f '[]) where Rec f '[] RNil <> :: Rec f '[] -> Rec f '[] -> Rec f '[] <> Rec f '[] RNil = Rec f '[] forall u (f :: u -> *). Rec f '[] RNil instance (Semigroup (f r), Semigroup (Rec f rs)) => Semigroup (Rec f (r ': rs)) where (f r x :& Rec f rs xs) <> :: Rec f (r : rs) -> Rec f (r : rs) -> Rec f (r : rs) <> (f r y :& Rec f rs ys) = (f r x f r -> f r -> f r forall a. Semigroup a => a -> a -> a <> f r f r y) f r -> Rec f rs -> Rec f (r : rs) forall a (f :: a -> *) (r :: a) (rs :: [a]). f r -> Rec f rs -> Rec f (r : rs) :& (Rec f rs xs Rec f rs -> Rec f rs -> Rec f rs forall a. Semigroup a => a -> a -> a <> Rec f rs Rec f rs ys) instance Monoid (Rec f '[]) where mempty :: Rec f '[] mempty = Rec f '[] forall u (f :: u -> *). Rec f '[] RNil Rec f '[] RNil mappend :: Rec f '[] -> Rec f '[] -> Rec f '[] `mappend` Rec f '[] RNil = Rec f '[] forall u (f :: u -> *). Rec f '[] RNil instance (Monoid (f r), Monoid (Rec f rs)) => Monoid (Rec f (r ': rs)) where mempty :: Rec f (r : rs) mempty = f r forall a. Monoid a => a mempty f r -> Rec f rs -> Rec f (r : rs) forall a (f :: a -> *) (r :: a) (rs :: [a]). f r -> Rec f rs -> Rec f (r : rs) :& Rec f rs forall a. Monoid a => a mempty (f r x :& Rec f rs xs) mappend :: Rec f (r : rs) -> Rec f (r : rs) -> Rec f (r : rs) `mappend` (f r y :& Rec f rs ys) = (f r -> f r -> f r forall a. Monoid a => a -> a -> a mappend f r x f r f r y) f r -> Rec f rs -> Rec f (r : rs) forall a (f :: a -> *) (r :: a) (rs :: [a]). f r -> Rec f rs -> Rec f (r : rs) :& (Rec f rs -> Rec f rs -> Rec f rs forall a. Monoid a => a -> a -> a mappend Rec f rs xs Rec f rs Rec f rs ys) instance Eq (Rec f '[]) where Rec f '[] _ == :: Rec f '[] -> Rec f '[] -> Bool == Rec f '[] _ = Bool True instance (Eq (f r), Eq (Rec f rs)) => Eq (Rec f (r ': rs)) where (f r x :& Rec f rs xs) == :: Rec f (r : rs) -> Rec f (r : rs) -> Bool == (f r y :& Rec f rs ys) = (f r x f r -> f r -> Bool forall a. Eq a => a -> a -> Bool == f r f r y) Bool -> Bool -> Bool && (Rec f rs xs Rec f rs -> Rec f rs -> Bool forall a. Eq a => a -> a -> Bool == Rec f rs Rec f rs ys) instance Ord (Rec f '[]) where compare :: Rec f '[] -> Rec f '[] -> Ordering compare Rec f '[] _ Rec f '[] _ = Ordering EQ instance (Ord (f r), Ord (Rec f rs)) => Ord (Rec f (r ': rs)) where compare :: Rec f (r : rs) -> Rec f (r : rs) -> Ordering compare (f r x :& Rec f rs xs) (f r y :& Rec f rs ys) = Ordering -> Ordering -> Ordering forall a. Monoid a => a -> a -> a mappend (f r -> f r -> Ordering forall a. Ord a => a -> a -> Ordering compare f r x f r f r y) (Rec f rs -> Rec f rs -> Ordering forall a. Ord a => a -> a -> Ordering compare Rec f rs xs Rec f rs Rec f rs ys) instance Storable (Rec f '[]) where sizeOf :: Rec f '[] -> Int sizeOf Rec f '[] _ = Int 0 alignment :: Rec f '[] -> Int alignment Rec f '[] _ = Int 0 peek :: Ptr (Rec f '[]) -> IO (Rec f '[]) peek Ptr (Rec f '[]) _ = Rec f '[] -> IO (Rec f '[]) forall (m :: * -> *) a. Monad m => a -> m a return Rec f '[] forall u (f :: u -> *). Rec f '[] RNil poke :: Ptr (Rec f '[]) -> Rec f '[] -> IO () poke Ptr (Rec f '[]) _ Rec f '[] RNil = () -> IO () forall (m :: * -> *) a. Monad m => a -> m a return () instance (Storable (f r), Storable (Rec f rs)) => Storable (Rec f (r ': rs)) where sizeOf :: Rec f (r : rs) -> Int sizeOf Rec f (r : rs) _ = f r -> Int forall a. Storable a => a -> Int sizeOf (f r forall a. HasCallStack => a undefined :: f r) Int -> Int -> Int forall a. Num a => a -> a -> a + Rec f rs -> Int forall a. Storable a => a -> Int sizeOf (Rec f rs forall a. HasCallStack => a undefined :: Rec f rs) {-# INLINE sizeOf #-} alignment :: Rec f (r : rs) -> Int alignment Rec f (r : rs) _ = f r -> Int forall a. Storable a => a -> Int alignment (f r forall a. HasCallStack => a undefined :: f r) {-# INLINE alignment #-} peek :: Ptr (Rec f (r : rs)) -> IO (Rec f (r : rs)) peek Ptr (Rec f (r : rs)) ptr = do !f r x <- Ptr (f r) -> IO (f r) forall a. Storable a => Ptr a -> IO a peek (Ptr (Rec f (r : rs)) -> Ptr (f r) forall a b. Ptr a -> Ptr b castPtr Ptr (Rec f (r : rs)) ptr) !Rec f rs xs <- Ptr (Rec f rs) -> IO (Rec f rs) forall a. Storable a => Ptr a -> IO a peek (Ptr (Rec f (r : rs)) ptr Ptr (Rec f (r : rs)) -> Int -> Ptr (Rec f rs) forall a b. Ptr a -> Int -> Ptr b `plusPtr` f r -> Int forall a. Storable a => a -> Int sizeOf (f r forall a. HasCallStack => a undefined :: f r)) Rec f (r : rs) -> IO (Rec f (r : rs)) forall (m :: * -> *) a. Monad m => a -> m a return (Rec f (r : rs) -> IO (Rec f (r : rs))) -> Rec f (r : rs) -> IO (Rec f (r : rs)) forall a b. (a -> b) -> a -> b $ f r x f r -> Rec f rs -> Rec f (r : rs) forall a (f :: a -> *) (r :: a) (rs :: [a]). f r -> Rec f rs -> Rec f (r : rs) :& Rec f rs xs {-# INLINE peek #-} poke :: Ptr (Rec f (r : rs)) -> Rec f (r : rs) -> IO () poke Ptr (Rec f (r : rs)) ptr (!f r x :& Rec f rs xs) = Ptr (f r) -> f r -> IO () forall a. Storable a => Ptr a -> a -> IO () poke (Ptr (Rec f (r : rs)) -> Ptr (f r) forall a b. Ptr a -> Ptr b castPtr Ptr (Rec f (r : rs)) ptr) f r x IO () -> IO () -> IO () forall (m :: * -> *) a b. Monad m => m a -> m b -> m b >> Ptr (Rec f rs) -> Rec f rs -> IO () forall a. Storable a => Ptr a -> a -> IO () poke (Ptr (Rec f (r : rs)) ptr Ptr (Rec f (r : rs)) -> Int -> Ptr (Rec f rs) forall a b. Ptr a -> Int -> Ptr b `plusPtr` f r -> Int forall a. Storable a => a -> Int sizeOf (f r forall a. HasCallStack => a undefined :: f r)) Rec f rs xs {-# INLINE poke #-} instance Generic (Rec f '[]) where type Rep (Rec f '[]) = C1 ('MetaCons "RNil" 'PrefixI 'False) (S1 ('MetaSel 'Nothing 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) U1) from :: Rec f '[] -> Rep (Rec f '[]) x from Rec f '[] RNil = M1 S ('MetaSel 'Nothing 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) U1 x -> M1 C ('MetaCons "RNil" 'PrefixI 'False) (M1 S ('MetaSel 'Nothing 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) U1) x forall k i (c :: Meta) (f :: k -> *) (p :: k). f p -> M1 i c f p M1 (U1 x -> M1 S ('MetaSel 'Nothing 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) U1 x forall k i (c :: Meta) (f :: k -> *) (p :: k). f p -> M1 i c f p M1 U1 x forall k (p :: k). U1 p U1) to :: Rep (Rec f '[]) x -> Rec f '[] to (M1 (M1 U1)) = Rec f '[] forall u (f :: u -> *). Rec f '[] RNil instance (Generic (Rec f rs)) => Generic (Rec f (r ': rs)) where type Rep (Rec f (r ': rs)) = C1 ('MetaCons ":&" ('InfixI 'RightAssociative 7) 'False) (S1 ('MetaSel 'Nothing 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 (f r)) :*: S1 ('MetaSel 'Nothing 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rep (Rec f rs))) from :: Rec f (r : rs) -> Rep (Rec f (r : rs)) x from (f r x :& Rec f rs xs) = (:*:) (M1 S ('MetaSel 'Nothing 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (K1 R (f r))) (M1 S ('MetaSel 'Nothing 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rep (Rec f rs))) x -> M1 C ('MetaCons ":&" ('InfixI 'RightAssociative 7) 'False) (M1 S ('MetaSel 'Nothing 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (K1 R (f r)) :*: M1 S ('MetaSel 'Nothing 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rep (Rec f rs))) x forall k i (c :: Meta) (f :: k -> *) (p :: k). f p -> M1 i c f p M1 (K1 R (f r) x -> M1 S ('MetaSel 'Nothing 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (K1 R (f r)) x forall k i (c :: Meta) (f :: k -> *) (p :: k). f p -> M1 i c f p M1 (f r -> K1 R (f r) x forall k i c (p :: k). c -> K1 i c p K1 f r x) M1 S ('MetaSel 'Nothing 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (K1 R (f r)) x -> M1 S ('MetaSel 'Nothing 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rep (Rec f rs)) x -> (:*:) (M1 S ('MetaSel 'Nothing 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (K1 R (f r))) (M1 S ('MetaSel 'Nothing 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rep (Rec f rs))) x forall k (f :: k -> *) (g :: k -> *) (p :: k). f p -> g p -> (:*:) f g p :*: Rep (Rec f rs) x -> M1 S ('MetaSel 'Nothing 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rep (Rec f rs)) x forall k i (c :: Meta) (f :: k -> *) (p :: k). f p -> M1 i c f p M1 (Rec f rs -> Rep (Rec f rs) x forall a x. Generic a => a -> Rep a x from Rec f rs xs)) to :: Rep (Rec f (r : rs)) x -> Rec f (r : rs) to (M1 (M1 (K1 x) :*: M1 xs)) = f r x f r -> Rec f rs -> Rec f (r : rs) forall a (f :: a -> *) (r :: a) (rs :: [a]). f r -> Rec f rs -> Rec f (r : rs) :& Rep (Rec f rs) x -> Rec f rs forall a x. Generic a => Rep a x -> a to Rep (Rec f rs) x xs instance ReifyConstraint NFData f xs => NFData (Rec f xs) where rnf :: Rec f xs -> () rnf = Rec (Dict NFData :. f) xs -> () forall (elems :: [u]). Rec (Dict NFData :. f) elems -> () go (Rec (Dict NFData :. f) xs -> ()) -> (Rec f xs -> Rec (Dict NFData :. f) xs) -> Rec f xs -> () forall b c a. (b -> c) -> (a -> b) -> a -> c . forall u (c :: * -> Constraint) (f :: u -> *) (rs :: [u]). ReifyConstraint c f rs => Rec f rs -> Rec (Dict c :. f) rs forall (f :: u -> *) (rs :: [u]). ReifyConstraint NFData f rs => Rec f rs -> Rec (Dict NFData :. f) rs reifyConstraint @NFData where go :: forall elems. Rec (Dict NFData :. f) elems -> () go :: Rec (Dict NFData :. f) elems -> () go Rec (Dict NFData :. f) elems RNil = () go (Compose (Dict f r x) :& Rec (Dict NFData :. f) rs xs) = f r -> () forall a. NFData a => a -> () rnf f r x () -> () -> () `seq` Rec (Dict NFData :. f) rs -> () forall (elems :: [u]). Rec (Dict NFData :. f) elems -> () go Rec (Dict NFData :. f) rs xs type family Head xs where Head (x ': _) = x type family Tail xs where Tail (_ ': xs) = xs type family AllRepsMatch_ (f :: j -> *) (xs :: [j]) (g :: k -> *) (ys :: [k]) :: Constraint where AllRepsMatch_ f (x ': xs) g ys = ( ys ~ (Head ys ': Tail ys) , Coercible (f x) (g (Head ys)) , AllRepsMatch_ f xs g (Tail ys) ) AllRepsMatch_ _ '[] _ ys = ys ~ '[] -- | @AllRepsMatch f xs g ys@ means that @xs@ and @ys@ have the -- same lengths, and that mapping @f@ over @xs@ and @g@ over @ys@ -- produces lists whose corresponding elements are 'Coercible' with -- each other. For example, the following hold: -- -- @AllRepsMatch Proxy '[1,2,3] Proxy '[4,5,6]@ -- @AllRepsMatch Sum '[Int,Word] Identity '[Min Int, Max Word]@ type AllRepsMatch f xs g ys = (AllRepsMatch_ f xs g ys, AllRepsMatch_ g ys f xs) -- This two-sided approach means that the *length* of each list -- can be inferred from the length of the other. I don't know how -- useful that is in practice, but we get it almost for free. -- | Given that for each element @x@ in the list @xs@, repsMatchCoercion :: AllRepsMatch f xs g ys => Coercion (Rec f xs) (Rec g ys) repsMatchCoercion :: Coercion (Rec f xs) (Rec g ys) repsMatchCoercion = Coercion () () -> Coercion (Rec f xs) (Rec g ys) forall a b. a -> b unsafeCoerce (Coercion () () forall k (a :: k) (b :: k). Coercible a b => Coercion a b Coercion :: Coercion () ()) {- -- "Proof" that repsMatchCoercion is sensible. repsMatchConvert :: AllRepsMatch f xs g ys => Rec f xs -> Rec g ys repsMatchConvert RNil = RNil repsMatchConvert (x :& xs) = coerce x :& repsMatchConvert xs -} #if __GLASGOW_HASKELL__ >= 806 consMatchCoercion :: (forall (x :: k). Coercible (f x) (g x)) => Coercion (Rec f xs) (Rec g xs) #else consMatchCoercion :: forall k (f :: k -> *) (g :: k -> *) (xs :: [k]). Forall (Similar f g) => Coercion (Rec f xs) (Rec g xs) #endif consMatchCoercion :: Coercion (Rec f xs) (Rec g xs) consMatchCoercion = Coercion () () -> Coercion (Rec f xs) (Rec g xs) forall a b. a -> b unsafeCoerce (Coercion () () forall k (a :: k) (b :: k). Coercible a b => Coercion a b Coercion :: Coercion () ()) {- -- "Proof" that consMatchCoercion is sensible. consMatchConvert :: (forall (x :: k). Coercible (f x) (g x)) => Rec f xs -> Rec g xs consMatchConvert RNil = RNil consMatchConvert (x :& xs) = coerce x :& consMatchConvert xs -- And for old GHC. consMatchConvert' :: forall k (f :: k -> *) (g :: k -> *) (xs :: [k]). Forall (Similar f g) => Rec f xs -> Rec g xs consMatchConvert' RNil = RNil consMatchConvert' ((x :: f x) :& xs) = case inst :: Forall (Similar f g) DC.:- Similar f g x of DC.Sub DC.Dict -> coerce x :& consMatchConvert' xs -} {- -- This is sensible, but I suspect the ergonomics will be awful -- thanks to the interaction between Coercible constraint resolution -- and constraint resolution with quantified constraints. Is there -- a good way to accomplish it? -- | Given -- -- @ -- forall x. Coercible (f x) (g x) -- @ -- -- provide the constraint -- -- @ -- forall xs. Coercible (Rec f xs) (Rec g xs) -- @ consMatchCoercible :: forall k f g rep (r :: TYPE rep). (forall (x :: k). Coercible (f x) (g x)) => ((forall (xs :: [k]). Coercible (Rec f xs) (Rec g xs)) => r) -> r consMatchCoercible f = case unsafeCoerce @(Zouch f f) @(Zouch f g) (Zouch $ \r -> r) of Zouch q -> q f newtype Zouch (f :: k -> *) (g :: k -> *) = Zouch (forall rep (r :: TYPE rep). ((forall (xs :: [k]). Coercible (Rec f xs) (Rec g xs)) => r) -> r) -}