Toying with type-level regular expressions

RE-type.hs

{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE UndecidableInstances #-}

module Regex where

data RE
  = forall (a :: *). Term a
  | Null
  | RE :| RE

type family Or (a :: Bool) (b :: Bool) :: Bool where
    Or 'True b  = 'True
    Or 'False b = b

type family Match a (b :: RE) where
    Match a ('Term a)   = 'True
    Match a (m1 ':| m2) = Match a m1 `Or` Match a m2
    Match a b           = 'False

x :: Match a ('Term Char ':| 'Term Int) ~ 'True => a -> a -> a
x = const