Pattern matching a data type fails to find the type of the scrutinee

[zanzix]

When pattern matching on the type Cat (\f,g => {0 x : Type} -> f x -> g x) it gives me the error: Can't infer type to match in errfun. Everything works if I use a non-parametric function, ie Cat (\a,b=>(a->b))

Steps to Reproduce:

data Cat : {o: Type} -> (o -> o -> Type) -> (o -> o -> Type) where
    Id   : {o: Type} -> {h : o -> o -> Type} -> {a:o} -> Cat h a a

errfun : (0 fn : Type -> Type) -> (0 nt : (Type -> Type) -> (Type -> Type) -> Type) -> Cat {o=Type -> Type} nt fn fn -> ()
errfun fn nt (Id {o=Type -> Type,a = fn, h = nt}) = ?nope

Expected Behavior

Type-checks as normal

Observed Behavior

Error: Can't infer type to match in errfun.

Algebra.Profunctor.Bug:5:1--5:58
 1 | data Cat : {o: Type} -> (o -> o -> Type) -> (o -> o -> Type) where
 2 |     Id   : {o: Type} -> {h : o -> o -> Type} -> {a:o} -> Cat h a a
 3 | 
 4 | errfun : (0 fn : Type -> Type) -> (0 nt : (Type -> Type) -> (Type -> Type) -> Type) -> Cat {o=Type -> Type} nt fn fn -> ()
 5 | errfun fn nt (Id {o=Type -> Type,a = fn, h = nt}) = ?nope
     ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

[mjustus]

I reduced the example a bit:

data D : Type -> Type where
  C : (a : Type) -> D a

f : D (Type -> Type) -> ()
f (C (Type -> Type)) = ()

If we explicitly mark the type argument as forced, Idris has no longer any trouble type checking the pattern:

g : D (Type -> Type) -> ()
g (C .(Type -> Type)) = ()

[zanzix]

Oh, thank you! I didn't know about this feature, where could I read more about it?
And is it possible to make it work with an implicit type?
ie g (C .{Type -> Type})

[zanzix]

(Going to keep this open since it's technically still a bug in the compiler)

[gallais]

You can write:

data D : Type -> Type where
  C : D a

f : D (Type -> Type) -> ()
f (C {a = .(Type -> Type)}) = ()

[zanzix]

Thank you!