{-# LANGUAGE CPP #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
{-# OPTIONS_GHC -Wno-unticked-promoted-constructors #-}
module Constrained.TypeErrors (
Computes,
AssertComputes,
AssertSpineComputes,
module X,
) where
import Data.Kind
#if MIN_VERSION_base(4,17,0)
import GHC.TypeError as X
#else
import GHC.TypeLits as X
#endif
type family Computes (ty :: k0) (err :: Constraint) (a :: k) :: k where
Computes Dummy _ _ =
TypeError
(Text "This shouldn't be reachable because " :<>: ShowType Dummy :<>: Text " shouldn't be exported!")
Computes (Dummy : as) _ _ =
TypeError
(Text "This shouldn't be reachable because " :<>: ShowType Dummy :<>: Text " shouldn't be exported!")
Computes _ _ a = a
data Dummy
type AssertComputes ty em = Computes ty (TypeError em) (() :: Constraint)
type family AssertSpineComputesF (help :: ErrorMessage) (xs :: [k]) (err :: ()) :: Constraint where
AssertSpineComputesF _ '[] _ = ()
AssertSpineComputesF help (_ : xs) err = AssertSpineComputes help xs
type AssertSpineComputes help (xs :: [k]) =
AssertSpineComputesF
help
xs
( TypeError
( Text "Type list computation is stuck on "
:$$: Text " "
:<>: ShowType xs
:$$: help
)
)