Mutually-recursive syntaxes with Bound

Question

Here's a syntax for a dependently-typed lambda calculus.

data TermI a = Var a
             | App (TermI a) (TermC a)  -- when type-checking an application, infer the type of the function and then check that its argument matches the domain
             | Star  -- the type of types
             | Pi (Type a) (Scope () Type a)  -- The range of a pi-type is allowed to refer to the argument's value
             | Ann (TermC a) (Type a)  -- embed a checkable term by declaring its type
             deriving (Functor, Foldable, Traversable)

data TermC a = Inf (TermI a)  -- embed an inferrable term
             | Lam (Scope () TermC a)
             deriving (Functor, Foldable, Traversable)

type Type = TermC  -- types are values in a dependent type system

(I more-or-less lifted this from Simply Easy.) The type system is bidirectional, splitting terms into those whose type can be inferred from the typing context, and those which can only be checked against a goal type. This is useful in dependent type systems because in general lambda terms will have no principal type.

Anyway, I've got stuck trying to define a Monad instance for this syntax:

instance Monad TermI where
    return = Var
    Var x >>= f = f x
    App fun arg >>= f = App (fun >>= f) (arg >>= Inf . f)  -- embed the substituted TermI into TermC using Inf
    Star >>= _ = Star
    Pi domain range >>= f = Pi (domain >>= Inf . f) (range >>>= Inf . f)
    Ann term ty >>= f = Ann (term >>= Inf . f) (ty >>= Inf . f)

instance Monad TermC where
    return = Inf . return
    Lam body >>= f = Lam (body >>>= f)
    Inf term >>= f = Inf (term >>= _)

To fill the hole in the last line of TermC's instance, I need something of type a -> TermI b but f has a type of a -> TermC b. I can't embed the resulting TermC into TermI using the Ann constructor because I don't know the type of the TermC.

Is this datatype incompatible with bound's model? Or is there a trick I can use to make the Monad instance go?

Answer 1

It's quite simply impossible to do: TermC is not a monad. Substitution puts terms in place of variables. For this to make sense, the terms need to be able to fit, i.e. to be similar enough so that the resulting term still has good properties. Here it means that its type must be inferrable. TermC won't do.

You can either implement:

 substI :: TermI a -> (a -> TermI b) -> TermI b
 substC :: TermC a -> (a -> TermI b) -> TermC b

and have

 instance Monad TermI where
   return = Var
   bind   = substI