{-# OPTIONS_GHC -O -fplugin GHC.Proof.Plugin #-}

{-# LANGUAGE AllowAmbiguousTypes             #-}
{-# LANGUAGE DataKinds                       #-}
{-# LANGUAGE DeriveGeneric                   #-}
{-# LANGUAGE DuplicateRecordFields           #-}
{-# LANGUAGE ExistentialQuantification       #-}
{-# LANGUAGE RankNTypes                      #-}
{-# LANGUAGE ScopedTypeVariables             #-}
{-# LANGUAGE TypeApplications                #-}

module Main where

import GHC.Generics
import Data.Generics.Product
import GHC.Proof

main :: IO ()
main = putStrLn "Hello world"

data Record = MkRecord
  { fieldA :: Int
  , fieldB :: Bool
  } deriving Generic

data Record2 = MkRecord2
  { fieldA :: Int
  } deriving Generic

type Lens' s a = forall f. Functor f => (a -> f a) -> s -> f s

fieldALensManual :: Lens' Record Int
fieldALensManual f (MkRecord a b) = (\a' -> MkRecord a' b) <$> f a

newtype L s a = L (Lens' s a)

subtypeLensManual :: Lens' Record Record2
subtypeLensManual f record
  = fmap (\ds -> case record of
                  MkRecord _ b -> MkRecord (case ds of {MkRecord2 g1 -> g1}) b
         ) (f (MkRecord2 (case record of {MkRecord a _ -> a})))

--------------------------------------------------------------------------------
-- * Tests
-- The ghc-proofs plugin checks that the following equalities hold, by checking
-- that the LHSs and the RHSs are CSEd. This also means that the runtime
-- characteristics of the derived lenses is the same as the manually written
-- ones above.

fieldP :: Proof
fieldP = L fieldALensManual === L (field @"fieldA")

typedP :: Proof
typedP = L fieldALensManual === L (typed @Int)

posP :: Proof
posP = L fieldALensManual === L (position @1)

subtypeP :: Proof
subtypeP = L subtypeLensManual === L super