@@ -86,10 +86,10 @@ class GIsList
8686
8787 glist :: Iso (f x) (g x) (List as) (List bs)
8888
89− glistL :: Lens (f x) (g x) (List as) (List bs)
90− glistL = glist @m
91−
92− glistR :: Lens (List bs) (List as) (g x) (f x)
89+ -- We define this reversed version, otherwise uses of `fromIso glist` are not
90+ -- properly inlined by GHC 8.0.2.
91+ -- This is not actually used.
92+ glistR :: Iso (List bs) (List as) (g x) (f x)
9393 glistR = fromIso (glist @m)
9494
9595instance
@@ -128,17 +128,23 @@ instance GIsList m U1 U1 '[] '[] where
128128 {-# INLINE glist #-}
129129
130130--------------------------------------------------------------------------------
131−-- as ++ bs == cs
132−-- as' + == cs'
131+-- | as ++ bs === cs
133132class Appending f (as :: [k]) bs cs (as' :: [k]) bs' cs' | as bs cs cs' -> as' bs', as' bs' cs cs' -> as bs, as bs -> cs, as' bs' -> cs' where
134133 appending :: Iso (f as, f bs) (f as', f bs') (f cs) (f cs')
135134
135+-- | [] ++ bs === bs
136136instance Appending List '[] bs bs '[] bs' bs' where
137137 appending = iso (\(_, b) -> b) (Nil,)
138138
139−instance Appending List as bs cs as' bs' cs'
139+-- | (a : as) ++ bs === (a : cs)
140+instance
141+ Appending List as bs cs as' bs' cs' -- as ++ bs == cs
140142 => Appending List ('(f, a) ': as) bs ('(f, a) ': cs) ('(f, a') ': as') bs' ('(f, a') ': cs') where
141− appending = pairing (fromIso consing) id . assoc3 . pairing id appending . consing
143+ appending
144+ = pairing (fromIso consing) id -- ((a, as), bs)
145+ . assoc3 -- (a, (as, bs))
146+ . pairing id appending -- (a, cs)
147+ . consing -- (a : cs)
142148
143149singleton :: Iso a b (List '[ '(field, a)]) (List '[ '(field, b)])
144150singleton = iso (:> Nil) (\(x :> _) -> x)
@@ -146,33 +152,6 @@ singleton = iso (:> Nil) (\(x :> _) -> x)
146152consing :: Iso (a, List as) (b, List bs) (List ('(f, a) ': as)) (List ('(f, b) ': bs))
147153consing = iso (\(x, xs) -> x :> xs) (\(x :> xs) -> (x, xs))
148154
149−--------------------------------------------------------------------------------
150−
151−-- This ended up not being used now... still cool to have
152−flipping :: Iso' (List (a1 ': a2 ': as)) (List (a2 ': a1 ': as))
153−flipping = iso
154− (\(a1 :> a2 :> as) -> a2 :> a1 :> as)
155− (\(a2 :> a1 :> as) -> a1 :> a2 :> as)
156−
157−class Inserting f a as bs | bs a -> as where
158− inserting :: Iso' (f (a ': as)) (f bs)
159−
160−instance Inserting f a as (a ': as) where
161− inserting = id
162−
163−instance Inserting List a as bs => Inserting List a ('(fb, b) ': as) ('(fb, b) ': bs) where
164− inserting = flipping . fromIso consing . pairing id (inserting @_ @a) . consing
165−
166−class Permuting f as bs where
167− permuting :: Iso' (f as) (f bs)
168−
169−instance Permuting List '[] '[] where
170− permuting = id
171−
172−instance (Permuting List as as', Inserting List '(fa, a) as' bs')
173− => Permuting List ('(fa, a) ': as) bs' where
174− permuting = fromIso consing . pairing id permuting . consing . inserting @_ @'(fa, _)
175−
176155--------------------------------------------------------------------------------
177156class IndexList (i :: Nat) as bs a b | i as -> a, i bs -> b, i as b -> bs, i bs a -> as where
178157 point :: Lens (List as) (List bs) a b