Example showing the need for typeable instances

gistfile1.txt

{-# LANGUAGE TypeOperators, GADTs, FlexibleContexts, AllowAmbiguousTypes, StandaloneDeriving, DeriveDataTypeable #-}

import Data.Typeable
import Data.Syntactic
import Data.Syntactic.Functional
import Data.Syntactic.Sugar.BindingT ()

deriving instance Typeable Construct
deriving instance Typeable BindingT
deriving instance Typeable AST
deriving instance Typeable (:+:)

type ExprDomain = BindingT :+: Construct :+: Let
type Expr a = ASTF ExprDomain a

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

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

instance Render Let
  where
    renderSym Let = "letBind"

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

main :: IO ()
main = print $ show $ (share (lit 3) id :: Expr Int)