{-# LANGUAGE StandaloneKindSignatures #-}
{-# OPTIONS_GHC -Wno-unused-top-binds #-}
{-# OPTIONS_GHC -fno-warn-orphans #-}
{-# OPTIONS_GHC -Wno-redundant-constraints #-}
module Michelson.Typed.Sing
( SingT (..)
, castSingE
, castM
, eqP
, requireEq
) where
import Data.Type.Equality ((:~:)(..))
import Data.Singletons (Demote, KindOf, SingI(..), demote)
import Data.Singletons.TH (genSingletons, singDecideInstance)
import Data.Singletons.TH.Options (Options(..), defaultOptions, withOptions)
import Language.Haskell.TH (Name, mkName, nameBase)
import Fmt ((+||), (||+))
import Michelson.Typed.T (T(..))
import Util.Sing (SingI1(..), castSing, eqI)
$(