Coercion and Higher-Order
Coercions are not applied under implicit higher-order application.
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.