An example of where I need an explicit `Typeable ExprTypes a` constraint

Foo.hs

{-# LANGUAGE ScopedTypeVariables, 
             TypeOperators, 
             DataKinds, 
             KindSignatures, 
             TypeFamilies, 
             GADTs, 
             FlexibleContexts, 
             FlexibleInstances, 
             MultiParamTypeClasses #-}

import Data.Syntactic
import Data.Syntactic.Functional hiding (eval)
import Data.Syntactic.TypeUniverse
import Data.Syntactic.Sugar.BindingT (VarUniverse)

data Let a where
    Let :: Let (a :-> (a -> b) :-> Full b)

instance Eval Let t where
  toSemSym Let = Sem (flip ($))

share :: (Let :<: sup,
          sup ~ Domain b, sup ~ Domain a,
          Syntactic a, Syntactic b,
          Syntactic (a -> b),
          SyntacticN (a -> (a -> b) -> b) 
                     (ASTF sup (Internal a) -> ASTF sup ((Internal a) -> (Internal b)) -> ASTF sup (Internal b)))
                    -- fi) -- requires AllowAmbiguousTypes
           => a -> (a -> b) -> b
share = sugarSym Let

lit :: (Syntactic a, Show (Internal a), Construct :<: Domain a) => Internal a -> a
lit a = sugar $ inj $ Construct (show a) a

eval :: (Syntactic a, Domain a ~ ExprDomain) => a -> Internal a
eval = evalClosed (Proxy :: Proxy ExprTypes) . desugar



type ExprDomain = Construct :+: BindingT ExprTypes :+: Let :+: Foo
type ExprTypes = IntType

type ExprDomain = Construct :+: BindingT ExprTypes2 :+: Let :+: Foo
type ExprTypes2 = IntType :+: BoolType

data Foo :: (* -> *) where
  Foo :: (Typeable ExprTypes zq) => Foo (zq :-> Full zq)

instance Eval Foo t where
  toSemSym Foo = Sem id

instance Render Foo where
  renderSym Foo = "Foo"

foo :: (Typeable ExprTypes zq, Foo :<: dom)
    => ASTF dom zq -> ASTF dom zq
foo = sugarSym Foo

shareFoo :: forall a dom . (Foo :<: dom, BindingT ExprTypes :<: dom, Let :<: dom, VarUniverse dom ~ ExprTypes) => ASTF dom a -> ASTF dom a
shareFoo (node :$ x) | Just Foo <- prj node,
                       (_ :: ASTF dom zq) <- x = share x id
shareFoo a = a

main :: IO ()
main = do
  -- the following line compiles with `ExprDomain`, but not for `ExprDomain2`.
  let ex = Main.foo (lit 5 :: ASTF ExprDomain Int)
  print $ show (eval $ everywhereUp shareFoo ex)