@@ -84,48 +84,22 @@ deriving instance Show k => Show (Const2 k v v')
8484deriving instance Read k => Read (Const2 k v v)
8585
8686instance Show k => GShow (Const2 k v) where
87−#ifdef EXPERIMENTAL_DEPENDENT_SUM_INSTANCES
88− gshowToShow (Const2 _) = id
89−#else
9087 gshowsPrec n x@(Const2 _) = showsPrec n x
91−#endif
9288
9389instance (Show k, Show (f v)) => ShowTag (Const2 k v) f where
94−#ifdef EXPERIMENTAL_DEPENDENT_SUM_INSTANCES
95− showTagToShow (Const2 _) _ = id
96−#else
9790 showTaggedPrec (Const2 _) = showsPrec
98−#endif
9991
10092instance Eq k => GEq (Const2 k v) where
101−#ifdef EXPERIMENTAL_DEPENDENT_SUM_INSTANCES
102− geqToEq _ = id
103− geqUnify (Const2 _) (Const2 _) _ = id
104−#else
10593 geq (Const2 a) (Const2 b) =
10694 if a == b
10795 then Just Refl
10896 else Nothing
109−#endif
11097
11198instance Ord k => GCompare (Const2 k v) where
112−#ifdef EXPERIMENTAL_DEPENDENT_SUM_INSTANCES
113− gcompareToOrd (Const2 _) = id
114− gcompare (Const2 a) (Const2 b) = strengthenOrdering $ compare a b
115−#else
11699 gcompare (Const2 a) (Const2 b) = case compare a b of
117100 LT -> GLT
118101 EQ -> GEQ
119102 GT -> GGT
120−#endif
121−
122−#ifdef EXPERIMENTAL_DEPENDENT_SUM_INSTANCES
123−instance {-# INCOHERENT #-} (Eq k, Eq v) => EqTag (Const2 k v) Identity where
124− eqTagToEq (Const2 _) _ = id
125−
126−instance {-# INCOHERENT #-} Eq k => EqTag (Const2 k v) (Const2 k v) where
127− eqTagToEq (Const2 _) _ = id
128−#endif
129103
130104-- | Convert a 'DMap' to a regular 'Map'
131105dmapToMap :: DMap (Const2 k v) Identity -> Map k v
@@ -175,17 +149,9 @@ deriving instance Show (f a) => Show (WrapArg g f (g' a))
175149deriving instance Read (f a) => Read (WrapArg g f (g a))
176150
177151instance GEq f => GEq (WrapArg g f) where
178−#ifdef EXPERIMENTAL_DEPENDENT_SUM_INSTANCES
179− geqToEq (WrapArg f) = geqToEq f
180− geqUnify (WrapArg a) (WrapArg b) = geqUnify a b
181−#else
182152 geq (WrapArg a) (WrapArg b) = (\Refl -> Refl) <$> geq a b
183−#endif
184153
185154instance GCompare f => GCompare (WrapArg g f) where
186−#ifdef EXPERIMENTAL_DEPENDENT_SUM_INSTANCES
187− gcompareToOrd (WrapArg f) = gcompareToOrd f
188−#endif
189155 gcompare (WrapArg a) (WrapArg b) = case gcompare a b of
190156 GLT -> GLT
191157 GEQ -> GEQ
@@ -237,34 +203,13 @@ deriving instance Show (EitherTag l r a)
237203deriving instance Eq (EitherTag l r a)
238204deriving instance Ord (EitherTag l r a)
239205
240−#ifdef EXPERIMENTAL_DEPENDENT_SUM_INSTANCES
241−instance {-# INCOHERENT #-} (Show (f l), Show (f r)) => ShowTag (EitherTag l r) f where
242− showTagToShow e _ = case e of
243− LeftTag -> id
244− RightTag -> id
245−
246−instance {-# INCOHERENT #-} (Eq (f l), Eq (f r)) => EqTag (EitherTag l r) f where
247− eqTagToEq e _ = case e of
248− LeftTag -> id
249− RightTag -> id
250−#endif
251−
252206instance GEq (EitherTag l r) where
253−#ifdef EXPERIMENTAL_DEPENDENT_SUM_INSTANCES
254− geqToEq _ = id
255− geqUnify LeftTag LeftTag _ same = same
256− geqUnify RightTag RightTag _ same = same
257− geqUnify _ _ unknown _ = unknown
258−#endif
259207 geq a b = case (a, b) of
260208 (LeftTag, LeftTag) -> Just Refl
261209 (RightTag, RightTag) -> Just Refl
262210 _ -> Nothing
263211
264212instance GCompare (EitherTag l r) where
265−#ifdef EXPERIMENTAL_DEPENDENT_SUM_INSTANCES
266− gcompareToOrd _ = id
267−#endif
268213 gcompare a b = case (a, b) of
269214 (LeftTag, LeftTag) -> GEQ
270215 (LeftTag, RightTag) -> GLT
@@ -272,24 +217,14 @@ instance GCompare (EitherTag l r) where
272217 (RightTag, RightTag) -> GEQ
273218
274219instance GShow (EitherTag l r) where
275−#ifdef EXPERIMENTAL_DEPENDENT_SUM_INSTANCES
276− gshowToShow _ = id
277−#else
278220 gshowsPrec _ a = case a of
279221 LeftTag -> showString "LeftTag"
280222 RightTag -> showString "RightTag"
281−#endif
282223
283224instance (Show l, Show r) => ShowTag (EitherTag l r) Identity where
284−#ifdef EXPERIMENTAL_DEPENDENT_SUM_INSTANCES
285− showTagToShow t _ = case t of
286− LeftTag -> id
287− RightTag -> id
288−#else
289225 showTaggedPrec t n (Identity a) = case t of
290226 LeftTag -> showsPrec n a
291227 RightTag -> showsPrec n a
292−#endif
293228
294229-- | Convert 'Either' to a 'DSum'. Inverse of 'dsumToEither'.
295230eitherToDSum :: Either a b -> DSum (EitherTag a b) Identity
@@ -319,13 +254,6 @@ newtype ComposeMaybe (f :: * -> *) (a :: *) =
319254
320255deriving instance Functor f => Functor (ComposeMaybe f)
321256
322−#ifdef EXPERIMENTAL_DEPENDENT_SUM_INSTANCES
323−instance {-# INCOHERENT #-} EqTag f g => EqTag f (ComposeMaybe g) where
324− eqTagToEq f _ = eqTagToEq f (Proxy :: Proxy g)
325−
326−instance {-# INCOHERENT #-} GShow k => ShowTag k (ComposeMaybe k) where
327− showTagToShow k _ r = gshowToShow k (showTagToShow k (Proxy :: Proxy k) r)
328−#endif
329257--------------------------------------------------------------------------------
330258-- Deprecated functions
331259--------------------------------------------------------------------------------