`matchNR` implements a `ViewPatterns` in order to match for an arbitrary deep `(R1 (R1 (R1 (L1 x)))` from `GHC.Generics`

NatNat.hs

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE ExplicitForAll #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}

{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE FlexibleContexts #-}
import GHC.Generics
import qualified GHC.TypeLits

type Example = (Either Int :+: (Either Double :+: Either Bool))

isSecondEither :: Example a -> Maybe (Either Double a)
isSecondEither (R1 (L1 v)) = Just v
isSecondEither _ = Nothing

isSecondEither' :: Example a -> Maybe (Either Double a)
isSecondEither' = matchNR @1

isThirdEither :: (Either String :+: Example) a -> Maybe (Either Double a)
isThirdEither = matchNR @2

class MatchNR (k :: Nat) a b c where
    matchNR' :: a c -> Maybe (b c)

instance MatchNR 'Z (a :+: b) a c where
    matchNR' (L1 a) = Just a
    matchNR' _ = Nothing

instance MatchNR n b c d => MatchNR ('S n) (a :+: b) c d where
    matchNR' (R1 v) = matchNR' @n v
    matchNR' _ = Nothing

matchNR :: forall (n :: GHC.TypeLits.Nat) a b c. MatchNR (NatNat n) a b c => a c -> Maybe (b c)
matchNR = matchNR' @(NatNat n)

data Nat = Z | S Nat

type family NatNat k where
  NatNat 0 = 'Z
  NatNat n = 'S (NatNat (n GHC.TypeLits.- 1))