    {-# LANGUAGE
        AllowAmbiguousTypes,
        ConstraintKinds,
        DataKinds,
        PolyKinds,
        RankNTypes,
        TypeFamilies,
        TypeOperators,
        UndecidableInstances #-}

    -- | Miscellaneous families.

    module Fcf.Utils
      ( Error
      , TError
      , Constraints
      , TyEq
      , Stuck
      , IsBool(_If)
      , Case
      , Match()
      , type (-->)
      , Is
      , Any
      , Else

        -- * From "Data.Type.Bool"

      , If

        -- * Compile-time asserts

      , Assert
      , AssertNot

        -- * Reexports

      , GHC.TypeLits.ErrorMessage(Text, ShowType, type (:<>:), type (:$$:))
      , GHC.TypeLits.TypeError
      ) where

    import Data.Kind (Constraint)
    import Data.Type.Bool (If)
    import GHC.TypeLits (Symbol, TypeError, ErrorMessage(..))

    import Fcf.Core
    import Fcf.Combinators (Pure, type (=<<))
    import Fcf.Data.Bool (Not)

    -- | Type-level 'error'.

    data Error :: Symbol -> Exp a
    type instance Eval (Error msg) = TypeError ('Text msg)

    -- | 'TypeError' as a fcf.

    data TError :: ErrorMessage -> Exp a
    type instance Eval (TError msg) = TypeError msg

    -- | Conjunction of a list of constraints.

    data Constraints :: [Constraint] -> Exp Constraint
    type instance Eval (Constraints '[]) = (() :: Constraint)
    type instance Eval (Constraints (a ': as)) = (a, Eval (Constraints as))

    -- | Type equality.

    --

    -- === __Details__

    --

    -- The base library also defines a similar @('Type.Equality.==')@;

    -- it differs from 'TyEq' in the following ways:

    --

    -- * 'TyEq' is heterogeneous: its arguments may have different kinds;

    -- * 'TyEq' is reflexive: @TyEq a a@ always reduces to 'True' even if @a@ is

    --   a variable.

    data TyEq :: a -> b -> Exp Bool
    type instance Eval (TyEq a b) = TyEqImpl a b

    type family TyEqImpl (a :: k) (b :: l) :: Bool where
      TyEqImpl a a = 'True
      TyEqImpl a b = 'False

    -- | A stuck type that can be used like a type-level 'undefined'.

    type family Stuck :: a

    -- * Reification

    class IsBool (b :: Bool) where
      _If :: ((b ~ 'True) => r) -> ((b ~ 'False) => r) -> r

    instance IsBool 'True  where _If :: forall r. (('True ~ 'True) => r) -> (('True ~ 'False) => r) -> r
    _If ('True ~ 'True) => r
    a ('True ~ 'False) => r
    _ = r
    ('True ~ 'True) => r
    a
    instance IsBool 'False where _If :: forall r. (('False ~ 'True) => r) -> (('False ~ 'False) => r) -> r
    _If ('False ~ 'True) => r
    _ ('False ~ 'False) => r
    b = r
    ('False ~ 'False) => r
    b

    -- * Case splitting

    infix 0 -->

    data Match j k
      = Match_ j k
      | Is_ (j -> Exp Bool) k
      | Any_ k
      | Else_ (j -> Exp k)

    -- | (Limited) equivalent of @\\case { .. }@ syntax. Supports matching of exact

    -- values ('-->') and final matches for any value ('Any') or for passing value

    -- to subcomputation ('Else'). Examples:

    --

    -- @

    -- type BoolToNat = 'Case'

    --   [ 'True  '-->' 0

    --   , 'False '-->' 1

    --   ]

    --

    -- type NatToBool = 'Case'

    --   [ 0 '-->' 'False

    --   , 'Any'   'True

    --   ]

    --

    -- type ZeroOneOrSucc = 'Case'

    --   [ 0  '-->' 0

    --   , 1  '-->' 1

    --   , 'Else'   (('+') 1)

    --   ]

    -- @

    data Case :: [Match j k] -> j -> Exp k
    type instance Eval (Case ms a) = Case_ ms a

    type family Case_ (ms :: [Match j k]) (a :: j) :: k where
      Case_ ('Match_ a' b : ms) a = Eval (If (TyEqImpl a' a) (Pure b) (Case ms a))
      Case_ ('Is_ p b    : ms) a = Case_ [ 'True  --> b
                                         , 'False --> Case_ ms a
                                         ] (p @@ a)
      Case_ ('Any_ b     : _ ) _ = b
      Case_ ('Else_ f    : _ ) a = f @@ a

    -- | Match concrete type in 'Case'.

    type (-->) = ('Match_ :: j -> k -> Match j k)

    -- | Match on predicate being successful with type in 'Case'.

    type Is = ('Is_ :: (j -> Exp Bool) -> k -> Match j k)

    -- | Match any type in 'Case'. Should be used as a final branch.

    --

    -- Note: this identifier conflicts with 'Fcf.Class.Foldable.Any' (from "Fcf.Class.Foldable")

    -- 'Data.Monoid.Any' (from "Data.Monoid"), and 'GHC.Exts.Any' (from "GHC.Exts").

    --

    -- We recommend importing this one qualified.

    type Any = ('Any_ :: k -> Match j k)

    -- | Pass type being matched in 'Case' to subcomputation. Should be used as a

    -- final branch.

    type Else = ('Else_ :: (j -> Exp k) -> Match j k)

    -- | A compile-time assert.

    --

    -- Raises the provided `TypeError`, whenever the condition evaluates to `False`.

    --

    -- Usage example:

    -- @

    -- type ExampleAssertionFailure = Eval (

    --   Pure '["foo", "bar"]

    --   >>= Length

    --   >>= Assert ('Text "Assertion") (TyEq Int Void)

    --   )

    -- @

    data Assert :: ErrorMessage -> Exp Bool -> r -> Exp r
    type instance Eval (Assert msg mcond k)
      = Eval (If (Eval mcond) (Pure k) (TError msg))

    -- | Compile-time assert, with condition negated.

    --

    -- Raises the provided `TypeError`, whenever the condition evaluates to `True`.

    --

    -- Also see 'Assert'.

    data AssertNot :: forall r. ErrorMessage -> Exp Bool -> r -> Exp r
    type instance Eval (AssertNot err mcond k)
      = Eval (Assert err (Not =<< mcond) k)