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?