-- SPDX-FileCopyrightText: 2021 Oxhead Alpha -- SPDX-License-Identifier: LicenseRef-MIT-OA {-# OPTIONS_GHC -Wno-unused-top-binds #-} {-# OPTIONS_GHC -fno-warn-orphans #-} {-# OPTIONS_GHC -Wno-redundant-constraints #-} -- | Module, providing singleton boilerplate for -- 'T' data types. -- -- Some functions from Data.Singletons are provided alternative version here. module Morley.Michelson.Typed.Sing ( SingT (..) , castSingE , castM , eqP , requireEq ) where import Data.Singletons (SingI(..), demote) import Data.Type.Equality ((:~:)(..)) import Fmt ((+|), (|+)) import Morley.Michelson.Typed.T (T(..)) import Morley.Util.MismatchError import Morley.Util.Sing (SingI1(..), castSing, eqI, genSingletonsType) -- | 'SingI' and 'Data.Singletons.TH.SDecide' instances for the 'T' kind. $(