These

these-n.hs

{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DerivingStrategies #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE ViewPatterns #-}

module W where

import Data.Kind
import GHC.TypeLits

data These :: [Type] -> Type where
  This :: a -> These (a : xs)
  That :: These xs -> These (a : xs)
  These :: a -> These xs -> These (a : xs)

instance Show (These '[]) where
  show = error "impossible"

deriving stock instance Show x => Show (These '[x])

deriving stock instance (Show (These (y : ys)), Show x) => Show (These (x : (y : ys)))

data A = A

data B = B

data C = C

xs :: [These '[A, B, C]]
xs =
  [ This A,
    That (This B),
    That (That (This C)),
    These A (This B),
    These A (That (This C)),
    That (These B (This C)),
    These A (These B (This C))
  ]

data N = Z | S N

type family FromNat (n :: Nat) :: N where
  FromNat 0 = Z
  FromNat n = S (FromNat (n - 1))

class TheseNth (n :: N) (xs :: [Type]) a | n xs -> a where
  has' :: These xs -> Maybe a
  only' :: a -> These xs

instance TheseNth Z (x : xs) x where
  has' (This x) = Just x
  has' (That _) = Nothing
  has' (These x _) = Just x
  only' x = This x

instance TheseNth n xs a => TheseNth (S n) (x : xs) a where
  has' (This _) = Nothing
  has' (That xs) = has' @n xs
  has' (These _ xs) = has' @n xs
  only' x = That (only' @n x)

has :: forall n a xs. TheseNth (FromNat n) xs a => These xs -> Maybe a
has = has' @(FromNat n)

only :: forall n a xs. TheseNth (FromNat n) xs a => a -> These xs
only = only' @(FromNat n)

instance Semigroup x => Semigroup (These '[x]) where
  This a <> This b = This (a <> b)
  _ <> _ = error "impossible case for these with only one value"

instance (Semigroup (These (y : ys)), Semigroup x) => Semigroup (These (x : (y : ys))) where
  This a <> This b = This (a <> b)
  This a <> That b = These a b
  This a <> These a' b = These (a <> a') b
  That b <> That b' = That (b <> b')
  That b <> These a b' = These a (b <> b')
  These a b <> These a' b' = These (a <> a') (b <> b')
  b <> a = a <> b

mergeByFirst :: These xs -> These xs -> These xs
mergeByFirst (This a) (This _) = This a
mergeByFirst (This a) (That b) = These a b
mergeByFirst (This a) (These _ b) = These a b
mergeByFirst (That b) (That b') = That (mergeByFirst b b')
mergeByFirst (That b) (These a b') = These a (mergeByFirst b b')
mergeByFirst (These a b) (These _ b') = These a (mergeByFirst b b')
mergeByFirst b a = mergeByFirst a b

f :: These [Int, String, Bool] -> String
f (has @0 -> Just _) = "first"
f (has @1 -> Just _) = "second"
f (has @2 -> Just _) = "third"
f _ = undefined

main :: IO ()
main = do
  putStrLn (f (only @0 42))
  putStrLn (f (only @1 "hello"))
  putStrLn (f (only @2 True))
  putStrLn (f (These 42 (This "hello")))
  print (mergeByFirst (only @0 42) (only @2 True) :: These [Int, String, Bool])
  print (foldr1 mergeByFirst [only @0 42, only @2 True, only @1 "hello"] :: These [Int, String, Bool])