Implicit coercion whose type is not in normal form ignored

[gallais]

I'm using a bunch of type-level combinators to deal with indexed types without explicitly plumbing the index everywhere. I'm also using an implicit coercion to automatically wrap some indexed values in a record wherever the expected type and the type of the expression I give don't match up.

Declaring an implicit with the type All (Vec a :-> Wrap (Vec a)) leads to argh being rejected with the error:

BugReport.idr:31:10-11:When checking right hand side of argh with expected type
        Wrap (Vec a) n

Type mismatch between
        Vec a n (Type of k)
and
        Wrap (Vec a) n (Expected type)

Manually normalising the type of wrapVec to Vec a n -> Wrap (Vec a) n solves the issue.

module BugReport

%default total
%access public export

-- Indexed arrows
infixr 1 :->
(:->) : (a, b : i -> Type) -> (i -> Type)
(:->) a b i = a i -> b i

-- Universal quantifier
All : (a : i -> Type) -> Type
All {i} a = {i : i} -> a i

-- An example of a Nat-indexed family
data Vec : Type -> Nat -> Type where
  Nil  : Vec a Z
  Cons : a -> Vec a n -> Vec a (S n)

-- The type of wrappers for Nat-indexed families
record Wrap (A : Nat -> Type) (n : Nat) where
  constructor MkWrap
  UnWrap : A n

-- Implicit coercion from vecs to wrapped vecs
implicit wrapVec : All (Vec a :-> Wrap (Vec a))
wrapVec = MkWrap

{- solution:
implicit wrapVec : Vec a n -> Wrap (Vec a) n
wrapVec = MkWrap
-}

argh : Vec a n -> Wrap (Vec a) n
argh k = k

I'd expect Idris to do the normalisation of the implicit's type itself.

[ahmadsalim]

Thanks for reporting the issue.
Unfortunately, I am not very familiar with implicit resolution myself.

Maybe @edwinb has an idea?