19 Mar
2016
19 Mar
'16
10:52 p.m.
Hi,
On 19 March 2016 at 21:46, Reid Barton
`extensions: StrictData` turns on the StrictData extension for all modules in the program. So every field of every data type defined in every module is made strict.
I was aware of it.
Is that really what you wanted?
No really. I added the extension just out curiosity.
For a large, complicated program like Agda, It seems about as likely to work as just passing the program into an ML compiler unmodified. Your errors are a typical example: note they are runtime errors from a generated happy parser, which probably does something like initializing a record with (error "Internal Happy error") and then trying to update it with record update syntax.
Thanks you for the explanation. Best, -- Andrés