NoMono

{-# LANGUAGE GADTs#-}

data Lam a  where
  Var :: a -> Lam a
  App :: Lam a -> Lam a -> Lam a
  Lam :: Lam (Maybe a) -> Lam a

mapLam :: (a -> b) -> Lam a -> Lam b
mapLam f (Var a)   = Var $ f a
mapLam f (App t u) = mapLam f t `App` mapLam f u
mapLam f (Lam b)   = Lam $ mapLam (fmap f) b

betaRedOk :: Lam (Maybe Int) -> Lam Int -> Lam Int
betaRedOk b u =
  let f = mapLam id
  in App (Lam $ f b) (f u)

betaRedFail :: Lam (Maybe Int) -> Lam Int -> Lam Int
betaRedFail b u = (\ f -> App (Lam $ f b) (f u)) $ mapLam id

{-
NoMono.hs:19:44:
    Couldn't match type `Maybe Int' with `Int'
    Expected type: Lam Int
      Actual type: Lam (Maybe Int)
    In the return type of a call of `f'
    In the second argument of `App', namely `(f u)'
    In the expression: App (Lam $ f b) (f u)

NoMono.hs:19:46:
    Couldn't match type `Int' with `Maybe Int'
    Expected type: Lam (Maybe Int)
      Actual type: Lam Int
    In the first argument of `f', namely `u'
    In the second argument of `App', namely `(f u)'
    In the expression: App (Lam $ f b) (f u)
-}