Improve coercion matching

[janmasrovira]

In the following example we get an error at the last return because we are unable to find a monad instance for M. We should detect Monad M because we have {{MonadS S M}} in scope and MonadS has an instance field {{monad}} : Monad M, thus we have the coercion coercion instance monad : {S : Type} → {M : Type → Type} → {{MonadS S M}} → Monad M.

The problem seems to be that MonadS has the extra (S : Type) argument and the coercion detection algorithm is not able to detect that.

module example;

trait
type Monad (f : Type -> Type) := mkMonad {return : {A : Type} -> A -> f A};

open Monad public;

trait
type MonadS (S : Type) (M : Type -> Type) :=
  mkMonadReader {
    {{monad}} : Monad M;
    getS : S
  };

projMonad {B S} {M : Type -> Type} {{MonadS S M}} : {A : Type} -> A -> M A := return;

[paulcadman]

• Closed by Make meta-variables introduced by coercion resolution non-rigid #3290