The following code fails type checking (with message "No such variable MkBar"):
mutual
interface Foo s where
foo : Bar
foo = MkBar
data Bar = MkBar
I am not sure whether this behaviour is intentional. However, the code can be made to type check by using a helper function that is added to the mutual block like this:
mutual
interface Foo s where
foo : Bar
foo = mkBar
data Bar = MkBar
mkBar : Bar
mkBar = MkBar
My expectation would be that either both or neither of the above two examples type checks.
Thanks for reporting the issue.
My guess is that this is because interface headers are elaborated at a different stage/scope than their bodies, but it should nonetheless work.
The following code fails type checking (with message "No such variable MkBar"):
I am not sure whether this behaviour is intentional. However, the code can be made to type check by using a helper function that is added to the mutual block like this:
My expectation would be that either both or neither of the above two examples type checks.