{-# language
    DataKinds
  , DerivingStrategies
  , GeneralisedNewtypeDeriving
  , InstanceSigs
  , LambdaCase
  , MultiParamTypeClasses
  , OverloadedRecordDot
#-}

import Data.Coerce
import Data.Either
import Data.Proxy

{- start stubs -}

data Refined p a = RefinedStub a

data RefineException = RefineExceptionStub

class Predicate p a where
  validate :: Proxy p -> a -> Maybe RefineException

data Not p = Not

refine :: (Predicate p x) => x -> Either RefineException (Refined p x)
refine = undefined

reallyUnsafeRefine :: x -> Refined p x
reallyUnsafeRefine x = RefinedStub x

-- not a stub, this should probably be in refined
refineMeNot :: forall p x. (Predicate p x) => x -> Either (Refined (Not p) x) (Refined p x)
refineMeNot x = case refine @p x of
  Right r -> Right r
  Left _ -> Left (reallyUnsafeRefine x)

{- end stubs -}

data Denomination
  = ZL10
  | ZL5
  | ZL2
  | ZL1
  | GR50
  | GR20
  | GR10
  | GR5
  | GR2
  | GR1
  deriving stock (Eq, Show, Enum, Bounded)

denominationYears :: Denomination -> [Year]
denominationYears = \case
  GR1 -> coerce @[Int] @[Year] [1923, 1925, 1927, 1928, 1930, 1931, 1932, 1933, 1934, 1935, 1936, 1937, 1938, 1939]
  _ -> undefined

data Mint
  = Warsaw
  | Paris
  | Birmingham
  deriving stock (Eq, Show, Enum, Bounded)

newtype Year = Year Int
  deriving stock (Show)
  deriving newtype (Eq)

data Coin = Coin
  { denomination :: Denomination,
    mint :: Mint,
    year :: Year
  }

data ValidCoin = ValidCoin

instance Predicate ValidCoin Coin where
  validate :: Proxy ValidCoin -> Coin -> Maybe RefineException
  validate _ coin
    | coin.year `elem` denominationYears coin.denomination = Nothing
    | otherwise = undefined -- throwRefine ...

allCoins :: ([Refined (Not ValidCoin) Coin], [Refined ValidCoin Coin])
allCoins = partitionEithers $ map (refineMeNot @ValidCoin)
  [ Coin d m (Year y)
  | d <- [minBound..maxBound]
  , m <- [minBound..maxBound]
  , y <- [1923..1970] -- I made up an upper bound
  ]

main :: IO ()
main = do
  pure ()