Some thoughts on how to do type annotations in Michelson

AnnotationProto.hs

{-# LANGUAGE ConstraintKinds           #-}
{-# LANGUAGE DataKinds                 #-}
{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE ExplicitNamespaces        #-}
{-# LANGUAGE FlexibleContexts          #-}
{-# LANGUAGE FlexibleInstances         #-}
{-# LANGUAGE GADTs                     #-}
{-# LANGUAGE PolyKinds                 #-}
{-# LANGUAGE ScopedTypeVariables       #-}
{-# LANGUAGE TypeApplications          #-}
{-# LANGUAGE TypeFamilies              #-}
{-# LANGUAGE TypeInType                #-}
{-# LANGUAGE TypeOperators             #-}
{-# LANGUAGE UndecidableInstances      #-}

import           Data.Kind          (Constraint, Type)
import           Data.Proxy         (Proxy (..))
import           Data.Type.Equality
import           GHC.TypeLits
import           GHC.Types          (Symbol)

data T ( t :: Symbol) where
  T_unit :: Symbol -> T t
  T_pair :: Symbol -> T a -> T b -> T t

type family EqType (t1 :: T a) (t2 :: T b) :: Bool where
  EqType a a = 'True
  EqType (_ "") _ = 'True
  EqType _ (_ "") = 'True
  EqType a b = 'False

data Val op t where
  VUnit :: Val op ('T_unit "")
  VPair :: (Val op l, Val op r) -> Val op ('T_pair "" l r)

data Instr op (inp :: [T a]) (out :: [T a]) where
  DROP :: Instr op (a ': s) s
  DUP  :: Instr op (a ': s) (a ': a ': s)
  SWAP :: Instr op (a ': b ': s) (b ': a ': s)
  PUSH :: forall t s op. Val op t -> Instr op s (t ': s)
  CAST :: Instr op (a ': s) (a ': s)