search

idris-lang / Idris-dev

A Dependently Typed Functional Programming Language
http://idris-lang.org
Other
3.43k stars 644 forks source link

`mutual` does not work for records #2248

Closed ziman closed 9 years ago

ziman commented 9 years ago

This code

mutual
  record A where
    b : B

  record B where
    a : A

does not typecheck, yielding the following message:

x.idr:5:10:When elaborating type of Main.MkA:
No such variable B
x.idr:8:10:When elaborating type of Main.MkB:
No such variable A

However, when I change the definition to use data instead of record, everything works fine.

The whole code: http://lpaste.net/2012644708815208448

ziman commented 9 years ago

If I change record A to data A (and leave B as record), the file still does not typecheck. If I change record B to data B (and leave A as record), the file typechecks successfully.

david-christiansen commented 9 years ago

My guess is that they're not respecting the EWhen flag in the mutual block elaborator, which causes the formation rules to be generated in one pass and the constructors/projections in another.