@@ -6,6 +6,7 @@
6{-# language FlexibleInstances #-}
6{-# language FlexibleInstances #-}
7{-# language LambdaCase #-}
7{-# language LambdaCase #-}
8{-# language MultiParamTypeClasses #-}
8{-# language MultiParamTypeClasses #-}
9+{-# language PolyKinds #-}
9{-# language QuantifiedConstraints #-}
10{-# language QuantifiedConstraints #-}
10{-# language ScopedTypeVariables #-}
11{-# language ScopedTypeVariables #-}
11{-# language StandaloneKindSignatures #-}
12{-# language StandaloneKindSignatures #-}
@@ -25,8 +26,9 @@ module Rel8.Generic.Rel8able
29+import Data.Functor.Identity ( Identity )
28import Data.Kind ( Constraint, Type )
30import Data.Kind ( Constraint, Type )
29−import Data.Type.Equality ( type (==) )
31+import Data.Type.Bool ( type (&&) )
30import GHC.Generics ( Generic, Rep, from, to )
32import GHC.Generics ( Generic, Rep, from, to )
31import Prelude
33import Prelude
@@ -58,6 +60,20 @@ type KRel8able :: Type
58type KRel8able = K.Rel8able
60type KRel8able = K.Rel8able
63+-- This is almost 'Data.Type.Equality.==', but we add an extra case.
64+type (==) :: k -> k -> Bool
65+type family a == b where
66+ -- This extra case is needed to solve the equation "a == Identity a",
67+ -- which occurs when we have polymorphic Rel8ables
68+ -- (e.g., newtype T a f = T { x :: Column f a })
69+ a == Identity a = 'False
71+ -- These cases are exactly the same as those in 'Data.Type.Equality.==.
72+ f a == g b = f == g && a == b
61type Serialize :: Bool -> Type -> Type -> Constraint
77type Serialize :: Bool -> Type -> Type -> Constraint
62class transposition ~ (a == Transpose Result expr) =>
78class transposition ~ (a == Transpose Result expr) =>
63 Serialize transposition expr a
79 Serialize transposition expr a