Coercion and Higher-Order
Coercions are not applied under implicit higher-order application.
Examples:
module Foo1
type t
type u
function f t : u
meta coercion function f
constant g : u -> bool
goal G : forall x:t. g x
end
module Foo2
type t
type u
function f t : u -> u
meta coercion function f
goal G : forall x:t,y:u. x y = y
end
In both modules, the occurrence of "x" within the goal is not coerced as one would expect, leading to a type error. However, when one explicit the higher-order application (operator (@)), those occurrences are coerced as expected.