@@ -1,4 +1,4 @@
1−{-# OPTIONS_GHC -O -fplugin GHC.Proof.Plugin #-}
1+{-# OPTIONS_GHC -O -fplugin Test.Inspection.Plugin #-}
22
33{-# LANGUAGE AllowAmbiguousTypes #-}
44{-# LANGUAGE DataKinds #-}
@@ -8,12 +8,16 @@
88{-# LANGUAGE RankNTypes #-}
99{-# LANGUAGE ScopedTypeVariables #-}
1010{-# LANGUAGE TypeApplications #-}
11+{-# LANGUAGE TemplateHaskell #-}
12+{-# LANGUAGE CPP #-}
1113
1214module Main where
1315
1416import GHC.Generics
1517import Data.Generics.Product
16−import GHC.Proof
18+#if MIN_VERSION_GLASGOW_HASKELL(8,2,0,0)
19+import Test.Inspection
20+#endif
1721
1822main :: IO ()
1923main = putStrLn "Hello world"
@@ -42,19 +46,28 @@ subtypeLensManual f record
4246
4347--------------------------------------------------------------------------------
4448-- * 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+-- The inspection-testing plugin checks that the following equalities hold, by
50+-- checking that the LHSs and the RHSs are CSEd. This also means that the
51+-- runtime characteristics of the derived lenses is the same as the manually
52+-- written ones above.
4953
50−fieldP :: Proof
51−fieldP = L fieldALensManual === L (field @"fieldA")
54+fieldALensName :: Lens' Record Int
55+fieldALensName = field @"fieldA"
5256
53−typedP :: Proof
54−typedP = L fieldALensManual === L (typed @Int)
57+fieldALensType :: Lens' Record Int
58+fieldALensType = typed @Int
5559
56−posP :: Proof
57−posP = L fieldALensManual === L (position @1)
60+fieldALensPos :: Lens' Record Int
61+fieldALensPos = position @1
5862
59−subtypeP :: Proof
60−subtypeP = L subtypeLensManual === L super
63+subtypeLensGeneric :: Lens' Record Record2
64+subtypeLensGeneric = super
65+
66+#if MIN_VERSION_GLASGOW_HASKELL(8,2,0,0)
67+-- It turns out that these equalities only hold with ghc-8.2 or newer,
68+-- probably due to improvements to CSE
69+inspect $ 'fieldALensManual === 'fieldALensName
70+inspect $ 'fieldALensManual === 'fieldALensType
71+inspect $ 'fieldALensManual === 'fieldALensPos
72+inspect $ 'subtypeLensManual === 'subtypeLensGeneric
73+#endif