GitLab

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.