Removing `Typeable` constraints?
Originally created by @rumkeller.
This is a suggestion.
It seems that the Typeable
constraints on the constructors of Sing :: T -> Type
and Sing :: CT -> Type
are not really necessary.
We can statically show that the universe of types they enumerate is a subset of Typeable
:
typeableSingCT :: forall (t::CT) a. Sing t -> (Typeable t => a) -> a
typeableSingCT SCInt = id
typeableSingCT SCNat = id
typeableSingCT SCString = id
typeableSingCT SCBytes = id
typeableSingCT SCMutez = id
typeableSingCT SCBool = id
typeableSingCT SCKeyHash = id
typeableSingCT SCTimestamp = id
typeableSingCT SCAddress = id
typeableSingT :: forall (t::T) a. Sing t -> (Typeable t => a) -> a
typeableSingT (STc ct ) x = typeableSingCT ct x
typeableSingT STKey {} x = x
typeableSingT STUnit {} x = x
typeableSingT STSignature {} x = x
typeableSingT (STOption t1) x = typeableSingT t1 x
typeableSingT (STList t1) x = typeableSingT t1 x
typeableSingT (STSet t1) x = typeableSingCT t1 x
typeableSingT (STContract t1) x = typeableSingT t1 x
typeableSingT STOperation {} x = x
typeableSingT (STPair t1 t2) x = typeableSingT t1 $ typeableSingT t2 x
typeableSingT (STOr t1 t2) x = typeableSingT t1 $ typeableSingT t2 x
typeableSingT (STLambda t1 t2) x = typeableSingT t1 $ typeableSingT t2 x
typeableSingT (STMap t1 t2) x = typeableSingCT t1 $ typeableSingT t2 x
typeableSingT (STBigMap t1 t2) x = typeableSingCT t1 $ typeableSingT t2 x
In other words, Sing t
is a witness of Typeable t
(if t
is of kind T
or CT
).
Furthermore, the Typeable
instances seem to be mostly used for equality checks on Michelson types. These can also be implemented directly, without taking the detour through Haskell types:
eqSingCT :: forall (t::CT) (u::CT). Sing t -> Sing u -> Maybe (t :~: u)
SCInt `eqSingCT` SCInt = Just Refl
SCNat `eqSingCT` SCNat = Just Refl
SCString `eqSingCT` SCString = Just Refl
...
_ `eqSingCT` _ = Nothing
eqSingT :: forall (t::T) (u::T). Sing t -> Sing u -> Maybe (t :~: u)
STc t `eqSingT` STc u = do Refl <- eqSingCT t u; return Refl
STKey `eqSingT` STKey = return Refl
STOption t `eqSingT` STOption u = do Refl <- eqSingT t u; return Refl
STBigMap t1 t2 `eqSingT` STBigMap u1 u2 = do Refl <- eqSingCT t1 u1; Refl <- eqSingT t2 u2; return Refl
...
_ `eqSingT` _ = Nothing
Perhaps this approach could help to remove some of the many Typeable
constraints.