typeCheckExpr :: Expr -> TypeCheck Type
typeCheckExpr = \case
  EVar x -> do
    env <- ask
    case Map.lookup x env of
      Just varTy -> return varTy
      Nothing -> raise (TCUnbound x)

  ELam x tArg body -> do
    tRet <- mapReader (Map.insert x tArg) (typeCheckExpr body)
    return (TFun tArg tRet)

  EApp e1 e2 -> do
    t1 <- typeCheckExpr e1
    t2 <- typeCheckExpr e2
    case t1 of
      TFun tArg tRet | tArg == t2 -> return tRet
                     | otherwise  -> raise (TCMismatch e2 tArg t2)
      _ -> raise (TCNonFun e1 t1)

  EConst c -> typeCheckConst c

  EUnop u e -> do
    tOp <- typeCheckUnop u
    t <- typeCheckExpr e
    case tOp of
      TFun tArg tRet | tArg == t -> return tRet
                     | otherwise -> raise (TCMismatch e tArg t)
      _ -> error "impossible: unop not a function type"

  EBinop b e1 e2 -> do
    tOp <- typeCheckBinop b
    t1 <- typeCheckExpr e1
    t2 <- typeCheckExpr e2
    case tOp of
      TFun tArg1 (TFun tArg2 tRet)
        | tArg1 == t1 && tArg2 == t2 -> return tRet
        | tArg1 == t1                -> raise (TCMismatch e2 tArg2 t2)
        |                tArg2 == t2 -> raise (TCMismatch e1 tArg1 t1)
      _ -> error "impossible: binop not a function type"

  EIfThenElse e1 e2 e3 -> do
    t1 <- typeCheckExpr e1
    unless (t1 == TBool) $ raise (TCMismatch e1 TBool t1)
    t2 <- typeCheckExpr e2
    t3 <- typeCheckExpr e3
    unless (t2 == t3) $ raise (TCMismatch e3 t2 t3)
    return t2
typeCheckExpr :: Expr -> TypeCheck Type
typeCheckExpr = \case
  EVar x -> do
    env <- ask
    case Map.lookup x env of
      Just varTy -> return varTy
      Nothing -> raise (TCUnbound x)

  ELam x tArg body -> do
    tRet <- mapReader (Map.insert x tArg) (typeCheckExpr body)
    return (TFun tArg tRet)

  EApp e1 e2 -> do
    t1 <- typeCheckExpr e1
    t2 <- typeCheckExpr e2
    case t1 of
      TFun tArg tRet | tArg == t2 -> return tRet
                     | otherwise  -> raise (TCMismatch e2 tArg t2)
      _ -> raise (TCNonFun e1 t1)

  EConst c -> typeCheckConst c

  EUnop u e -> do
    tOp <- typeCheckUnop u
    t <- typeCheckExpr e
    case tOp of
      TFun tArg tRet | tArg == t -> return tRet
                     | otherwise -> raise (TCMismatch e tArg t)
      _ -> error "impossible: unop not a function type"

  EBinop b e1 e2 -> do
    tOp <- typeCheckBinop b
    t1 <- typeCheckExpr e1
    t2 <- typeCheckExpr e2
    case tOp of
      TFun tArg1 (TFun tArg2 tRet)
        | tArg1 == t1 && tArg2 == t2 -> return tRet
        | tArg1 == t1                -> raise (TCMismatch e2 tArg2 t2)
        |                tArg2 == t2 -> raise (TCMismatch e1 tArg1 t1)
      _ -> error "impossible: binop not a function type"

  EIfThenElse e1 e2 e3 -> do
    t1 <- typeCheckExpr e1
    unless (t1 == TBool) $ raise (TCMismatch e1 TBool t1)
    t2 <- typeCheckExpr e2
    t3 <- typeCheckExpr e3
    unless (t2 == t3) $ raise (TCMismatch e3 t2 t3)
    return t2
typeCheckExpr = \case
  EVar x -> do
    env <- ask
    case Map.lookup x env of
      Just varTy -> return varTy
      Nothing -> raise (TCUnbound x)

  ELam x tArg body -> do
    tRet <- mapReader (Map.insert x tArg) (typeCheckExpr body)
    return (TFun tArg tRet)

  EApp e1 e2 -> do
    t1 <- typeCheckExpr e1
    t2 <- typeCheckExpr e2
    case t1 of
      TFun tArg tRet | tArg == t2 -> return tRet
                     | otherwise  -> raise (TCMismatch e2 tArg t2)
      _ -> raise (TCNonFun e1 t1)

  EConst c -> typeCheckConst c

  EUnop u e -> do
    tOp <- typeCheckUnop u
    t <- typeCheckExpr e
    case tOp of
      TFun tArg tRet | tArg == t -> return tRet
                     | otherwise -> raise (TCMismatch e tArg t)
      _ -> error "impossible: unop not a function type"

  EBinop b e1 e2 -> do
    tOp <- typeCheckBinop b
    t1 <- typeCheckExpr e1
    t2 <- typeCheckExpr e2
    case tOp of
      TFun tArg1 (TFun tArg2 tRet)
        | tArg1 == t1 && tArg2 == t2 -> return tRet
        | tArg1 == t1                -> raise (TCMismatch e2 tArg2 t2)
        |                tArg2 == t2 -> raise (TCMismatch e1 tArg1 t1)
      _ -> error "impossible: binop not a function type"

  EIfThenElse e1 e2 e3 -> do
    t1 <- typeCheckExpr e1
    unless (t1 == TBool) $ raise (TCMismatch e1 TBool t1)
    t2 <- typeCheckExpr e2
    t3 <- typeCheckExpr e3
    unless (t2 == t3) $ raise (TCMismatch e3 t2 t3)
    return t2