Idris: Implicit parameters in records

Question

When I try to compile this example

record R where
    f: () -> {t: Type} -> t

I get this error:

Type mismatch between
        () -> t1 (Type of f)
and
        () -> t (Expected type)

Specifically:
        Type mismatch between
                t1
        and
                t

On the other hand this example

record R where
    f: {t: Type} -> () -> t

works just fine. Can you tell me what's wrong with the first one?

Answer 1

This is a bug in Idris: sometimes the -> operator is not right-associative: issue #4077.

To see it we can desugar the record syntax:

data R : Type where
  MkR : (() -> {t : Type} -> t) -> R

Now we need to manually implement the f projection. It turns out that

f : R -> (() -> {t : Type} -> t)
f (MkR g) = g

does not typecheck, but

f : R -> () -> {t : Type} -> t
f (MkR g) = g

does.

It seems to me Idris uses the first variant to desugar record into data, hence the error you observed.