@@ -1 +1,57 @@
1−{-# OPTIONS_GHC -F -pgmF hspec-discover #-}
1+{-# OPTIONS_GHC -O -fplugin GHC.Proof.Plugin #-}
2+
3+{-# LANGUAGE AllowAmbiguousTypes #-}
4+{-# LANGUAGE DataKinds #-}
5+{-# LANGUAGE DeriveGeneric #-}
6+{-# LANGUAGE DuplicateRecordFields #-}
7+{-# LANGUAGE ExistentialQuantification #-}
8+{-# LANGUAGE RankNTypes #-}
9+{-# LANGUAGE ScopedTypeVariables #-}
10+{-# LANGUAGE TypeApplications #-}
11+
12+module Main where
13+
14+import GHC.Generics
15+import Data.Generics.Product
16+import GHC.Proof
17+
18+main :: IO ()
19+main = putStrLn "Hello world"
20+
21+data Record = MkRecord
22+ { fieldA :: Int
23+ , fieldB :: Bool
24+ } deriving Generic
25+
26+data Record2 = MkRecord2
27+ { fieldA :: Int
28+ } deriving Generic
29+
30+type Lens' s a = forall f. Functor f => (a -> f a) -> s -> f s
31+
32+fieldALensManual :: Lens' Record Int
33+fieldALensManual f (MkRecord a b) = (\a' -> MkRecord a' b) <$> f a
34+
35+newtype L s a = L (Lens' s a)
36+
37+subtypeLensManual :: Lens' Record Record2
38+subtypeLensManual f record
39+ = fmap (\ds -> case record of
40+ MkRecord _ b -> MkRecord (case ds of {MkRecord2 g1 -> g1}) b
41+ ) (f (MkRecord2 (case record of {MkRecord a _ -> a})))
42+
43+--------------------------------------------------------------------------------
44+-- * Tests
45+-- The ghc-proofs plugin checks that the following equalities hold, by checking
46+-- that the LHSs and the RHSs are CSEd. This also means that the runtime
47+-- characteristics of the derived lenses is the same as the manually written
48+-- ones above.
49+
50+fieldP :: Proof
51+fieldP = L fieldALensManual === L (field @"fieldA")
52+
53+posP :: Proof
54+posP = L fieldALensManual === L (position @1)
55+
56+subtypeP :: Proof
57+subtypeP = L subtypeLensManual === L super