{-# OPTIONS_GHC -Wno-unused-top-binds #-}
{-# OPTIONS_GHC -fno-warn-orphans #-}
{-# OPTIONS_GHC -Wno-redundant-constraints #-}
module Morley.Michelson.Typed.Sing
( SingT (..)
, castSingE
, castM
, eqP
, requireEq
) where
import Data.Singletons (SingI(..), demote, fromSing)
import Data.Type.Equality ((:~:)(..))
import Fmt (Buildable(..), fmt, nameF)
import Morley.Michelson.Typed.T (T(..))
import Morley.Util.MismatchError
import Morley.Util.Sing (castSing, eqI, genSingletonsType)
import Morley.Util.TH (deriveGADTNFData)
$