Using type applications in patterns to obtain the set of patterns tried in a pattern match at the type level

TAP.hs

{-# LANGUAGE AllowAmbiguousTypes      #-}
{-# LANGUAGE DataKinds                #-}
{-# LANGUAGE FlexibleContexts         #-}
{-# LANGUAGE FlexibleInstances        #-}
{-# LANGUAGE LambdaCase               #-}
{-# LANGUAGE MagicHash                #-}
{-# LANGUAGE MultiParamTypeClasses    #-}
{-# LANGUAGE NamedWildCards           #-}
{-# LANGUAGE PatternSynonyms          #-}
{-# LANGUAGE PartialTypeSignatures    #-}
{-# LANGUAGE PolyKinds                #-}
{-# LANGUAGE RankNTypes               #-}
{-# LANGUAGE ScopedTypeVariables      #-}
{-# LANGUAGE StandaloneKindSignatures #-}
{-# LANGUAGE TypeApplications         #-}
{-# LANGUAGE TypeFamilies             #-}
{-# LANGUAGE TypeOperators            #-}
{-# LANGUAGE UndecidableInstances     #-}
{-# LANGUAGE ViewPatterns             #-}

{-# OPTIONS_GHC -Wall -fno-warn-partial-type-signatuers #-}

module TAP where

-- base
import Control.Arrow
  ( (&&&) )
import Data.Coerce
  ( coerce )
import Data.Kind
  ( Constraint, Type )
import Data.List
  ( sort )
import Data.Proxy
  ( Proxy(Proxy) )
import Data.Type.Bool
  ( If )
import Data.Type.Equality
  ( type (==) )
import GHC.Exts
  ( Proxy#, proxy# )
import GHC.TypeLits
  ( TypeError, ErrorMessage(..) )
import GHC.TypeNats
  ( Nat, KnownNat, natVal' )

-----------------------------------------------
-- case alternatives

type Elem :: k -> [k] -> Bool
type family Elem x xs where
  Elem _ '[] = False
  Elem x (x ': xs) = True
  Elem x (_ ': xs) = Elem x xs

newtype Case (is :: [Nat]) = UnsafeCase { scrutiniseCase :: Nat }

here :: forall i is. KnownNat i => Case (i ': is)
here = UnsafeCase ( natVal' @i proxy# )

there :: forall x is. Case is -> Case (x ': is)
there ( UnsafeCase i ) = UnsafeCase i

class HasCase ( i :: Nat ) ( is :: [ Nat ] ) where
  injCase :: Case is
instance {-# OVERLAPPING #-}
  ( KnownNat i
  , If (Elem i is)
      ( TypeError
        ( Text "Duplicate case in pattern: Case " :<>: ShowType i :<>: Text "." )
      )
      ( () :: Constraint )
  ) => HasCase i (i ': is) where
  injCase = here @i @is
instance ( HasCase i is )
      => HasCase i (x ': is) where
  injCase = there @x ( injCase @i @is )
instance {-# INCOHERENT #-}
         ( KnownNat i, xs ~ (i ': ys) )
      => HasCase i xs        where
  injCase = here @i @ys

pattern Case :: forall ( i :: Nat ) ( is :: [Nat] ). ( KnownNat i, HasCase i is ) => () => Case is
pattern Case <- ( ( natVal' @i proxy# == ) . scrutiniseCase -> True )
  where
    Case @i = UnsafeCase ( natVal' @i proxy# )


-- * Found type wildcard `_cases'
--     standing for `7 : 1 : 3 : 4 : ys :: [Nat]'
--
-- > :t test1
-- test1 ::  Case (7:1:3:4:ys) -> String
test1 :: Case _cases -> String
test1 = \case
  Case @7 -> "case 7"
  Case @1 -> "case 1"
  Case @3 -> "case 3"
  Case @4 -> "case 4"
  _       -> "default"

{-
-- * Duplicate case in pattern: Case 3.
test2 :: Case _cases -> String
test2 = \case
  Case @7 -> "case 7"
  Case @1 -> "case 1"
  Case @3 -> "case 3"
  Case @4 -> "case 4"
  Case @3 -> "case 3 again"
  _       -> "default"
-}

-- * Found type wildcard `_cases'
--     standing for `7 : 1 : 3 : 4 : ys :: [Nat]'
--
--  Pattern match(es) are non-exhaustive
--  In a case alternative:
--      Patterns of type `Case (7 : 1 : 3 : 4 : ys)' not matched:
--          UnsafeCase _
test3 :: Case _cases -> String
test3 = \case
  Case @7 -> "case 7"
  Case @1 -> "case 1"
  Case @3 -> "case 3"
  Case @4 -> "case 4"

-----------------------------------------------

class KnownCases is where
  casesVal :: [Case is]
instance KnownCases '[] where
  casesVal = []
instance (KnownNat i, KnownCases is) => KnownCases (i ': is) where
  casesVal = here : map there ( casesVal @is )
instance {-# INCOHERENT #-} KnownCases is where
  casesVal = []

switch
  :: forall
       ( t  :: Type  )
       ( is :: [Nat] )
  .  ( Case is -> t )
  -> KnownCases is -- this constraint needs to be passed here so that 'is' can be correctly inferred beforehand
  => ( [ ( Nat, t ) ], t )
switch f = ( switchCases &&& defaultCase ) ( casesVal @is )
  where
    switchCases :: [ Case is ] -> [ (Nat, t) ]
    switchCases = map ( scrutiniseCase &&& f )
    defaultCase :: [ Case is ] -> t
    defaultCase = f . coerce new

new :: [Nat] -> Nat
new = firstGap (0 :: Nat) . sort
    where
      firstGap :: Nat -> [Nat] -> Nat
      firstGap a [] = a
      firstGap a (x:xs)
        | a < x     = a
        | otherwise = firstGap (succ x) xs

-- > test1Cases
-- ([(7,"case 7"),(1,"case 1"),(3,"case 3"),(4,"case 4")],"default")
test1Cases :: ( [ ( Nat, String ) ], String )
test1Cases = switch test1

{-
-- > test2Cases
-- ([(7,"case 7"),(1,"case 1"),(3,"case 3"),(4,"case 4")],"default")
test2Cases :: ( [ ( Nat, String ) ], String )
test2Cases = switch test2
-}

-- > test3Cases
-- ([(7,"case 7"),(1,"case 1"),(3,"case 3"),(4,"case 4")],"*** Exception: TAP.hs:(120,9)-(124,21): Non-exhaustive patterns in case
test3Cases :: ( [ ( Nat, String ) ], String )
test3Cases = switch test3