Issue799.agda:8,5-6 D should be a function type, but it isn't when checking that {_} {_} {interesting-argument = _} {_} {_} {_} are valid arguments to a function of type D