class ArrowExpr: public Expr{
public:

	Expr typecheck(Context& c){
		Expr p = paramType.nf(c);
		Expr b = bodyType.subst(0, p).nf(c);

		if ( p is not TypeExpr or b is not TypeExpr ){
			throw err;
		}

		int lev = max(((TypeExpr)p).level, ((TypeExpr)b).level);

		return TypeExpr(lev);
	}

	Expr nf(Context& c){
		Expr paramNF = paramType.nf(c);
		return ArrowExpr(paramNF, c.withBinding(paramNF, [](Context& c){
			return bodyType.nf(c)
		});
	}

	Expr subst(int index, Expr e){
		return ArrowExpr(paramType.subst(index, e), body.bodyType(index + 1, e));
	}

	bool depends(int index){
		return paramType.depends(index) || bodyType.depends(index + 1)
	}

private:
	Expr paramType;
	Expr bodyType;
};